From 9e6d135781898137c22f3acf1dad4f9c0e9b5f95 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 15 Mar 2017 16:00:00 +0100 Subject: [PATCH] Implemented explicit syntax tree representation for first-order formulas. --- include/anthem/AST.h | 437 ++++++++++++++++++++++++++- include/anthem/ASTForward.h | 45 +-- include/anthem/Body.h | 217 +++++++------ include/anthem/Head.h | 134 ++++---- include/anthem/StatementVisitor.h | 107 ++++--- include/anthem/Term.h | 132 ++++++++ include/anthem/output/AST.h | 345 +++++++++++++++++++++ include/anthem/output/ClingoOutput.h | 36 --- include/anthem/output/Formatting.h | 2 +- src/anthem/Translation.cpp | 8 +- src/anthem/output/ClingoOutput.cpp | 257 ---------------- tests/TestTranslation.cpp | 74 +++-- 12 files changed, 1225 insertions(+), 569 deletions(-) create mode 100644 include/anthem/Term.h create mode 100644 include/anthem/output/AST.h delete mode 100644 include/anthem/output/ClingoOutput.h delete mode 100644 src/anthem/output/ClingoOutput.cpp diff --git a/include/anthem/AST.h b/include/anthem/AST.h index 5463bb4..bc5e4e6 100644 --- a/include/anthem/AST.h +++ b/include/anthem/AST.h @@ -22,10 +22,20 @@ struct BinaryOperation { enum class Operator { - Add, - Subtract + Plus, + Minus, + Multiplication, + Division, + Modulo }; + BinaryOperation(Operator operator_, Term &&left, Term &&right) + : operator_{operator_}, + left{std::move(left)}, + right{std::move(right)} + { + } + Operator operator_; Term left; Term right; @@ -35,53 +45,173 @@ struct BinaryOperation struct Boolean { + Boolean(bool value) + : value{value} + { + } + bool value = false; }; //////////////////////////////////////////////////////////////////////////////////////////////////// -struct Equals +struct Comparison { + enum class Operator + { + GreaterThan, + LessThan, + LessEqual, + GreaterEqual, + NotEqual, + Equal + }; + + Comparison(Operator operator_, Term &&left, Term &&right) + : operator_{operator_}, + left{std::move(left)}, + right{std::move(right)} + { + } + + Operator operator_; Term left; Term right; }; //////////////////////////////////////////////////////////////////////////////////////////////////// +struct Constant +{ + Constant(std::string &&name) + : name{std::move(name)} + { + } + + std::string name; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + struct Function { - const char *name = nullptr; + Function(std::string &&name, std::vector &&arguments) + : name{std::move(name)}, + arguments{std::move(arguments)} + { + } + + std::string name; std::vector arguments; }; //////////////////////////////////////////////////////////////////////////////////////////////////// +struct In +{ + In(Term &&element, Term &&set) + : element{std::move(element)}, + set{std::move(set)} + { + } + + Term element; + Term set; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + struct Integer { + Integer(int value) + : value{value} + { + } + int value; }; //////////////////////////////////////////////////////////////////////////////////////////////////// -struct IntegerRange +struct Interval { - Integer from; - Integer to; + Interval(Term &&from, Term &&to) + : from{std::move(from)}, + to{std::move(to)} + { + } + + Term from; + Term to; }; //////////////////////////////////////////////////////////////////////////////////////////////////// struct Predicate { - const char *name = nullptr; + Predicate(std::string &&name) + : name{std::move(name)} + { + } + + Predicate(std::string &&name, std::vector &&arguments) + : name{std::move(name)}, + arguments{std::move(arguments)} + { + } + + std::string name; std::vector arguments; }; //////////////////////////////////////////////////////////////////////////////////////////////////// +struct SpecialInteger +{ + enum class Type + { + Infimum, + Supremum + }; + + SpecialInteger(Type type) + : type{type} + { + } + + Type type; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct String +{ + String(std::string &&text) + : text{std::move(text)} + { + } + + std::string text; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + struct Variable { - const char *name = nullptr; + enum class Type + { + UserDefined, + Reserved + }; + + Variable(std::string &&name, Type type) + : name{std::move(name)}, + type{type} + { + } + + std::string name; + Type type; }; //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -90,6 +220,13 @@ struct Variable struct And { + And() = default; + + And(std::vector &&arguments) + : arguments{std::move(arguments)} + { + } + std::vector arguments; }; @@ -97,6 +234,12 @@ struct And struct Biconditional { + Biconditional(Formula &&left, Formula &&right) + : left{std::move(left)}, + right{std::move(right)} + { + } + Formula left; Formula right; }; @@ -105,22 +248,40 @@ struct Biconditional struct Exists { + Exists(std::vector &&variables, Formula &&argument) + : variables{std::move(variables)}, + argument{std::move(argument)} + { + } + std::vector variables; - Formula formula; + Formula argument; }; //////////////////////////////////////////////////////////////////////////////////////////////////// struct ForAll { + ForAll(std::vector &&variables, Formula &&argument) + : variables{std::move(variables)}, + argument{std::move(argument)} + { + } + std::vector variables; - Formula formula; + Formula argument; }; //////////////////////////////////////////////////////////////////////////////////////////////////// struct Implies { + Implies(Formula &&antecedent, Formula &&consequent) + : antecedent{std::move(antecedent)}, + consequent{std::move(consequent)} + { + } + Formula antecedent; Formula consequent; }; @@ -129,6 +290,11 @@ struct Implies struct Not { + Not(Formula &&argument) + : argument{std::move(argument)} + { + } + Formula argument; }; @@ -136,12 +302,261 @@ struct Not struct Or { + Or() = default; + + Or(std::vector &&arguments) + : arguments{std::move(arguments)} + { + } + std::vector arguments; }; +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Deep Copying //////////////////////////////////////////////////////////////////////////////////////////////////// +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); + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +const auto deepCopyUniquePtr = + [](const auto &uniquePtr) -> typename std::decay::type + { + using Type = typename std::decay::type::element_type; + return std::make_unique(deepCopy(*uniquePtr)); + }; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +const auto deepCopyUniquePtrVector = + [](const auto &uniquePtrVector) -> typename std::decay::type + { + using Type = typename std::decay::type::value_type; + + std::vector result; + result.reserve(uniquePtrVector.size()); + + for (const auto &uniquePtr : uniquePtrVector) + result.emplace_back(deepCopyUniquePtr(uniquePtr)); + + return result; + }; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +const auto deepCopyVariant = + [](const auto &variant) -> typename std::decay::type + { + return variant.match([](const auto &x) -> typename std::decay::type {return deepCopyUniquePtr(x);}); + }; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +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; + }; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +BinaryOperation deepCopy(const BinaryOperation &other) +{ + return BinaryOperation(other.operator_, deepCopy(other.left), deepCopy(other.right)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Boolean deepCopy(const Boolean &other) +{ + return Boolean(other.value); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Comparison deepCopy(const Comparison &other) +{ + return Comparison(other.operator_, deepCopy(other.left), deepCopy(other.right)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Constant deepCopy(const Constant &other) +{ + return Constant(std::string(other.name)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Function deepCopy(const Function &other) +{ + return Function(std::string(other.name), deepCopy(other.arguments)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Integer deepCopy(const Integer &other) +{ + return Integer(other.value); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Interval deepCopy(const Interval &other) +{ + return Interval(deepCopy(other.from), deepCopy(other.to)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Predicate deepCopy(const Predicate &other) +{ + return Predicate(std::string(other.name), deepCopy(other.arguments)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +SpecialInteger deepCopy(const SpecialInteger &other) +{ + return SpecialInteger(other.type); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +String deepCopy(const String &other) +{ + return String(std::string(other.text)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Variable deepCopy(const Variable &other) +{ + return Variable(std::string(other.name), other.type); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +std::vector deepCopy(const std::vector &other) +{ + return deepCopyUniquePtrVector(other); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +And deepCopy(const And &other) +{ + return And(deepCopy(other.arguments)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Biconditional deepCopy(const Biconditional &other) +{ + return Biconditional(deepCopy(other.left), deepCopy(other.right)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Exists deepCopy(const Exists &other) +{ + return Exists(deepCopy(other.variables), deepCopy(other.argument)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +ForAll deepCopy(const ForAll &other) +{ + return ForAll(deepCopy(other.variables), deepCopy(other.argument)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +In deepCopy(const In &other) +{ + return In(deepCopy(other.element), deepCopy(other.set)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Implies deepCopy(const Implies &other) +{ + return Implies(deepCopy(other.antecedent), deepCopy(other.consequent)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Not deepCopy(const Not &other) +{ + return Not(deepCopy(other.argument)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Or deepCopy(const Or &other) +{ + return Or(deepCopy(other.arguments)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Formula deepCopy(const Formula &formula) +{ + return deepCopyVariant(formula); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +std::vector deepCopy(const std::vector &formulas) +{ + return deepCopyVariantVector(formulas); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +Term deepCopy(const Term &term) +{ + return deepCopyVariant(term); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +std::vector deepCopy(const std::vector &terms) +{ + return deepCopyVariantVector(terms); +} //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/ASTForward.h b/include/anthem/ASTForward.h index 4c9f3c2..37eee39 100644 --- a/include/anthem/ASTForward.h +++ b/include/anthem/ASTForward.h @@ -24,60 +24,55 @@ struct And; struct BinaryOperation; struct Biconditional; struct Boolean; +struct Comparison; struct Constant; -struct Equals; struct Exists; struct ForAll; struct Function; struct Implies; +struct In; struct Integer; -struct IntegerRange; +struct Interval; struct Not; struct Or; struct Predicate; +struct SpecialInteger; +struct String; struct Variable; using AndPointer = std::unique_ptr; using BinaryOperationPointer = std::unique_ptr; using BiconditionalPointer = std::unique_ptr; using BooleanPointer = std::unique_ptr; +using ComparisonPointer = std::unique_ptr; using ConstantPointer = std::unique_ptr; -using EqualsPointer = std::unique_ptr; using ExistsPointer = std::unique_ptr; using ForAllPointer = std::unique_ptr; using FunctionPointer = std::unique_ptr; using ImpliesPointer = std::unique_ptr; +using InPointer = std::unique_ptr; using IntegerPointer = std::unique_ptr; -using IntegerRangePointer = std::unique_ptr; +using IntervalPointer = std::unique_ptr; using NotPointer = std::unique_ptr; using OrPointer = std::unique_ptr; using PredicatePointer = std::unique_ptr; +using SpecialIntegerPointer = std::unique_ptr; +using StringPointer = std::unique_ptr; using VariablePointer = std::unique_ptr; //////////////////////////////////////////////////////////////////////////////////////////////////// // Variants //////////////////////////////////////////////////////////////////////////////////////////////////// -using TermT = mapbox::util::variant< - BinaryOperationPointer, - ConstantPointer, - IntegerPointer, - FunctionPointer, - VariablePointer>; - -class Term : public TermT -{ - using TermT::TermT; -}; - using FormulaT = mapbox::util::variant< AndPointer, BiconditionalPointer, BooleanPointer, - EqualsPointer, + ComparisonPointer, ExistsPointer, ForAllPointer, ImpliesPointer, + InPointer, NotPointer, OrPointer, PredicatePointer>; @@ -87,7 +82,21 @@ class Formula : public FormulaT using FormulaT::FormulaT; }; -using Formulas = std::vector; +using TermT = mapbox::util::variant< + BinaryOperationPointer, + BooleanPointer, + ConstantPointer, + FunctionPointer, + IntegerPointer, + IntervalPointer, + SpecialIntegerPointer, + StringPointer, + VariablePointer>; + +class Term : public TermT +{ + using TermT::TermT; +}; //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/Body.h b/include/anthem/Body.h index 63eb17b..9a9b9fc 100644 --- a/include/anthem/Body.h +++ b/include/anthem/Body.h @@ -3,9 +3,9 @@ #include -#include +#include +#include #include -#include #include namespace anthem @@ -17,204 +17,199 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -struct TermPrintVisitor +ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOperator) { - void visit(const Clingo::Symbol &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) + switch (comparisonOperator) + { + case Clingo::AST::ComparisonOperator::GreaterThan: + return ast::Comparison::Operator::GreaterThan; + case Clingo::AST::ComparisonOperator::LessThan: + return ast::Comparison::Operator::LessThan; + case Clingo::AST::ComparisonOperator::LessEqual: + return ast::Comparison::Operator::LessEqual; + case Clingo::AST::ComparisonOperator::GreaterEqual: + return ast::Comparison::Operator::GreaterEqual; + case Clingo::AST::ComparisonOperator::NotEqual: + return ast::Comparison::Operator::NotEqual; + case Clingo::AST::ComparisonOperator::Equal: + return ast::Comparison::Operator::Equal; + } + + return ast::Comparison::Operator::NotEqual; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +ast::VariablePointer makeAuxiliaryBodyVariable(const int i) +{ + auto variableName = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(i); + + return std::make_unique(std::move(variableName), ast::Variable::Type::Reserved); +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct BodyTermTranslateVisitor +{ + std::experimental::optional visit(const Clingo::Symbol &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) { throwErrorAtLocation(term.location, "“symbol” terms currently unsupported in this context", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::Variable &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::Variable &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) { throwErrorAtLocation(term.location, "“variable” terms currently unsupported in this context", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) { throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported in this context", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) { throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported in this context", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::Interval &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::Interval &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) { throwErrorAtLocation(term.location, "“interval” terms currently unsupported in this context", context); + return std::experimental::nullopt; } - // TODO: check correctness - void visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, Context &context) + // TODO: refactor + std::experimental::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, Context &context) { if (literal.sign == Clingo::AST::Sign::DoubleNegation) throwErrorAtLocation(literal.location, "double-negated literals currently unsupported", context); - auto &outputStream = context.logger.outputStream(); - if (function.arguments.empty()) + return std::make_unique(std::string(function.name)); + + std::vector variables; + variables.reserve(function.arguments.size()); + + for (size_t i = 0; i < function.arguments.size(); i++) + variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i)); + + auto conjunction = std::make_unique(); + + for (size_t i = 0; i < function.arguments.size(); i++) { - outputStream << output::Function(function.name); - return; + const auto &argument = function.arguments[i]; + conjunction->arguments.emplace_back(std::make_unique(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i), translate(argument, context))); } - outputStream << output::Keyword("exists") << " "; + auto predicate = std::make_unique(std::string(function.name)); + predicate->arguments.reserve(function.arguments.size()); - for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++) - { - if (i != function.arguments.cbegin()) - outputStream << ", "; + for (size_t i = 0; i < function.arguments.size(); i++) + predicate->arguments.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i)); - const auto variableName = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(context.auxiliaryBodyLiteralID + i - function.arguments.cbegin()); - - outputStream << output::Variable(variableName.c_str()); - } - - outputStream << " ("; - - for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++) - { - const auto &argument = *i; - - if (i != function.arguments.cbegin()) - outputStream << " " << Clingo::AST::BinaryOperator::And << " "; - - const auto variableName = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(context.auxiliaryBodyLiteralID + i - function.arguments.cbegin()); - - outputStream - << output::Variable(variableName.c_str()) - << " " << output::Keyword("in") << " " - << argument; - } - - outputStream - << " " << Clingo::AST::BinaryOperator::And << " " - << literal.sign - << output::Function(function.name) << "("; - - for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++) - { - if (i != function.arguments.cbegin()) - outputStream << ", "; - - const auto variableName = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(context.auxiliaryBodyLiteralID + i - function.arguments.cbegin()); - - outputStream << output::Variable(variableName.c_str()); - } - - outputStream << "))"; + if (literal.sign == Clingo::AST::Sign::None) + conjunction->arguments.emplace_back(std::move(predicate)); + else + conjunction->arguments.emplace_back(std::make_unique(std::move(predicate))); context.auxiliaryBodyLiteralID += function.arguments.size(); + + return std::make_unique(std::move(variables), std::move(conjunction)); } - void visit(const Clingo::AST::Pool &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::Pool &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context) { throwErrorAtLocation(term.location, "“pool” terms currently unsupported", context); + return std::experimental::nullopt; } }; //////////////////////////////////////////////////////////////////////////////////////////////////// -struct LiteralPrintVisitor +struct BodyLiteralTranslateVisitor { - void visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &literal, Context &context) + std::experimental::optional visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &literal, Context &context) { throwErrorAtLocation(literal.location, "“boolean” literals currently unsupported in this context", context); + return std::experimental::nullopt; } - void 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) { - term.data.accept(TermPrintVisitor(), literal, term, context); + return term.data.accept(BodyTermTranslateVisitor(), literal, term, context); + return std::experimental::nullopt; } // TODO: refactor - void 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) { assert(literal.sign == Clingo::AST::Sign::None); - const char *operatorName = ""; + const auto operator_ = translate(comparison.comparison); - switch (comparison.comparison) - { - case Clingo::AST::ComparisonOperator::GreaterThan: - operatorName = ">"; - break; - case Clingo::AST::ComparisonOperator::LessThan: - operatorName = "<"; - break; - case Clingo::AST::ComparisonOperator::LessEqual: - operatorName = "<="; - break; - case Clingo::AST::ComparisonOperator::GreaterEqual: - operatorName = ">="; - break; - case Clingo::AST::ComparisonOperator::NotEqual: - operatorName = "!="; - break; - case Clingo::AST::ComparisonOperator::Equal: - operatorName = "="; - break; - } + std::vector variables; + variables.reserve(2); + variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID)); + variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1)); - const auto variableName1 = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(context.auxiliaryBodyLiteralID); - const auto variableName2 = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(context.auxiliaryBodyLiteralID + 1); - - context.logger.outputStream() - << output::Keyword("exists") << " " << output::Variable(variableName1.c_str()) - << ", " << output::Variable(variableName2.c_str()) - << " (" - << output::Variable(variableName1.c_str()) - << " " << output::Keyword("in") << " " << comparison.left - << " " << Clingo::AST::BinaryOperator::And << " " - << output::Variable(variableName2.c_str()) - << " " << output::Keyword("in") << " " << comparison.right - << " " << Clingo::AST::BinaryOperator::And << " " - << output::Variable(variableName1.c_str()) - << " " << output::Operator(operatorName) << " " - << output::Variable(variableName2.c_str()) - << ")"; + auto conjunction = std::make_unique(); + conjunction->arguments.reserve(3); + conjunction->arguments.emplace_back(std::make_unique(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID), translate(comparison.left, context))); + conjunction->arguments.emplace_back(std::make_unique(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1), translate(comparison.right, context))); + conjunction->arguments.emplace_back(std::make_unique(operator_, makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID), makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1))); context.auxiliaryBodyLiteralID += 2; + + return std::make_unique(std::move(variables), std::move(conjunction)); } - void visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &context) + std::experimental::optional visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &context) { throwErrorAtLocation(literal.location, "CSP literals currently unsupported", context); + return std::experimental::nullopt; } }; //////////////////////////////////////////////////////////////////////////////////////////////////// -struct BodyLiteralPrintVisitor +struct BodyBodyLiteralTranslateVisitor { - void visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &, Context &context) + std::experimental::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &, Context &context) { - literal.data.accept(LiteralPrintVisitor(), literal, context); + return literal.data.accept(BodyLiteralTranslateVisitor(), literal, context); } - void visit(const Clingo::AST::ConditionalLiteral &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context) + std::experimental::optional visit(const Clingo::AST::ConditionalLiteral &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context) { throwErrorAtLocation(bodyLiteral.location, "“conditional literal” body literals currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::Aggregate &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context) + std::experimental::optional visit(const Clingo::AST::Aggregate &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context) { throwErrorAtLocation(bodyLiteral.location, "“aggregate” body literals currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::BodyAggregate &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context) + std::experimental::optional visit(const Clingo::AST::BodyAggregate &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context) { throwErrorAtLocation(bodyLiteral.location, "“body aggregate” body literals currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context) + std::experimental::optional visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context) { throwErrorAtLocation(bodyLiteral.location, "“theory atom” body literals currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::Disjoint &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context) + std::experimental::optional visit(const Clingo::AST::Disjoint &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context) { throwErrorAtLocation(bodyLiteral.location, "“disjoint” body literals currently unsupported", context); + return std::experimental::nullopt; } }; diff --git a/include/anthem/Head.h b/include/anthem/Head.h index b695657..95a2150 100644 --- a/include/anthem/Head.h +++ b/include/anthem/Head.h @@ -3,8 +3,8 @@ #include +#include #include -#include #include namespace anthem @@ -139,155 +139,179 @@ struct HeadLiteralCollectFunctionTermsVisitor //////////////////////////////////////////////////////////////////////////////////////////////////// -struct TermPrintSubstitutedVisitor +struct FunctionTermTranslateVisitor { - void visit(const Clingo::Symbol &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::Symbol &, const Clingo::AST::Term &term, Context &context) { throwErrorAtLocation(term.location, "“symbol” terms not allowed, function expected", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term, Context &context) { throwErrorAtLocation(term.location, "“variable” terms currently unsupported, function expected", context); + return std::experimental::nullopt; } - void 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) { throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported, function expected", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term, Context &context) { throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported, function expected", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term, Context &context) + std::experimental::optional visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term, Context &context) { throwErrorAtLocation(term.location, "“interval” terms currently unsupported, function expected", context); + return std::experimental::nullopt; } // TODO: check correctness - void 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) { if (function.external) throwErrorAtLocation(term.location, "external functions currently unsupported", context); - auto &outputStream = context.logger.outputStream(); - - outputStream << output::Function(function.name); - - if (function.arguments.empty()) - return; - - outputStream << "("; + std::vector arguments; + arguments.reserve(function.arguments.size()); for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++) { - if (i != function.arguments.cbegin()) - outputStream << ", "; - const auto &argument = *i; - const auto matchingTerm = std::find(context.headTerms.cbegin(), context.headTerms.cend(), &argument); assert(matchingTerm != context.headTerms.cend()); - const auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(matchingTerm - context.headTerms.cbegin() + 1); - - outputStream << output::Variable(variableName.c_str()); + auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(matchingTerm - context.headTerms.cbegin() + 1); + arguments.emplace_back(std::make_unique(std::move(variableName), ast::Variable::Type::Reserved)); } - outputStream << ")"; + return std::make_unique(function.name, std::move(arguments)); } - void 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) { throwErrorAtLocation(term.location, "“pool” terms currently unsupported, function expected", context); + return std::experimental::nullopt; } }; //////////////////////////////////////////////////////////////////////////////////////////////////// -struct LiteralPrintSubstitutedVisitor +struct LiteralTranslateVisitor { - void visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, Context &context) + std::experimental::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, Context &) { - context.logger.outputStream() << boolean; + return std::make_unique(boolean.value); } - void 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) { - term.data.accept(TermPrintSubstitutedVisitor(), term, context); + return term.data.accept(FunctionTermTranslateVisitor(), term, context); } - void visit(const Clingo::AST::Comparison &, const Clingo::AST::Literal &literal, Context &context) + std::experimental::optional visit(const Clingo::AST::Comparison &, const Clingo::AST::Literal &literal, Context &context) { throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &context) + std::experimental::optional visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &context) { throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals", context); + return std::experimental::nullopt; } }; //////////////////////////////////////////////////////////////////////////////////////////////////// -struct HeadLiteralPrintSubstitutedVisitor +struct HeadLiteralTranslateToConsequentVisitor { - void 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) { if (literal.sign == Clingo::AST::Sign::DoubleNegation) - throwErrorAtLocation(literal.location, "double-negated literals currently unsupported", context); + throwErrorAtLocation(literal.location, "double-negated head literals currently unsupported", context); - context.logger.outputStream() << literal.sign; + auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, context); - literal.data.accept(LiteralPrintSubstitutedVisitor(), literal, context); + if (literal.sign == Clingo::AST::Sign::None) + return translatedLiteral; + + if (!translatedLiteral) + return std::experimental::nullopt; + + return std::make_unique(std::move(translatedLiteral.value())); } - void 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) { - for (auto i = disjunction.elements.cbegin(); i != disjunction.elements.cend(); i++) - { - const auto &conditionalLiteral = *i; + std::vector arguments; + arguments.reserve(disjunction.elements.size()); + for (const auto &conditionalLiteral : disjunction.elements) + { if (!conditionalLiteral.condition.empty()) throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported", context); - if (i != disjunction.elements.cbegin()) - context.logger.outputStream() << " " << Clingo::AST::BinaryOperator::Or << " "; + auto argument = visit(conditionalLiteral.literal, headLiteral, context); - visit(conditionalLiteral.literal, headLiteral, context); + if (!argument) + throwErrorAtLocation(headLiteral.location, "could not parse argument", context); + + arguments.emplace_back(std::move(argument.value())); } + + return std::make_unique(std::move(arguments)); } - void 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) { if (aggregate.left_guard || aggregate.right_guard) throwErrorAtLocation(headLiteral.location, "aggregates with left or right guards not allowed", context); - for (auto i = aggregate.elements.cbegin(); i != aggregate.elements.cend(); i++) + const auto translateConditionalLiteral = + [&](const auto &conditionalLiteral) + { + if (!conditionalLiteral.condition.empty()) + throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported", context); + + return this->visit(conditionalLiteral.literal, headLiteral, context); + }; + + if (aggregate.elements.size() == 1) + return translateConditionalLiteral(aggregate.elements[0]); + + std::vector arguments; + arguments.reserve(aggregate.elements.size()); + + for (const auto &conditionalLiteral : aggregate.elements) { - const auto &conditionalLiteral = *i; + auto argument = translateConditionalLiteral(conditionalLiteral); - if (!conditionalLiteral.condition.empty()) - throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported", context); + if (!argument) + throwErrorAtLocation(headLiteral.location, "could not parse argument", context); - if (i != aggregate.elements.cbegin()) - context.logger.outputStream() << " " << Clingo::AST::BinaryOperator::Or << " "; - - visit(conditionalLiteral.literal, headLiteral, context); + arguments.emplace_back(std::move(argument.value())); } + + return std::make_unique(std::move(arguments)); } - void visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, Context &context) + std::experimental::optional visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, Context &context) { throwErrorAtLocation(headLiteral.location, "“head aggregate” head literals currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::HeadLiteral &headLiteral, Context &context) + std::experimental::optional visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::HeadLiteral &headLiteral, Context &context) { throwErrorAtLocation(headLiteral.location, "“theory” head literals currently unsupported", context); + return std::experimental::nullopt; } }; diff --git a/include/anthem/StatementVisitor.h b/include/anthem/StatementVisitor.h index 78e1e04..6b3df03 100644 --- a/include/anthem/StatementVisitor.h +++ b/include/anthem/StatementVisitor.h @@ -1,10 +1,11 @@ #ifndef __ANTHEM__STATEMENT_VISITOR_H #define __ANTHEM__STATEMENT_VISITOR_H +#include #include #include +#include #include -#include namespace anthem { @@ -17,37 +18,46 @@ namespace anthem struct StatementVisitor { - void visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, Context &context) + std::experimental::optional visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, Context &context) { // TODO: refactor context.logger.log(output::Priority::Debug, (std::string("[program] ") + program.name).c_str()); if (!program.parameters.empty()) throwErrorAtLocation(statement.location, "program parameters currently unsupported", context); + + return std::experimental::nullopt; } - void visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, Context &context) + std::experimental::optional visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, Context &context) { context.reset(); - auto &outputStream = context.logger.outputStream(); - // Concatenate all head terms rule.head.data.accept(HeadLiteralCollectFunctionTermsVisitor(), rule.head, context); + auto antecedent = std::make_unique(); + + // Compute consequent + auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, context); + + if (!consequent) + { + context.logger.log(output::Priority::Error, "could not translate formula consequent"); + return std::experimental::nullopt; + } + // Print auxiliary variables replacing the head atom’s arguments for (auto i = context.headTerms.cbegin(); i != context.headTerms.cend(); i++) { const auto &headTerm = **i; - if (i != context.headTerms.cbegin()) - outputStream << " " << Clingo::AST::BinaryOperator::And << " "; + auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i - context.headTerms.cbegin() + 1); + auto element = std::make_unique(std::move(variableName), ast::Variable::Type::Reserved); + auto set = translate(headTerm, context); + auto in = std::make_unique(std::move(element), std::move(set)); - const auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i - context.headTerms.cbegin() + 1); - - outputStream - << output::Variable(variableName.c_str()) - << " " << output::Keyword("in") << " " << headTerm; + antecedent->arguments.emplace_back(std::move(in)); } // Print translated body literals @@ -55,97 +65,94 @@ struct StatementVisitor { const auto &bodyLiteral = *i; - if (!context.headTerms.empty() || i != rule.body.cbegin()) - outputStream << " " << Clingo::AST::BinaryOperator::And << " "; - if (bodyLiteral.sign != Clingo::AST::Sign::None) throwErrorAtLocation(bodyLiteral.location, "only positive literals currently supported", context); - bodyLiteral.data.accept(BodyLiteralPrintVisitor(), bodyLiteral, context); + auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, context); + + if (!argument) + throwErrorAtLocation(bodyLiteral.location, "could not translate body literal", context); + + antecedent->arguments.emplace_back(std::move(argument.value())); } // Handle choice rules if (context.isChoiceRule) - { - const bool isFirstOutput = rule.body.empty() && context.headTerms.empty(); + antecedent->arguments.emplace_back(ast::deepCopy(consequent.value())); - if (!isFirstOutput) - outputStream << " " << Clingo::AST::BinaryOperator::And << " "; + // Use “true” as the consequent in case it is empty + if (antecedent->arguments.empty()) + return std::make_unique(std::make_unique(true), std::move(consequent.value())); + else if (antecedent->arguments.size() == 1) + return std::make_unique(std::move(antecedent->arguments[0]), std::move(consequent.value())); - if (context.numberOfHeadLiterals > 1 && !isFirstOutput) - outputStream << "("; - - rule.head.data.accept(HeadLiteralPrintSubstitutedVisitor(), rule.head, context); - - if (context.numberOfHeadLiterals > 1 && !isFirstOutput) - outputStream << ")"; - } - - // Print “true” on the left side of the formula in case there is nothing else - if (rule.body.empty() && context.headTerms.empty() && !context.isChoiceRule) - outputStream << Clingo::AST::Boolean({true}); - - outputStream << " " << output::Operator("->") << " "; - - // Print consequent of the implication - rule.head.data.accept(HeadLiteralPrintSubstitutedVisitor(), rule.head, context); - - outputStream << std::endl; + return std::make_unique(std::move(antecedent), std::move(consequent.value())); } - void visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement, Context &context) + std::experimental::optional visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement, Context &context) { throwErrorAtLocation(statement.location, "“definition” statements currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::ShowSignature &, const Clingo::AST::Statement &statement, Context &context) + std::experimental::optional visit(const Clingo::AST::ShowSignature &, const Clingo::AST::Statement &statement, Context &context) { throwErrorAtLocation(statement.location, "“show signature” statements currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, Context &context) + std::experimental::optional visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, Context &context) { throwErrorAtLocation(statement.location, "“show term” statements currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::Minimize &, const Clingo::AST::Statement &statement, Context &context) + std::experimental::optional visit(const Clingo::AST::Minimize &, const Clingo::AST::Statement &statement, Context &context) { throwErrorAtLocation(statement.location, "“minimize” statements currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::Script &, const Clingo::AST::Statement &statement, Context &context) + std::experimental::optional visit(const Clingo::AST::Script &, const Clingo::AST::Statement &statement, Context &context) { throwErrorAtLocation(statement.location, "“script” statements currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::External &, const Clingo::AST::Statement &statement, Context &context) + std::experimental::optional visit(const Clingo::AST::External &, const Clingo::AST::Statement &statement, Context &context) { throwErrorAtLocation(statement.location, "“external” statements currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::Edge &, const Clingo::AST::Statement &statement, Context &context) + std::experimental::optional visit(const Clingo::AST::Edge &, const Clingo::AST::Statement &statement, Context &context) { throwErrorAtLocation(statement.location, "“edge” statements currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::Heuristic &, const Clingo::AST::Statement &statement, Context &context) + std::experimental::optional visit(const Clingo::AST::Heuristic &, const Clingo::AST::Statement &statement, Context &context) { throwErrorAtLocation(statement.location, "“heuristic” statements currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::ProjectAtom &, const Clingo::AST::Statement &statement, Context &context) + std::experimental::optional visit(const Clingo::AST::ProjectAtom &, const Clingo::AST::Statement &statement, Context &context) { throwErrorAtLocation(statement.location, "“project atom” statements currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::ProjectSignature &, const Clingo::AST::Statement &statement, Context &context) + std::experimental::optional visit(const Clingo::AST::ProjectSignature &, const Clingo::AST::Statement &statement, Context &context) { throwErrorAtLocation(statement.location, "“project signature” statements currently unsupported", context); + return std::experimental::nullopt; } - void visit(const Clingo::AST::TheoryDefinition &, const Clingo::AST::Statement &statement, Context &context) + std::experimental::optional visit(const Clingo::AST::TheoryDefinition &, const Clingo::AST::Statement &statement, Context &context) { throwErrorAtLocation(statement.location, "“theory definition” statements currently unsupported", context); + return std::experimental::nullopt; } }; diff --git a/include/anthem/Term.h b/include/anthem/Term.h new file mode 100644 index 0000000..e00ec25 --- /dev/null +++ b/include/anthem/Term.h @@ -0,0 +1,132 @@ +#ifndef __ANTHEM__TERM_H +#define __ANTHEM__TERM_H + +#include + +#include +#include +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Term +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOperator, const Clingo::AST::Term &term, Context &context) +{ + switch (binaryOperator) + { + case Clingo::AST::BinaryOperator::Plus: + return ast::BinaryOperation::Operator::Plus; + case Clingo::AST::BinaryOperator::Minus: + return ast::BinaryOperation::Operator::Minus; + case Clingo::AST::BinaryOperator::Multiplication: + return ast::BinaryOperation::Operator::Multiplication; + case Clingo::AST::BinaryOperator::Division: + return ast::BinaryOperation::Operator::Division; + case Clingo::AST::BinaryOperator::Modulo: + return ast::BinaryOperation::Operator::Modulo; + default: + throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported", context); + } + + return ast::BinaryOperation::Operator::Plus; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +ast::Term translate(const Clingo::AST::Term &term, Context &context); + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct TermTranslateVisitor +{ + std::experimental::optional visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, Context &context) + { + switch (symbol.type()) + { + case Clingo::SymbolType::Number: + return std::make_unique(symbol.number()); + case Clingo::SymbolType::Infimum: + return std::make_unique(ast::SpecialInteger::Type::Infimum); + case Clingo::SymbolType::Supremum: + return std::make_unique(ast::SpecialInteger::Type::Supremum); + case Clingo::SymbolType::String: + return std::make_unique(std::string(symbol.string())); + default: + throwErrorAtLocation(term.location, "only numeric “symbol” terms allowed", context); + } + + return std::experimental::nullopt; + } + + std::experimental::optional visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, Context &) + { + return std::make_unique(std::string(variable.name), ast::Variable::Type::UserDefined); + } + + std::experimental::optional visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, Context &context) + { + 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) + { + const auto operator_ = translate(binaryOperation.binary_operator, term, context); + auto left = translate(binaryOperation.left, context); + auto right = translate(binaryOperation.right, context); + + return std::make_unique(operator_, std::move(left), std::move(right)); + } + + std::experimental::optional visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, Context &context) + { + auto left = translate(interval.left, context); + auto right = translate(interval.right, context); + + return std::make_unique(std::move(left), std::move(right)); + } + + std::experimental::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context) + { + if (function.external) + throwErrorAtLocation(term.location, "external functions currently unsupported", context); + + std::vector arguments; + arguments.reserve(function.arguments.size()); + + for (const auto &argument : function.arguments) + arguments.emplace_back(translate(argument, context)); + + return std::make_unique(function.name, std::move(arguments)); + } + + std::experimental::optional visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, Context &context) + { + throwErrorAtLocation(term.location, "“pool” terms currently unsupported", context); + return std::experimental::nullopt; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +ast::Term translate(const Clingo::AST::Term &term, Context &context) +{ + auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, context); + + if (!translatedTerm) + throwErrorAtLocation(term.location, "could not translate term", context); + + return std::move(translatedTerm.value()); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} + +#endif diff --git a/include/anthem/output/AST.h b/include/anthem/output/AST.h new file mode 100644 index 0000000..68b48bd --- /dev/null +++ b/include/anthem/output/AST.h @@ -0,0 +1,345 @@ +#ifndef __ANTHEM__OUTPUT__AST_H +#define __ANTHEM__OUTPUT__AST_H + +#include + +#include +#include +#include +#include + +namespace anthem +{ +namespace ast +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// 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); + +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); + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Primitives +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, BinaryOperation::Operator operator_) +{ + switch (operator_) + { + case BinaryOperation::Operator::Plus: + return (stream << output::Operator("+")); + case BinaryOperation::Operator::Minus: + return (stream << output::Operator("-")); + case BinaryOperation::Operator::Multiplication: + return (stream << output::Operator("*")); + case BinaryOperation::Operator::Division: + return (stream << output::Operator("/")); + case BinaryOperation::Operator::Modulo: + return (stream << output::Operator("%")); + } + + return stream; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const BinaryOperation &binaryOperation) +{ + return (stream << "(" << binaryOperation.left << " " << binaryOperation.operator_ << " " << binaryOperation.right << ")"); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Boolean &boolean) +{ + if (boolean.value) + return (stream << output::Boolean("#true")); + + return (stream << output::Boolean("#false")); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, Comparison::Operator operator_) +{ + switch (operator_) + { + case Comparison::Operator::GreaterThan: + return (stream << output::Operator(">")); + case Comparison::Operator::LessThan: + return (stream << output::Operator("<")); + case Comparison::Operator::LessEqual: + return (stream << output::Operator("<=")); + case Comparison::Operator::GreaterEqual: + return (stream << output::Operator(">=")); + case Comparison::Operator::NotEqual: + return (stream << output::Operator("!=")); + case Comparison::Operator::Equal: + return (stream << output::Operator("=")); + } + + return stream; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Comparison &comparison) +{ + return (stream << comparison.left << " " << comparison.operator_ << " " << comparison.right); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Constant &constant) +{ + return (stream << constant.name); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Function &function) +{ + stream << function.name; + + if (function.arguments.empty()) + return stream; + + stream << "("; + + for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++) + { + if (i != function.arguments.cbegin()) + stream << ", "; + + stream << (*i); + } + + if (function.name.empty() && function.arguments.size() == 1) + stream << ","; + + return (stream << ")"); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const In &in) +{ + return (stream << in.element << " " << output::Keyword("in") << " " << in.set); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Integer &integer) +{ + return (stream << output::Number(integer.value)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Interval &interval) +{ + return (stream << interval.from << ".." << interval.to); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Predicate &predicate) +{ + stream << predicate.name; + + if (predicate.arguments.empty()) + return stream; + + stream << "("; + + for (auto i = predicate.arguments.cbegin(); i != predicate.arguments.cend(); i++) + { + if (i != predicate.arguments.cbegin()) + stream << ", "; + + stream << (*i); + } + + return (stream << ")"); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const SpecialInteger &specialInteger) +{ + switch (specialInteger.type) + { + case SpecialInteger::Type::Infimum: + return (stream << output::Number("#inf")); + case SpecialInteger::Type::Supremum: + return (stream << output::Number("#sup")); + } + + return stream; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const String &string) +{ + return (stream << output::String(string.text.c_str())); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Variable &variable) +{ + assert(!variable.name.empty()); + assert(variable.name[0] >= 65 && variable.name[0] <= 90); + + if (variable.type == ast::Variable::Type::Reserved || !isReservedVariableName(variable.name.c_str())) + return (stream << output::Variable(variable.name.c_str())); + + const auto variableName = std::string(UserVariablePrefix) + variable.name; + + return (stream << output::Variable(variableName.c_str())); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Expressions +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const And &and_) +{ + stream << "("; + + for (auto i = and_.arguments.cbegin(); i != and_.arguments.cend(); i++) + { + if (i != and_.arguments.cbegin()) + stream << " " << output::Keyword("and") << " "; + + stream << (*i); + } + + return (stream << ")"); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Biconditional &biconditional) +{ + return (stream << "(" << biconditional.left << " <-> " << biconditional.right << ")"); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Exists &exists) +{ + stream << output::Keyword("exists") << " "; + + for (auto i = exists.variables.cbegin(); i != exists.variables.cend(); i++) + { + if (i != exists.variables.cbegin()) + stream << ", "; + + stream << (**i); + } + + return (stream << " " << exists.argument); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const ForAll &forAll) +{ + stream << output::Keyword("forall") << " "; + + for (auto i = forAll.variables.cbegin(); i != forAll.variables.cend(); i++) + { + if (i != forAll.variables.cbegin()) + stream << ", "; + + stream << (**i); + } + + return (stream << " " << forAll.argument); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Implies &implies) +{ + return (stream << "(" << implies.antecedent << " -> " << implies.consequent << ")"); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Not ¬_) +{ + return (stream << output::Keyword("not ") << not_.argument); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Or &or_) +{ + stream << "("; + + for (auto i = or_.arguments.cbegin(); i != or_.arguments.cend(); i++) + { + if (i != or_.arguments.cbegin()) + stream << " " << output::Keyword("or") << " "; + + stream << (*i); + } + + return (stream << ")"); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// Variants +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Formula &formula) +{ + formula.match([&](const auto &x){stream << *x;}); + + return stream; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +output::ColorStream &operator<<(output::ColorStream &stream, const Term &term) +{ + term.match([&](const auto &x){stream << *x;}); + + return stream; +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} +} + +#endif diff --git a/include/anthem/output/ClingoOutput.h b/include/anthem/output/ClingoOutput.h deleted file mode 100644 index bef9a51..0000000 --- a/include/anthem/output/ClingoOutput.h +++ /dev/null @@ -1,36 +0,0 @@ -#ifndef __ANTHEM__OUTPUT__CLINGO_OUTPUT_H -#define __ANTHEM__OUTPUT__CLINGO_OUTPUT_H - -#include - -#include - -namespace anthem -{ -namespace output -{ - -//////////////////////////////////////////////////////////////////////////////////////////////////// -// -// ClingoOutput -// -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ColorStream &operator<<(ColorStream &stream, const Clingo::Symbol &symbol); -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Sign &sign); -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Boolean &boolean); -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Variable &variable); -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::BinaryOperator &binaryOperator); -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::UnaryOperation &unaryOperation); -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::BinaryOperation &binaryOperation); -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Interval &interval); -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Function &function); -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Pool &pool); -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Term &term); - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -} -} - -#endif diff --git a/include/anthem/output/Formatting.h b/include/anthem/output/Formatting.h index 4a556eb..fe5410d 100644 --- a/include/anthem/output/Formatting.h +++ b/include/anthem/output/Formatting.h @@ -118,7 +118,7 @@ struct Keyword inline ColorStream &operator<<(ColorStream &stream, const Keyword &keyword) { return (stream - << Format({Color::Blue, FontWeight::Bold}) + << Format({Color::Blue, FontWeight::Normal}) << keyword.name << ResetFormat()); } diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index f9d55fd..300470d 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -8,6 +8,7 @@ #include #include +#include namespace anthem { @@ -40,7 +41,12 @@ void translate(const char *fileName, std::istream &stream, Context &context) const auto translateStatement = [&context](const Clingo::AST::Statement &statement) { - statement.data.accept(StatementVisitor(), statement, context); + const auto formula = statement.data.accept(StatementVisitor(), statement, context); + + if (!formula) + return; + + context.logger.outputStream() << formula.value() << std::endl; }; const auto logger = diff --git a/src/anthem/output/ClingoOutput.cpp b/src/anthem/output/ClingoOutput.cpp deleted file mode 100644 index 9571125..0000000 --- a/src/anthem/output/ClingoOutput.cpp +++ /dev/null @@ -1,257 +0,0 @@ -#include - -#include -#include - -namespace anthem -{ -namespace output -{ - -//////////////////////////////////////////////////////////////////////////////////////////////////// -// -// ClingoOutput -// -//////////////////////////////////////////////////////////////////////////////////////////////////// - -const auto printCollection = [](auto &stream, const auto &collection, - const auto &preToken, const auto &delimiter, const auto &postToken, bool printTokensIfEmpty) -{ - if (collection.empty() && !printTokensIfEmpty) - return; - - if (collection.empty() && printTokensIfEmpty) - { - stream << preToken << postToken; - return; - } - - stream << preToken; - - // TODO: use cbegin/cend (requires support by Clingo::SymbolSpan) - for (auto i = collection.begin(); i != collection.end(); i++) - { - if (i != collection.begin()) - stream << delimiter; - - stream << *i; - } - - stream << postToken; -}; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ColorStream &operator<<(ColorStream &stream, const Clingo::Symbol &symbol) -{ - switch (symbol.type()) - { - case Clingo::SymbolType::Infimum: - return (stream << Keyword("#inf")); - case Clingo::SymbolType::Supremum: - return (stream << Keyword("#sup")); - case Clingo::SymbolType::Number: - return (stream << Number(symbol.number())); - case Clingo::SymbolType::String: - return (stream << String(symbol.string())); - case Clingo::SymbolType::Function: - { - const auto isNegative = symbol.is_negative(); - assert(isNegative != symbol.is_positive()); - - const auto isUnaryTuple = (symbol.name()[0] == '\0' && symbol.arguments().size() == 1); - const auto printIfEmpty = (symbol.name()[0] == '\0' || !symbol.arguments().empty()); - - if (isNegative) - stream << Operator("-"); - - stream << Function(symbol.name()); - - const auto postToken = (isUnaryTuple ? ",)" : ")"); - - printCollection(stream, symbol.arguments(), "(", ", ", postToken, printIfEmpty); - - return stream; - } - } - - return stream; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Sign &sign) -{ - switch (sign) - { - case Clingo::AST::Sign::None: - return stream; - case Clingo::AST::Sign::Negation: - return (stream << Keyword("not") << " "); - case Clingo::AST::Sign::DoubleNegation: - return (stream << Keyword("not") << " " << Keyword("not") << " "); - } - - return stream; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Boolean &boolean) -{ - if (boolean.value == true) - return (stream << Boolean("#true")); - - return (stream << Boolean("#false")); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Variable &variable) -{ - if (!isReservedVariableName(variable.name)) - return (stream << Variable(variable.name)); - - const auto variableName = std::string(UserVariablePrefix) + variable.name; - - return (stream << Variable(variableName.c_str())); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::BinaryOperator &binaryOperator) -{ - switch (binaryOperator) - { - case Clingo::AST::BinaryOperator::XOr: - return (stream << Keyword("xor")); - case Clingo::AST::BinaryOperator::Or: - return (stream << Keyword("or")); - case Clingo::AST::BinaryOperator::And: - return (stream << Keyword("and")); - case Clingo::AST::BinaryOperator::Plus: - return (stream << Operator("+")); - case Clingo::AST::BinaryOperator::Minus: - return (stream << Operator("-")); - case Clingo::AST::BinaryOperator::Multiplication: - return (stream << Operator("*")); - case Clingo::AST::BinaryOperator::Division: - return (stream << Operator("/")); - case Clingo::AST::BinaryOperator::Modulo: - return (stream << Operator("\\")); - } - - return stream; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::UnaryOperation &unaryOperation) -{ - return (stream - << Keyword(Clingo::AST::left_hand_side(unaryOperation.unary_operator)) - << unaryOperation.argument - << Keyword(Clingo::AST::right_hand_side(unaryOperation.unary_operator))); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::BinaryOperation &binaryOperation) -{ - return (stream << "(" << binaryOperation.left - << " " << binaryOperation.binary_operator - << " " << binaryOperation.right << ")"); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Interval &interval) -{ - return (stream << "(" << interval.left << Operator("..") << interval.right << ")"); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Function &function) -{ - const auto isUnaryTuple = (function.name[0] == '\0' && function.arguments.size() == 1); - const auto printIfEmpty = (function.name[0] == '\0' || !function.arguments.empty()); - - if (function.external) - stream << Operator("@"); - - stream << output::Function(function.name); - - const auto postToken = (isUnaryTuple ? ",)" : ")"); - - printCollection(stream, function.arguments, "(", ", ", postToken, printIfEmpty); - - return stream; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Pool &pool) -{ - // Note: There is no representation for an empty pool - if (pool.arguments.empty()) - return (stream << "(" << Number(1) << "/" << Number(0) << ")"); - - printCollection(stream, pool.arguments, "(", ";", ")", true); - - return stream; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -struct TermOutputVisitor -{ - void visit(const Clingo::Symbol &symbol, ColorStream &stream) - { - stream << symbol; - } - - void visit(const Clingo::AST::Variable &variable, ColorStream &stream) - { - stream << variable; - } - - void visit(const Clingo::AST::UnaryOperation &unaryOperation, ColorStream &stream) - { - stream << unaryOperation; - } - - void visit(const Clingo::AST::BinaryOperation &binaryOperation, ColorStream &stream) - { - stream << binaryOperation; - } - - void visit(const Clingo::AST::Interval &interval, ColorStream &stream) - { - stream << interval; - } - - void visit(const Clingo::AST::Function &function, ColorStream &stream) - { - stream << function; - } - - void visit(const Clingo::AST::Pool &pool, ColorStream &stream) - { - stream << pool; - } -}; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Term &term) -{ - term.data.accept(TermOutputVisitor(), stream); - - return stream; -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - -} -} diff --git a/tests/TestTranslation.cpp b/tests/TestTranslation.cpp index a98d1b8..370c579 100644 --- a/tests/TestTranslation.cpp +++ b/tests/TestTranslation.cpp @@ -21,7 +21,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(1..5)."; anthem::translate("input", input, context); - REQUIRE(output.str() == "V1 in (1..5) -> p(V1)\n"); + REQUIRE(output.str() == "(V1 in 1..5 -> p(V1))\n"); } SECTION("simple example 2") @@ -29,7 +29,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(N) :- N = 1..5."; anthem::translate("input", input, context); - REQUIRE(output.str() == "V1 in N and exists X1, X2 (X1 in N and X2 in (1..5) and X1 = X2) -> p(V1)\n"); + REQUIRE(output.str() == "((V1 in N and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> p(V1))\n"); } SECTION("simple example 3") @@ -37,7 +37,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(N + 1) :- q(N)."; anthem::translate("input", input, context); - REQUIRE(output.str() == "V1 in (N + 1) and exists X1 (X1 in N and q(X1)) -> p(V1)\n"); + REQUIRE(output.str() == "((V1 in (N + 1) and exists X1 (X1 in N and q(X1))) -> p(V1))\n"); } SECTION("n-ary head") @@ -45,7 +45,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(N, 1, 2) :- N = 1..5."; anthem::translate("input", input, context); - REQUIRE(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"); + REQUIRE(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"); } SECTION("disjunctive head") @@ -54,7 +54,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); - REQUIRE(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"); + REQUIRE(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"); } SECTION("disjunctive head (alternative syntax)") @@ -63,7 +63,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); - REQUIRE(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"); + REQUIRE(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"); } SECTION("escaping conflicting variable names") @@ -71,7 +71,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X1, V1) :- q(X1), q(V1)."; anthem::translate("input", input, context); - REQUIRE(output.str() == "V1 in _X1 and V2 in _V1 and exists X1 (X1 in _X1 and q(X1)) and exists X2 (X2 in _V1 and q(X2)) -> p(V1, V2)\n"); + REQUIRE(output.str() == "((V1 in _X1 and V2 in _V1 and exists X1 (X1 in _X1 and q(X1)) and exists X2 (X2 in _V1 and q(X2))) -> p(V1, V2))\n"); } SECTION("fact") @@ -79,7 +79,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(42)."; anthem::translate("input", input, context); - REQUIRE(output.str() == "V1 in 42 -> p(V1)\n"); + REQUIRE(output.str() == "(V1 in 42 -> p(V1))\n"); } SECTION("0-ary fact") @@ -87,7 +87,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p."; anthem::translate("input", input, context); - REQUIRE(output.str() == "#true -> p\n"); + REQUIRE(output.str() == "(#true -> p)\n"); } SECTION("disjunctive fact (no arguments)") @@ -95,7 +95,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "q; p."; anthem::translate("input", input, context); - REQUIRE(output.str() == "#true -> p or q\n"); + REQUIRE(output.str() == "(#true -> (p or q))\n"); } SECTION("disjunctive fact (arguments)") @@ -103,7 +103,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "q; p(42)."; anthem::translate("input", input, context); - REQUIRE(output.str() == "V1 in 42 -> p(V1) or q\n"); + REQUIRE(output.str() == "(V1 in 42 -> (p(V1) or q))\n"); } SECTION("integrity constraint (no arguments)") @@ -111,7 +111,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << ":- p, q."; anthem::translate("input", input, context); - REQUIRE(output.str() == "p and q -> #false\n"); + REQUIRE(output.str() == "((p and q) -> #false)\n"); } SECTION("contradiction") @@ -119,7 +119,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << ":-."; anthem::translate("input", input, context); - REQUIRE(output.str() == "#true -> #false\n"); + REQUIRE(output.str() == "(#true -> #false)\n"); } SECTION("integrity constraint (arguments)") @@ -127,7 +127,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << ":- p(42), q."; anthem::translate("input", input, context); - REQUIRE(output.str() == "exists X1 (X1 in 42 and p(X1)) and q -> #false\n"); + REQUIRE(output.str() == "((exists X1 (X1 in 42 and p(X1)) and q) -> #false)\n"); } SECTION("inf/sup") @@ -135,7 +135,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X, #inf) :- q(X, #sup)."; anthem::translate("input", input, context); - REQUIRE(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"); + REQUIRE(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"); } SECTION("strings") @@ -143,7 +143,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X, \"foo\") :- q(X, \"bar\")."; anthem::translate("input", input, context); - REQUIRE(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"); + REQUIRE(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"); } SECTION("tuples") @@ -151,7 +151,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X, (1, 2, 3)) :- q(X, (4, 5))."; anthem::translate("input", input, context); - REQUIRE(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"); + REQUIRE(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"); } SECTION("1-ary tuples") @@ -159,7 +159,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X, (1,)) :- q(X, (2,))."; anthem::translate("input", input, context); - REQUIRE(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"); + REQUIRE(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"); } SECTION("intervals") @@ -167,7 +167,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X, 1..10) :- q(X, 6..12)."; anthem::translate("input", input, context); - REQUIRE(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"); + REQUIRE(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"); } SECTION("comparisons") @@ -175,7 +175,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(M, N, O, P) :- M < N, P != O."; anthem::translate("input", input, context); - REQUIRE(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"); + REQUIRE(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"); } SECTION("single negation") @@ -183,7 +183,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "not p(X, 1) :- not q(X, 2)."; anthem::translate("input", input, context); - REQUIRE(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"); + REQUIRE(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"); } SECTION("variable numbering") @@ -192,9 +192,9 @@ 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); - REQUIRE(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))" - " -> q(V1, V2) or p(V3, V4) or g(V5) or f\n"); + REQUIRE(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)))" + " -> (q(V1, V2) or p(V3, V4) or g(V5) or f))\n"); } SECTION("nested functions") @@ -202,7 +202,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); - REQUIRE(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"); + REQUIRE(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"); } SECTION("choice rule (simple)") @@ -210,7 +210,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "{p}."; anthem::translate("input", input, context); - REQUIRE(output.str() == "p -> p\n"); + REQUIRE(output.str() == "(p -> p)\n"); } SECTION("choice rule (two elements)") @@ -218,7 +218,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "{p; q}."; anthem::translate("input", input, context); - REQUIRE(output.str() == "p or q -> p or q\n"); + REQUIRE(output.str() == "((p or q) -> (p or q))\n"); } SECTION("choice rule (n-ary elements)") @@ -226,7 +226,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "{p(1..3, N); q(2..4)}."; anthem::translate("input", input, context); - REQUIRE(output.str() == "V1 in (1..3) and V2 in N and V3 in (2..4) and (p(V1, V2) or q(V3)) -> p(V1, V2) or q(V3)\n"); + REQUIRE(output.str() == "((V1 in 1..3 and V2 in N and V3 in 2..4 and (p(V1, V2) or q(V3))) -> (p(V1, V2) or q(V3)))\n"); } SECTION("choice rule with body") @@ -234,6 +234,22 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "{p(M, N); q(P)} :- s(M, N, P)."; anthem::translate("input", input, context); - REQUIRE(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) or q(V3)) -> p(V1, V2) or q(V3)\n"); + REQUIRE(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) or q(V3))) -> (p(V1, V2) or q(V3)))\n"); + } + + SECTION("choice rule with negation") + { + input << "{not p(X, 1)} :- not q(X, 2)."; + anthem::translate("input", input, context); + + REQUIRE(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"); + } + + SECTION("choice rule with negation (two elements)") + { + input << "{not p(X, 1); not s} :- not q(X, 2)."; + anthem::translate("input", input, context); + + REQUIRE(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) or not s)) -> (not p(V1, V2) or not s))\n"); } }