diff --git a/app/main.cpp b/app/main.cpp index 1478c64..511de1d 100644 --- a/app/main.cpp +++ b/app/main.cpp @@ -2,6 +2,7 @@ #include +#include #include #include diff --git a/include/anthem/AST.h b/include/anthem/AST.h index 1e5cf60..ce76ad6 100644 --- a/include/anthem/AST.h +++ b/include/anthem/AST.h @@ -35,18 +35,18 @@ struct BinaryOperation Modulo }; - BinaryOperation(const BinaryOperation &other) = delete; - BinaryOperation &operator=(const BinaryOperation &other) = delete; - BinaryOperation(BinaryOperation &&other) noexcept = default; - BinaryOperation &operator=(BinaryOperation &&other) noexcept = default; - - BinaryOperation(Operator operator_, Term &&left, Term &&right) + explicit BinaryOperation(Operator operator_, Term &&left, Term &&right) : operator_{operator_}, left{std::move(left)}, right{std::move(right)} { } + BinaryOperation(const BinaryOperation &other) = delete; + BinaryOperation &operator=(const BinaryOperation &other) = delete; + BinaryOperation(BinaryOperation &&other) noexcept = default; + BinaryOperation &operator=(BinaryOperation &&other) noexcept = default; + Operator operator_; Term left; Term right; @@ -56,7 +56,7 @@ struct BinaryOperation struct Boolean { - Boolean(bool value) + explicit Boolean(bool value) : value{value} { } @@ -83,7 +83,7 @@ struct Comparison Equal }; - Comparison(Operator operator_, Term &&left, Term &&right) + explicit Comparison(Operator operator_, Term &&left, Term &&right) : operator_{operator_}, left{std::move(left)}, right{std::move(right)} @@ -104,7 +104,7 @@ struct Comparison struct Constant { - Constant(std::string &&name) + explicit Constant(std::string &&name) : name{std::move(name)} { } @@ -121,12 +121,12 @@ struct Constant struct Function { - Function(std::string &&name) + explicit Function(std::string &&name) : name{std::move(name)} { } - Function(std::string &&name, std::vector &&arguments) + explicit Function(std::string &&name, std::vector &&arguments) : name{std::move(name)}, arguments{std::move(arguments)} { @@ -146,7 +146,7 @@ struct Function // TODO: refactor (limit element type to primitive terms) struct In { - In(Term &&element, Term &&set) + explicit In(Term &&element, Term &&set) : element{std::move(element)}, set{std::move(set)} { @@ -167,7 +167,7 @@ struct In struct Integer { - Integer(int value) + explicit Integer(int value) : value{value} { } @@ -184,7 +184,7 @@ struct Integer struct Interval { - Interval(Term &&from, Term &&to) + explicit Interval(Term &&from, Term &&to) : from{std::move(from)}, to{std::move(to)} { @@ -201,14 +201,15 @@ struct Interval //////////////////////////////////////////////////////////////////////////////////////////////////// +// TODO: implement declaration/signature struct Predicate { - Predicate(std::string &&name) + explicit Predicate(std::string &&name) : name{std::move(name)} { } - Predicate(std::string &&name, std::vector &&arguments) + explicit Predicate(std::string &&name, std::vector &&arguments) : name{std::move(name)}, arguments{std::move(arguments)} { @@ -238,7 +239,7 @@ struct SpecialInteger Supremum }; - SpecialInteger(Type type) + explicit SpecialInteger(Type type) : type{type} { } @@ -255,7 +256,7 @@ struct SpecialInteger struct String { - String(std::string &&text) + explicit String(std::string &&text) : text{std::move(text)} { } @@ -272,15 +273,8 @@ struct String struct Variable { - enum class Type - { - UserDefined, - Reserved - }; - - Variable(std::string &&name, Type type) - : name{std::move(name)}, - type{type} + explicit Variable(VariableDeclaration *declaration) + : declaration{declaration} { } @@ -289,6 +283,32 @@ struct Variable Variable(Variable &&other) = default; Variable &operator=(Variable &&other) = default; + VariableDeclaration *declaration = nullptr; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct VariableDeclaration +{ + // TODO: remove + enum class Type + { + UserDefined, + Head, + Body + }; + + explicit VariableDeclaration(std::string &&name, Type type) + : name{std::move(name)}, + type{type} + { + } + + VariableDeclaration(const VariableDeclaration &other) = delete; + VariableDeclaration &operator=(const VariableDeclaration &other) = delete; + VariableDeclaration(VariableDeclaration &&other) = default; + VariableDeclaration &operator=(VariableDeclaration &&other) = default; + std::string name; Type type; }; @@ -301,7 +321,7 @@ struct And { And() = default; - And(std::vector &&arguments) + explicit And(std::vector &&arguments) : arguments{std::move(arguments)} { } @@ -318,7 +338,7 @@ struct And struct Biconditional { - Biconditional(Formula &&left, Formula &&right) + explicit Biconditional(Formula &&left, Formula &&right) : left{std::move(left)}, right{std::move(right)} { @@ -337,7 +357,8 @@ struct Biconditional struct Exists { - Exists(std::vector &&variables, Formula &&argument) + // TODO: rename “variables” + explicit Exists(std::vector> &&variables, Formula &&argument) : variables{std::move(variables)}, argument{std::move(argument)} { @@ -348,7 +369,7 @@ struct Exists Exists(Exists &&other) noexcept = default; Exists &operator=(Exists &&other) noexcept = default; - std::vector variables; + std::vector> variables; Formula argument; }; @@ -356,7 +377,7 @@ struct Exists struct ForAll { - ForAll(std::vector &&variables, Formula &&argument) + explicit ForAll(std::vector> &&variables, Formula &&argument) : variables{std::move(variables)}, argument{std::move(argument)} { @@ -367,7 +388,7 @@ struct ForAll ForAll(ForAll &&other) noexcept = default; ForAll &operator=(ForAll &&other) noexcept = default; - std::vector variables; + std::vector> variables; Formula argument; }; @@ -375,7 +396,7 @@ struct ForAll struct Implies { - Implies(Formula &&antecedent, Formula &&consequent) + explicit Implies(Formula &&antecedent, Formula &&consequent) : antecedent{std::move(antecedent)}, consequent{std::move(consequent)} { @@ -394,7 +415,7 @@ struct Implies struct Not { - Not(Formula &&argument) + explicit Not(Formula &&argument) : argument{std::move(argument)} { } @@ -413,7 +434,7 @@ struct Or { Or() = default; - Or(std::vector &&arguments) + explicit Or(std::vector &&arguments) : arguments{std::move(arguments)} { } @@ -427,258 +448,23 @@ struct Or }; //////////////////////////////////////////////////////////////////////////////////////////////////// -// Deep Copying +// High-Level //////////////////////////////////////////////////////////////////////////////////////////////////// -BinaryOperation deepCopy(const BinaryOperation &other); -Boolean deepCopy(const Boolean &other); -Comparison deepCopy(const Comparison &other); -Constant deepCopy(const Constant &other); -Function deepCopy(const Function &other); -Integer deepCopy(const Integer &other); -Interval deepCopy(const Interval &other); -Predicate deepCopy(const Predicate &other); -SpecialInteger deepCopy(const SpecialInteger &other); -String deepCopy(const String &other); -Variable deepCopy(const Variable &other); -std::vector deepCopy(const std::vector &other); -And deepCopy(const And &other); -Biconditional deepCopy(const Biconditional &other); -Exists deepCopy(const Exists &other); -ForAll deepCopy(const ForAll &other); -Implies deepCopy(const Implies &other); -Not deepCopy(const Not &other); -Or deepCopy(const Or &other); - -Formula deepCopy(const Formula &formula); -std::vector deepCopy(const std::vector &formulas); -Term deepCopy(const Term &term); -std::vector deepCopy(const std::vector &terms); - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -template -struct VariantDeepCopyVisitor +struct ScopedFormula { - template - Variant visit(const T &x) + explicit ScopedFormula(ast::Formula &&formula, std::vector> &&freeVariables) + : formula{std::move(formula)}, + freeVariables{std::move(freeVariables)} { - return deepCopy(x); } + + ast::Formula formula; + std::vector> freeVariables; }; //////////////////////////////////////////////////////////////////////////////////////////////////// -const auto deepCopyVariant = - [](const auto &variant) -> typename std::decay::type - { - using VariantType = typename std::decay::type; - - return variant.accept(VariantDeepCopyVisitor()); - }; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -const auto deepCopyVariantVector = - [](const auto &variantVector) -> typename std::decay::type - { - using Type = typename std::decay::type::value_type; - - std::vector result; - result.reserve(variantVector.size()); - - for (const auto &variant : variantVector) - result.emplace_back(deepCopyVariant(variant)); - - return result; - }; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -const auto deepCopyVector = - [](const auto &vector) -> typename std::decay::type - { - using Type = typename std::decay::type::value_type; - - std::vector result; - result.reserve(vector.size()); - - for (const auto &element : vector) - result.emplace_back(deepCopy(element)); - - return result; - }; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline BinaryOperation deepCopy(const BinaryOperation &other) -{ - return BinaryOperation(other.operator_, deepCopy(other.left), deepCopy(other.right)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Boolean deepCopy(const Boolean &other) -{ - return Boolean(other.value); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Comparison deepCopy(const Comparison &other) -{ - return Comparison(other.operator_, deepCopy(other.left), deepCopy(other.right)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Constant deepCopy(const Constant &other) -{ - return Constant(std::string(other.name)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Function deepCopy(const Function &other) -{ - return Function(std::string(other.name), deepCopy(other.arguments)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Integer deepCopy(const Integer &other) -{ - return Integer(other.value); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Interval deepCopy(const Interval &other) -{ - return Interval(deepCopy(other.from), deepCopy(other.to)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Predicate deepCopy(const Predicate &other) -{ - return Predicate(std::string(other.name), deepCopy(other.arguments)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline SpecialInteger deepCopy(const SpecialInteger &other) -{ - return SpecialInteger(other.type); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline String deepCopy(const String &other) -{ - return String(std::string(other.text)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Variable deepCopy(const Variable &other) -{ - return Variable(std::string(other.name), other.type); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline std::vector deepCopy(const std::vector &other) -{ - return deepCopyVector(other); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline And deepCopy(const And &other) -{ - return And(deepCopy(other.arguments)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Biconditional deepCopy(const Biconditional &other) -{ - return Biconditional(deepCopy(other.left), deepCopy(other.right)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Exists deepCopy(const Exists &other) -{ - return Exists(deepCopy(other.variables), deepCopy(other.argument)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline ForAll deepCopy(const ForAll &other) -{ - return ForAll(deepCopy(other.variables), deepCopy(other.argument)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline In deepCopy(const In &other) -{ - return In(deepCopy(other.element), deepCopy(other.set)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Implies deepCopy(const Implies &other) -{ - return Implies(deepCopy(other.antecedent), deepCopy(other.consequent)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Not deepCopy(const Not &other) -{ - return Not(deepCopy(other.argument)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Or deepCopy(const Or &other) -{ - return Or(deepCopy(other.arguments)); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Formula deepCopy(const Formula &formula) -{ - return deepCopyVariant(formula); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline std::vector deepCopy(const std::vector &formulas) -{ - return deepCopyVariantVector(formulas); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline Term deepCopy(const Term &term) -{ - return deepCopyVariant(term); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline std::vector deepCopy(const std::vector &terms) -{ - return deepCopyVariantVector(terms); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - } } diff --git a/include/anthem/ASTCopy.h b/include/anthem/ASTCopy.h new file mode 100644 index 0000000..ca2bae4 --- /dev/null +++ b/include/anthem/ASTCopy.h @@ -0,0 +1,60 @@ +#ifndef __ANTHEM__AST_COPY_H +#define __ANTHEM__AST_COPY_H + +#include +#include + +namespace anthem +{ +namespace ast +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// ASTCopy +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Preparing Deep Copying +//////////////////////////////////////////////////////////////////////////////////////////////////// + +BinaryOperation prepareCopy(const BinaryOperation &other); +Boolean prepareCopy(const Boolean &other); +Comparison prepareCopy(const Comparison &other); +Constant prepareCopy(const Constant &other); +Function prepareCopy(const Function &other); +In prepareCopy(const In &other); +Integer prepareCopy(const Integer &other); +Interval prepareCopy(const Interval &other); +Predicate prepareCopy(const Predicate &other); +SpecialInteger prepareCopy(const SpecialInteger &other); +String prepareCopy(const String &other); +Variable prepareCopy(const Variable &other); +VariableDeclaration prepareCopy(const VariableDeclaration &other); +VariableDeclarationPointers prepareCopy(const VariableDeclarationPointers &other); +And prepareCopy(const And &other); +Biconditional prepareCopy(const Biconditional &other); +Exists prepareCopy(const Exists &other); +ForAll prepareCopy(const ForAll &other); +Implies prepareCopy(const Implies &other); +Not prepareCopy(const Not &other); +Or prepareCopy(const Or &other); + +Term prepareCopy(const Term &term); +std::vector prepareCopy(const std::vector &terms); +Formula prepareCopy(const Formula &formula); +std::vector prepareCopy(const std::vector &formulas); + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Fixing Dangling Variables +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void fixDanglingVariables(ScopedFormula &scopedFormula); + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} +} + +#endif diff --git a/include/anthem/ASTForward.h b/include/anthem/ASTForward.h index 4024bf5..d679222 100644 --- a/include/anthem/ASTForward.h +++ b/include/anthem/ASTForward.h @@ -1,7 +1,7 @@ #ifndef __ANTHEM__AST_FORWARD_H #define __ANTHEM__AST_FORWARD_H -#include +#include #include @@ -38,6 +38,9 @@ struct Predicate; struct SpecialInteger; struct String; struct Variable; +struct VariableDeclaration; +using VariableDeclarationPointer = std::unique_ptr; +using VariableDeclarationPointers = std::vector; //////////////////////////////////////////////////////////////////////////////////////////////////// // Variants @@ -67,6 +70,12 @@ using Term = Clingo::Variant< String, Variable>; +//////////////////////////////////////////////////////////////////////////////////////////////////// +// High-Level +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct ScopedFormula; + //////////////////////////////////////////////////////////////////////////////////////////////////// } diff --git a/include/anthem/ASTUtils.h b/include/anthem/ASTUtils.h index 8f62d90..550415d 100644 --- a/include/anthem/ASTUtils.h +++ b/include/anthem/ASTUtils.h @@ -1,6 +1,8 @@ #ifndef __ANTHEM__AST_UTILS_H #define __ANTHEM__AST_UTILS_H +#include + #include namespace anthem @@ -14,16 +16,18 @@ namespace ast // //////////////////////////////////////////////////////////////////////////////////////////////////// +// TODO: rename to VariableDeclarationStack or ParameterStack class VariableStack { public: - using Layer = const std::vector *; + using Layer = ast::VariableDeclarationPointers *; public: void push(Layer layer); void pop(); - bool contains(const ast::Variable &variable) const; + std::experimental::optional findVariableDeclaration(const char *variableName) const; + bool contains(const ast::VariableDeclaration &variableDeclaration) const; private: std::vector m_layers; @@ -31,8 +35,8 @@ class VariableStack //////////////////////////////////////////////////////////////////////////////////////////////////// -std::vector collectFreeVariables(const ast::Formula &formula); -std::vector collectFreeVariables(const ast::Formula &formula, ast::VariableStack &variableStack); +std::vector collectFreeVariables(ast::Formula &formula); +std::vector collectFreeVariables(ast::Formula &formula, ast::VariableStack &variableStack); bool matches(const ast::Predicate &lhs, const ast::Predicate &rhs); void collectPredicates(const ast::Formula &formula, std::vector &predicates); diff --git a/include/anthem/ASTVisitors.h b/include/anthem/ASTVisitors.h index 49db5d7..bdca776 100644 --- a/include/anthem/ASTVisitors.h +++ b/include/anthem/ASTVisitors.h @@ -110,6 +110,7 @@ struct RecursiveFormulaVisitor template struct RecursiveTermVisitor { + // TODO: return type is incorrect template void visit(ast::BinaryOperation &binaryOperation, ast::Term &term, Arguments &&... arguments) { diff --git a/include/anthem/Body.h b/include/anthem/Body.h index 4e5bf4e..710c10c 100644 --- a/include/anthem/Body.h +++ b/include/anthem/Body.h @@ -40,11 +40,12 @@ ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOp //////////////////////////////////////////////////////////////////////////////////////////////////// -ast::Variable makeAuxiliaryBodyVariable(int i) +std::unique_ptr makeBodyVariableDeclaration(int i) { - auto variableName = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(i); + // TODO: drop name + auto variableName = "#" + std::string(BodyVariablePrefix) + std::to_string(i); - return ast::Variable(std::move(variableName), ast::Variable::Type::Reserved); + return std::make_unique(std::move(variableName), ast::VariableDeclaration::Type::Body); } //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -52,7 +53,7 @@ ast::Variable makeAuxiliaryBodyVariable(int i) struct BodyTermTranslateVisitor { // TODO: refactor - std::experimental::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, Context &context) + std::experimental::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, Context &context, RuleContext &ruleContext, ast::VariableStack &variableStack) { if (literal.sign == Clingo::AST::Sign::DoubleNegation) throwErrorAtLocation(literal.location, "double-negated literals currently unsupported", context); @@ -67,39 +68,42 @@ struct BodyTermTranslateVisitor return ast::Formula::make(std::move(predicate)); } - std::vector variables; - variables.reserve(function.arguments.size()); + // Create new body variable declarations + std::vector> parameters; + parameters.reserve(function.arguments.size()); + + variableStack.push(¶meters); for (size_t i = 0; i < function.arguments.size(); i++) - variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID + i)); + parameters.emplace_back(makeBodyVariableDeclaration(i + 1)); ast::And conjunction; for (size_t i = 0; i < function.arguments.size(); i++) { - const auto &argument = function.arguments[i]; - conjunction.arguments.emplace_back(ast::Formula::make(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID + i), translate(argument, context))); + auto &argument = function.arguments[i]; + conjunction.arguments.emplace_back(ast::Formula::make(ast::Variable(parameters[i].get()), translate(argument, context, ruleContext, variableStack))); } ast::Predicate predicate(std::string(function.name)); predicate.arguments.reserve(function.arguments.size()); for (size_t i = 0; i < function.arguments.size(); i++) - predicate.arguments.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID + i)); + predicate.arguments.emplace_back(ast::Variable(parameters[i].get())); if (literal.sign == Clingo::AST::Sign::None) conjunction.arguments.emplace_back(std::move(predicate)); else if (literal.sign == Clingo::AST::Sign::Negation) conjunction.arguments.emplace_back(ast::Formula::make(std::move(predicate))); - context.auxiliaryBodyVariableID += function.arguments.size(); - - return ast::Formula::make(std::move(variables), std::move(conjunction)); + return ast::Formula::make(std::move(parameters), std::move(conjunction)); } template - std::experimental::optional visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context, RuleContext &, ast::VariableStack &) { + assert(!term.data.is()); + throwErrorAtLocation(term.location, "term currently unsupported in this context, expected function", context); return std::experimental::nullopt; } @@ -109,18 +113,18 @@ struct BodyTermTranslateVisitor struct BodyLiteralTranslateVisitor { - std::experimental::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, Context &) + std::experimental::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, Context &, RuleContext &, ast::VariableStack &) { return ast::Formula::make(boolean.value); } - std::experimental::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, Context &context) + std::experimental::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, Context &context, RuleContext &ruleContext, ast::VariableStack &variableStack) { - return term.data.accept(BodyTermTranslateVisitor(), literal, term, context); + return term.data.accept(BodyTermTranslateVisitor(), literal, term, context, ruleContext, variableStack); } // TODO: refactor - std::experimental::optional visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, Context &context) + std::experimental::optional visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, Context &context, RuleContext &ruleContext, ast::VariableStack &variableStack) { // Comparisons should never have a sign, because these are converted to positive comparisons by clingo if (literal.sign != Clingo::AST::Sign::None) @@ -128,24 +132,22 @@ struct BodyLiteralTranslateVisitor const auto operator_ = translate(comparison.comparison); - std::vector variables; - variables.reserve(2); - variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID)); - variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID + 1)); + std::vector> parameters; + parameters.reserve(2); + parameters.emplace_back(makeBodyVariableDeclaration(1)); + parameters.emplace_back(makeBodyVariableDeclaration(2)); ast::And conjunction; conjunction.arguments.reserve(3); - conjunction.arguments.emplace_back(ast::Formula::make(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID), translate(comparison.left, context))); - conjunction.arguments.emplace_back(ast::Formula::make(makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID + 1), translate(comparison.right, context))); - conjunction.arguments.emplace_back(ast::Formula::make(operator_, makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID), makeAuxiliaryBodyVariable(context.auxiliaryBodyVariableID + 1))); + conjunction.arguments.emplace_back(ast::Formula::make(ast::Variable(parameters[0].get()), translate(comparison.left, context, ruleContext, variableStack))); + conjunction.arguments.emplace_back(ast::Formula::make(ast::Variable(parameters[1].get()), translate(comparison.right, context, ruleContext, variableStack))); + conjunction.arguments.emplace_back(ast::Formula::make(operator_, ast::Variable(parameters[0].get()), ast::Variable(parameters[1].get()))); - context.auxiliaryBodyVariableID += 2; - - return ast::Formula::make(std::move(variables), std::move(conjunction)); + return ast::Formula::make(std::move(parameters), std::move(conjunction)); } template - std::experimental::optional visit(const T &, const Clingo::AST::Literal &literal, Context &context) + std::experimental::optional visit(const T &, const Clingo::AST::Literal &literal, Context &context, RuleContext &, ast::VariableStack &) { throwErrorAtLocation(literal.location, "literal currently unsupported in this context, expected function or term", context); return std::experimental::nullopt; @@ -156,16 +158,16 @@ struct BodyLiteralTranslateVisitor struct BodyBodyLiteralTranslateVisitor { - std::experimental::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context) + std::experimental::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context, RuleContext &ruleContext, ast::VariableStack &variableStack) { if (bodyLiteral.sign != Clingo::AST::Sign::None) throwErrorAtLocation(bodyLiteral.location, "only positive body literals supported currently", context); - return literal.data.accept(BodyLiteralTranslateVisitor(), literal, context); + return literal.data.accept(BodyLiteralTranslateVisitor(), literal, context, ruleContext, variableStack); } template - std::experimental::optional visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context) + std::experimental::optional visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context, RuleContext &, ast::VariableStack &) { throwErrorAtLocation(bodyLiteral.location, "body literal currently unsupported in this context, expected literal", context); return std::experimental::nullopt; diff --git a/include/anthem/Completion.h b/include/anthem/Completion.h index b777a48..11bd30c 100644 --- a/include/anthem/Completion.h +++ b/include/anthem/Completion.h @@ -12,7 +12,7 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -void complete(std::vector &formulas); +void complete(std::vector &scopedFormulas); //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/Context.h b/include/anthem/Context.h index 026ebd1..236fca7 100644 --- a/include/anthem/Context.h +++ b/include/anthem/Context.h @@ -1,8 +1,6 @@ #ifndef __ANTHEM__CONTEXT_H #define __ANTHEM__CONTEXT_H -#include - #include namespace anthem @@ -16,25 +14,19 @@ namespace anthem struct Context { - void reset() + Context() = default; + + explicit Context(output::Logger &&logger) + : logger{std::move(logger)} { - headTerms.clear(); - isChoiceRule = false; - numberOfHeadLiterals = 0; - auxiliaryBodyVariableID = 1; - anonymousVariableID = 1; } output::Logger logger; - std::vector headTerms; - bool isChoiceRule = false; - size_t numberOfHeadLiterals = 0; - size_t auxiliaryBodyVariableID = 1; - size_t anonymousVariableID = 1; - bool simplify = false; bool complete = false; + + size_t anonymousVariableID = 1; }; //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/Head.h b/include/anthem/Head.h index 4f53ed6..a44ee60 100644 --- a/include/anthem/Head.h +++ b/include/anthem/Head.h @@ -2,8 +2,10 @@ #define __ANTHEM__HEAD_H #include +#include #include +#include #include #include @@ -16,21 +18,25 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Collect Head Terms +//////////////////////////////////////////////////////////////////////////////////////////////////// + struct TermCollectFunctionTermsVisitor { - void visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context) + void visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context, RuleContext &ruleContext) { if (function.external) throwErrorAtLocation(term.location, "external functions currently unsupported", context); - context.headTerms.reserve(context.headTerms.size() + function.arguments.size()); + ruleContext.headTerms.reserve(ruleContext.headTerms.size() + function.arguments.size()); for (const auto &argument : function.arguments) - context.headTerms.emplace_back(&argument); + ruleContext.headTerms.emplace_back(&argument); } template - void visit(const T &, const Clingo::AST::Term &term, Context &context) + void visit(const T &, const Clingo::AST::Term &term, Context &context, RuleContext &) { throwErrorAtLocation(term.location, "term currently unsupported in this context, function expected", context); } @@ -40,17 +46,17 @@ struct TermCollectFunctionTermsVisitor struct LiteralCollectFunctionTermsVisitor { - void visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &, Context &) + void visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &, Context &, RuleContext &) { } - void visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, Context &context) + void visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, Context &context, RuleContext &ruleContext) { - term.data.accept(TermCollectFunctionTermsVisitor(), term, context); + term.data.accept(TermCollectFunctionTermsVisitor(), term, context, ruleContext); } template - void visit(const T &, const Clingo::AST::Literal &literal, Context &context) + void visit(const T &, const Clingo::AST::Literal &literal, Context &context, RuleContext &) { throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals", context); } @@ -61,30 +67,30 @@ struct LiteralCollectFunctionTermsVisitor // TODO: rename, because not only terms are collected anymore struct HeadLiteralCollectFunctionTermsVisitor { - void visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, Context &context) + void visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, Context &context, RuleContext &ruleContext) { - context.numberOfHeadLiterals = 1; + ruleContext.numberOfHeadLiterals = 1; - literal.data.accept(LiteralCollectFunctionTermsVisitor(), literal, context); + literal.data.accept(LiteralCollectFunctionTermsVisitor(), literal, context, ruleContext); } - void visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, Context &context) + void visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, Context &context, RuleContext &ruleContext) { - context.numberOfHeadLiterals = disjunction.elements.size(); + ruleContext.numberOfHeadLiterals = disjunction.elements.size(); for (const auto &conditionalLiteral : disjunction.elements) { if (!conditionalLiteral.condition.empty()) throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported", context); - conditionalLiteral.literal.data.accept(LiteralCollectFunctionTermsVisitor(), conditionalLiteral.literal, context); + conditionalLiteral.literal.data.accept(LiteralCollectFunctionTermsVisitor(), conditionalLiteral.literal, context, ruleContext); } } - void visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, Context &context) + void visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, Context &context, RuleContext &ruleContext) { - context.isChoiceRule = true; - context.numberOfHeadLiterals = aggregate.elements.size(); + ruleContext.isChoiceRule = true; + ruleContext.numberOfHeadLiterals = aggregate.elements.size(); if (aggregate.left_guard || aggregate.right_guard) throwErrorAtLocation(headLiteral.location, "aggregates with left or right guards currently unsupported", context); @@ -94,23 +100,25 @@ struct HeadLiteralCollectFunctionTermsVisitor if (!conditionalLiteral.condition.empty()) throwErrorAtLocation(headLiteral.location, "conditional literals in aggregates currently unsupported", context); - conditionalLiteral.literal.data.accept(LiteralCollectFunctionTermsVisitor(), conditionalLiteral.literal, context); + conditionalLiteral.literal.data.accept(LiteralCollectFunctionTermsVisitor(), conditionalLiteral.literal, context, ruleContext); } } template - void visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, Context &context) + void visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, Context &context, RuleContext &) { throwErrorAtLocation(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate", context); } }; +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Translate Head //////////////////////////////////////////////////////////////////////////////////////////////////// struct FunctionTermTranslateVisitor { // TODO: check correctness - std::experimental::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context, RuleContext &ruleContext, size_t &headVariableIndex) { if (function.external) throwErrorAtLocation(term.location, "external functions currently unsupported", context); @@ -118,22 +126,14 @@ struct FunctionTermTranslateVisitor std::vector arguments; arguments.reserve(function.arguments.size()); - for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++) - { - const auto &argument = *i; - const auto matchingTerm = std::find(context.headTerms.cbegin(), context.headTerms.cend(), &argument); - - assert(matchingTerm != context.headTerms.cend()); - - auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(matchingTerm - context.headTerms.cbegin() + 1); - arguments.emplace_back(ast::Variable(std::move(variableName), ast::Variable::Type::Reserved)); - } + for (size_t i = 0; i < function.arguments.size(); i++) + arguments.emplace_back(ast::Variable(ruleContext.freeVariables[headVariableIndex++].get())); return ast::Formula::make(function.name, std::move(arguments)); } template - std::experimental::optional visit(const T &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const T &, const Clingo::AST::Term &term, Context &context, RuleContext &, size_t &) { throwErrorAtLocation(term.location, "term currently unsupported in this context, function expected", context); return std::experimental::nullopt; @@ -144,18 +144,18 @@ struct FunctionTermTranslateVisitor struct LiteralTranslateVisitor { - std::experimental::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, Context &) + std::experimental::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, Context &, RuleContext &, size_t &) { return ast::Formula::make(boolean.value); } - std::experimental::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, Context &context) + std::experimental::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, Context &context, RuleContext &ruleContext, size_t &headVariableIndex) { - return term.data.accept(FunctionTermTranslateVisitor(), term, context); + return term.data.accept(FunctionTermTranslateVisitor(), term, context, ruleContext, headVariableIndex); } template - std::experimental::optional visit(const T &, const Clingo::AST::Literal &literal, Context &context) + std::experimental::optional visit(const T &, const Clingo::AST::Literal &literal, Context &context, RuleContext &, size_t &) { throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals", context); return std::experimental::nullopt; @@ -166,12 +166,12 @@ struct LiteralTranslateVisitor struct HeadLiteralTranslateToConsequentVisitor { - std::experimental::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, Context &context) + std::experimental::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, Context &context, RuleContext &ruleContext, size_t &headVariableIndex) { if (literal.sign == Clingo::AST::Sign::DoubleNegation) throwErrorAtLocation(literal.location, "double-negated head literals currently unsupported", context); - auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, context); + auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, context, ruleContext, headVariableIndex); if (literal.sign == Clingo::AST::Sign::None) return translatedLiteral; @@ -182,7 +182,7 @@ struct HeadLiteralTranslateToConsequentVisitor return ast::Formula::make(std::move(translatedLiteral.value())); } - std::experimental::optional visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, Context &context) + std::experimental::optional visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, Context &context, RuleContext &ruleContext, size_t &headVariableIndex) { std::vector arguments; arguments.reserve(disjunction.elements.size()); @@ -192,7 +192,7 @@ struct HeadLiteralTranslateToConsequentVisitor if (!conditionalLiteral.condition.empty()) throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported", context); - auto argument = visit(conditionalLiteral.literal, headLiteral, context); + auto argument = visit(conditionalLiteral.literal, headLiteral, context, ruleContext, headVariableIndex); if (!argument) throwErrorAtLocation(headLiteral.location, "could not parse argument", context); @@ -203,7 +203,7 @@ struct HeadLiteralTranslateToConsequentVisitor return ast::Formula::make(std::move(arguments)); } - std::experimental::optional visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, Context &context) + std::experimental::optional visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, Context &context, RuleContext &ruleContext, size_t &headVariableIndex) { if (aggregate.left_guard || aggregate.right_guard) throwErrorAtLocation(headLiteral.location, "aggregates with left or right guards currently unsupported", context); @@ -214,7 +214,7 @@ struct HeadLiteralTranslateToConsequentVisitor if (!conditionalLiteral.condition.empty()) throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported", context); - return this->visit(conditionalLiteral.literal, headLiteral, context); + return this->visit(conditionalLiteral.literal, headLiteral, context, ruleContext, headVariableIndex); }; if (aggregate.elements.size() == 1) @@ -237,7 +237,7 @@ struct HeadLiteralTranslateToConsequentVisitor } template - std::experimental::optional visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, Context &context) + std::experimental::optional visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, Context &context, RuleContext &, size_t &) { throwErrorAtLocation(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate", context); return std::experimental::nullopt; diff --git a/include/anthem/RuleContext.h b/include/anthem/RuleContext.h new file mode 100644 index 0000000..6543aaa --- /dev/null +++ b/include/anthem/RuleContext.h @@ -0,0 +1,34 @@ +#ifndef __ANTHEM__RULE_CONTEXT_H +#define __ANTHEM__RULE_CONTEXT_H + +#include + +#include +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// RuleContext +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct RuleContext +{ + std::vector headTerms; + ast::VariableDeclarationPointers freeVariables; + + // Index of the first auxiliary head variable into the vector freeVariables + size_t headVariablesStartIndex = 0; + + bool isChoiceRule = false; + size_t numberOfHeadLiterals = 0; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} + +#endif diff --git a/include/anthem/StatementVisitor.h b/include/anthem/StatementVisitor.h index b895d3b..226e4f9 100644 --- a/include/anthem/StatementVisitor.h +++ b/include/anthem/StatementVisitor.h @@ -2,8 +2,10 @@ #define __ANTHEM__STATEMENT_VISITOR_H #include +#include #include #include +#include #include #include @@ -35,7 +37,7 @@ inline void reduce(ast::Implies &implies) struct StatementVisitor { - void visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, std::vector &, Context &context) + void visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, std::vector &, Context &context) { // TODO: refactor context.logger.log(output::Priority::Debug, (std::string("[program] ") + program.name).c_str()); @@ -44,17 +46,35 @@ struct StatementVisitor throwErrorAtLocation(statement.location, "program parameters currently unsupported", context); } - void visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, std::vector &formulas, Context &context) + void visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, std::vector &scopedFormulas, Context &context) { - context.reset(); + RuleContext ruleContext; + ast::VariableStack variableStack; + variableStack.push(&ruleContext.freeVariables); - // Concatenate all head terms - rule.head.data.accept(HeadLiteralCollectFunctionTermsVisitor(), rule.head, context); + // Collect all head terms + rule.head.data.accept(HeadLiteralCollectFunctionTermsVisitor(), rule.head, context, ruleContext); + + // Create new variable declarations for the head terms + ruleContext.headVariablesStartIndex = ruleContext.freeVariables.size(); + ruleContext.freeVariables.reserve(ruleContext.headTerms.size()); + + for (size_t i = 0; i < ruleContext.headTerms.size(); i++) + { + // TODO: drop name + auto variableName = "#" + std::string(HeadVariablePrefix) + std::to_string(ruleContext.freeVariables.size() + 1); + auto variableDeclaration = std::make_unique(std::move(variableName), ast::VariableDeclaration::Type::Head); + + ruleContext.freeVariables.emplace_back(std::move(variableDeclaration)); + } ast::And antecedent; // Compute consequent - auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, context); + auto headVariableIndex = ruleContext.headVariablesStartIndex; + auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, context, ruleContext, headVariableIndex); + + assert(ruleContext.headTerms.size() == headVariableIndex - ruleContext.headVariablesStartIndex); if (!consequent) { @@ -64,13 +84,13 @@ struct StatementVisitor } // Generate auxiliary variables replacing the head atom’s arguments - for (auto i = context.headTerms.cbegin(); i != context.headTerms.cend(); i++) + for (auto i = ruleContext.headTerms.cbegin(); i != ruleContext.headTerms.cend(); i++) { const auto &headTerm = **i; - auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i - context.headTerms.cbegin() + 1); - auto element = ast::Variable(std::move(variableName), ast::Variable::Type::Reserved); - auto set = translate(headTerm, context); + const auto auxiliaryHeadVariableID = ruleContext.headVariablesStartIndex + i - ruleContext.headTerms.cbegin(); + auto element = ast::Variable(ruleContext.freeVariables[auxiliaryHeadVariableID].get()); + auto set = translate(headTerm, context, ruleContext, variableStack); auto in = ast::In(std::move(element), std::move(set)); antecedent.arguments.emplace_back(std::move(in)); @@ -81,7 +101,7 @@ struct StatementVisitor { const auto &bodyLiteral = *i; - auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, context); + auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, context, ruleContext, variableStack); if (!argument) throwErrorAtLocation(bodyLiteral.location, "could not translate body literal", context); @@ -89,26 +109,38 @@ struct StatementVisitor antecedent.arguments.emplace_back(std::move(argument.value())); } - if (!context.isChoiceRule) + if (!ruleContext.isChoiceRule) { - formulas.emplace_back(ast::Formula::make(std::move(antecedent), std::move(consequent.value()))); - reduce(formulas.back().get()); + auto formula = ast::Formula::make(std::move(antecedent), std::move(consequent.value())); + ast::ScopedFormula scopedFormula(std::move(formula), std::move(ruleContext.freeVariables)); + scopedFormulas.emplace_back(std::move(scopedFormula)); + reduce(scopedFormulas.back().formula.get()); } else { const auto createFormula = [&](ast::Formula &argument, bool isLastOne) { - auto consequent = std::move(argument); + auto &consequent = argument; if (!isLastOne) - formulas.emplace_back(ast::Formula::make(ast::deepCopy(antecedent), std::move(consequent))); + { + auto formula = ast::Formula::make(ast::prepareCopy(antecedent), std::move(consequent)); + ast::ScopedFormula scopedFormula(std::move(formula), {}); + ast::fixDanglingVariables(scopedFormula); + scopedFormulas.emplace_back(std::move(scopedFormula)); + } else - formulas.emplace_back(ast::Formula::make(std::move(antecedent), std::move(consequent))); + { + auto formula = ast::Formula::make(std::move(antecedent), std::move(consequent)); + ast::ScopedFormula scopedFormula(std::move(formula), std::move(ruleContext.freeVariables)); + scopedFormulas.emplace_back(std::move(scopedFormula)); + } - auto &implies = formulas.back().get(); + auto &implies = scopedFormulas.back().formula.get(); auto &antecedent = implies.antecedent.get(); - antecedent.arguments.emplace_back(ast::deepCopy(implies.consequent)); + antecedent.arguments.emplace_back(ast::prepareCopy(implies.consequent)); + ast::fixDanglingVariables(scopedFormulas.back()); reduce(implies); }; @@ -127,7 +159,7 @@ struct StatementVisitor } template - void visit(const T &, const Clingo::AST::Statement &statement, std::vector &, Context &context) + void visit(const T &, const Clingo::AST::Statement &statement, std::vector &, Context &context) { throwErrorAtLocation(statement.location, "statement currently unsupported, expected rule", context); } diff --git a/include/anthem/Term.h b/include/anthem/Term.h index 974a24d..3b10fac 100644 --- a/include/anthem/Term.h +++ b/include/anthem/Term.h @@ -4,6 +4,8 @@ #include #include +#include +#include #include #include @@ -39,13 +41,13 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera //////////////////////////////////////////////////////////////////////////////////////////////////// -ast::Term translate(const Clingo::AST::Term &term, Context &context); +ast::Term translate(const Clingo::AST::Term &term, Context &context, RuleContext &ruleContext, const ast::VariableStack &variableStack); //////////////////////////////////////////////////////////////////////////////////////////////////// struct TermTranslateVisitor { - std::experimental::optional visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, Context &context, RuleContext &ruleContext, const ast::VariableStack &variableStack) { switch (symbol.type()) { @@ -66,7 +68,7 @@ struct TermTranslateVisitor for (const auto &argument : symbol.arguments()) { - auto translatedArgument = visit(argument, term, context); + auto translatedArgument = visit(argument, term, context, ruleContext, variableStack); if (!translatedArgument) throwErrorAtLocation(term.location, "could not translate argument", context); @@ -81,43 +83,46 @@ struct TermTranslateVisitor return std::experimental::nullopt; } - std::experimental::optional visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, Context &context) + std::experimental::optional visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, Context &, RuleContext &ruleContext, const ast::VariableStack &variableStack) { - if (strcmp(variable.name, "_") == 0) - { - std::string variableName = AnonymousVariablePrefix + std::to_string(context.anonymousVariableID); - context.anonymousVariableID++; + const auto matchingVariableDeclaration = variableStack.findVariableDeclaration(variable.name); + const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0); + const auto isUndeclaredUserVariable = !matchingVariableDeclaration; + const auto isUndeclared = isAnonymousVariable || isUndeclaredUserVariable; - return ast::Term::make(std::move(variableName), ast::Variable::Type::Reserved); - } + if (!isUndeclared) + return ast::Term::make(*matchingVariableDeclaration); - return ast::Term::make(std::string(variable.name), ast::Variable::Type::UserDefined); + auto variableDeclaration = std::make_unique(std::string(variable.name), ast::VariableDeclaration::Type::UserDefined); + ruleContext.freeVariables.emplace_back(std::move(variableDeclaration)); + + return ast::Term::make(ruleContext.freeVariables.back().get()); } - std::experimental::optional visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, Context &context, RuleContext &, const ast::VariableStack &) { throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported", context); return std::experimental::nullopt; } - std::experimental::optional visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, Context &context, RuleContext &ruleContext, const ast::VariableStack &variableStack) { const auto operator_ = translate(binaryOperation.binary_operator, term, context); - auto left = translate(binaryOperation.left, context); - auto right = translate(binaryOperation.right, context); + auto left = translate(binaryOperation.left, context, ruleContext, variableStack); + auto right = translate(binaryOperation.right, context, ruleContext, variableStack); return ast::Term::make(operator_, std::move(left), std::move(right)); } - std::experimental::optional visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, Context &context) + std::experimental::optional visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, Context &context, RuleContext &ruleContext, const ast::VariableStack &variableStack) { - auto left = translate(interval.left, context); - auto right = translate(interval.right, context); + auto left = translate(interval.left, context, ruleContext, variableStack); + auto right = translate(interval.right, context, ruleContext, variableStack); return ast::Term::make(std::move(left), std::move(right)); } - std::experimental::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context, RuleContext &ruleContext, const ast::VariableStack &variableStack) { if (function.external) throwErrorAtLocation(term.location, "external functions currently unsupported", context); @@ -126,12 +131,12 @@ struct TermTranslateVisitor arguments.reserve(function.arguments.size()); for (const auto &argument : function.arguments) - arguments.emplace_back(translate(argument, context)); + arguments.emplace_back(translate(argument, context, ruleContext, variableStack)); return ast::Term::make(function.name, std::move(arguments)); } - std::experimental::optional visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, Context &context, RuleContext &, const ast::VariableStack &) { throwErrorAtLocation(term.location, "“pool” terms currently unsupported", context); return std::experimental::nullopt; @@ -140,9 +145,9 @@ struct TermTranslateVisitor //////////////////////////////////////////////////////////////////////////////////////////////////// -ast::Term translate(const Clingo::AST::Term &term, Context &context) +ast::Term translate(const Clingo::AST::Term &term, Context &context, RuleContext &ruleContext, const ast::VariableStack &variableStack) { - auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, context); + auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, context, ruleContext, variableStack); if (!translatedTerm) throwErrorAtLocation(term.location, "could not translate term", context); diff --git a/include/anthem/Utils.h b/include/anthem/Utils.h index b7f64ca..49e75a1 100644 --- a/include/anthem/Utils.h +++ b/include/anthem/Utils.h @@ -57,39 +57,9 @@ inline bool isPrefix(const char *prefix, const char *string) //////////////////////////////////////////////////////////////////////////////////////////////////// -constexpr const auto AuxiliaryHeadVariablePrefix = "V"; -constexpr const auto AuxiliaryBodyVariablePrefix = "X"; -constexpr const auto AnonymousVariablePrefix = "A"; -constexpr const auto UserVariablePrefix = "_"; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -inline bool isReservedVariableName(const char *variableName) -{ - if (!isPrefix(AuxiliaryBodyVariablePrefix, variableName) - && !isPrefix(AuxiliaryHeadVariablePrefix, variableName) - && !isPrefix(AnonymousVariablePrefix, variableName)) - { - return false; - } - - assert(std::strlen(AuxiliaryBodyVariablePrefix) == std::strlen(AuxiliaryHeadVariablePrefix)); - assert(std::strlen(AuxiliaryBodyVariablePrefix) == std::strlen(AnonymousVariablePrefix)); - assert(std::strlen(AuxiliaryBodyVariablePrefix) == std::strlen(UserVariablePrefix)); - - const auto prefixLength = std::strlen(AuxiliaryBodyVariablePrefix); - - if (strlen(variableName) == prefixLength) - return false; - - const char *suffix = variableName + prefixLength; - - for (const auto *i = suffix; *i != '\0'; i++) - if (!std::isdigit(*i)) - return false; - - return true; -} +constexpr const auto HeadVariablePrefix = "V"; +constexpr const auto BodyVariablePrefix = "X"; +constexpr const auto UserVariablePrefix = "U"; //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/output/AST.h b/include/anthem/output/AST.h index cbad6be..b678e49 100644 --- a/include/anthem/output/AST.h +++ b/include/anthem/output/AST.h @@ -2,6 +2,7 @@ #define __ANTHEM__OUTPUT__AST_H #include +#include #include #include @@ -19,36 +20,46 @@ namespace ast // //////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, BinaryOperation::Operator operator_); -output::ColorStream &operator<<(output::ColorStream &stream, const BinaryOperation &binaryOperation); -output::ColorStream &operator<<(output::ColorStream &stream, const Boolean &boolean); -output::ColorStream &operator<<(output::ColorStream &stream, const Comparison &comparison); -output::ColorStream &operator<<(output::ColorStream &stream, const Constant &constant); -output::ColorStream &operator<<(output::ColorStream &stream, const Function &function); -output::ColorStream &operator<<(output::ColorStream &stream, const In &in); -output::ColorStream &operator<<(output::ColorStream &stream, const Integer &integer); -output::ColorStream &operator<<(output::ColorStream &stream, const Interval &interval); -output::ColorStream &operator<<(output::ColorStream &stream, const Predicate &predicate); -output::ColorStream &operator<<(output::ColorStream &stream, const SpecialInteger &specialInteger); -output::ColorStream &operator<<(output::ColorStream &stream, const String &string); -output::ColorStream &operator<<(output::ColorStream &stream, const Variable &variable); +struct PrintContext +{ + std::map userVariableIDs; + std::map headVariableIDs; + std::map bodyVariableIDs; +}; -output::ColorStream &operator<<(output::ColorStream &stream, const And &and_); -output::ColorStream &operator<<(output::ColorStream &stream, const Biconditional &biconditional); -output::ColorStream &operator<<(output::ColorStream &stream, const Exists &exists); -output::ColorStream &operator<<(output::ColorStream &stream, const ForAll &forAll); -output::ColorStream &operator<<(output::ColorStream &stream, const Implies &implies); -output::ColorStream &operator<<(output::ColorStream &stream, const Not ¬_); -output::ColorStream &operator<<(output::ColorStream &stream, const Or &or_); +//////////////////////////////////////////////////////////////////////////////////////////////////// -output::ColorStream &operator<<(output::ColorStream &stream, const Formula &formula); -output::ColorStream &operator<<(output::ColorStream &stream, const Term &term); +output::ColorStream &print(output::ColorStream &stream, const BinaryOperation::Operator operator_, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext); + +output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Not ¬_, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext); + +output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext); +output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext); //////////////////////////////////////////////////////////////////////////////////////////////////// // Primitives //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, BinaryOperation::Operator operator_) +inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &) { switch (operator_) { @@ -69,14 +80,22 @@ inline output::ColorStream &operator<<(output::ColorStream &stream, BinaryOperat //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const BinaryOperation &binaryOperation) +inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext) { - return (stream << "(" << binaryOperation.left << " " << binaryOperation.operator_ << " " << binaryOperation.right << ")"); + stream << "("; + print(stream, binaryOperation.left, printContext); + stream << " "; + print(stream, binaryOperation.operator_, printContext); + stream << " "; + print(stream, binaryOperation.right, printContext); + stream << ")"; + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Boolean &boolean) +inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &) { if (boolean.value) return (stream << output::Boolean("#true")); @@ -86,7 +105,7 @@ inline output::ColorStream &operator<<(output::ColorStream &stream, const Boolea //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, Comparison::Operator operator_) +inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &) { switch (operator_) { @@ -109,21 +128,27 @@ inline output::ColorStream &operator<<(output::ColorStream &stream, Comparison:: //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Comparison &comparison) +inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext) { - return (stream << comparison.left << " " << comparison.operator_ << " " << comparison.right); + print(stream, comparison.left, printContext); + stream << " "; + print(stream, comparison.operator_, printContext); + stream << " "; + print(stream, comparison.right, printContext); + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Constant &constant) +inline output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &) { return (stream << constant.name); } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Function &function) +inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext) { stream << function.name; @@ -137,39 +162,49 @@ inline output::ColorStream &operator<<(output::ColorStream &stream, const Functi if (i != function.arguments.cbegin()) stream << ", "; - stream << (*i); + print(stream, *i, printContext); } if (function.name.empty() && function.arguments.size() == 1) stream << ","; - return (stream << ")"); + stream << ")"; + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const In &in) +inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext) { - return (stream << in.element << " " << output::Keyword("in") << " " << in.set); + print(stream, in.element, printContext); + stream << " " << output::Keyword("in") << " "; + print(stream, in.set, printContext); + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Integer &integer) +inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &) { return (stream << output::Number(integer.value)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Interval &interval) +inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext) { - return (stream << interval.from << ".." << interval.to); + print(stream, interval.from, printContext); + stream << ".."; + print(stream, interval.to, printContext); + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Predicate &predicate) +inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext) { stream << predicate.name; @@ -183,15 +218,17 @@ inline output::ColorStream &operator<<(output::ColorStream &stream, const Predic if (i != predicate.arguments.cbegin()) stream << ", "; - stream << (*i); + print(stream, *i, printContext); } - return (stream << ")"); + stream << ")"; + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const SpecialInteger &specialInteger) +inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &) { switch (specialInteger.type) { @@ -206,31 +243,59 @@ inline output::ColorStream &operator<<(output::ColorStream &stream, const Specia //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const String &string) +inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &) { return (stream << output::String(string.text.c_str())); } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Variable &variable) +inline output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext) { - assert(!variable.name.empty()); - assert(variable.name != "_"); + assert(variable.declaration != nullptr); - if (variable.type == ast::Variable::Type::Reserved || !isReservedVariableName(variable.name.c_str())) - return (stream << output::Variable(variable.name.c_str())); + return print(stream, *variable.declaration, printContext); +} - const auto variableName = std::string(UserVariablePrefix) + variable.name; +//////////////////////////////////////////////////////////////////////////////////////////////////// - return (stream << output::Variable(variableName.c_str())); +inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext) +{ + const auto printVariableDeclaration = + [&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream & + { + auto matchingVariableID = variableIDs.find(&variableDeclaration); + + if (matchingVariableID == variableIDs.cend()) + { + auto emplaceResult = variableIDs.emplace(std::make_pair(&variableDeclaration, variableIDs.size() + 1)); + assert(emplaceResult.second); + matchingVariableID = emplaceResult.first; + } + + const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second); + + return (stream << output::Variable(variableName.c_str())); + }; + + switch (variableDeclaration.type) + { + case VariableDeclaration::Type::UserDefined: + return printVariableDeclaration(UserVariablePrefix, printContext.userVariableIDs); + case VariableDeclaration::Type::Head: + return printVariableDeclaration(HeadVariablePrefix, printContext.headVariableIDs); + case VariableDeclaration::Type::Body: + return printVariableDeclaration(BodyVariablePrefix, printContext.bodyVariableIDs); + } + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// // Expressions //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const And &and_) +inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext) { stream << "("; @@ -239,22 +304,30 @@ inline output::ColorStream &operator<<(output::ColorStream &stream, const And &a if (i != and_.arguments.cbegin()) stream << " " << output::Keyword("and") << " "; - stream << (*i); + print(stream, *i, printContext); } - return (stream << ")"); + stream << ")"; + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Biconditional &biconditional) +inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext) { - return (stream << "(" << biconditional.left << " <-> " << biconditional.right << ")"); + stream << "("; + print(stream, biconditional.left, printContext); + stream << " <-> "; + print(stream, biconditional.right, printContext); + stream << ")"; + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Exists &exists) +inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext) { stream << output::Keyword("exists") << " "; @@ -263,15 +336,18 @@ inline output::ColorStream &operator<<(output::ColorStream &stream, const Exists if (i != exists.variables.cbegin()) stream << ", "; - stream << (*i); + print(stream, **i, printContext); } - return (stream << " " << exists.argument); + stream << " "; + print(stream, exists.argument, printContext); + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const ForAll &forAll) +inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext) { stream << output::Keyword("forall") << " "; @@ -280,29 +356,41 @@ inline output::ColorStream &operator<<(output::ColorStream &stream, const ForAll if (i != forAll.variables.cbegin()) stream << ", "; - stream << (*i); + print(stream, **i, printContext); } - return (stream << " " << forAll.argument); + stream << " "; + print(stream, forAll.argument, printContext); + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Implies &implies) +inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext) { - return (stream << "(" << implies.antecedent << " -> " << implies.consequent << ")"); + stream << "("; + print(stream, implies.antecedent, printContext); + stream << " -> "; + print(stream, implies.consequent, printContext); + stream << ")"; + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Not ¬_) +inline output::ColorStream &print(output::ColorStream &stream, const Not ¬_, PrintContext &printContext) { - return (stream << output::Keyword("not ") << not_.argument); + stream << output::Keyword("not") << " "; + print(stream, not_.argument, printContext); + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Or &or_) +inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext) { stream << "("; @@ -311,10 +399,12 @@ inline output::ColorStream &operator<<(output::ColorStream &stream, const Or &or if (i != or_.arguments.cbegin()) stream << " " << output::Keyword("or") << " "; - stream << (*i); + print(stream, *i, printContext); } - return (stream << ")"); + stream << ")"; + + return stream; } //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -325,24 +415,24 @@ template struct VariantPrintVisitor { template - output::ColorStream &visit(const T &x, output::ColorStream &stream) + output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext) { - return (stream << x); + return print(stream, x, printContext); } }; //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Formula &formula) +inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext) { - return formula.accept(VariantPrintVisitor(), stream); + return formula.accept(VariantPrintVisitor(), stream, printContext); } //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &operator<<(output::ColorStream &stream, const Term &term) +inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext) { - return term.accept(VariantPrintVisitor(), stream); + return term.accept(VariantPrintVisitor(), stream, printContext); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/anthem/ASTCopy.cpp b/src/anthem/ASTCopy.cpp new file mode 100644 index 0000000..8f6bc59 --- /dev/null +++ b/src/anthem/ASTCopy.cpp @@ -0,0 +1,498 @@ +#include + +#include + +#include +#include + +namespace anthem +{ +namespace ast +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// ASTCopy +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Replacing Variables +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Replaces all occurrences of a variable in a given term with another term +struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor +{ + static void accept(ast::Variable &variable, ast::Term &, const ast::VariableDeclaration *original, ast::VariableDeclaration *replacement) + { + if (variable.declaration == original) + variable.declaration = replacement; + } + + // Ignore all other types of expressions + template + static void accept(T &, ast::Term &, const ast::VariableDeclaration *, ast::VariableDeclaration *) + { + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Replaces all occurrences of a variable in a given formula with a term +struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor +{ + static void accept(ast::Comparison &comparison, ast::Formula &, const ast::VariableDeclaration *original, ast::VariableDeclaration *replacement) + { + comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, original, replacement); + comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, original, replacement); + } + + static void accept(ast::In &in, ast::Formula &, const ast::VariableDeclaration *original, ast::VariableDeclaration *replacement) + { + in.element.accept(ReplaceVariableInTermVisitor(), in.element, original, replacement); + in.set.accept(ReplaceVariableInTermVisitor(), in.set, original, replacement); + } + + static void accept(ast::Predicate &predicate, ast::Formula &, const ast::VariableDeclaration *original, ast::VariableDeclaration *replacement) + { + for (auto &argument : predicate.arguments) + argument.accept(ReplaceVariableInTermVisitor(), argument, original, replacement); + } + + // Ignore all other types of expressions + template + static void accept(T &, ast::Formula &, const ast::VariableDeclaration *, ast::VariableDeclaration *) + { + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Preparing Copying +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +struct VariantDeepCopyVisitor +{ + template + Variant visit(const T &x) + { + return prepareCopy(x); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +std::unique_ptr prepareCopy(const std::unique_ptr &uniquePtr) +{ + return std::make_unique(prepareCopy(*uniquePtr)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +const auto prepareCopyVariant = + [](const auto &variant) -> typename std::decay::type + { + using VariantType = typename std::decay::type; + + return variant.accept(VariantDeepCopyVisitor()); + }; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +const auto prepareCopyVariantVector = + [](const auto &variantVector) -> typename std::decay::type + { + using Type = typename std::decay::type::value_type; + + std::vector result; + result.reserve(variantVector.size()); + + for (const auto &variant : variantVector) + result.emplace_back(prepareCopyVariant(variant)); + + return result; + }; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +const auto prepareCopyVector = + [](const auto &vector) -> typename std::decay::type + { + using Type = typename std::decay::type::value_type; + + std::vector result; + result.reserve(vector.size()); + + for (const auto &element : vector) + result.emplace_back(prepareCopy(element)); + + return result; + }; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +BinaryOperation prepareCopy(const BinaryOperation &other) +{ + return BinaryOperation(other.operator_, prepareCopy(other.left), prepareCopy(other.right)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Boolean prepareCopy(const Boolean &other) +{ + return Boolean(other.value); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Comparison prepareCopy(const Comparison &other) +{ + return Comparison(other.operator_, prepareCopy(other.left), prepareCopy(other.right)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Constant prepareCopy(const Constant &other) +{ + return Constant(std::string(other.name)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Function prepareCopy(const Function &other) +{ + return Function(std::string(other.name), prepareCopy(other.arguments)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +In prepareCopy(const In &other) +{ + return In(prepareCopy(other.element), prepareCopy(other.set)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Integer prepareCopy(const Integer &other) +{ + return Integer(other.value); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Interval prepareCopy(const Interval &other) +{ + return Interval(prepareCopy(other.from), prepareCopy(other.to)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Predicate prepareCopy(const Predicate &other) +{ + return Predicate(std::string(other.name), prepareCopy(other.arguments)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +SpecialInteger prepareCopy(const SpecialInteger &other) +{ + return SpecialInteger(other.type); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +String prepareCopy(const String &other) +{ + return String(std::string(other.text)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Variable prepareCopy(const Variable &other) +{ + return Variable(other.declaration); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +VariableDeclaration prepareCopy(const VariableDeclaration &other) +{ + return VariableDeclaration(std::string(other.name), other.type); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +VariableDeclarationPointers prepareCopy(const VariableDeclarationPointers &other) +{ + return prepareCopyVector(other); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +And prepareCopy(const And &other) +{ + return And(prepareCopy(other.arguments)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Biconditional prepareCopy(const Biconditional &other) +{ + return Biconditional(prepareCopy(other.left), prepareCopy(other.right)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Exists prepareCopy(const Exists &other) +{ + Exists copy(prepareCopy(other.variables), prepareCopy(other.argument)); + + // TODO: refactor + for (size_t i = 0; i < other.variables.size(); i++) + copy.argument.accept(ReplaceVariableInFormulaVisitor(), copy.argument, other.variables[i].get(), copy.variables[i].get()); + + return copy; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +ForAll prepareCopy(const ForAll &other) +{ + ForAll copy(prepareCopy(other.variables), prepareCopy(other.argument)); + + // TODO: refactor + for (size_t i = 0; i < other.variables.size(); i++) + copy.argument.accept(ReplaceVariableInFormulaVisitor(), copy.argument, other.variables[i].get(), copy.variables[i].get()); + + return copy; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Implies prepareCopy(const Implies &other) +{ + return Implies(prepareCopy(other.antecedent), prepareCopy(other.consequent)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Not prepareCopy(const Not &other) +{ + return Not(prepareCopy(other.argument)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Or prepareCopy(const Or &other) +{ + return Or(prepareCopy(other.arguments)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Formula prepareCopy(const Formula &formula) +{ + return prepareCopyVariant(formula); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Term prepareCopy(const Term &term) +{ + return prepareCopyVariant(term); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +std::vector prepareCopy(const std::vector &terms) +{ + return prepareCopyVariantVector(terms); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +std::vector prepareCopy(const std::vector &formulas) +{ + return prepareCopyVariantVector(formulas); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Fixing Dangling Variables +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Fix all dangling variables in a given term +struct FixDanglingVariablesInTermVisitor +{ + template + void visit(BinaryOperation &binaryOperation, Arguments &&... arguments) + { + binaryOperation.left.accept(*this, std::forward(arguments)...); + binaryOperation.right.accept(*this, std::forward(arguments)...); + } + + template + void visit(Boolean &, Arguments &&...) + { + } + + template + void visit(Constant &, Arguments &&...) + { + } + + template + void visit(Function &function, Arguments &&... arguments) + { + for (auto &argument : function.arguments) + argument.accept(*this, std::forward(arguments)...); + } + + template + void visit(Integer &, Arguments &&...) + { + } + + template + void visit(Interval &interval, Arguments &&... arguments) + { + interval.from.accept(*this, std::forward(arguments)...); + interval.to.accept(*this, std::forward(arguments)...); + } + + template + void visit(SpecialInteger &, Arguments &&...) + { + } + + template + void visit(String &, Arguments &&...) + { + } + + void visit(Variable &variable, ScopedFormula &scopedFormula, VariableStack &variableStack, + std::map &replacements) + { + const auto match = replacements.find(variable.declaration); + + // Replace the variable if it is flagged for replacement + if (match != replacements.cend()) + { + variable.declaration = match->second; + return; + } + + // If the variable is not flagged for replacement yet, check whether it is dangling + const auto isVariableDangling = !variableStack.contains(*variable.declaration); + + if (!isVariableDangling) + return; + + // If the variable is dangling, declare it correctly and flag it for future replacement + auto newVariableDeclaration = std::make_unique(std::string(variable.declaration->name), variable.declaration->type); + scopedFormula.freeVariables.emplace_back(std::move(newVariableDeclaration)); + + replacements[variable.declaration] = scopedFormula.freeVariables.back().get(); + variable.declaration = scopedFormula.freeVariables.back().get(); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Fix all dangling variables in a given formula +struct FixDanglingVariablesInFormulaVisitor +{ + template + void visit(And &and_, Arguments &&... arguments) + { + for (auto &argument : and_.arguments) + argument.accept(*this, std::forward(arguments)...); + } + + template + void visit(Biconditional &biconditional, Arguments &&... arguments) + { + biconditional.left.accept(*this, std::forward(arguments)...); + biconditional.right.accept(*this, std::forward(arguments)...); + } + + template + void visit(Boolean &, Arguments &&...) + { + } + + template + void visit(Comparison &comparison, Arguments &&... arguments) + { + comparison.left.accept(FixDanglingVariablesInTermVisitor(), std::forward(arguments)...); + comparison.right.accept(FixDanglingVariablesInTermVisitor(), std::forward(arguments)...); + } + + void visit(Exists &exists, ScopedFormula &scopedFormula, VariableStack &variableStack, + std::map &replacements) + { + variableStack.push(&exists.variables); + exists.argument.accept(*this, scopedFormula, variableStack, replacements); + variableStack.pop(); + } + + void visit(ForAll &forAll, ScopedFormula &scopedFormula, VariableStack &variableStack, + std::map &replacements) + { + variableStack.push(&forAll.variables); + forAll.argument.accept(*this, scopedFormula, variableStack, replacements); + variableStack.pop(); + } + + template + void visit(Implies &implies, Arguments &&... arguments) + { + implies.antecedent.accept(*this, std::forward(arguments)...); + implies.consequent.accept(*this, std::forward(arguments)...); + } + + template + void visit(In &in, Arguments &&... arguments) + { + in.element.accept(FixDanglingVariablesInTermVisitor(), std::forward(arguments)...); + in.set.accept(FixDanglingVariablesInTermVisitor(), std::forward(arguments)...); + } + + template + void visit(Not ¬_, Arguments &&... arguments) + { + not_.argument.accept(*this, std::forward(arguments)...); + } + + template + void visit(Or &or_, Arguments &&... arguments) + { + for (auto &argument : or_.arguments) + argument.accept(*this, std::forward(arguments)...); + } + + template + void visit(Predicate &predicate, Arguments &&... arguments) + { + for (auto &argument : predicate.arguments) + argument.accept(FixDanglingVariablesInTermVisitor(), std::forward(arguments)...); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void fixDanglingVariables(ScopedFormula &scopedFormula) +{ + VariableStack variableStack; + variableStack.push(&scopedFormula.freeVariables); + + std::map replacements; + + scopedFormula.formula.accept(FixDanglingVariablesInFormulaVisitor(), scopedFormula, + variableStack, replacements); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} +} diff --git a/src/anthem/ASTUtils.cpp b/src/anthem/ASTUtils.cpp index af8a43d..f7b84a3 100644 --- a/src/anthem/ASTUtils.cpp +++ b/src/anthem/ASTUtils.cpp @@ -27,21 +27,43 @@ void VariableStack::pop() //////////////////////////////////////////////////////////////////////////////////////////////////// -bool VariableStack::contains(const ast::Variable &variable) const +std::experimental::optional VariableStack::findVariableDeclaration(const char *variableName) const { - const auto variableMatches = - [&variable](const auto &otherVariable) + const auto variableNameMatches = + [&variableName](const auto &variableDeclaration) { - return variable.name == otherVariable.name; + return variableDeclaration->name == variableName; }; - const auto layerContainsVariable = - [&variable, &variableMatches](const auto &layer) + for (auto i = m_layers.rbegin(); i != m_layers.rend(); i++) + { + auto &layer = **i; + const auto matchingVariableDeclaration = std::find_if(layer.begin(), layer.end(), variableNameMatches); + + if (matchingVariableDeclaration != layer.end()) + return matchingVariableDeclaration->get(); + } + + return std::experimental::nullopt; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +bool VariableStack::contains(const ast::VariableDeclaration &variableDeclaration) const +{ + const auto variableDeclarationMatches = + [&variableDeclaration](const auto &other) { - return (std::find_if(layer->cbegin(), layer->cend(), variableMatches) != layer->cend()); + return variableDeclaration.name == other->name; }; - return (std::find_if(m_layers.cbegin(), m_layers.cend(), layerContainsVariable) != m_layers.cend()); + const auto layerContainsVariableDeclaration = + [&variableDeclaration, &variableDeclarationMatches](const auto &layer) + { + return (std::find_if(layer->cbegin(), layer->cend(), variableDeclarationMatches) != layer->cend()); + }; + + return (std::find_if(m_layers.cbegin(), m_layers.cend(), layerContainsVariableDeclaration) != m_layers.cend()); } //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -52,68 +74,68 @@ struct CollectFreeVariablesVisitor // Formulas //////////////////////////////////////////////////////////////////////////////////////////////// - void visit(const ast::And &and_, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::And &and_, VariableStack &variableStack, std::vector &freeVariables) { - for (const auto &argument : and_.arguments) + for (auto &argument : and_.arguments) argument.accept(*this, variableStack, freeVariables); } - void visit(const ast::Biconditional &biconditional, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::Biconditional &biconditional, VariableStack &variableStack, std::vector &freeVariables) { biconditional.left.accept(*this, variableStack, freeVariables); biconditional.right.accept(*this, variableStack, freeVariables); } - void visit(const ast::Boolean &, VariableStack &, std::vector &) + void visit(ast::Boolean &, VariableStack &, std::vector &) { } - void visit(const ast::Comparison &comparison, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::Comparison &comparison, VariableStack &variableStack, std::vector &freeVariables) { comparison.left.accept(*this, variableStack, freeVariables); comparison.right.accept(*this, variableStack, freeVariables); } - void visit(const ast::Exists &exists, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::Exists &exists, VariableStack &variableStack, std::vector &freeVariables) { variableStack.push(&exists.variables); exists.argument.accept(*this, variableStack, freeVariables); variableStack.pop(); } - void visit(const ast::ForAll &forAll, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::ForAll &forAll, VariableStack &variableStack, std::vector &freeVariables) { variableStack.push(&forAll.variables); forAll.argument.accept(*this, variableStack, freeVariables); variableStack.pop(); } - void visit(const ast::Implies &implies, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::Implies &implies, VariableStack &variableStack, std::vector &freeVariables) { implies.antecedent.accept(*this, variableStack, freeVariables); implies.consequent.accept(*this, variableStack, freeVariables); } - void visit(const ast::In &in, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::In &in, VariableStack &variableStack, std::vector &freeVariables) { in.element.accept(*this, variableStack, freeVariables); in.set.accept(*this, variableStack, freeVariables); } - void visit(const ast::Not ¬_, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::Not ¬_, VariableStack &variableStack, std::vector &freeVariables) { not_.argument.accept(*this, variableStack, freeVariables); } - void visit(const ast::Or &or_, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::Or &or_, VariableStack &variableStack, std::vector &freeVariables) { - for (const auto &argument : or_.arguments) + for (auto &argument : or_.arguments) argument.accept(*this, variableStack, freeVariables); } - void visit(const ast::Predicate &predicate, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::Predicate &predicate, VariableStack &variableStack, std::vector &freeVariables) { - for (const auto &argument : predicate.arguments) + for (auto &argument : predicate.arguments) argument.accept(*this, variableStack, freeVariables); } @@ -121,61 +143,55 @@ struct CollectFreeVariablesVisitor // Terms //////////////////////////////////////////////////////////////////////////////////////////////// - void visit(const ast::BinaryOperation &binaryOperation, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::BinaryOperation &binaryOperation, VariableStack &variableStack, std::vector &freeVariables) { binaryOperation.left.accept(*this, variableStack, freeVariables); binaryOperation.right.accept(*this, variableStack, freeVariables); } - void visit(const ast::Constant &, VariableStack &, std::vector &) + void visit(ast::Constant &, VariableStack &, std::vector &) { } - void visit(const ast::Function &function, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::Function &function, VariableStack &variableStack, std::vector &freeVariables) { - for (const auto &argument : function.arguments) + for (auto &argument : function.arguments) argument.accept(*this, variableStack, freeVariables); } - void visit(const ast::Integer &, VariableStack &, std::vector &) + void visit(ast::Integer &, VariableStack &, std::vector &) { } - void visit(const ast::Interval &interval, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::Interval &interval, VariableStack &variableStack, std::vector &freeVariables) { interval.from.accept(*this, variableStack, freeVariables); interval.to.accept(*this, variableStack, freeVariables); } - void visit(const ast::SpecialInteger &, VariableStack &, std::vector &) + void visit(ast::SpecialInteger &, VariableStack &, std::vector &) { } - void visit(const ast::String &, VariableStack &, std::vector &) + void visit(ast::String &, VariableStack &, std::vector &) { } - void visit(const ast::Variable &variable, VariableStack &variableStack, std::vector &freeVariables) + void visit(ast::Variable &variable, VariableStack &variableStack, std::vector &freeVariables) { - if (variableStack.contains(variable)) + if (variableStack.contains(*variable.declaration)) return; - const auto &variableMatches = - [&variable](auto &otherVariable) - { - return variable.name == otherVariable.name; - }; - - if (std::find_if(freeVariables.cbegin(), freeVariables.cend(), variableMatches) != freeVariables.cend()) + if (std::find(freeVariables.cbegin(), freeVariables.cend(), variable.declaration) != freeVariables.cend()) return; - freeVariables.emplace_back(ast::deepCopy(variable)); + freeVariables.emplace_back(variable.declaration); } }; //////////////////////////////////////////////////////////////////////////////////////////////////// -std::vector collectFreeVariables(const ast::Formula &formula) +std::vector collectFreeVariables(ast::Formula &formula) { ast::VariableStack variableStack; return collectFreeVariables(formula, variableStack); @@ -183,9 +199,9 @@ std::vector collectFreeVariables(const ast::Formula &formula) //////////////////////////////////////////////////////////////////////////////////////////////////// -std::vector collectFreeVariables(const ast::Formula &formula, ast::VariableStack &variableStack) +std::vector collectFreeVariables(ast::Formula &formula, ast::VariableStack &variableStack) { - std::vector freeVariables; + std::vector freeVariables; formula.accept(CollectFreeVariablesVisitor(), variableStack, freeVariables); diff --git a/src/anthem/Completion.cpp b/src/anthem/Completion.cpp index 8c118c7..eb2ed80 100644 --- a/src/anthem/Completion.cpp +++ b/src/anthem/Completion.cpp @@ -1,5 +1,6 @@ -#include + #include +#include #include #include #include @@ -14,16 +15,17 @@ namespace anthem //////////////////////////////////////////////////////////////////////////////////////////////////// // Copies the parameters of a predicate -std::vector copyParameters(const ast::Predicate &predicate) +std::vector> copyParameters(const ast::Predicate &predicate) { - std::vector parameters; - parameters.reserve(predicate.arity()); + std::vector> parameters; + /*parameters.reserve(predicate.arity()); - for (const auto ¶meter : predicate.arguments) + for (const auto &argument : predicate.arguments) { - assert(parameter.is()); - parameters.emplace_back(ast::deepCopy(parameter.get())); - } + assert(argument.is()); + // TODO: reimplement + //parameters.emplace_back(ast::deepCopy(parameter.get())); + }*/ return parameters; } @@ -31,18 +33,18 @@ std::vector copyParameters(const ast::Predicate &predicate) //////////////////////////////////////////////////////////////////////////////////////////////////// // Builds the conjunction within the completed formula for a given predicate -ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, const std::vector ¶meters, const std::vector &formulas) +ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, std::vector> ¶meters, std::vector &scopedFormulas) { auto disjunction = ast::Formula::make(); - ast::VariableStack variableStack; + /*ast::VariableStack variableStack; variableStack.push(¶meters); // Build the conjunction of all formulas with the predicate as consequent - for (const auto &formula : formulas) + for (auto &scopedFormula : scopedFormulas) { - assert(formula.is()); - const auto &implies = formula.get(); + assert(scopedFormula.formula.is()); + auto &implies = scopedFormula.formula.get(); if (!implies.consequent.is()) continue; @@ -55,6 +57,7 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c auto variables = ast::collectFreeVariables(implies.antecedent, variableStack); // TODO: avoid deep copies + // TODO: reimplement if (variables.empty()) disjunction.get().arguments.emplace_back(ast::deepCopy(implies.antecedent)); else @@ -62,7 +65,7 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c auto exists = ast::Formula::make(std::move(variables), ast::deepCopy(implies.antecedent)); disjunction.get().arguments.emplace_back(std::move(exists)); } - } + }*/ return disjunction; } @@ -74,7 +77,7 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo { assert(innerFormula.is()); - if (innerFormula.get().arguments.empty()) + /*if (innerFormula.get().arguments.empty()) return ast::Formula::make(std::move(predicate)); if (innerFormula.get().arguments.size() == 1) @@ -88,17 +91,17 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo return std::move(predicate); else return ast::Formula::make(std::move(predicate)); - } + }*/ return ast::Formula::make(std::move(predicate), std::move(innerFormula)); } //////////////////////////////////////////////////////////////////////////////////////////////////// -void completePredicate(ast::Predicate &&predicate, const std::vector &formulas, std::vector &completedFormulas) +void completePredicate(ast::Predicate &&predicate, std::vector &scopedFormulas, std::vector &completedScopedFormulas) { - auto parameters = copyParameters(predicate); - auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicate, parameters, formulas); + /*auto parameters = copyParameters(predicate); + auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicate, parameters, scopedFormulas); auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicate), std::move(completedFormulaDisjunction)); if (parameters.empty()) @@ -108,14 +111,14 @@ void completePredicate(ast::Predicate &&predicate, const std::vector(std::move(parameters), std::move(completedFormulaQuantified)); - completedFormulas.emplace_back(std::move(completedFormula)); + completedFormulas.emplace_back(std::move(completedFormula));*/ } //////////////////////////////////////////////////////////////////////////////////////////////////// -void completeIntegrityConstraint(const ast::Formula &formula, std::vector &completedFormulas) +void completeIntegrityConstraint(ast::Formula &formula, std::vector &) { - assert(formula.is()); + /*assert(formula.is()); auto &implies = formula.get(); assert(implies.consequent.is()); assert(implies.consequent.get().value == false); @@ -123,6 +126,7 @@ void completeIntegrityConstraint(const ast::Formula &formula, std::vector(ast::deepCopy(implies.antecedent)); if (variables.empty()) @@ -132,20 +136,20 @@ void completeIntegrityConstraint(const ast::Formula &formula, std::vector(std::move(variables), std::move(argument)); - completedFormulas.emplace_back(std::move(completedFormula)); + completedFormulas.emplace_back(std::move(completedFormula));*/ } //////////////////////////////////////////////////////////////////////////////////////////////////// -void complete(std::vector &formulas) +void complete(std::vector &scopedFormulas) { - // Check whether formulas are in normal form - for (const auto &formula : formulas) + /*// Check whether formulas are in normal form + for (const auto &scopedFormula : scopedFormulas) { - if (!formula.is()) + if (!scopedFormula.formula.is()) throw std::runtime_error("cannot perform completion, formula not in normal form"); - auto &implies = formula.get(); + auto &implies = scopedFormula.formula.get(); if (!implies.consequent.is() && !implies.consequent.is()) throw std::runtime_error("cannot perform completion, only single predicates and Booleans supported as formula consequent currently"); @@ -153,8 +157,8 @@ void complete(std::vector &formulas) std::vector predicates; - for (const auto &formula : formulas) - ast::collectPredicates(formula, predicates); + for (const auto &scopedFormula : scopedFormulas) + ast::collectPredicates(scopedFormula.formula, predicates); std::sort(predicates.begin(), predicates.end(), [](const auto *lhs, const auto *rhs) @@ -167,7 +171,7 @@ void complete(std::vector &formulas) return lhs->arity() < rhs->arity(); }); - std::vector completedFormulas; + std::vector completedScopedFormulas; // Complete predicates for (const auto *predicate : predicates) @@ -176,19 +180,20 @@ void complete(std::vector &formulas) ast::Predicate signature(std::string(predicate->name)); signature.arguments.reserve(predicate->arguments.size()); + // TODO: reimplement for (std::size_t i = 0; i < predicate->arguments.size(); i++) { auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i + 1); - signature.arguments.emplace_back(ast::Term::make(std::move(variableName), ast::Variable::Type::Reserved)); + signature.arguments.emplace_back(ast::Term::make(std::move(variableName), ast::VariableDeclaration::Type::Reserved)); } - completePredicate(std::move(signature), formulas, completedFormulas); + completePredicate(std::move(signature), scopedFormulas, completedScopedFormulas); } // Complete integrity constraints - for (const auto &formula : formulas) + for (auto &scopedFormula : scopedFormulas) { - auto &implies = formula.get(); + auto &implies = scopedFormula.formula.get(); if (!implies.consequent.is()) continue; @@ -199,10 +204,10 @@ void complete(std::vector &formulas) if (boolean.value == true) continue; - completeIntegrityConstraint(formula, completedFormulas); + completeIntegrityConstraint(scopedFormula.formula, completedScopedFormulas); } - std::swap(formulas, completedFormulas); + std::swap(scopedFormulas, completedScopedFormulas);*/ } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index 1de33d5..0493bba 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -1,5 +1,7 @@ #include +#include + #include namespace anthem @@ -12,21 +14,19 @@ namespace anthem //////////////////////////////////////////////////////////////////////////////////////////////////// // Determines whether a term is a specific variable -bool matchesVariable(const ast::Term &term, const ast::Variable &variable) +bool matchesVariableDeclaration(const ast::Term &term, const ast::VariableDeclaration &variableDeclaration) { if (!term.is()) return false; - const auto &otherVariable = term.get(); - - return variable.name == otherVariable.name; + return term.get().declaration == &variableDeclaration; } //////////////////////////////////////////////////////////////////////////////////////////////////// // Extracts the term t if the given formula is of the form “X = t” and X matches the given variable // The input formula is not usable if a term is returned -std::experimental::optional extractAssignedTerm(ast::Formula &formula, const ast::Variable &variable) +std::experimental::optional extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration &variableDeclaration) { if (!formula.is()) return std::experimental::nullopt; @@ -36,10 +36,10 @@ std::experimental::optional extractAssignedTerm(ast::Formula &formula if (comparison.operator_ != ast::Comparison::Operator::Equal) return std::experimental::nullopt; - if (matchesVariable(comparison.left, variable)) + if (matchesVariableDeclaration(comparison.left, variableDeclaration)) return std::move(comparison.right); - if (matchesVariable(comparison.right, variable)) + if (matchesVariableDeclaration(comparison.right, variableDeclaration)) return std::move(comparison.left); return std::experimental::nullopt; @@ -50,15 +50,16 @@ std::experimental::optional extractAssignedTerm(ast::Formula &formula // Replaces all occurrences of a variable in a given term with another term struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor { - static void accept(ast::Variable &variable, ast::Term &term, const ast::Variable &variableToReplace, const ast::Term &replacementTerm) + static void accept(ast::Variable &, ast::Term &, const ast::VariableDeclaration &, const ast::Term &) { - if (variable.name == variableToReplace.name) - term = ast::deepCopy(replacementTerm); + // TODO: reimplement + //if (variable.name == variableToReplace.name) + // term = ast::deepCopy(replacementTerm); } // Ignore all other types of expressions template - static void accept(T &, ast::Term &, const ast::Variable &, const ast::Term &) + static void accept(T &, ast::Term &, const ast::VariableDeclaration &, const ast::Term &) { } }; @@ -68,27 +69,27 @@ struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor { - static void accept(ast::Comparison &comparison, ast::Formula &, const ast::Variable &variable, const ast::Term &term) + static void accept(ast::Comparison &comparison, ast::Formula &, const ast::VariableDeclaration &variableDeclaration, const ast::Term &term) { - comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, variable, term); - comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, variable, term); + comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, variableDeclaration, term); + comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, variableDeclaration, term); } - static void accept(ast::In &in, ast::Formula &, const ast::Variable &variable, const ast::Term &term) + static void accept(ast::In &in, ast::Formula &, const ast::VariableDeclaration &variableDeclaration, const ast::Term &term) { - in.element.accept(ReplaceVariableInTermVisitor(), in.element, variable, term); - in.set.accept(ReplaceVariableInTermVisitor(), in.set, variable, term); + in.element.accept(ReplaceVariableInTermVisitor(), in.element, variableDeclaration, term); + in.set.accept(ReplaceVariableInTermVisitor(), in.set, variableDeclaration, term); } - static void accept(ast::Predicate &predicate, ast::Formula &, const ast::Variable &variable, const ast::Term &term) + static void accept(ast::Predicate &predicate, ast::Formula &, const ast::VariableDeclaration &variableDeclaration, const ast::Term &term) { for (auto &argument : predicate.arguments) - argument.accept(ReplaceVariableInTermVisitor(), argument, variable, term); + argument.accept(ReplaceVariableInTermVisitor(), argument, variableDeclaration, term); } // Ignore all other types of expressions template - static void accept(T &, ast::Formula &, const ast::Variable &, const ast::Term &) + static void accept(T &, ast::Formula &, const ast::VariableDeclaration &, const ast::Term &) { } }; @@ -108,7 +109,7 @@ void simplify(ast::Exists &exists, ast::Formula &formula) // Simplify formulas of type “exists X (X = t and F(X))” to “F(t)” for (auto i = exists.variables.begin(); i != exists.variables.end();) { - auto &variable = *i; + auto &variableDeclaration = *i->get(); bool wasVariableReplaced = false; @@ -117,7 +118,7 @@ void simplify(ast::Exists &exists, ast::Formula &formula) { auto &argument = *j; // Find term that is equivalent to the given variable - auto assignedTerm = extractAssignedTerm(argument, variable); + auto assignedTerm = extractAssignedTerm(argument, variableDeclaration); if (!assignedTerm) continue; @@ -129,7 +130,7 @@ void simplify(ast::Exists &exists, ast::Formula &formula) continue; auto &otherArgument = *k; - otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variable, assignedTerm.value()); + otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value()); } arguments.erase(j); diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index 24f8371..bed8eb5 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -40,12 +40,12 @@ void translate(const char *fileName, std::istream &stream, Context &context) auto fileContent = std::string(std::istreambuf_iterator(stream), {}); - std::vector formulas; + std::vector scopedFormulas; const auto translateStatement = - [&formulas, &context](const Clingo::AST::Statement &statement) + [&scopedFormulas, &context](const Clingo::AST::Statement &statement) { - statement.data.accept(StatementVisitor(), statement, formulas, context); + statement.data.accept(StatementVisitor(), statement, scopedFormulas, context); }; const auto logger = @@ -57,14 +57,19 @@ void translate(const char *fileName, std::istream &stream, Context &context) Clingo::parse_program(fileContent.c_str(), translateStatement, logger); if (context.simplify) - for (auto &formula : formulas) - simplify(formula); + for (auto &scopedFormula : scopedFormulas) + simplify(scopedFormula.formula); if (context.complete) - complete(formulas); + complete(scopedFormulas); - for (const auto &formula : formulas) - context.logger.outputStream() << formula << std::endl; + ast::PrintContext printContext; + + for (const auto &scopedFormula : scopedFormulas) + { + ast::print(context.logger.outputStream(), scopedFormula.formula, printContext); + context.logger.outputStream() << std::endl; + } } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/tests/TestCompletion.cpp b/tests/TestCompletion.cpp index 89a7336..165b7d9 100644 --- a/tests/TestCompletion.cpp +++ b/tests/TestCompletion.cpp @@ -2,12 +2,13 @@ #include +#include #include #include //////////////////////////////////////////////////////////////////////////////////////////////////// -TEST_CASE("[completion] Rules are completed", "[completion]") +/*TEST_CASE("[completion] Rules are completed", "[completion]") { std::stringstream input; std::stringstream output; @@ -147,3 +148,4 @@ TEST_CASE("[completion] Rules are completed", "[completion]") // TODO: test collecting free variables } +*/ diff --git a/tests/TestSimplification.cpp b/tests/TestSimplification.cpp index fa16bbb..0ec2f5c 100644 --- a/tests/TestSimplification.cpp +++ b/tests/TestSimplification.cpp @@ -2,12 +2,13 @@ #include +#include #include #include //////////////////////////////////////////////////////////////////////////////////////////////////// -TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]") +/*TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]") { std::stringstream input; std::stringstream output; @@ -50,3 +51,4 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]") CHECK(output.str() == "(M > N -> #false)\n"); } } +*/ diff --git a/tests/TestTranslation.cpp b/tests/TestTranslation.cpp index b735d33..e2355b6 100644 --- a/tests/TestTranslation.cpp +++ b/tests/TestTranslation.cpp @@ -2,6 +2,7 @@ #include +#include #include #include @@ -14,7 +15,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") std::stringstream errors; anthem::output::Logger logger(output, errors); - anthem::Context context = {logger, {}}; + anthem::Context context(std::move(logger)); context.simplify = false; context.complete = false; @@ -31,7 +32,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(N) :- N = 1..5."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in N and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> p(V1))\n"); + CHECK(output.str() == "((V1 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> p(V1))\n"); } SECTION("simple example 3") @@ -39,7 +40,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(N + 1) :- q(N)."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in (N + 1) and exists X1 (X1 in N and q(X1))) -> p(V1))\n"); + CHECK(output.str() == "((V1 in (U1 + 1) and exists X1 (X1 in U1 and q(X1))) -> p(V1))\n"); } SECTION("n-ary head") @@ -47,7 +48,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(N, 1, 2) :- N = 1..5."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in N and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> p(V1, V2, V3))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> p(V1, V2, V3))\n"); } SECTION("disjunctive head") @@ -56,7 +57,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "q(3, N); p(N, 1, 2) :- N = 1..5."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in N and V2 in 1 and V3 in 2 and V4 in 3 and V5 in N and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n"); } SECTION("disjunctive head (alternative syntax)") @@ -65,7 +66,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "q(3, N), p(N, 1, 2) :- N = 1..5."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in N and V2 in 1 and V3 in 2 and V4 in 3 and V5 in N and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n"); } SECTION("escaping conflicting variable names") @@ -73,7 +74,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X1, V1, A1) :- q(X1), q(V1), q(A1)."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in _X1 and V2 in _V1 and V3 in _A1 and exists X1 (X1 in _X1 and q(X1)) and exists X2 (X2 in _V1 and q(X2)) and exists X3 (X3 in _A1 and q(X3))) -> p(V1, V2, V3))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in U2 and V3 in U3 and exists X1 (X1 in U1 and q(X1)) and exists X2 (X2 in U2 and q(X2)) and exists X3 (X3 in U3 and q(X3))) -> p(V1, V2, V3))\n"); } SECTION("fact") @@ -97,7 +98,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << ":- not p(I), I = 1..n."; anthem::translate("input", input, context); - CHECK(output.str() == "((exists X1 (X1 in I and not p(X1)) and exists X2, X3 (X2 in I and X3 in 1..n and X2 = X3)) -> #false)\n"); + CHECK(output.str() == "((exists X1 (X1 in U1 and not p(X1)) and exists X2, X3 (X2 in U1 and X3 in 1..n and X2 = X3)) -> #false)\n"); } SECTION("disjunctive fact (no arguments)") @@ -145,7 +146,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X, #inf) :- q(X, #sup)."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in X and V2 in #inf and exists X1, X2 (X1 in X and X2 in #sup and q(X1, X2))) -> p(V1, V2))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in #inf and exists X1, X2 (X1 in U1 and X2 in #sup and q(X1, X2))) -> p(V1, V2))\n"); } SECTION("strings") @@ -153,7 +154,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X, \"foo\") :- q(X, \"bar\")."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in X and V2 in \"foo\" and exists X1, X2 (X1 in X and X2 in \"bar\" and q(X1, X2))) -> p(V1, V2))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in \"foo\" and exists X1, X2 (X1 in U1 and X2 in \"bar\" and q(X1, X2))) -> p(V1, V2))\n"); } SECTION("tuples") @@ -161,7 +162,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X, (1, 2, 3)) :- q(X, (4, 5))."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in X and V2 in (1, 2, 3) and exists X1, X2 (X1 in X and X2 in (4, 5) and q(X1, X2))) -> p(V1, V2))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in (1, 2, 3) and exists X1, X2 (X1 in U1 and X2 in (4, 5) and q(X1, X2))) -> p(V1, V2))\n"); } SECTION("1-ary tuples") @@ -169,7 +170,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X, (1,)) :- q(X, (2,))."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in X and V2 in (1,) and exists X1, X2 (X1 in X and X2 in (2,) and q(X1, X2))) -> p(V1, V2))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in (1,) and exists X1, X2 (X1 in U1 and X2 in (2,) and q(X1, X2))) -> p(V1, V2))\n"); } SECTION("intervals") @@ -177,7 +178,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X, 1..10) :- q(X, 6..12)."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in X and V2 in 1..10 and exists X1, X2 (X1 in X and X2 in 6..12 and q(X1, X2))) -> p(V1, V2))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in 1..10 and exists X1, X2 (X1 in U1 and X2 in 6..12 and q(X1, X2))) -> p(V1, V2))\n"); } SECTION("comparisons") @@ -185,7 +186,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(M, N, O, P) :- M < N, P != O."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in M and V2 in N and V3 in O and V4 in P and exists X1, X2 (X1 in M and X2 in N and X1 < X2) and exists X3, X4 (X3 in P and X4 in O and X3 != X4)) -> p(V1, V2, V3, V4))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in U2 and V3 in U3 and V4 in U4 and exists X1, X2 (X1 in U1 and X2 in U2 and X1 < X2) and exists X3, X4 (X3 in U4 and X4 in U3 and X3 != X4)) -> p(V1, V2, V3, V4))\n"); } SECTION("single negation with 0-ary predicates") @@ -201,7 +202,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "not p(X, 1) :- not q(X, 2)."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2))) -> not p(V1, V2))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in 1 and exists X1, X2 (X1 in U1 and X2 in 2 and not q(X1, X2))) -> not p(V1, V2))\n"); } SECTION("variable numbering") @@ -210,8 +211,8 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "f; q(A1, A2); p(A3, r(A4)); g(g(A5)) :- g(A3), f, q(A4, A1), p(A2, A5)."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in _A1 and V2 in _A2 and V3 in _A3 and V4 in r(_A4) and V5 in g(_A5)" - " and exists X1 (X1 in _A3 and g(X1)) and f and exists X2, X3 (X2 in _A4 and X3 in _A1 and q(X2, X3)) and exists X4, X5 (X4 in _A2 and X5 in _A5 and p(X4, X5)))" + CHECK(output.str() == "((V1 in U1 and V2 in U2 and V3 in U3 and V4 in r(U4) and V5 in g(U5)" + " and exists X1 (X1 in U3 and g(X1)) and f and exists X2, X3 (X2 in U4 and X3 in U1 and q(X2, X3)) and exists X4, X5 (X4 in U2 and X5 in U5 and p(X4, X5)))" " -> (q(V1, V2) or p(V3, V4) or g(V5) or f))\n"); } @@ -220,7 +221,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(q(s(t(X1))), u(X2)) :- u(v(w(X2)), z(X1))."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in q(s(t(_X1))) and V2 in u(_X2) and exists X1, X2 (X1 in v(w(_X2)) and X2 in z(_X1) and u(X1, X2))) -> p(V1, V2))\n"); + CHECK(output.str() == "((V1 in q(s(t(U1))) and V2 in u(U2) and exists X1, X2 (X1 in v(w(U2)) and X2 in z(U1) and u(X1, X2))) -> p(V1, V2))\n"); } SECTION("choice rule (simple)") @@ -244,7 +245,8 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "{p(1..3, N); q(2..4)}."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in 1..3 and V2 in N and V3 in 2..4 and p(V1, V2)) -> p(V1, V2))\n((V1 in 1..3 and V2 in N and V3 in 2..4 and q(V3)) -> q(V3))\n"); + // TODO: eliminate V5: not needed + CHECK(output.str() == "((V1 in 1..3 and V2 in U1 and V3 in 2..4 and p(V1, V2)) -> p(V1, V2))\n((V4 in 1..3 and V5 in U2 and V6 in 2..4 and q(V6)) -> q(V6))\n"); } SECTION("choice rule with body") @@ -252,7 +254,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "{p(M, N); q(P)} :- s(M, N, P)."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in M and V2 in N and V3 in P and exists X1, X2, X3 (X1 in M and X2 in N and X3 in P and s(X1, X2, X3)) and p(V1, V2)) -> p(V1, V2))\n((V1 in M and V2 in N and V3 in P and exists X1, X2, X3 (X1 in M and X2 in N and X3 in P and s(X1, X2, X3)) and q(V3)) -> q(V3))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in U2 and V3 in U3 and exists X1, X2, X3 (X1 in U1 and X2 in U2 and X3 in U3 and s(X1, X2, X3)) and p(V1, V2)) -> p(V1, V2))\n((V4 in U4 and V5 in U5 and V6 in U6 and exists X4, X5, X6 (X4 in U4 and X5 in U5 and X6 in U6 and s(X4, X5, X6)) and q(V6)) -> q(V6))\n"); } SECTION("choice rule with negation") @@ -260,7 +262,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "{not p(X, 1)} :- not q(X, 2)."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and not p(V1, V2)) -> not p(V1, V2))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in 1 and exists X1, X2 (X1 in U1 and X2 in 2 and not q(X1, X2)) and not p(V1, V2)) -> not p(V1, V2))\n"); } SECTION("choice rule with negation (two elements)") @@ -268,7 +270,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "{not p(X, 1); not s} :- not q(X, 2)."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and not p(V1, V2)) -> not p(V1, V2))\n((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and not s) -> not s)\n"); + CHECK(output.str() == "((V1 in U1 and V2 in 1 and exists X1, X2 (X1 in U1 and X2 in 2 and not q(X1, X2)) and not p(V1, V2)) -> not p(V1, V2))\n((V3 in U2 and V4 in 1 and exists X3, X4 (X3 in U2 and X4 in 2 and not q(X3, X4)) and not s) -> not s)\n"); } SECTION("anonymous variables") @@ -276,6 +278,6 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(_, _) :- q(_, _)."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in A1 and V2 in A2 and exists X1, X2 (X1 in A3 and X2 in A4 and q(X1, X2))) -> p(V1, V2))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in U2 and exists X1, X2 (X1 in U3 and X2 in U4 and q(X1, X2))) -> p(V1, V2))\n"); } }