diff --git a/CMakeLists.txt b/CMakeLists.txt index a0064c9..b73e5ac 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -7,7 +7,7 @@ option(ANTHEM_BUILD_STATIC "Build static binaries" OFF) set(CMAKE_CXX_FLAGS "-Wall -Wextra -Wpedantic ${CMAKE_CXX_FLAGS}") set(CMAKE_CXX_FLAGS_DEBUG "-g ${CMAKE_CXX_FLAGS_DEBUG}") -set(CMAKE_CXX_STANDARD 14) +set(CMAKE_CXX_STANDARD 17) set(CMAKE_CXX_STANDARD_REQUIRED ON) set(CMAKE_CXX_EXTENSIONS OFF) diff --git a/README.md b/README.md index bca293a..5edb50a 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ With the option `--simplify`, output formulas are simplified by applying several ## Building `anthem` requires [CMake](https://cmake.org/) and [Boost](http://www.boost.org/) for building. -After installing the dependencies, `anthem` is built with a C++14 compiler (GCC ≥ 6.1 or clang ≥ 3.8). +After installing the dependencies, `anthem` is built with a C++17 compiler (GCC ≥ 7.3 or clang ≥ 5.0). ```bash $ git clone https://github.com/potassco/anthem.git diff --git a/include/anthem/ASTUtils.h b/include/anthem/ASTUtils.h index 113cd3a..a0afb56 100644 --- a/include/anthem/ASTUtils.h +++ b/include/anthem/ASTUtils.h @@ -1,7 +1,7 @@ #ifndef __ANTHEM__AST_UTILS_H #define __ANTHEM__AST_UTILS_H -#include +#include #include #include @@ -28,7 +28,7 @@ class VariableStack void push(Layer layer); void pop(); - std::experimental::optional findUserVariableDeclaration(const char *variableName) const; + std::optional findUserVariableDeclaration(const char *variableName) const; bool contains(const VariableDeclaration &variableDeclaration) const; private: diff --git a/include/anthem/Body.h b/include/anthem/Body.h index 62e96a5..3b30e3d 100644 --- a/include/anthem/Body.h +++ b/include/anthem/Body.h @@ -43,7 +43,7 @@ ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOp struct BodyTermTranslateVisitor { // TODO: refactor - std::experimental::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext, ast::VariableStack &variableStack) + std::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext, ast::VariableStack &variableStack) { if (literal.sign == Clingo::AST::Sign::DoubleNegation) throw TranslationException(literal.location, "double-negated literals currently unsupported"); @@ -93,12 +93,12 @@ struct BodyTermTranslateVisitor } template - std::experimental::optional visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, RuleContext &, ast::VariableStack &) + std::optional visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, RuleContext &, ast::VariableStack &) { assert(!term.data.is()); throw TranslationException(term.location, "term currently unsupported in this context, expected function"); - return std::experimental::nullopt; + return std::nullopt; } }; @@ -106,18 +106,18 @@ struct BodyTermTranslateVisitor struct BodyLiteralTranslateVisitor { - std::experimental::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, ast::VariableStack &) + std::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, ast::VariableStack &) { return ast::Formula::make(boolean.value); } - std::experimental::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack) + std::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack) { return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, variableStack); } // TODO: refactor - std::experimental::optional visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack) + std::optional visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, 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) @@ -140,10 +140,10 @@ struct BodyLiteralTranslateVisitor } template - std::experimental::optional visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, ast::VariableStack &) + std::optional visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, ast::VariableStack &) { throw TranslationException(literal.location, "literal currently unsupported in this context, expected function or term"); - return std::experimental::nullopt; + return std::nullopt; } }; @@ -151,7 +151,7 @@ struct BodyLiteralTranslateVisitor struct BodyBodyLiteralTranslateVisitor { - std::experimental::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, ast::VariableStack &variableStack) + std::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, ast::VariableStack &variableStack) { if (bodyLiteral.sign != Clingo::AST::Sign::None) throw TranslationException(bodyLiteral.location, "only positive body literals supported currently"); @@ -160,10 +160,10 @@ struct BodyBodyLiteralTranslateVisitor } template - std::experimental::optional visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, ast::VariableStack &) + std::optional visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, ast::VariableStack &) { throw TranslationException(bodyLiteral.location, "body literal currently unsupported in this context, expected literal"); - return std::experimental::nullopt; + return std::nullopt; } }; diff --git a/include/anthem/Context.h b/include/anthem/Context.h index 44bc1dc..33ec6ac 100644 --- a/include/anthem/Context.h +++ b/include/anthem/Context.h @@ -1,7 +1,7 @@ #ifndef __ANTHEM__CONTEXT_H #define __ANTHEM__CONTEXT_H -#include +#include #include #include @@ -30,7 +30,7 @@ struct Context bool performSimplification = false; bool performCompletion = false; - std::experimental::optional> visiblePredicateSignatures; + std::optional> visiblePredicateSignatures; ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal; }; diff --git a/include/anthem/Head.h b/include/anthem/Head.h index 6430ac8..f4804a0 100644 --- a/include/anthem/Head.h +++ b/include/anthem/Head.h @@ -2,7 +2,7 @@ #define __ANTHEM__HEAD_H #include -#include +#include #include #include @@ -119,7 +119,7 @@ struct HeadLiteralCollectFunctionTermsVisitor struct FunctionTermTranslateVisitor { // TODO: check correctness - std::experimental::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, size_t &headVariableIndex) + std::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, size_t &headVariableIndex) { if (function.external) throw TranslationException(term.location, "external functions currently unsupported"); @@ -134,10 +134,10 @@ struct FunctionTermTranslateVisitor } template - std::experimental::optional visit(const T &, const Clingo::AST::Term &term, RuleContext &, size_t &) + std::optional visit(const T &, const Clingo::AST::Term &term, RuleContext &, size_t &) { throw TranslationException(term.location, "term currently unsupported in this context, function expected"); - return std::experimental::nullopt; + return std::nullopt; } }; @@ -145,21 +145,21 @@ struct FunctionTermTranslateVisitor struct LiteralTranslateVisitor { - std::experimental::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, size_t &) + std::optional visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, size_t &) { return ast::Formula::make(boolean.value); } - std::experimental::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, size_t &headVariableIndex) + std::optional visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, size_t &headVariableIndex) { return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, headVariableIndex); } template - std::experimental::optional visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, size_t &) + std::optional visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, size_t &) { throw TranslationException(literal.location, "only disjunctions of literals allowed as head literals"); - return std::experimental::nullopt; + return std::nullopt; } }; @@ -167,7 +167,7 @@ struct LiteralTranslateVisitor struct HeadLiteralTranslateToConsequentVisitor { - std::experimental::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, size_t &headVariableIndex) + std::optional visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, size_t &headVariableIndex) { if (literal.sign == Clingo::AST::Sign::DoubleNegation) throw TranslationException(literal.location, "double-negated head literals currently unsupported"); @@ -178,12 +178,12 @@ struct HeadLiteralTranslateToConsequentVisitor return translatedLiteral; if (!translatedLiteral) - return std::experimental::nullopt; + return std::nullopt; return ast::Formula::make(std::move(translatedLiteral.value())); } - std::experimental::optional visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex) + std::optional visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex) { std::vector arguments; arguments.reserve(disjunction.elements.size()); @@ -204,7 +204,7 @@ struct HeadLiteralTranslateToConsequentVisitor return ast::Formula::make(std::move(arguments)); } - std::experimental::optional visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex) + std::optional visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex) { if (aggregate.left_guard || aggregate.right_guard) throw TranslationException(headLiteral.location, "aggregates with left or right guards currently unsupported"); @@ -238,10 +238,10 @@ struct HeadLiteralTranslateToConsequentVisitor } template - std::experimental::optional visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, size_t &) + std::optional visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, size_t &) { throw TranslationException(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate"); - return std::experimental::nullopt; + return std::nullopt; } }; diff --git a/include/anthem/Term.h b/include/anthem/Term.h index f82aecf..3addeb9 100644 --- a/include/anthem/Term.h +++ b/include/anthem/Term.h @@ -48,7 +48,7 @@ ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, con struct TermTranslateVisitor { - std::experimental::optional visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack) + std::optional visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack) { switch (symbol.type()) { @@ -81,10 +81,10 @@ struct TermTranslateVisitor } } - return std::experimental::nullopt; + return std::nullopt; } - std::experimental::optional visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack) + std::optional visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack) { const auto matchingVariableDeclaration = variableStack.findUserVariableDeclaration(variable.name); const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0); @@ -100,13 +100,13 @@ struct TermTranslateVisitor return ast::Term::make(ruleContext.freeVariables.back().get()); } - std::experimental::optional visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &) + std::optional visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &) { throw TranslationException(term.location, "“unary operation” terms currently unsupported"); - return std::experimental::nullopt; + return std::nullopt; } - std::experimental::optional visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack) + std::optional visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack) { const auto operator_ = translate(binaryOperation.binary_operator, term); auto left = translate(binaryOperation.left, ruleContext, variableStack); @@ -115,7 +115,7 @@ struct TermTranslateVisitor return ast::Term::make(operator_, std::move(left), std::move(right)); } - std::experimental::optional visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack) + std::optional visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack) { auto left = translate(interval.left, ruleContext, variableStack); auto right = translate(interval.right, ruleContext, variableStack); @@ -123,7 +123,7 @@ struct TermTranslateVisitor return ast::Term::make(std::move(left), std::move(right)); } - std::experimental::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack) + std::optional visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack) { if (function.external) throw TranslationException(term.location, "external functions currently unsupported"); @@ -137,10 +137,10 @@ struct TermTranslateVisitor return ast::Term::make(function.name, std::move(arguments)); } - std::experimental::optional visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &) + std::optional visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &) { throw TranslationException(term.location, "“pool” terms currently unsupported"); - return std::experimental::nullopt; + return std::nullopt; } }; diff --git a/src/anthem/ASTUtils.cpp b/src/anthem/ASTUtils.cpp index 34ab31a..db98911 100644 --- a/src/anthem/ASTUtils.cpp +++ b/src/anthem/ASTUtils.cpp @@ -27,7 +27,7 @@ void VariableStack::pop() //////////////////////////////////////////////////////////////////////////////////////////////////// -std::experimental::optional VariableStack::findUserVariableDeclaration(const char *variableName) const +std::optional VariableStack::findUserVariableDeclaration(const char *variableName) const { const auto variableDeclarationMatches = [&variableName](const auto &variableDeclaration) @@ -45,7 +45,7 @@ std::experimental::optional VariableStack::findUserVariab return matchingVariableDeclaration->get(); } - return std::experimental::nullopt; + return std::nullopt; } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index b6a4250..8ec309b 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -1,6 +1,6 @@ #include -#include +#include #include #include @@ -27,15 +27,15 @@ bool matchesVariableDeclaration(const ast::Term &term, const ast::VariableDeclar // Extracts the term t if the given formula is of the form “X = t” and X matches the given variable // The input formula is no longer usable after this call if a term is returned -std::experimental::optional extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration &variableDeclaration) +std::optional extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration &variableDeclaration) { if (!formula.is()) - return std::experimental::nullopt; + return std::nullopt; auto &comparison = formula.get(); if (comparison.operator_ != ast::Comparison::Operator::Equal) - return std::experimental::nullopt; + return std::nullopt; if (matchesVariableDeclaration(comparison.left, variableDeclaration)) return std::move(comparison.right); @@ -43,7 +43,7 @@ std::experimental::optional extractAssignedTerm(ast::Formula &formula if (matchesVariableDeclaration(comparison.right, variableDeclaration)) return std::move(comparison.left); - return std::experimental::nullopt; + return std::nullopt; } ////////////////////////////////////////////////////////////////////////////////////////////////////