From 6e3e3878acc44fc2d6018f264b5b9ecf96f93d0c Mon Sep 17 00:00:00 2001 From: Ernesto Casablanca Date: Wed, 16 Oct 2024 19:11:02 +0100 Subject: [PATCH] ref: introduce templated formula and expression visitors --- dlinear/parser/smt2/Driver.cpp | 4 +- dlinear/parser/smt2/Sort.h | 48 ++--- dlinear/parser/vnnlib/Driver.cpp | 4 +- dlinear/solver/ContextImpl.cpp | 6 +- dlinear/solver/SatSolver.cpp | 6 +- dlinear/symbolic/BUILD.bazel | 27 ++- dlinear/symbolic/ExpressionEvaluator.cpp | 27 +-- dlinear/symbolic/ExpressionEvaluator.h | 69 +++---- dlinear/symbolic/FormulaVisitor.cpp | 44 ----- dlinear/symbolic/FormulaVisitor.h | 44 ++--- dlinear/symbolic/GenericExpressionVisitor.h | 125 +++++++++++++ dlinear/symbolic/GenericFormulaVisitor.h | 97 ++++++++++ dlinear/symbolic/IfThenElseEliminator.cpp | 173 +++++++++--------- dlinear/symbolic/IfThenElseEliminator.h | 117 ++++++------ dlinear/symbolic/NaiveCnfizer.cpp | 25 +-- dlinear/symbolic/NaiveCnfizer.h | 17 +- dlinear/symbolic/Nnfizer.cpp | 19 +- dlinear/symbolic/Nnfizer.h | 53 +++--- dlinear/symbolic/PlaistedGreenbaumCnfizer.cpp | 49 ++--- dlinear/symbolic/PlaistedGreenbaumCnfizer.h | 31 ++-- dlinear/symbolic/PredicateAbstractor.cpp | 40 ++-- dlinear/symbolic/PredicateAbstractor.h | 46 ++--- dlinear/symbolic/PrefixPrinter.cpp | 98 +++++----- dlinear/symbolic/PrefixPrinter.h | 110 ++++++----- dlinear/symbolic/TseitinCnfizer.cpp | 42 +++-- dlinear/symbolic/TseitinCnfizer.h | 26 +-- test/solver/TestBoundPreprocessor.cpp | 4 +- test/symbolic/TestNnfizer.cpp | 38 ++-- .../symbolic/TestPlaistedGreenbaumCnfizer.cpp | 2 +- test/symbolic/TestPredicateAbstractor.cpp | 26 +-- test/symbolic/TestTseitinCnfizer.cpp | 2 +- 31 files changed, 810 insertions(+), 609 deletions(-) delete mode 100644 dlinear/symbolic/FormulaVisitor.cpp create mode 100644 dlinear/symbolic/GenericExpressionVisitor.h create mode 100644 dlinear/symbolic/GenericFormulaVisitor.h diff --git a/dlinear/parser/smt2/Driver.cpp b/dlinear/parser/smt2/Driver.cpp index 7f4be9a..0eee59a 100644 --- a/dlinear/parser/smt2/Driver.cpp +++ b/dlinear/parser/smt2/Driver.cpp @@ -91,10 +91,10 @@ void Smt2Driver::GetValue(const std::vector &term_list) const { switch (term.type()) { case Term::Type::EXPRESSION: { const Expression &e{term.expression()}; - const ExpressionEvaluator evaluator{e}; + const ExpressionEvaluator evaluator{e, context_.config()}; pp.Print(e); term_str = ss.str(); - const Interval iv{ExpressionEvaluator(term.expression())(box)}; + const Interval iv{ExpressionEvaluator(term.expression(), context_.config())(box)}; value_str = (std::stringstream{} << iv).str(); break; } diff --git a/dlinear/parser/smt2/Sort.h b/dlinear/parser/smt2/Sort.h index 9289857..ad3469d 100644 --- a/dlinear/parser/smt2/Sort.h +++ b/dlinear/parser/smt2/Sort.h @@ -1,9 +1,9 @@ /** -* @author Ernesto Casablanca (casablancaernesto@gmail.com) -* @copyright 2024 dlinear -* @licence BSD 3-Clause License -* Sort enum. -*/ + * @author Ernesto Casablanca (casablancaernesto@gmail.com) + * @copyright 2024 dlinear + * @licence BSD 3-Clause License + * Sort enum. + */ #pragma once #include @@ -15,34 +15,34 @@ namespace dlinear::smt2 { /** Sort of a term. */ enum class Sort { - Binary, ///< Binary sort. - Bool, ///< Boolean sort. - Int, ///< Integer sort. - Real, ///< Real sort. + Binary, ///< Binary sort. + Bool, ///< Boolean sort. + Int, ///< Integer sort. + Real, ///< Real sort. }; /** -* Parse a string to a sort. -* @param s string to parse -* @return sort parsed from @p s -*/ + * Parse a string to a sort. + * @param s string to parse + * @return sort parsed from @p s + */ Sort ParseSort(const std::string &s); /** -* Convert a sort to a variable type. -* -* The conversion is as follows: -* - Binary -> BINARY -* - Bool -> BOOLEAN -* - Int -> INTEGER -* - Real -> CONTINUOUS -* @param sort sort to convert -* @return variable type corresponding to @p sort -*/ + * Convert a sort to a variable type. + * + * The conversion is as follows: + * - Binary -> BINARY + * - Bool -> BOOLEAN + * - Int -> INTEGER + * - Real -> CONTINUOUS + * @param sort sort to convert + * @return variable type corresponding to @p sort + */ Variable::Type SortToType(Sort sort); std::ostream &operator<<(std::ostream &os, const Sort &sort); -} // namespace dlinear::vnnlib +} // namespace dlinear::smt2 #ifdef DLINEAR_INCLUDE_FMT diff --git a/dlinear/parser/vnnlib/Driver.cpp b/dlinear/parser/vnnlib/Driver.cpp index c03c97e..9e565f0 100644 --- a/dlinear/parser/vnnlib/Driver.cpp +++ b/dlinear/parser/vnnlib/Driver.cpp @@ -95,10 +95,10 @@ void VnnlibDriver::GetValue(const std::vector &term_list) const { switch (term.type()) { case Term::Type::EXPRESSION: { const Expression &e{term.expression()}; - const ExpressionEvaluator evaluator{e}; + const ExpressionEvaluator evaluator{e, context_.config()}; pp.Print(e); term_str = ss.str(); - const Interval iv{ExpressionEvaluator(term.expression())(box)}; + const Interval iv{ExpressionEvaluator(term.expression(), context_.config())(box)}; value_str = (std::stringstream{} << iv).str(); break; } diff --git a/dlinear/solver/ContextImpl.cpp b/dlinear/solver/ContextImpl.cpp index 9dc84cf..baca7a8 100644 --- a/dlinear/solver/ContextImpl.cpp +++ b/dlinear/solver/ContextImpl.cpp @@ -89,9 +89,9 @@ void Context::Impl::AssertPiecewiseLinearFunction(const Variable &var, const For DLINEAR_ASSERT(!var.is_dummy() && var.get_type() == Variable::Type::CONTINUOUS, "Variable must be a real variable"); DLINEAR_ASSERT(is_relational(cond), "Condition must be a relational formula"); - const Formula condition_lit = predicate_abstractor_.Convert(cond); - const Formula active_lit = predicate_abstractor_.Convert(var - active == 0); - const Formula inactive_lit = predicate_abstractor_.Convert(var - inactive == 0); + const Formula condition_lit = predicate_abstractor_(cond); + const Formula active_lit = predicate_abstractor_(var - active == 0); + const Formula inactive_lit = predicate_abstractor_(var - inactive == 0); // Make sure the cond is assigned a value (true or false) in the SAT solver const Formula force_assignment(condition_lit || !condition_lit); const Formula active_assertion{active_lit || !condition_lit}; diff --git a/dlinear/solver/SatSolver.cpp b/dlinear/solver/SatSolver.cpp index 12bfd59..1306fb4 100644 --- a/dlinear/solver/SatSolver.cpp +++ b/dlinear/solver/SatSolver.cpp @@ -41,13 +41,13 @@ std::vector> SatSolver::clauses() const { void SatSolver::AddFormula(const Formula &f) { DLINEAR_DEBUG_FMT("SatSolver::AddFormula({})", f); - std::vector clauses{cnfizer_.Convert(f)}; + auto [clauses, aux] = cnfizer_(f); // Collect CNF variables and store them in `cnf_variables_`. - for (const Variable &p : cnfizer_.vars()) cnf_variables_.insert(p.get_id()); + for (const Variable &p : aux) cnf_variables_.insert(p.get_id()); // Convert a first-order clauses into a Boolean formula by predicate abstraction // The original can be retrieved by `predicate_abstractor_[abstracted_formula]`. - for (Formula &clause : clauses) clause = predicate_abstractor_.Convert(clause); + for (Formula &clause : clauses) clause = predicate_abstractor_.Process(clause); AddClauses(clauses); } diff --git a/dlinear/symbolic/BUILD.bazel b/dlinear/symbolic/BUILD.bazel index 5edfcc1..2a2aec3 100644 --- a/dlinear/symbolic/BUILD.bazel +++ b/dlinear/symbolic/BUILD.bazel @@ -24,7 +24,11 @@ dlinear_cc_library( ":literal", "//dlinear/libs:gmp", ], - deps = [":symbolic"], + deps = [ + ":expression_visitor", + ":formula_visitor", + ":symbolic", + ], ) dlinear_cc_library( @@ -44,9 +48,20 @@ dlinear_cc_library( dlinear_cc_library( name = "formula_visitor", - srcs = ["FormulaVisitor.cpp"], - hdrs = ["FormulaVisitor.h"], - implementation_deps = ["//dlinear/util:exception"], + hdrs = [ + "FormulaVisitor.h", + "GenericFormulaVisitor.h", + ], + deps = [ + ":symbolic", + "//dlinear/util:config", + "//dlinear/util:stats", + ], +) + +dlinear_cc_library( + name = "expression_visitor", + hdrs = ["GenericExpressionVisitor.h"], deps = [ ":symbolic", "//dlinear/util:config", @@ -94,6 +109,7 @@ dlinear_cc_library( "//dlinear/util:exception", ], deps = [ + ":expression_visitor", ":symbolic", "//dlinear/util:box", ], @@ -105,6 +121,7 @@ dlinear_cc_library( hdrs = ["Nnfizer.h"], implementation_deps = ["//dlinear/util:logging"], deps = [ + ":formula_visitor", ":symbolic", "//dlinear/util:config", ], @@ -132,6 +149,8 @@ dlinear_cc_library( "//dlinear/util:timer", ], deps = [ + ":expression_visitor", + ":formula_visitor", ":literal", ":symbolic", "//dlinear/util:config", diff --git a/dlinear/symbolic/ExpressionEvaluator.cpp b/dlinear/symbolic/ExpressionEvaluator.cpp index 93974c2..6551c54 100644 --- a/dlinear/symbolic/ExpressionEvaluator.cpp +++ b/dlinear/symbolic/ExpressionEvaluator.cpp @@ -16,22 +16,26 @@ namespace dlinear { -ExpressionEvaluator::ExpressionEvaluator(Expression e) : e_{std::move(e)} {} +ExpressionEvaluator::ExpressionEvaluator(Expression e, const Config& config) + : GenericExpressionVisitor{config, "ExpressionEvaluator"}, e_{std::move(e)} {} -Interval ExpressionEvaluator::operator()(const Box& box) const { return Visit(e_, box); } - -Interval ExpressionEvaluator::Visit(const Expression& e, const Box& box) const { - return VisitExpression(this, e, box); +Interval ExpressionEvaluator::Process(const Box& box) const { + const TimerGuard timer_guard(&stats_.m_timer(), stats_.enabled()); + stats_.Increase(); + return VisitExpression(e_, box); } +Interval ExpressionEvaluator::operator()(const Box& box) const { return Process(box); } -Interval ExpressionEvaluator::VisitVariable(const Expression& e, const Box& box) { +Interval ExpressionEvaluator::VisitVariable(const Expression& e, const Box& box) const { const Variable& var{get_variable(e)}; return box[var]; } -Interval ExpressionEvaluator::VisitConstant(const Expression& e, const Box&) { return Interval{get_constant_value(e)}; } +Interval ExpressionEvaluator::VisitConstant(const Expression& e, const Box&) const { + return Interval{get_constant_value(e)}; +} -Interval ExpressionEvaluator::VisitRealConstant(const Expression&, const Box&) { +Interval ExpressionEvaluator::VisitRealConstant(const Expression&, const Box&) const { DLINEAR_RUNTIME_ERROR("Operation is not supported yet."); } @@ -40,7 +44,7 @@ Interval ExpressionEvaluator::VisitAddition(const Expression& e, const Box& box) const auto& expr_to_coeff_map = get_expr_to_coeff_map_in_addition(e); return std::accumulate(expr_to_coeff_map.begin(), expr_to_coeff_map.end(), Interval{c}, [this, &box](const Interval& init, const std::pair& p) { - return init + Visit(p.first, box) * p.second; + return init + VisitExpression(p.first, box) * p.second; }); } @@ -148,11 +152,12 @@ Interval ExpressionEvaluator::VisitMax(const Expression&, const Box&) const { DLINEAR_RUNTIME_ERROR("Operation is not supported yet."); } -Interval ExpressionEvaluator::VisitIfThenElse(const Expression& /* unused */, const Box& /* unused */) { +Interval ExpressionEvaluator::VisitIfThenElse(const Expression& /* unused */, const Box& /* unused */) const { DLINEAR_RUNTIME_ERROR("If-then-else expression is not supported yet."); } -Interval ExpressionEvaluator::VisitUninterpretedFunction(const Expression& /* unused */, const Box& /* unused */) { +Interval ExpressionEvaluator::VisitUninterpretedFunction(const Expression& /* unused */, + const Box& /* unused */) const { DLINEAR_RUNTIME_ERROR("Uninterpreted function is not supported."); } diff --git a/dlinear/symbolic/ExpressionEvaluator.h b/dlinear/symbolic/ExpressionEvaluator.h index 3a3f098..a91a648 100644 --- a/dlinear/symbolic/ExpressionEvaluator.h +++ b/dlinear/symbolic/ExpressionEvaluator.h @@ -8,6 +8,7 @@ #include +#include "dlinear/symbolic/GenericExpressionVisitor.h" #include "dlinear/symbolic/symbolic.h" #include "dlinear/util/Box.h" #include "dlinear/util/Interval.h" @@ -20,51 +21,51 @@ namespace dlinear { * The ExpressionEvaluator is used to evaluate an expression with a given box. * The box provides the values of the variables in the expression with intervals. */ -class ExpressionEvaluator { +class ExpressionEvaluator : public GenericExpressionVisitor { public: - explicit ExpressionEvaluator(Expression e); + /** + * Construct a new ExpressionEvaluator object with the given expression and configuration. + * @param e expression to evaluate + * @param config configuration to use + */ + ExpressionEvaluator(Expression e, const Config& config); /// Evaluates the expression with @p box. - Interval operator()(const Box& box) const; + [[nodiscard]] Interval Process(const Box& box) const; + [[nodiscard]] Interval operator()(const Box& box) const; [[nodiscard]] const Variables& variables() const { return e_.GetVariables(); } - [[nodiscard]] const Expression& expression() const { return e_; } private: - [[nodiscard]] Interval Visit(const Expression& e, const Box& box) const; - static Interval VisitVariable(const Expression& e, const Box& box); - static Interval VisitConstant(const Expression& e, const Box& box); - static Interval VisitRealConstant(const Expression& e, const Box& box); - [[nodiscard]] Interval VisitAddition(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitMultiplication(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitDivision(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitLog(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitAbs(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitExp(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitSqrt(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitPow(const Expression& e, const Box& box) const; + [[nodiscard]] Interval VisitVariable(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitConstant(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitRealConstant(const Expression& e, const Box& box) const; + [[nodiscard]] Interval VisitAddition(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitMultiplication(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitDivision(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitLog(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitAbs(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitExp(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitSqrt(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitPow(const Expression& e, const Box& box) const override; // Evaluates `pow(e1, e2)` with the @p box. [[nodiscard]] Interval VisitPow(const Expression& e1, const Expression& e2, const Box& box) const; - [[nodiscard]] Interval VisitSin(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitCos(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitTan(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitAsin(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitAcos(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitAtan(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitAtan2(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitSinh(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitCosh(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitTanh(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitMin(const Expression& e, const Box& box) const; - [[nodiscard]] Interval VisitMax(const Expression& e, const Box& box) const; - static Interval VisitIfThenElse(const Expression& e, const Box& box); - static Interval VisitUninterpretedFunction(const Expression& e, const Box& box); - - // Makes VisitExpression a friend of this class so that it can use private - // operator()s. - friend Interval drake::symbolic::VisitExpression(const ExpressionEvaluator*, const Expression&, const Box&); + [[nodiscard]] Interval VisitSin(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitCos(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitTan(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitAsin(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitAcos(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitAtan(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitAtan2(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitSinh(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitCosh(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitTanh(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitMin(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitMax(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitIfThenElse(const Expression& e, const Box& box) const override; + [[nodiscard]] Interval VisitUninterpretedFunction(const Expression& e, const Box& box) const override; const Expression e_; }; diff --git a/dlinear/symbolic/FormulaVisitor.cpp b/dlinear/symbolic/FormulaVisitor.cpp deleted file mode 100644 index 4dad5ac..0000000 --- a/dlinear/symbolic/FormulaVisitor.cpp +++ /dev/null @@ -1,44 +0,0 @@ -/** - * @author Ernesto Casablanca (casablancaernesto@gmail.com) - * @copyright 2024 dlinear - * @licence BSD 3-Clause License - */ -#include "FormulaVisitor.h" - -#include "dlinear/util/exception.h" - -namespace dlinear { - -Formula FormulaVisitor::Visit(const Formula &f) { - switch (f.get_kind()) { - case FormulaKind::False: - return VisitFalse(f); - case FormulaKind::True: - return VisitTrue(f); - case FormulaKind::Var: - return VisitVariable(f); - case FormulaKind::Eq: - return VisitEqualTo(f); - case FormulaKind::Neq: - return VisitNotEqualTo(f); - case FormulaKind::Gt: - return VisitGreaterThan(f); - case FormulaKind::Geq: - return VisitGreaterThanOrEqualTo(f); - case FormulaKind::Lt: - return VisitLessThan(f); - case FormulaKind::Leq: - return VisitLessThanOrEqualTo(f); - case FormulaKind::And: - return VisitConjunction(f); - case FormulaKind::Or: - return VisitDisjunction(f); - case FormulaKind::Not: - return VisitNegation(f); - case FormulaKind::Forall: - return VisitForall(f); - } - DLINEAR_UNREACHABLE(); -} - -} // namespace dlinear diff --git a/dlinear/symbolic/FormulaVisitor.h b/dlinear/symbolic/FormulaVisitor.h index de64286..067e3fe 100644 --- a/dlinear/symbolic/FormulaVisitor.h +++ b/dlinear/symbolic/FormulaVisitor.h @@ -13,22 +13,20 @@ #include +#include "dlinear/symbolic/GenericFormulaVisitor.h" #include "dlinear/symbolic/symbolic.h" #include "dlinear/util/Config.h" #include "dlinear/util/Stats.h" namespace dlinear { + /** * This base class provides all the methods expected to visit the underlying formula and return a modified version. + * * By default, the visitor returns the original formula, but it can be overridden by the derived classes. */ -class FormulaVisitor { - public: - /** @getter{statistics, FormulaVisitor} */ - [[nodiscard]] const IterationStats &stats() const { return stats_; } - /** @getter{configuration, FormulaVisitor} */ - [[nodiscard]] const Config &config() const { return config_; } - +template +class FormulaVisitor : public GenericFormulaVisitor { protected: /** * Construct a new FormulaVisitor object with the given @p config. @@ -36,25 +34,21 @@ class FormulaVisitor { * @param class_name name of the subclass */ explicit FormulaVisitor(const Config &config, const std::string &class_name = "FormulaVisitor") - : config_{config}, stats_{config.with_timings(), class_name, "Converting"} {} - virtual ~FormulaVisitor() = default; - [[nodiscard]] virtual Formula Visit(const Formula &f); - [[nodiscard]] virtual Formula VisitFalse(const Formula &f) { return f; } - [[nodiscard]] virtual Formula VisitTrue(const Formula &f) { return f; } - [[nodiscard]] virtual Formula VisitVariable(const Formula &f) { return f; } - [[nodiscard]] virtual Formula VisitEqualTo(const Formula &f) { return f; } - [[nodiscard]] virtual Formula VisitNotEqualTo(const Formula &f) { return f; } - [[nodiscard]] virtual Formula VisitGreaterThan(const Formula &f) { return f; } - [[nodiscard]] virtual Formula VisitGreaterThanOrEqualTo(const Formula &f) { return f; } - [[nodiscard]] virtual Formula VisitLessThan(const Formula &f) { return f; } - [[nodiscard]] virtual Formula VisitLessThanOrEqualTo(const Formula &f) { return f; } - [[nodiscard]] virtual Formula VisitConjunction(const Formula &f) { return f; } - [[nodiscard]] virtual Formula VisitDisjunction(const Formula &f) { return f; } - [[nodiscard]] virtual Formula VisitNegation(const Formula &f) { return f; } - [[nodiscard]] virtual Formula VisitForall(const Formula &f) { return f; } + : GenericFormulaVisitor{config, class_name} {} - const Config &config_; ///< Configuration. - IterationStats stats_; ///< Statistics. + [[nodiscard]] Formula VisitFalse(const Formula &f, Args...) const override { return f; } + [[nodiscard]] Formula VisitTrue(const Formula &f, Args...) const override { return f; } + [[nodiscard]] Formula VisitVariable(const Formula &f, Args...) const override { return f; } + [[nodiscard]] Formula VisitEqualTo(const Formula &f, Args...) const override { return f; } + [[nodiscard]] Formula VisitNotEqualTo(const Formula &f, Args...) const override { return f; } + [[nodiscard]] Formula VisitGreaterThan(const Formula &f, Args...) const override { return f; } + [[nodiscard]] Formula VisitGreaterThanOrEqualTo(const Formula &f, Args...) const override { return f; } + [[nodiscard]] Formula VisitLessThan(const Formula &f, Args...) const override { return f; } + [[nodiscard]] Formula VisitLessThanOrEqualTo(const Formula &f, Args...) const override { return f; } + [[nodiscard]] Formula VisitConjunction(const Formula &f, Args...) const override { return f; } + [[nodiscard]] Formula VisitDisjunction(const Formula &f, Args...) const override { return f; } + [[nodiscard]] Formula VisitNegation(const Formula &f, Args...) const override { return f; } + [[nodiscard]] Formula VisitForall(const Formula &f, Args...) const override { return f; } }; } // namespace dlinear diff --git a/dlinear/symbolic/GenericExpressionVisitor.h b/dlinear/symbolic/GenericExpressionVisitor.h new file mode 100644 index 0000000..2bc3007 --- /dev/null +++ b/dlinear/symbolic/GenericExpressionVisitor.h @@ -0,0 +1,125 @@ +/** +* @author Ernesto Casablanca (casablancaernesto@gmail.com) +* @copyright 2024 dlinear +* @licence BSD 3-Clause License +* GenericExpressionVisitor class. +*/ +#pragma once + +#include + +#include "dlinear/symbolic/symbolic.h" +#include "dlinear/util/Config.h" +#include "dlinear/util/Stats.h" + +namespace dlinear { + +/** + * Generic expression visitor implementing the visitor pattern. + * + * It will iterate over the expression tree and call the appropriate method for each node. + * @tparam Result return type of each visit method + * @tparam Args additional arguments to pass to each visit method + */ +template +class GenericExpressionVisitor { + public: + /** @getter{statistics, GenericExpressionVisitor} */ + [[nodiscard]] const IterationStats &stats() const { return stats_; } + /** @getter{configuration, GenericExpressionVisitor} */ + [[nodiscard]] const Config &config() const { return config_; } + + protected: + explicit GenericExpressionVisitor(const Config &config, const std::string &class_name = "GenericExpressionVisitor") + : config_{config}, stats_{config.with_timings(), class_name, "Converting"} {} + virtual ~GenericExpressionVisitor() = default; + + [[nodiscard]] virtual Result VisitExpression(const Expression &e, Args... args) const { + switch (e.get_kind()) { + case ExpressionKind::Constant: + return VisitConstant(e, std::forward(args)...); + case ExpressionKind::Var: + return VisitVariable(e, std::forward(args)...); + case ExpressionKind::Add: + return VisitAddition(e, std::forward(args)...); + case ExpressionKind::Mul: + return VisitMultiplication(e, std::forward(args)...); + case ExpressionKind::Div: + return VisitDivision(e, std::forward(args)...); + case ExpressionKind::Log: + return VisitLog(e, std::forward(args)...); + case ExpressionKind::Abs: + return VisitAbs(e, std::forward(args)...); + case ExpressionKind::Exp: + return VisitExp(e, std::forward(args)...); + case ExpressionKind::Sqrt: + return VisitSqrt(e, std::forward(args)...); + case ExpressionKind::Pow: + return VisitPow(e, std::forward(args)...); + case ExpressionKind::Sin: + return VisitSin(e, std::forward(args)...); + case ExpressionKind::Cos: + return VisitCos(e, std::forward(args)...); + case ExpressionKind::Tan: + return VisitTan(e, std::forward(args)...); + case ExpressionKind::Asin: + return VisitAsin(e, std::forward(args)...); + case ExpressionKind::Acos: + return VisitAcos(e, std::forward(args)...); + case ExpressionKind::Atan: + return VisitAtan(e, std::forward(args)...); + case ExpressionKind::Atan2: + return VisitAtan2(e, std::forward(args)...); + case ExpressionKind::Sinh: + return VisitSinh(e, std::forward(args)...); + case ExpressionKind::Cosh: + return VisitCosh(e, std::forward(args)...); + case ExpressionKind::Tanh: + return VisitTanh(e, std::forward(args)...); + case ExpressionKind::Min: + return VisitMin(e, std::forward(args)...); + case ExpressionKind::Max: + return VisitMax(e, std::forward(args)...); + case ExpressionKind::IfThenElse: + return VisitIfThenElse(e, std::forward(args)...); + case ExpressionKind::Infty: + throw std::runtime_error("An infinity is detected while visiting an expression."); + case ExpressionKind::NaN: + throw std::runtime_error("NaN is detected while visiting an expression."); + case ExpressionKind::UninterpretedFunction: + return VisitUninterpretedFunction(e, std::forward(args)...); + default: + throw std::runtime_error("Unreachable code."); + } + } + + virtual Result VisitVariable(const Expression &e, Args... args) const = 0; + virtual Result VisitConstant(const Expression &e, Args... args) const = 0; + virtual Result VisitAddition(const Expression &e, Args... args) const = 0; + virtual Result VisitMultiplication(const Expression &e, Args... args) const = 0; + virtual Result VisitDivision(const Expression &e, Args... args) const = 0; + virtual Result VisitLog(const Expression &e, Args... args) const = 0; + virtual Result VisitAbs(const Expression &e, Args... args) const = 0; + virtual Result VisitExp(const Expression &e, Args... args) const = 0; + virtual Result VisitSqrt(const Expression &e, Args... args) const = 0; + virtual Result VisitPow(const Expression &e, Args... args) const = 0; + virtual Result VisitSin(const Expression &e, Args... args) const = 0; + virtual Result VisitCos(const Expression &e, Args... args) const = 0; + virtual Result VisitTan(const Expression &e, Args... args) const = 0; + virtual Result VisitAsin(const Expression &e, Args... args) const = 0; + virtual Result VisitAcos(const Expression &e, Args... args) const = 0; + virtual Result VisitAtan(const Expression &e, Args... args) const = 0; + virtual Result VisitAtan2(const Expression &e, Args... args) const = 0; + virtual Result VisitSinh(const Expression &e, Args... args) const = 0; + virtual Result VisitCosh(const Expression &e, Args... args) const = 0; + virtual Result VisitTanh(const Expression &e, Args... args) const = 0; + virtual Result VisitMin(const Expression &e, Args... args) const = 0; + virtual Result VisitMax(const Expression &e, Args... args) const = 0; + virtual Result VisitIfThenElse(const Expression &e, Args... args) const = 0; + virtual Result VisitUninterpretedFunction(const Expression &e, Args... args) const = 0; + + const Config &config_; ///< Configuration + mutable IterationStats stats_; ///< Statistics +}; + +} // namespace dlinear diff --git a/dlinear/symbolic/GenericFormulaVisitor.h b/dlinear/symbolic/GenericFormulaVisitor.h new file mode 100644 index 0000000..a0ca6bd --- /dev/null +++ b/dlinear/symbolic/GenericFormulaVisitor.h @@ -0,0 +1,97 @@ +/** + * @author Ernesto Casablanca (casablancaernesto@gmail.com) + * @copyright 2024 dlinear + * @licence BSD 3-Clause License + * Base class for visitors of symbolic formulas. + * + * The class provides all the methods expected to visit the underlying + * formula and return a modified version. + * By default, the visitor returns the original formula, but it can be + * overridden by the derived classes. + */ +#pragma once + +#include + +#include "dlinear/symbolic/symbolic.h" +#include "dlinear/util/Config.h" +#include "dlinear/util/Stats.h" + +namespace dlinear { + +/** + * Generic formula visitor implementing the visitor pattern. + * + * It will iterate over the formula tree and call the appropriate method for each node. + * @tparam Result return type of each visit method + * @tparam Args additional arguments to pass to each visit method + */ +template +class GenericFormulaVisitor { + public: + /** @getter{statistics, FormulaVisitor} */ + [[nodiscard]] const IterationStats &stats() const { return stats_; } + /** @getter{configuration, FormulaVisitor} */ + [[nodiscard]] const Config &config() const { return config_; } + + protected: + /** + * Construct a new FormulaVisitor object with the given @p config. + * @param config configuration + * @param class_name name of the subclass + */ + explicit GenericFormulaVisitor(const Config &config, const std::string &class_name = "GenericFormulaVisitor") + : config_{config}, stats_{config.with_timings(), class_name, "Converting"} {} + virtual ~GenericFormulaVisitor() = default; + + [[nodiscard]] virtual Result VisitFormula(const Formula &f, Args... args) const { + switch (f.get_kind()) { + case FormulaKind::False: + return VisitFalse(f, args...); + case FormulaKind::True: + return VisitTrue(f, args...); + case FormulaKind::Var: + return VisitVariable(f, args...); + case FormulaKind::Eq: + return VisitEqualTo(f, args...); + case FormulaKind::Neq: + return VisitNotEqualTo(f, args...); + case FormulaKind::Gt: + return VisitGreaterThan(f, args...); + case FormulaKind::Geq: + return VisitGreaterThanOrEqualTo(f, args...); + case FormulaKind::Lt: + return VisitLessThan(f, args...); + case FormulaKind::Leq: + return VisitLessThanOrEqualTo(f, args...); + case FormulaKind::And: + return VisitConjunction(f, args...); + case FormulaKind::Or: + return VisitDisjunction(f, args...); + case FormulaKind::Not: + return VisitNegation(f, args...); + case FormulaKind::Forall: + return VisitForall(f, args...); + default: + throw std::runtime_error("Unknown formula kind"); + } + } + [[nodiscard]] virtual Result VisitFalse(const Formula &f, Args... args) const = 0; + [[nodiscard]] virtual Result VisitTrue(const Formula &f, Args... args) const = 0; + [[nodiscard]] virtual Result VisitVariable(const Formula &f, Args... args) const = 0; + [[nodiscard]] virtual Result VisitEqualTo(const Formula &f, Args... args) const = 0; + [[nodiscard]] virtual Result VisitNotEqualTo(const Formula &f, Args... args) const = 0; + [[nodiscard]] virtual Result VisitGreaterThan(const Formula &f, Args... args) const = 0; + [[nodiscard]] virtual Result VisitGreaterThanOrEqualTo(const Formula &f, Args... args) const = 0; + [[nodiscard]] virtual Result VisitLessThan(const Formula &f, Args... args) const = 0; + [[nodiscard]] virtual Result VisitLessThanOrEqualTo(const Formula &f, Args... args) const = 0; + [[nodiscard]] virtual Result VisitConjunction(const Formula &f, Args... args) const = 0; + [[nodiscard]] virtual Result VisitDisjunction(const Formula &f, Args... args) const = 0; + [[nodiscard]] virtual Result VisitNegation(const Formula &f, Args... args) const = 0; + [[nodiscard]] virtual Result VisitForall(const Formula &f, Args... args) const = 0; + + const Config &config_; ///< Configuration. + mutable IterationStats stats_; ///< Statistics. +}; + +} // namespace dlinear diff --git a/dlinear/symbolic/IfThenElseEliminator.cpp b/dlinear/symbolic/IfThenElseEliminator.cpp index 178e5bc..14937bd 100644 --- a/dlinear/symbolic/IfThenElseEliminator.cpp +++ b/dlinear/symbolic/IfThenElseEliminator.cpp @@ -19,153 +19,150 @@ namespace dlinear { Formula IfThenElseEliminator::Process(const Formula &f) { - TimerGuard timer_guard(&stats_.m_timer(), stats_.enabled()); - stats_.Increase(); + const TimerGuard timer_guard(&FormulaVisitor::stats_.m_timer(), FormulaVisitor::stats_.enabled()); + FormulaVisitor::stats_.Increase(); added_formulas_.clear(); - Formula new_f{Visit(f, Formula::True())}; + const Formula new_f{VisitFormula(f, Formula::True())}; if (f.EqualTo(new_f) && added_formulas_.empty()) return f; return new_f && make_conjunction(added_formulas_); } std::pair IfThenElseEliminator::Process(const Expression &e) { - TimerGuard timer_guard(&stats_.m_timer(), stats_.enabled()); - stats_.Increase(); + const TimerGuard timer_guard(&FormulaVisitor::stats_.m_timer(), FormulaVisitor::stats_.enabled()); + FormulaVisitor::stats_.Increase(); added_formulas_.clear(); - Expression new_e{Visit(e, Formula::True())}; + const Expression new_e{VisitExpression(e, Formula::True())}; if (e.EqualTo(new_e) && added_formulas_.empty()) return {e, {}}; return {new_e, make_conjunction(added_formulas_)}; } -const std::unordered_map &IfThenElseEliminator::variables() const { - return ite_to_var_; -} +const std::unordered_map &IfThenElseEliminator::variables() const { return ite_to_var_; } -Expression IfThenElseEliminator::Visit(const Expression &e, const Formula &guard) { - if (e.include_ite()) return VisitExpression(this, e, guard); - return e; +Expression IfThenElseEliminator::VisitExpression(const Expression &e, const Formula &guard) const { + return e.include_ite() ? GenericExpressionVisitor::VisitExpression(e, guard) : e; } -Expression IfThenElseEliminator::VisitVariable(const Expression &e, const Formula &) { return e; } +Expression IfThenElseEliminator::VisitVariable(const Expression &e, const Formula &) const { return e; } -Expression IfThenElseEliminator::VisitConstant(const Expression &e, const Formula &) { return e; } +Expression IfThenElseEliminator::VisitConstant(const Expression &e, const Formula &) const { return e; } -Expression IfThenElseEliminator::VisitAddition(const Expression &e, const Formula &guard) { +Expression IfThenElseEliminator::VisitAddition(const Expression &e, const Formula &guard) const { // e = c₀ + ∑ᵢ cᵢ * eᵢ Expression ret{get_constant_in_addition(e)}; for (const auto &p : get_expr_to_coeff_map_in_addition(e)) { const Expression &e_i{p.first}; const mpq_class &c_i{p.second}; - ret += c_i * Visit(e_i, guard); + ret += c_i * VisitExpression(e_i, guard); } return ret; } -Expression IfThenElseEliminator::VisitMultiplication(const Expression &e, const Formula &guard) { +Expression IfThenElseEliminator::VisitMultiplication(const Expression &e, const Formula &guard) const { // e = c₀ * ∏ᵢ pow(eᵢ₁, eᵢ₂) Expression ret{get_constant_in_multiplication(e)}; for (const auto &p : get_base_to_exponent_map_in_multiplication(e)) { const Expression &e_i1{p.first}; const Expression &e_i2{p.second}; - ret *= pow(Visit(e_i1, guard), Visit(e_i2, guard)); + ret *= pow(VisitExpression(e_i1, guard), VisitExpression(e_i2, guard)); } return ret; } -Expression IfThenElseEliminator::VisitDivision(const Expression &e, const Formula &guard) { - return Visit(get_first_argument(e), guard) / Visit(get_second_argument(e), guard); +Expression IfThenElseEliminator::VisitDivision(const Expression &e, const Formula &guard) const { + return VisitExpression(get_first_argument(e), guard) / VisitExpression(get_second_argument(e), guard); } -Expression IfThenElseEliminator::VisitLog(const Expression &e, const Formula &guard) { - return log(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitLog(const Expression &e, const Formula &guard) const { + return log(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitAbs(const Expression &e, const Formula &guard) { - return abs(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitAbs(const Expression &e, const Formula &guard) const { + return abs(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitExp(const Expression &e, const Formula &guard) { - return exp(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitExp(const Expression &e, const Formula &guard) const { + return exp(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitSqrt(const Expression &e, const Formula &guard) { - return sqrt(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitSqrt(const Expression &e, const Formula &guard) const { + return sqrt(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitPow(const Expression &e, const Formula &guard) { - return pow(Visit(get_first_argument(e), guard), Visit(get_second_argument(e), guard)); +Expression IfThenElseEliminator::VisitPow(const Expression &e, const Formula &guard) const { + return pow(VisitExpression(get_first_argument(e), guard), VisitExpression(get_second_argument(e), guard)); } -Expression IfThenElseEliminator::VisitSin(const Expression &e, const Formula &guard) { - return sin(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitSin(const Expression &e, const Formula &guard) const { + return sin(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitCos(const Expression &e, const Formula &guard) { - return cos(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitCos(const Expression &e, const Formula &guard) const { + return cos(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitTan(const Expression &e, const Formula &guard) { - return tan(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitTan(const Expression &e, const Formula &guard) const { + return tan(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitAsin(const Expression &e, const Formula &guard) { - return asin(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitAsin(const Expression &e, const Formula &guard) const { + return asin(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitAcos(const Expression &e, const Formula &guard) { - return acos(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitAcos(const Expression &e, const Formula &guard) const { + return acos(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitAtan(const Expression &e, const Formula &guard) { - return atan(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitAtan(const Expression &e, const Formula &guard) const { + return atan(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitAtan2(const Expression &e, const Formula &guard) { - return atan2(Visit(get_first_argument(e), guard), Visit(get_second_argument(e), guard)); +Expression IfThenElseEliminator::VisitAtan2(const Expression &e, const Formula &guard) const { + return atan2(VisitExpression(get_first_argument(e), guard), VisitExpression(get_second_argument(e), guard)); } -Expression IfThenElseEliminator::VisitSinh(const Expression &e, const Formula &guard) { - return sinh(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitSinh(const Expression &e, const Formula &guard) const { + return sinh(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitCosh(const Expression &e, const Formula &guard) { - return cosh(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitCosh(const Expression &e, const Formula &guard) const { + return cosh(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitTanh(const Expression &e, const Formula &guard) { - return tanh(Visit(get_argument(e), guard)); +Expression IfThenElseEliminator::VisitTanh(const Expression &e, const Formula &guard) const { + return tanh(VisitExpression(get_argument(e), guard)); } -Expression IfThenElseEliminator::VisitMin(const Expression &e, const Formula &guard) { - return min(Visit(get_first_argument(e), guard), Visit(get_second_argument(e), guard)); +Expression IfThenElseEliminator::VisitMin(const Expression &e, const Formula &guard) const { + return min(VisitExpression(get_first_argument(e), guard), VisitExpression(get_second_argument(e), guard)); } -Expression IfThenElseEliminator::VisitMax(const Expression &e, const Formula &guard) { - return max(Visit(get_first_argument(e), guard), Visit(get_second_argument(e), guard)); +Expression IfThenElseEliminator::VisitMax(const Expression &e, const Formula &guard) const { + return max(VisitExpression(get_first_argument(e), guard), VisitExpression(get_second_argument(e), guard)); } -Expression IfThenElseEliminator::VisitIfThenElse(const Expression &e, const Formula &guard) { +Expression IfThenElseEliminator::VisitIfThenElse(const Expression &e, const Formula &guard) const { // Both then and else expressions are the same. const auto it = ite_to_var_.find(e); if (it != ite_to_var_.end()) { added_formulas_.push_back(ite_var_to_formulas_.at(it->second)); return it->second; } - if (get_then_expression(e).EqualTo(get_else_expression(e))) return Visit(get_then_expression(e), guard); + if (get_then_expression(e).EqualTo(get_else_expression(e))) return VisitExpression(get_then_expression(e), guard); - const Formula c{Visit(get_conditional_formula(e), guard)}; + const Formula c{VisitFormula(get_conditional_formula(e), guard)}; // If the guard is the same (or inverted) as the current condition, short-circuit the ITE. - if (c.EqualTo(guard)) return Visit(get_then_expression(e), guard); - if (c.EqualTo(!guard)) return Visit(get_else_expression(e), guard); + if (c.EqualTo(guard)) return VisitExpression(get_then_expression(e), guard); + if (c.EqualTo(!guard)) return VisitExpression(get_else_expression(e), guard); const Variable new_var{"ITE" + std::to_string(counter_++), Variable::Type::CONTINUOUS}; const Formula then_guard{guard && c}; const Formula else_guard{guard && !c}; - const Expression e1{Visit(get_then_expression(e), then_guard)}; - const Expression e2{Visit(get_else_expression(e), else_guard)}; + const Expression e1{VisitExpression(get_then_expression(e), then_guard)}; + const Expression e2{VisitExpression(get_else_expression(e), else_guard)}; added_formulas_.push_back(!then_guard || (new_var == e1)); // then_guard => (new_var = e1) added_formulas_.push_back(!else_guard || (new_var == e2)); // else_guard => (new_var = e2) ite_to_var_.emplace(e, new_var); @@ -173,65 +170,61 @@ Expression IfThenElseEliminator::VisitIfThenElse(const Expression &e, const Form return new_var; } -Expression IfThenElseEliminator::VisitUninterpretedFunction(const Expression &e, const Formula &) { return e; } - -Formula IfThenElseEliminator::Visit(const Formula &f, const Formula &guard) { - return VisitFormula(this, f, guard); -} +Expression IfThenElseEliminator::VisitUninterpretedFunction(const Expression &e, const Formula &) const { return e; } -Formula IfThenElseEliminator::VisitFalse(const Formula &f, const Formula &) { return f; } +Formula IfThenElseEliminator::VisitFalse(const Formula &f, const Formula &) const { return f; } -Formula IfThenElseEliminator::VisitTrue(const Formula &f, const Formula &) { return f; } +Formula IfThenElseEliminator::VisitTrue(const Formula &f, const Formula &) const { return f; } -Formula IfThenElseEliminator::VisitVariable(const Formula &f, const Formula &) { return f; } +Formula IfThenElseEliminator::VisitVariable(const Formula &f, const Formula &) const { return f; } -Formula IfThenElseEliminator::VisitEqualTo(const Formula &f, const Formula &guard) { - return Visit(get_lhs_expression(f), guard) == Visit(get_rhs_expression(f), guard); +Formula IfThenElseEliminator::VisitEqualTo(const Formula &f, const Formula &guard) const { + return VisitExpression(get_lhs_expression(f), guard) == VisitExpression(get_rhs_expression(f), guard); } -Formula IfThenElseEliminator::VisitNotEqualTo(const Formula &f, const Formula &guard) { - return Visit(get_lhs_expression(f), guard) != Visit(get_rhs_expression(f), guard); +Formula IfThenElseEliminator::VisitNotEqualTo(const Formula &f, const Formula &guard) const { + return VisitExpression(get_lhs_expression(f), guard) != VisitExpression(get_rhs_expression(f), guard); } -Formula IfThenElseEliminator::VisitGreaterThan(const Formula &f, const Formula &guard) { - return Visit(get_lhs_expression(f), guard) > Visit(get_rhs_expression(f), guard); +Formula IfThenElseEliminator::VisitGreaterThan(const Formula &f, const Formula &guard) const { + return VisitExpression(get_lhs_expression(f), guard) > VisitExpression(get_rhs_expression(f), guard); } -Formula IfThenElseEliminator::VisitGreaterThanOrEqualTo(const Formula &f, const Formula &guard) { - return Visit(get_lhs_expression(f), guard) >= Visit(get_rhs_expression(f), guard); +Formula IfThenElseEliminator::VisitGreaterThanOrEqualTo(const Formula &f, const Formula &guard) const { + return VisitExpression(get_lhs_expression(f), guard) >= VisitExpression(get_rhs_expression(f), guard); } -Formula IfThenElseEliminator::VisitLessThan(const Formula &f, const Formula &guard) { - return Visit(get_lhs_expression(f), guard) < Visit(get_rhs_expression(f), guard); +Formula IfThenElseEliminator::VisitLessThan(const Formula &f, const Formula &guard) const { + return VisitExpression(get_lhs_expression(f), guard) < VisitExpression(get_rhs_expression(f), guard); } -Formula IfThenElseEliminator::VisitLessThanOrEqualTo(const Formula &f, const Formula &guard) { - return Visit(get_lhs_expression(f), guard) <= Visit(get_rhs_expression(f), guard); +Formula IfThenElseEliminator::VisitLessThanOrEqualTo(const Formula &f, const Formula &guard) const { + return VisitExpression(get_lhs_expression(f), guard) <= VisitExpression(get_rhs_expression(f), guard); } -Formula IfThenElseEliminator::VisitConjunction(const Formula &f, const Formula &guard) { +Formula IfThenElseEliminator::VisitConjunction(const Formula &f, const Formula &guard) const { // f := f₁ ∧ ... ∧ fₙ std::set new_conjuncts; for (const Formula &f_i : get_operands(f)) { - new_conjuncts.emplace(Visit(f_i, guard)); + new_conjuncts.emplace(VisitFormula(f_i, guard)); } return make_conjunction(new_conjuncts); } -Formula IfThenElseEliminator::VisitDisjunction(const Formula &f, const Formula &guard) { +Formula IfThenElseEliminator::VisitDisjunction(const Formula &f, const Formula &guard) const { // f := f₁ ∨ ... ∨ fₙ std::set new_disjuncts; for (const Formula &f_i : get_operands(f)) { - new_disjuncts.emplace(Visit(f_i, guard)); + new_disjuncts.emplace(VisitFormula(f_i, guard)); } return make_disjunction(new_disjuncts); } -Formula IfThenElseEliminator::VisitNegation(const Formula &f, const Formula &guard) { - return !Visit(get_operand(f), guard); +Formula IfThenElseEliminator::VisitNegation(const Formula &f, const Formula &guard) const { + return !VisitFormula(get_operand(f), guard); } -Formula IfThenElseEliminator::VisitForall(const Formula &f, const Formula &) { +Formula IfThenElseEliminator::VisitForall(const Formula &f, const Formula &) const { // ∃x. ∀y. ITE(f, e₁, e₂) > 0 // => ∃x. ¬∃y. ¬(ITE(f, e₁, e₂) > 0) // => ∃x. ¬∃y. ∃v. ¬(v > 0) ∧ (f → (v = e₁)) ∧ (¬f → (v = e₂)) @@ -253,12 +246,12 @@ Formula IfThenElseEliminator::VisitForall(const Formula &f, const Formula &) { // variables). In this way, we can use the existing ITE-elim routine. Variables quantified_variables{get_quantified_variables(f)}; const Formula &quantified_formula{get_quantified_formula(f)}; - IfThenElseEliminator ite_eliminator_forall{config_}; + IfThenElseEliminator ite_eliminator_forall{FormulaVisitor::config_}; const Formula eliminated{ite_eliminator_forall.Process(!quantified_formula)}; for (const auto &[_, v] : ite_eliminator_forall.variables()) { quantified_variables.insert(v); } - return forall(quantified_variables, Nnfizer{config_}.Convert(!eliminated)); + return forall(quantified_variables, Nnfizer{FormulaVisitor::config_}.Process(!eliminated)); } } // namespace dlinear diff --git a/dlinear/symbolic/IfThenElseEliminator.h b/dlinear/symbolic/IfThenElseEliminator.h index 06257fb..35d86bd 100644 --- a/dlinear/symbolic/IfThenElseEliminator.h +++ b/dlinear/symbolic/IfThenElseEliminator.h @@ -9,6 +9,8 @@ #include #include +#include "dlinear/symbolic/FormulaVisitor.h" +#include "dlinear/symbolic/GenericExpressionVisitor.h" #include "dlinear/symbolic/literal.h" #include "dlinear/symbolic/symbolic.h" #include "dlinear/util/Config.h" @@ -22,87 +24,80 @@ namespace dlinear { * @todo Check "Efficient Term ITE Conversion for Satisfiability Modulo Theories", H. Kim, F. Somenzi, H. Jin. Twelfth * International Conference on Theory and Applications of Satisfiability Testing (SAT'09). */ -class IfThenElseEliminator { +class IfThenElseEliminator : public FormulaVisitor, + public GenericExpressionVisitor { public: + using FormulaVisitor::stats; + explicit IfThenElseEliminator(const Config &config) - : counter_{0}, config_{config}, stats_{config.with_timings(), "IfThenElseEliminator", "Process"} {} + : FormulaVisitor{config, "IfThenElseEliminator"}, + GenericExpressionVisitor{config, "IfThenElseEliminator"}, + counter_{0} {} /** * Returns a equisatisfiable formula by eliminating if-then-expressions in @p f by introducing new variables. * @param f Formula to be processed. * @return Processed formula. */ - Formula Process(const Formula &f); - std::pair Process(const Expression &e); - const std::unordered_map &variables() const; - const IterationStats &stats() const { return stats_; } + [[nodiscard]] Formula Process(const Formula &f); + [[nodiscard]] std::pair Process(const Expression &e); + [[nodiscard]] const std::unordered_map &variables() const; private: // Handle expressions. - Expression Visit(const Expression &e, const Formula &guard); - Expression VisitVariable(const Expression &e, const Formula &guard); - Expression VisitConstant(const Expression &e, const Formula &guard); - Expression VisitAddition(const Expression &e, const Formula &guard); - Expression VisitMultiplication(const Expression &e, const Formula &guard); - Expression VisitDivision(const Expression &e, const Formula &guard); - Expression VisitLog(const Expression &e, const Formula &guard); - Expression VisitAbs(const Expression &e, const Formula &guard); - Expression VisitExp(const Expression &e, const Formula &guard); - Expression VisitSqrt(const Expression &e, const Formula &guard); - Expression VisitPow(const Expression &e, const Formula &guard); - Expression VisitSin(const Expression &e, const Formula &guard); - Expression VisitCos(const Expression &e, const Formula &guard); - Expression VisitTan(const Expression &e, const Formula &guard); - Expression VisitAsin(const Expression &e, const Formula &guard); - Expression VisitAcos(const Expression &e, const Formula &guard); - Expression VisitAtan(const Expression &e, const Formula &guard); - Expression VisitAtan2(const Expression &e, const Formula &guard); - Expression VisitSinh(const Expression &e, const Formula &guard); - Expression VisitCosh(const Expression &e, const Formula &guard); - Expression VisitTanh(const Expression &e, const Formula &guard); - Expression VisitMin(const Expression &e, const Formula &guard); - Expression VisitMax(const Expression &e, const Formula &guard); - Expression VisitIfThenElse(const Expression &e, const Formula &guard); - Expression VisitUninterpretedFunction(const Expression &e, const Formula &guard); + Expression VisitExpression(const Expression &e, const Formula &guard) const override; + Expression VisitVariable(const Expression &e, const Formula &guard) const override; + Expression VisitConstant(const Expression &e, const Formula &guard) const override; + Expression VisitAddition(const Expression &e, const Formula &guard) const override; + Expression VisitMultiplication(const Expression &e, const Formula &guard) const override; + Expression VisitDivision(const Expression &e, const Formula &guard) const override; + Expression VisitLog(const Expression &e, const Formula &guard) const override; + Expression VisitAbs(const Expression &e, const Formula &guard) const override; + Expression VisitExp(const Expression &e, const Formula &guard) const override; + Expression VisitSqrt(const Expression &e, const Formula &guard) const override; + Expression VisitPow(const Expression &e, const Formula &guard) const override; + Expression VisitSin(const Expression &e, const Formula &guard) const override; + Expression VisitCos(const Expression &e, const Formula &guard) const override; + Expression VisitTan(const Expression &e, const Formula &guard) const override; + Expression VisitAsin(const Expression &e, const Formula &guard) const override; + Expression VisitAcos(const Expression &e, const Formula &guard) const override; + Expression VisitAtan(const Expression &e, const Formula &guard) const override; + Expression VisitAtan2(const Expression &e, const Formula &guard) const override; + Expression VisitSinh(const Expression &e, const Formula &guard) const override; + Expression VisitCosh(const Expression &e, const Formula &guard) const override; + Expression VisitTanh(const Expression &e, const Formula &guard) const override; + Expression VisitMin(const Expression &e, const Formula &guard) const override; + Expression VisitMax(const Expression &e, const Formula &guard) const override; + Expression VisitIfThenElse(const Expression &e, const Formula &guard) const override; + Expression VisitUninterpretedFunction(const Expression &e, const Formula &guard) const override; // Handle formula - Formula Visit(const Formula &f, const Formula &guard); - Formula VisitFalse(const Formula &f, const Formula &guard); - Formula VisitTrue(const Formula &f, const Formula &guard); - Formula VisitVariable(const Formula &f, const Formula &guard); - Formula VisitEqualTo(const Formula &f, const Formula &guard); - Formula VisitNotEqualTo(const Formula &f, const Formula &guard); - Formula VisitGreaterThan(const Formula &f, const Formula &guard); - Formula VisitGreaterThanOrEqualTo(const Formula &f, const Formula &guard); - Formula VisitLessThan(const Formula &f, const Formula &guard); - Formula VisitLessThanOrEqualTo(const Formula &f, const Formula &guard); - Formula VisitConjunction(const Formula &f, const Formula &guard); - Formula VisitDisjunction(const Formula &f, const Formula &guard); - Formula VisitNegation(const Formula &f, const Formula &guard); - Formula VisitForall(const Formula &f, const Formula &guard); + Formula VisitFalse(const Formula &f, const Formula &guard) const override; + Formula VisitTrue(const Formula &f, const Formula &guard) const override; + Formula VisitVariable(const Formula &f, const Formula &guard) const override; + Formula VisitEqualTo(const Formula &f, const Formula &guard) const override; + Formula VisitNotEqualTo(const Formula &f, const Formula &guard) const override; + Formula VisitGreaterThan(const Formula &f, const Formula &guard) const override; + Formula VisitGreaterThanOrEqualTo(const Formula &f, const Formula &guard) const override; + Formula VisitLessThan(const Formula &f, const Formula &guard) const override; + Formula VisitLessThanOrEqualTo(const Formula &f, const Formula &guard) const override; + Formula VisitConjunction(const Formula &f, const Formula &guard) const override; + Formula VisitDisjunction(const Formula &f, const Formula &guard) const override; + Formula VisitNegation(const Formula &f, const Formula &guard) const override; + Formula VisitForall(const Formula &f, const Formula &guard) const override; // --------------- // Member fields // --------------- - std::vector added_formulas_; ///< The added formulas introduced by the elimination process. Resets after - ///< each call to Process. - std::unordered_set ite_variables_; ///< The variables introduced by the elimination process. - std::unordered_map + mutable std::vector added_formulas_; ///< The added formulas introduced by the elimination process. Resets + ///< after each call to Process. + mutable std::unordered_set ite_variables_; ///< The variables introduced by the elimination process. + mutable std::unordered_map ite_to_var_; ///< Mapping from ITE to the corresponding variable obtained by ITE elimination. - std::unordered_map + mutable std::unordered_map ite_var_to_formulas_; ///< Mapping from ITE to the corresponding variable obtained by ITE elimination. - std::size_t counter_; ///< Counter for the number of introduced variables. - const Config& config_; ///< Configuration of the elimination process. - IterationStats stats_; ///< Statistics of the elimination process. - - // Makes VisitFormula a friend of this class so that it can use private - // operator()s. - friend Formula drake::symbolic::VisitFormula(IfThenElseEliminator *, const Formula &, const Formula &); - // Makes VisitExpression a friend of this class so that it can use private - // operator()s. - friend Expression drake::symbolic::VisitExpression(IfThenElseEliminator *, const Expression &, - const Formula &); + mutable std::size_t counter_; ///< Counter for the number of introduced variables. }; } // namespace dlinear diff --git a/dlinear/symbolic/NaiveCnfizer.cpp b/dlinear/symbolic/NaiveCnfizer.cpp index 2615af9..ccbaefa 100644 --- a/dlinear/symbolic/NaiveCnfizer.cpp +++ b/dlinear/symbolic/NaiveCnfizer.cpp @@ -17,37 +17,40 @@ namespace dlinear { // - It visits each node and introduce a Boolean variable `b` for // each subterm `f`, and keep the relation `b ⇔ f`. // - Then it cnfizes each `b ⇔ f` and make a conjunction of them. -Formula NaiveCnfizer::Convert(const Formula &f) { +Formula NaiveCnfizer::Process(const Formula &f) const { + const TimerGuard timer_guard{&stats_.m_timer(), stats_.enabled()}; + stats_.Increase(); // TODO(soonho): Using cache if needed. - return Visit(nnfizer_.Convert(f, true)); + return VisitFormula(nnfizer_.Process(f, true)); } +Formula NaiveCnfizer::operator()(const Formula &f) const { return Process(f); } -Formula NaiveCnfizer::VisitEqualTo(const Formula &f) { +Formula NaiveCnfizer::VisitEqualTo(const Formula &f) const { const Expression &lhs{get_lhs_expression(f)}; const Expression &rhs{get_rhs_expression(f)}; return (lhs >= rhs) && (lhs <= rhs); } -Formula NaiveCnfizer::VisitNotEqualTo(const Formula &f) { +Formula NaiveCnfizer::VisitNotEqualTo(const Formula &f) const { const Expression &lhs{get_lhs_expression(f)}; const Expression &rhs{get_rhs_expression(f)}; return (lhs > rhs) || (lhs < rhs); } -Formula NaiveCnfizer::VisitForall(const Formula &f) { +Formula NaiveCnfizer::VisitForall(const Formula &f) const { // f = ∀y. φ(x, y). const Variables &quantified_variables{get_quantified_variables(f)}; // y const Formula &quantified_formula{get_quantified_formula(f)}; // φ(x, y) - return forall(quantified_variables, Convert(quantified_formula)); + return forall(quantified_variables, Process(quantified_formula)); } -Formula NaiveCnfizer::VisitConjunction(const Formula &f) { +Formula NaiveCnfizer::VisitConjunction(const Formula &f) const { const std::set transformed_operands{ - map(get_operands(f), [this](const Formula &formula) { return this->Visit(formula); })}; + map(get_operands(f), [this](const Formula &formula) { return this->VisitFormula(formula); })}; return make_conjunction(transformed_operands); } -Formula NaiveCnfizer::VisitDisjunction(const Formula &f) { +Formula NaiveCnfizer::VisitDisjunction(const Formula &f) const { const std::set &transformed_operands{ - map(get_operands(f), [this](const Formula &formula) { return this->Visit(formula); })}; + map(get_operands(f), [this](const Formula &formula) { return this->VisitFormula(formula); })}; return std::accumulate(transformed_operands.begin(), transformed_operands.end(), Formula::False(), [](const Formula &cnf1, const Formula &cnf2) { std::set clauses; @@ -80,7 +83,7 @@ Formula NaiveCnfizer::VisitDisjunction(const Formula &f) { }); } -Formula NaiveCnfizer::VisitNegation(const Formula &f) { +Formula NaiveCnfizer::VisitNegation(const Formula &f) const { DLINEAR_ASSERT(is_atomic(get_operand(f)), "The formula must be atomic"); return f; } diff --git a/dlinear/symbolic/NaiveCnfizer.h b/dlinear/symbolic/NaiveCnfizer.h index 22420fd..b0419a5 100644 --- a/dlinear/symbolic/NaiveCnfizer.h +++ b/dlinear/symbolic/NaiveCnfizer.h @@ -19,7 +19,7 @@ namespace dlinear { * We are using this transformation in TseitinCnfizer * when we process the nested formula in a universally quantified formula. */ -class NaiveCnfizer : public FormulaVisitor { +class NaiveCnfizer : public FormulaVisitor<> { public: /** * Construct a new NaiveCnfizer object with the given @p config. @@ -32,15 +32,16 @@ class NaiveCnfizer : public FormulaVisitor { * @param f formula to be converted * @return cnf converted formula */ - [[nodiscard]] Formula Convert(const Formula &f); + [[nodiscard]] Formula Process(const Formula &f) const; + [[nodiscard]] Formula operator()(const Formula &f) const; private: - [[nodiscard]] Formula VisitEqualTo(const Formula &f) override; - [[nodiscard]] Formula VisitNotEqualTo(const Formula &f) override; - [[nodiscard]] Formula VisitConjunction(const Formula &f) override; - [[nodiscard]] Formula VisitDisjunction(const Formula &f) override; - [[nodiscard]] Formula VisitNegation(const Formula &f) override; - [[nodiscard]] Formula VisitForall(const Formula &f) override; + [[nodiscard]] Formula VisitEqualTo(const Formula &f) const override; + [[nodiscard]] Formula VisitNotEqualTo(const Formula &f) const override; + [[nodiscard]] Formula VisitConjunction(const Formula &f) const override; + [[nodiscard]] Formula VisitDisjunction(const Formula &f) const override; + [[nodiscard]] Formula VisitNegation(const Formula &f) const override; + [[nodiscard]] Formula VisitForall(const Formula &f) const override; Nnfizer nnfizer_{config_}; ///< NNFizer. Used to convert the formula into NNF. }; diff --git a/dlinear/symbolic/Nnfizer.cpp b/dlinear/symbolic/Nnfizer.cpp index 7ee9c52..29e3571 100644 --- a/dlinear/symbolic/Nnfizer.cpp +++ b/dlinear/symbolic/Nnfizer.cpp @@ -12,13 +12,16 @@ namespace dlinear { -Formula Nnfizer::Convert(const Formula &f, const bool push_negation_into_relationals) const { +Nnfizer::Nnfizer(const dlinear::Config &config) : FormulaVisitor{config, "Nnfizer"} {} + +Formula Nnfizer::Process(const Formula &f, bool push_negation_into_relationals) const { DLINEAR_TRACE_FMT("Nnfizer::Convert({}, {})", f, push_negation_into_relationals); - return Visit(f, true, push_negation_into_relationals); + const TimerGuard timer_guard{&stats_.m_timer(), stats_.enabled()}; + stats_.Increase(); + return VisitFormula(f, true, push_negation_into_relationals); } - -Formula Nnfizer::Visit(const Formula &f, const bool polarity, const bool push_negation_into_relationals) const { - return VisitFormula(this, f, polarity, push_negation_into_relationals); +Formula Nnfizer::operator()(const Formula &f, const bool push_negation_into_relationals) const { + return Process(f, push_negation_into_relationals); } Formula Nnfizer::VisitFalse(const Formula &, const bool polarity, const bool) const { @@ -85,7 +88,7 @@ Formula Nnfizer::VisitConjunction(const Formula &f, const bool polarity, // NNF(¬(f₁ ∧ ... ∨ fₙ)) = NNF(¬f₁) ∨ ... ∨ NNF(¬fₙ) const std::set new_operands{ map(get_operands(f), [this, polarity, push_negation_into_relationals](const Formula &formula) { - return this->Visit(formula, polarity, push_negation_into_relationals); + return this->VisitFormula(formula, polarity, push_negation_into_relationals); })}; return polarity ? make_conjunction(new_operands) : make_disjunction(new_operands); } @@ -96,7 +99,7 @@ Formula Nnfizer::VisitDisjunction(const Formula &f, const bool polarity, // NNF(¬(f₁ ∨ ... ∨ fₙ)) = NNF(¬f₁) ∧ ... ∧ NNF(¬fₙ) const std::set new_operands{ map(get_operands(f), [this, polarity, push_negation_into_relationals](const Formula &formula) { - return this->Visit(formula, polarity, push_negation_into_relationals); + return this->VisitFormula(formula, polarity, push_negation_into_relationals); })}; return polarity ? make_disjunction(new_operands) : make_conjunction(new_operands); } @@ -104,7 +107,7 @@ Formula Nnfizer::VisitDisjunction(const Formula &f, const bool polarity, Formula Nnfizer::VisitNegation(const Formula &f, const bool polarity, const bool push_negation_into_relationals) const { // NNF(¬f, ⊤) = NNF(f, ⊥) // NNF(¬f, ⊥) = NNF(f, ⊤) - return Visit(get_operand(f), !polarity, push_negation_into_relationals); + return VisitFormula(get_operand(f), !polarity, push_negation_into_relationals); } Formula Nnfizer::VisitForall(const Formula &f, const bool polarity, const bool) const { diff --git a/dlinear/symbolic/Nnfizer.h b/dlinear/symbolic/Nnfizer.h index 6523af9..e7b838a 100644 --- a/dlinear/symbolic/Nnfizer.h +++ b/dlinear/symbolic/Nnfizer.h @@ -6,6 +6,7 @@ */ #pragma once +#include "dlinear/symbolic/FormulaVisitor.h" #include "dlinear/symbolic/symbolic.h" #include "dlinear/util/Config.h" @@ -17,18 +18,19 @@ namespace dlinear { * When `push_negation_into_relationals` is true, it pushes negations into relational formulas by flipping relational * @par Example: * @f$ ¬(x \ge 10) @f$ becomes @f$ (x < 10) @f$ - * @see [Wikipedia](https://en.wikipedia.org/wiki/Negation_normal_form) + * @see [Wikipedia](https://en.wikipedia.org/wiki/Negation_normal_form). */ -class Nnfizer { +class Nnfizer : public FormulaVisitor { public: - explicit Nnfizer(const Config &config) : config_{config} {} + explicit Nnfizer(const Config &config); /** * Convert a @p f into an equivalent formula @c f' in NNF. * @param f formula to be converted * @param push_negation_into_relationals whether to push negation into relational formulas * @return nnf converted formula */ - [[nodiscard]] Formula Convert(const Formula &f, bool push_negation_into_relationals = false) const; + [[nodiscard]] Formula Process(const Formula &f, bool push_negation_into_relationals = false) const; + [[nodiscard]] Formula operator()(const Formula &f, bool push_negation_into_relationals = false) const; private: /** @@ -39,28 +41,29 @@ class Nnfizer { * @param push_negation_into_relationals whether to push negation into relational formulas * @return nnf converted formula */ - [[nodiscard]] Formula Visit(const Formula &f, bool polarity, bool push_negation_into_relationals) const; - - [[nodiscard]] Formula VisitFalse(const Formula &f, bool polarity, bool push_negation_into_relationals) const; - [[nodiscard]] Formula VisitTrue(const Formula &f, bool polarity, bool push_negation_into_relationals) const; - [[nodiscard]] Formula VisitVariable(const Formula &f, bool polarity, bool push_negation_into_relationals) const; - [[nodiscard]] Formula VisitEqualTo(const Formula &f, bool polarity, bool push_negation_into_relationals) const; - [[nodiscard]] Formula VisitNotEqualTo(const Formula &f, bool polarity, bool push_negation_into_relationals) const; - [[nodiscard]] Formula VisitGreaterThan(const Formula &f, bool polarity, bool push_negation_into_relationals) const; + [[nodiscard]] Formula VisitFalse(const Formula &f, bool polarity, bool push_negation_into_relationals) const override; + [[nodiscard]] Formula VisitTrue(const Formula &f, bool polarity, bool push_negation_into_relationals) const override; + [[nodiscard]] Formula VisitVariable(const Formula &f, bool polarity, + bool push_negation_into_relationals) const override; + [[nodiscard]] Formula VisitEqualTo(const Formula &f, bool polarity, + bool push_negation_into_relationals) const override; + [[nodiscard]] Formula VisitNotEqualTo(const Formula &f, bool polarity, + bool push_negation_into_relationals) const override; + [[nodiscard]] Formula VisitGreaterThan(const Formula &f, bool polarity, + bool push_negation_into_relationals) const override; [[nodiscard]] Formula VisitGreaterThanOrEqualTo(const Formula &f, bool polarity, - bool push_negation_into_relationals) const; - [[nodiscard]] Formula VisitLessThan(const Formula &f, bool polarity, bool push_negation_into_relationals) const; + bool push_negation_into_relationals) const override; + [[nodiscard]] Formula VisitLessThan(const Formula &f, bool polarity, + bool push_negation_into_relationals) const override; [[nodiscard]] Formula VisitLessThanOrEqualTo(const Formula &f, bool polarity, - bool push_negation_into_relationals) const; - [[nodiscard]] Formula VisitConjunction(const Formula &f, bool polarity, bool push_negation_into_relationals) const; - [[nodiscard]] Formula VisitDisjunction(const Formula &f, bool polarity, bool push_negation_into_relationals) const; - [[nodiscard]] Formula VisitNegation(const Formula &f, bool polarity, bool push_negation_into_relationals) const; - [[nodiscard]] Formula VisitForall(const Formula &f, bool polarity, bool push_negation_into_relationals) const; - - const Config &config_; - - // Makes VisitFormula a friend of this class so that it can use private - // methods. - friend Formula drake::symbolic::VisitFormula(const Nnfizer *, const Formula &, const bool &, const bool &); + bool push_negation_into_relationals) const override; + [[nodiscard]] Formula VisitConjunction(const Formula &f, bool polarity, + bool push_negation_into_relationals) const override; + [[nodiscard]] Formula VisitDisjunction(const Formula &f, bool polarity, + bool push_negation_into_relationals) const override; + [[nodiscard]] Formula VisitNegation(const Formula &f, bool polarity, + bool push_negation_into_relationals) const override; + [[nodiscard]] Formula VisitForall(const Formula &f, bool polarity, + bool push_negation_into_relationals) const override; }; } // namespace dlinear diff --git a/dlinear/symbolic/PlaistedGreenbaumCnfizer.cpp b/dlinear/symbolic/PlaistedGreenbaumCnfizer.cpp index 63694fb..2d02bec 100644 --- a/dlinear/symbolic/PlaistedGreenbaumCnfizer.cpp +++ b/dlinear/symbolic/PlaistedGreenbaumCnfizer.cpp @@ -14,23 +14,27 @@ #include "dlinear/util/exception.h" namespace dlinear { -std::vector PlaistedGreenbaumCnfizer::Convert(const Formula &f) { +std::pair, std::vector> PlaistedGreenbaumCnfizer::Process(const Formula &f) const { TimerGuard timer_guard(&stats_.m_timer(), stats_.enabled()); stats_.Increase(); // Put the Formula into negation normal form - const Formula &g{nnfizer_.Convert(f, true /* push_negation_into_relationals */)}; - aux_.clear(); - vars_.clear(); - const Formula head{Visit(g)}; - aux_.push_back(head); - return aux_; + const Formula &g{nnfizer_.Process(f, true /* push_negation_into_relationals */)}; + std::vector aux; + std::vector vars; + const Formula head{VisitFormula(g, aux, vars)}; + aux.push_back(head); + return {aux, vars}; +} +std::pair, std::vector> PlaistedGreenbaumCnfizer::operator()(const Formula &f) const { + return Process(f); } -Formula PlaistedGreenbaumCnfizer::VisitForall(const Formula &f) { +Formula PlaistedGreenbaumCnfizer::VisitForall(const Formula &f, std::vector &aux, + std::vector &vars) const { // We always need a variable static std::size_t id{0}; const Variable bvar{std::string("forall") + std::to_string(id++), Variable::Type::BOOLEAN}; - vars_.push_back(bvar); + vars.push_back(bvar); // Given: f := ∀y. φ(x, y), this process CNFizes φ(x, y), pushes the // universal quantifier over conjunctions, and inserts ¬b: @@ -40,7 +44,7 @@ Formula PlaistedGreenbaumCnfizer::VisitForall(const Formula &f) { const Variables &quantified_variables{get_quantified_variables(f)}; // y const Formula &quantified_formula{get_quantified_formula(f)}; // φ(x, y) // clause₁(x, y) ∧ ... ∧ clauseₙ(x, y) - const std::set clauses{get_clauses(naive_cnfizer_.Convert(quantified_formula))}; + const std::set clauses{get_clauses(naive_cnfizer_.Process(quantified_formula))}; for (const Formula &clause : clauses) { std::set new_clause_set{!bvar}; if (is_disjunction(clause)) { @@ -54,39 +58,42 @@ Formula PlaistedGreenbaumCnfizer::VisitForall(const Formula &f) { DLINEAR_ASSERT(is_clause(new_clause), "Must be a clause"); // Only the old clause's variables can intersect if (HaveIntersection(clause.GetFreeVariables(), quantified_variables)) { - aux_.emplace_back(forall(quantified_variables, new_clause)); + aux.emplace_back(forall(quantified_variables, new_clause)); } else { - aux_.emplace_back(new_clause); + aux.emplace_back(new_clause); } } return Formula{bvar}; } -Formula PlaistedGreenbaumCnfizer::VisitConjunction(const Formula &f) { +Formula PlaistedGreenbaumCnfizer::VisitConjunction(const Formula &f, std::vector &aux, + std::vector &vars) const { static std::size_t id{0}; // Introduce a new Boolean variable, `bvar` for `f`. const Variable bvar{std::string("conj") + std::to_string(id++), Variable::Type::BOOLEAN}; - vars_.push_back(bvar); + vars.push_back(bvar); for (const Formula &op : get_operands(f)) { - aux_.emplace_back(!bvar || this->Visit(op)); + aux.emplace_back(!bvar || VisitFormula(op, aux, vars)); } return Formula{bvar}; } -Formula PlaistedGreenbaumCnfizer::VisitDisjunction(const Formula &f) { +Formula PlaistedGreenbaumCnfizer::VisitDisjunction(const Formula &f, std::vector &aux, + std::vector &vars) const { static std::size_t id{0}; // Introduce a new Boolean variable, `bvar` for `f`. const Variable bvar{std::string("disj") + std::to_string(id++), Variable::Type::BOOLEAN}; - vars_.push_back(bvar); - std::set clause{ - ::dlinear::map(get_operands(f), [this](const Formula &formula) { return this->Visit(formula); })}; + vars.push_back(bvar); + std::set clause{::dlinear::map( + get_operands(f), [this, &aux, &vars](const Formula &formula) { return VisitFormula(formula, aux, vars); })}; clause.insert(!bvar); - aux_.emplace_back(make_disjunction(clause)); + aux.emplace_back(make_disjunction(clause)); return Formula{bvar}; } -Formula PlaistedGreenbaumCnfizer::VisitNegation(const Formula &f) { +Formula PlaistedGreenbaumCnfizer::VisitNegation(const Formula &f, std::vector &, + std::vector &) const { DLINEAR_ASSERT(is_atomic(get_operand(f)), "Must be atomic"); return f; } diff --git a/dlinear/symbolic/PlaistedGreenbaumCnfizer.h b/dlinear/symbolic/PlaistedGreenbaumCnfizer.h index 1bbb587..3e9535e 100644 --- a/dlinear/symbolic/PlaistedGreenbaumCnfizer.h +++ b/dlinear/symbolic/PlaistedGreenbaumCnfizer.h @@ -24,7 +24,7 @@ namespace dlinear { * The method can introduce extra Boolean variables. * Check [Wikipedia](https://en.wikipedia.org/wiki/Plaisted-Greenbaum_transformation) for more information. */ -class PlaistedGreenbaumCnfizer : public FormulaVisitor { +class PlaistedGreenbaumCnfizer : public FormulaVisitor &, std::vector &> { public: /** * Construct a new PlaistedGreenbaumCnfizer object with the given @p config. @@ -38,25 +38,22 @@ class PlaistedGreenbaumCnfizer : public FormulaVisitor { * @param f A formula to be converted. * @return A vector of clauses. */ - std::vector Convert(const Formula &f); - - /** @getter{auxiliary variables introduced during the conversion, PlaistedGreenbaumCnfizer} */ - [[nodiscard]] const std::vector &vars() const { return vars_; } + [[nodiscard]] std::pair, std::vector> Process(const Formula &f) const; + [[nodiscard]] std::pair, std::vector> operator()(const Formula &f) const; private: - Formula VisitConjunction(const Formula &f) override; - Formula VisitDisjunction(const Formula &f) override; - Formula VisitNegation(const Formula &f) override; - Formula VisitForall(const Formula &f) override; - const Nnfizer nnfizer_; - - NaiveCnfizer naive_cnfizer_; ///< Naive CNFizer. Used to transform nested formulas inside universal quantification. + [[nodiscard]] Formula VisitConjunction(const Formula &f, std::vector &aux, + std::vector &vars) const override; + [[nodiscard]] Formula VisitDisjunction(const Formula &f, std::vector &aux, + std::vector &vars) const override; + [[nodiscard]] Formula VisitNegation(const Formula &f, std::vector &aux, + std::vector &vars) const override; + [[nodiscard]] Formula VisitForall(const Formula &f, std::vector &aux, + std::vector &vars) const override; - std::vector - aux_; ///< Auxiliary clauses collected during conversion. @note It is cleared at the beginning of `Convert` call. - - std::vector - vars_; ///< Variables generated during conversion. @note It is cleared at the beginning of `Convert` call. + const Nnfizer nnfizer_; + const NaiveCnfizer + naive_cnfizer_; ///< Naive CNFizer. Used to transform nested formulas inside universal quantification. }; } // namespace dlinear diff --git a/dlinear/symbolic/PredicateAbstractor.cpp b/dlinear/symbolic/PredicateAbstractor.cpp index 3d7f618..3fb1abe 100644 --- a/dlinear/symbolic/PredicateAbstractor.cpp +++ b/dlinear/symbolic/PredicateAbstractor.cpp @@ -15,17 +15,19 @@ namespace dlinear { -Formula PredicateAbstractor::Convert(const Formula &f) { +Formula PredicateAbstractor::Process(const Formula &f) { TimerGuard timer_guard(&stats_.m_timer(), stats_.enabled()); stats_.Increase(); - return Visit(f); + return VisitFormula(f); } +Formula PredicateAbstractor::operator()(const Formula &f) { return Process(f); } -Formula PredicateAbstractor::Convert(const std::vector &formulas) { - return Convert(make_conjunction(std::set{formulas.begin(), formulas.end()})); +Formula PredicateAbstractor::Process(const std::vector &formulas) { + return Process(make_conjunction(std::set{formulas.begin(), formulas.end()})); } +Formula PredicateAbstractor::operator()(const std::vector &formulas) { return Process(formulas); } -Formula PredicateAbstractor::Visit(const Formula &f) { +Formula PredicateAbstractor::VisitFormula(const Formula &f) const { const Formula flattened_f{flattener_.Flatten(f)}; const bool is_negated = is_negation(flattened_f); const Formula &unary_f = is_negated ? get_operand(flattened_f) : flattened_f; @@ -34,14 +36,14 @@ Formula PredicateAbstractor::Visit(const Formula &f) { const auto it = formula_to_var_map_.find(unary_f); if (it == formula_to_var_map_.cend()) { // No, we haven't processed it before. - return FormulaVisitor::Visit(flattened_f); + return FormulaVisitor::VisitFormula(flattened_f); } else { // Yes, we have processed this formula before. return is_negated ? !Formula{it->second} : Formula{it->second}; } } -Formula PredicateAbstractor::VisitAtomic(const Formula &f) { +Formula PredicateAbstractor::VisitAtomic(const Formula &f) const { // Flatten linear formulas to make sure they have the standard form (ax + by <=> c). const Formula flattened_f{flattener_.Flatten(f)}; const bool is_negated = is_negation(flattened_f); @@ -58,23 +60,23 @@ Formula PredicateAbstractor::VisitAtomic(const Formula &f) { return is_negated ? !Formula{it->second} : Formula{it->second}; } -Formula PredicateAbstractor::VisitEqualTo(const Formula &f) { return VisitAtomic(f); } -Formula PredicateAbstractor::VisitNotEqualTo(const Formula &f) { return VisitAtomic(f); } -Formula PredicateAbstractor::VisitLessThan(const Formula &f) { return VisitAtomic(f); } -Formula PredicateAbstractor::VisitLessThanOrEqualTo(const Formula &f) { return VisitAtomic(f); } -Formula PredicateAbstractor::VisitGreaterThan(const Formula &f) { return VisitAtomic(f); } -Formula PredicateAbstractor::VisitGreaterThanOrEqualTo(const Formula &f) { return VisitAtomic(f); } +Formula PredicateAbstractor::VisitEqualTo(const Formula &f) const { return VisitAtomic(f); } +Formula PredicateAbstractor::VisitNotEqualTo(const Formula &f) const { return VisitAtomic(f); } +Formula PredicateAbstractor::VisitLessThan(const Formula &f) const { return VisitAtomic(f); } +Formula PredicateAbstractor::VisitLessThanOrEqualTo(const Formula &f) const { return VisitAtomic(f); } +Formula PredicateAbstractor::VisitGreaterThan(const Formula &f) const { return VisitAtomic(f); } +Formula PredicateAbstractor::VisitGreaterThanOrEqualTo(const Formula &f) const { return VisitAtomic(f); } -Formula PredicateAbstractor::VisitNegation(const Formula &f) { return !Visit(get_operand(f)); } -Formula PredicateAbstractor::VisitForall(const Formula &f) { return VisitAtomic(f); } -Formula PredicateAbstractor::VisitConjunction(const Formula &f) { +Formula PredicateAbstractor::VisitNegation(const Formula &f) const { return !VisitFormula(get_operand(f)); } +Formula PredicateAbstractor::VisitForall(const Formula &f) const { return VisitAtomic(f); } +Formula PredicateAbstractor::VisitConjunction(const Formula &f) const { const std::set operands{ - map(get_operands(f), [this](const Formula &formula) { return this->Visit(formula); })}; + map(get_operands(f), [this](const Formula &formula) { return VisitFormula(formula); })}; return make_conjunction(operands); } -Formula PredicateAbstractor::VisitDisjunction(const Formula &f) { +Formula PredicateAbstractor::VisitDisjunction(const Formula &f) const { const std::set operands{ - map(get_operands(f), [this](const Formula &formula) { return this->Visit(formula); })}; + map(get_operands(f), [this](const Formula &formula) { return VisitFormula(formula); })}; return make_disjunction(operands); } diff --git a/dlinear/symbolic/PredicateAbstractor.h b/dlinear/symbolic/PredicateAbstractor.h index c2fb41a..f3a568c 100644 --- a/dlinear/symbolic/PredicateAbstractor.h +++ b/dlinear/symbolic/PredicateAbstractor.h @@ -23,7 +23,7 @@ namespace dlinear { * The boolean formula will be a boolean variable or a conjunction of boolean variables. * The object keeps a bijective map between newly introduced the boolean variables and the first-order logic formulae. */ -class PredicateAbstractor : public FormulaVisitor { +class PredicateAbstractor : public FormulaVisitor<> { public: /** * Construct a new PredicateAbstractor object with the given @p config. @@ -40,7 +40,8 @@ class PredicateAbstractor : public FormulaVisitor { * @param f formula to be converted * @return boolean formula */ - Formula Convert(const Formula &f); + [[nodiscard]] Formula Process(const Formula &f); + [[nodiscard]] Formula operator()(const Formula &f); /** * Convert a vector first-order logic formula @p formulas into a Boolean formula @@ -52,13 +53,14 @@ class PredicateAbstractor : public FormulaVisitor { * @param f formula to be converted * @return boolean formula */ - Formula Convert(const std::vector &formulas); + [[nodiscard]] Formula Process(const std::vector &formulas); + [[nodiscard]] Formula operator()(const std::vector &formulas); /** @getter{map of previously converted formulae to variable, PredicateAbstractor} */ - const std::unordered_map &var_to_formula_map() const { return var_to_formula_map_; } + [[nodiscard]] const std::unordered_map &var_to_formula_map() const { return var_to_formula_map_; } - const Variable &operator[](const Formula &f) const { return formula_to_var_map_.at(f); } - const Formula &operator[](const Variable &var) const { return var_to_formula_map_.at(var); } + [[nodiscard]] const Variable &operator[](const Formula &f) const { return formula_to_var_map_.at(f); } + [[nodiscard]] const Formula &operator[](const Variable &var) const { return var_to_formula_map_.at(var); } private: /** @@ -70,24 +72,24 @@ class PredicateAbstractor : public FormulaVisitor { * @return newly created Boolean variable in the map @ref var_to_formula_map_ if the formula is not present * @return existing Boolean variable in the map @ref var_to_formula_map_ if the formula was already present */ - Formula Visit(const Formula &f) override; - Formula VisitAtomic(const Formula &f); - Formula VisitEqualTo(const Formula &f) override; - Formula VisitNotEqualTo(const Formula &f) override; - Formula VisitGreaterThan(const Formula &f) override; - Formula VisitGreaterThanOrEqualTo(const Formula &f) override; - Formula VisitLessThan(const Formula &f) override; - Formula VisitLessThanOrEqualTo(const Formula &f) override; - Formula VisitConjunction(const Formula &f) override; - Formula VisitDisjunction(const Formula &f) override; - Formula VisitNegation(const Formula &f) override; - Formula VisitForall(const Formula &f) override; + [[nodiscard]] Formula VisitFormula(const Formula &f) const override; + [[nodiscard]] Formula VisitAtomic(const Formula &f) const; + [[nodiscard]] Formula VisitEqualTo(const Formula &f) const override; + [[nodiscard]] Formula VisitNotEqualTo(const Formula &f) const override; + [[nodiscard]] Formula VisitGreaterThan(const Formula &f) const override; + [[nodiscard]] Formula VisitGreaterThanOrEqualTo(const Formula &f) const override; + [[nodiscard]] Formula VisitLessThan(const Formula &f) const override; + [[nodiscard]] Formula VisitLessThanOrEqualTo(const Formula &f) const override; + [[nodiscard]] Formula VisitConjunction(const Formula &f) const override; + [[nodiscard]] Formula VisitDisjunction(const Formula &f) const override; + [[nodiscard]] Formula VisitNegation(const Formula &f) const override; + [[nodiscard]] Formula VisitForall(const Formula &f) const override; - std::unordered_map + mutable std::unordered_map var_to_formula_map_; ///< Map from Boolean variable to previously converted formula. - std::unordered_map - formula_to_var_map_; ///< Map from previously converted formula to Boolean variable. - LinearFormulaFlattener flattener_; ///< Linear formula flattener. + mutable std::unordered_map + formula_to_var_map_; ///< Map from previously converted formula to Boolean variable. + mutable LinearFormulaFlattener flattener_; ///< Linear formula flattener. }; } // namespace dlinear diff --git a/dlinear/symbolic/PrefixPrinter.cpp b/dlinear/symbolic/PrefixPrinter.cpp index 49dc2c1..b7d6246 100644 --- a/dlinear/symbolic/PrefixPrinter.cpp +++ b/dlinear/symbolic/PrefixPrinter.cpp @@ -16,17 +16,23 @@ namespace dlinear { -PrefixPrinter::PrefixPrinter(std::ostream &os) : os_{os}, old_precision_{os.precision()} {} +PrefixPrinter::PrefixPrinter(std::ostream &os, const Config &config) + : GenericFormulaVisitor(config, "PrefixPrinter"), + GenericExpressionVisitor(config, "PrefixPrinter"), + os_{os}, + old_precision_{os.precision()} {} PrefixPrinter::~PrefixPrinter() { os_.precision(old_precision_); } -std::ostream &PrefixPrinter::Print(const Expression &e) { return VisitExpression(this, e); } +std::ostream &PrefixPrinter::Print(const Expression &e) const { return GenericExpressionVisitor::VisitExpression(e); } +std::ostream &PrefixPrinter::operator()(const Expression &e) const { return Print(e); } -std::ostream &PrefixPrinter::Print(const Formula &f) { return VisitFormula(this, f); } +std::ostream &PrefixPrinter::Print(const Formula &f) const { return VisitFormula(f); } +std::ostream &PrefixPrinter::operator()(const Formula &f) const { return Print(f); } -std::ostream &PrefixPrinter::VisitVariable(const Expression &e) { return os_ << get_variable(e); } +std::ostream &PrefixPrinter::VisitVariable(const Expression &e) const { return os_ << get_variable(e); } -std::ostream &PrefixPrinter::VisitConstant(const Expression &e) { +std::ostream &PrefixPrinter::VisitConstant(const Expression &e) const { const mpq_class &constant{get_constant_value(e)}; bool print_den = constant.get_den() != 1; if (print_den) { @@ -41,13 +47,13 @@ std::ostream &PrefixPrinter::VisitConstant(const Expression &e) { return os_; } -std::ostream &PrefixPrinter::VisitUnaryFunction(const std::string &name, const Expression &e) { +std::ostream &PrefixPrinter::VisitUnaryFunction(const std::string &name, const Expression &e) const { os_ << "(" << name << " "; Print(get_argument(e)); return os_ << ")"; } -std::ostream &PrefixPrinter::VisitBinaryFunction(const std::string &name, const Expression &e) { +std::ostream &PrefixPrinter::VisitBinaryFunction(const std::string &name, const Expression &e) const { os_ << "(" << name << " "; Print(get_first_argument(e)); os_ << " "; @@ -55,7 +61,7 @@ std::ostream &PrefixPrinter::VisitBinaryFunction(const std::string &name, const return os_ << ")"; } -std::ostream &PrefixPrinter::VisitAddition(const Expression &e) { +std::ostream &PrefixPrinter::VisitAddition(const Expression &e) const { const mpq_class &constant{get_constant_in_addition(e)}; os_ << "(+"; if (constant != 0.0) { @@ -79,7 +85,7 @@ std::ostream &PrefixPrinter::VisitAddition(const Expression &e) { return os_ << ")"; } -std::ostream &PrefixPrinter::VisitMultiplication(const Expression &e) { +std::ostream &PrefixPrinter::VisitMultiplication(const Expression &e) const { const mpq_class &constant{get_constant_in_multiplication(e)}; os_ << "(*"; if (constant != 1.0) { @@ -103,43 +109,43 @@ std::ostream &PrefixPrinter::VisitMultiplication(const Expression &e) { return os_ << ")"; } -std::ostream &PrefixPrinter::VisitDivision(const Expression &e) { return VisitBinaryFunction("/", e); } +std::ostream &PrefixPrinter::VisitDivision(const Expression &e) const { return VisitBinaryFunction("/", e); } -std::ostream &PrefixPrinter::VisitLog(const Expression &e) { return VisitUnaryFunction("log", e); } +std::ostream &PrefixPrinter::VisitLog(const Expression &e) const { return VisitUnaryFunction("log", e); } -std::ostream &PrefixPrinter::VisitAbs(const Expression &e) { return VisitUnaryFunction("abs", e); } +std::ostream &PrefixPrinter::VisitAbs(const Expression &e) const { return VisitUnaryFunction("abs", e); } -std::ostream &PrefixPrinter::VisitExp(const Expression &e) { return VisitUnaryFunction("exp", e); } +std::ostream &PrefixPrinter::VisitExp(const Expression &e) const { return VisitUnaryFunction("exp", e); } -std::ostream &PrefixPrinter::VisitSqrt(const Expression &e) { return VisitUnaryFunction("sqrt", e); } +std::ostream &PrefixPrinter::VisitSqrt(const Expression &e) const { return VisitUnaryFunction("sqrt", e); } -std::ostream &PrefixPrinter::VisitPow(const Expression &e) { return VisitBinaryFunction("^", e); } +std::ostream &PrefixPrinter::VisitPow(const Expression &e) const { return VisitBinaryFunction("^", e); } -std::ostream &PrefixPrinter::VisitSin(const Expression &e) { return VisitUnaryFunction("sin", e); } +std::ostream &PrefixPrinter::VisitSin(const Expression &e) const { return VisitUnaryFunction("sin", e); } -std::ostream &PrefixPrinter::VisitCos(const Expression &e) { return VisitUnaryFunction("cos", e); } +std::ostream &PrefixPrinter::VisitCos(const Expression &e) const { return VisitUnaryFunction("cos", e); } -std::ostream &PrefixPrinter::VisitTan(const Expression &e) { return VisitUnaryFunction("tan", e); } +std::ostream &PrefixPrinter::VisitTan(const Expression &e) const { return VisitUnaryFunction("tan", e); } -std::ostream &PrefixPrinter::VisitAsin(const Expression &e) { return VisitUnaryFunction("asin", e); } +std::ostream &PrefixPrinter::VisitAsin(const Expression &e) const { return VisitUnaryFunction("asin", e); } -std::ostream &PrefixPrinter::VisitAcos(const Expression &e) { return VisitUnaryFunction("acos", e); } +std::ostream &PrefixPrinter::VisitAcos(const Expression &e) const { return VisitUnaryFunction("acos", e); } -std::ostream &PrefixPrinter::VisitAtan(const Expression &e) { return VisitUnaryFunction("atan", e); } +std::ostream &PrefixPrinter::VisitAtan(const Expression &e) const { return VisitUnaryFunction("atan", e); } -std::ostream &PrefixPrinter::VisitAtan2(const Expression &e) { return VisitBinaryFunction("atan2", e); } +std::ostream &PrefixPrinter::VisitAtan2(const Expression &e) const { return VisitBinaryFunction("atan2", e); } -std::ostream &PrefixPrinter::VisitSinh(const Expression &e) { return VisitUnaryFunction("sinh", e); } +std::ostream &PrefixPrinter::VisitSinh(const Expression &e) const { return VisitUnaryFunction("sinh", e); } -std::ostream &PrefixPrinter::VisitCosh(const Expression &e) { return VisitUnaryFunction("cosh", e); } +std::ostream &PrefixPrinter::VisitCosh(const Expression &e) const { return VisitUnaryFunction("cosh", e); } -std::ostream &PrefixPrinter::VisitTanh(const Expression &e) { return VisitUnaryFunction("tanh", e); } +std::ostream &PrefixPrinter::VisitTanh(const Expression &e) const { return VisitUnaryFunction("tanh", e); } -std::ostream &PrefixPrinter::VisitMin(const Expression &e) { return VisitBinaryFunction("min", e); } +std::ostream &PrefixPrinter::VisitMin(const Expression &e) const { return VisitBinaryFunction("min", e); } -std::ostream &PrefixPrinter::VisitMax(const Expression &e) { return VisitBinaryFunction("max", e); } +std::ostream &PrefixPrinter::VisitMax(const Expression &e) const { return VisitBinaryFunction("max", e); } -std::ostream &PrefixPrinter::VisitIfThenElse(const Expression &e) { +std::ostream &PrefixPrinter::VisitIfThenElse(const Expression &e) const { os_ << "(ite "; Print(get_conditional_formula(e)); os_ << " "; @@ -149,17 +155,17 @@ std::ostream &PrefixPrinter::VisitIfThenElse(const Expression &e) { return os_ << ")"; } -std::ostream &PrefixPrinter::VisitUninterpretedFunction(const Expression &) { +std::ostream &PrefixPrinter::VisitUninterpretedFunction(const Expression &) const { throw std::runtime_error("Not implemented."); } -std::ostream &PrefixPrinter::VisitFalse(const Formula &) { return os_ << "false"; } +std::ostream &PrefixPrinter::VisitFalse(const Formula &) const { return os_ << "false"; } -std::ostream &PrefixPrinter::VisitTrue(const Formula &) { return os_ << "true"; } +std::ostream &PrefixPrinter::VisitTrue(const Formula &) const { return os_ << "true"; } -std::ostream &PrefixPrinter::VisitVariable(const Formula &f) { return os_ << get_variable(f); } +std::ostream &PrefixPrinter::VisitVariable(const Formula &f) const { return os_ << get_variable(f); } -std::ostream &PrefixPrinter::VisitEqualTo(const Formula &f) { +std::ostream &PrefixPrinter::VisitEqualTo(const Formula &f) const { os_ << "(= "; Print(get_lhs_expression(f)); os_ << " "; @@ -167,7 +173,7 @@ std::ostream &PrefixPrinter::VisitEqualTo(const Formula &f) { return os_ << ")"; } -std::ostream &PrefixPrinter::VisitNotEqualTo(const Formula &f) { +std::ostream &PrefixPrinter::VisitNotEqualTo(const Formula &f) const { os_ << "(not (= "; Print(get_lhs_expression(f)); os_ << " "; @@ -175,7 +181,7 @@ std::ostream &PrefixPrinter::VisitNotEqualTo(const Formula &f) { return os_ << "))"; } -std::ostream &PrefixPrinter::VisitGreaterThan(const Formula &f) { +std::ostream &PrefixPrinter::VisitGreaterThan(const Formula &f) const { os_ << "(> "; Print(get_lhs_expression(f)); os_ << " "; @@ -183,7 +189,7 @@ std::ostream &PrefixPrinter::VisitGreaterThan(const Formula &f) { return os_ << ")"; } -std::ostream &PrefixPrinter::VisitGreaterThanOrEqualTo(const Formula &f) { +std::ostream &PrefixPrinter::VisitGreaterThanOrEqualTo(const Formula &f) const { os_ << "(>= "; Print(get_lhs_expression(f)); os_ << " "; @@ -191,7 +197,7 @@ std::ostream &PrefixPrinter::VisitGreaterThanOrEqualTo(const Formula &f) { return os_ << ")"; } -std::ostream &PrefixPrinter::VisitLessThan(const Formula &f) { +std::ostream &PrefixPrinter::VisitLessThan(const Formula &f) const { os_ << "(< "; Print(get_lhs_expression(f)); os_ << " "; @@ -199,7 +205,7 @@ std::ostream &PrefixPrinter::VisitLessThan(const Formula &f) { return os_ << ")"; } -std::ostream &PrefixPrinter::VisitLessThanOrEqualTo(const Formula &f) { +std::ostream &PrefixPrinter::VisitLessThanOrEqualTo(const Formula &f) const { os_ << "(<= "; Print(get_lhs_expression(f)); os_ << " "; @@ -207,7 +213,7 @@ std::ostream &PrefixPrinter::VisitLessThanOrEqualTo(const Formula &f) { return os_ << ")"; } -std::ostream &PrefixPrinter::VisitConjunction(const Formula &f) { +std::ostream &PrefixPrinter::VisitConjunction(const Formula &f) const { os_ << "(and"; for (const auto &f_i : get_operands(f)) { os_ << " "; @@ -216,7 +222,7 @@ std::ostream &PrefixPrinter::VisitConjunction(const Formula &f) { return os_ << ")"; } -std::ostream &PrefixPrinter::VisitDisjunction(const Formula &f) { +std::ostream &PrefixPrinter::VisitDisjunction(const Formula &f) const { os_ << "(or"; for (const auto &f_i : get_operands(f)) { os_ << " "; @@ -225,24 +231,28 @@ std::ostream &PrefixPrinter::VisitDisjunction(const Formula &f) { return os_ << ")"; } -std::ostream &PrefixPrinter::VisitNegation(const Formula &f) { +std::ostream &PrefixPrinter::VisitNegation(const Formula &f) const { os_ << "(not "; Print(get_operand(f)); return os_ << ")"; } -std::ostream &PrefixPrinter::VisitForall(const Formula &) { throw std::runtime_error("Not implemented."); } +std::ostream &PrefixPrinter::VisitForall(const Formula &) const { throw std::runtime_error("Not implemented."); } std::string ToPrefix(const Expression &e) { std::ostringstream oss; - PrefixPrinter pp{oss}; + static Config config; + config.m_with_timings() = false; + PrefixPrinter pp{oss, config}; pp.Print(e); return oss.str(); } std::string ToPrefix(const Formula &f) { std::ostringstream oss; - PrefixPrinter pp{oss}; + static Config config; + config.m_with_timings() = false; + PrefixPrinter pp{oss, config}; pp.Print(f); return oss.str(); } diff --git a/dlinear/symbolic/PrefixPrinter.h b/dlinear/symbolic/PrefixPrinter.h index 370f54f..54fedef 100644 --- a/dlinear/symbolic/PrefixPrinter.h +++ b/dlinear/symbolic/PrefixPrinter.h @@ -9,6 +9,8 @@ #include #include +#include "dlinear/symbolic/GenericExpressionVisitor.h" +#include "dlinear/symbolic/GenericFormulaVisitor.h" #include "dlinear/symbolic/symbolic.h" namespace dlinear { @@ -18,7 +20,7 @@ namespace dlinear { * * It is mainly used for debugging purposes. */ -class PrefixPrinter { +class PrefixPrinter : public GenericFormulaVisitor, public GenericExpressionVisitor { public: /** * Constructs a new PrefixPrinter object with @p os. @@ -26,7 +28,7 @@ class PrefixPrinter { * It temporarily sets the precision of @p os to the maximum precision. * @param os stream to print to. */ - explicit PrefixPrinter(std::ostream &os); + explicit PrefixPrinter(std::ostream &os, const Config &config = Config{}); PrefixPrinter(const PrefixPrinter &) = delete; PrefixPrinter(PrefixPrinter &&) = delete; @@ -34,75 +36,69 @@ class PrefixPrinter { PrefixPrinter &operator=(PrefixPrinter &&) = delete; /** Restore the original precision of the ostream. */ - ~PrefixPrinter(); + ~PrefixPrinter() override; /** * Print the prefix form of the expression @p e to the ostream. * @param e expression to print * @return updated ostream */ - std::ostream &Print(const Expression &e); + std::ostream &Print(const Expression &e) const; + std::ostream &operator()(const Expression &e) const; /** * Print the prefix form of the formula @p f to the ostream. * @param f formula to print * @return updated ostream */ - std::ostream &Print(const Formula &f); + std::ostream &Print(const Formula &f) const; + std::ostream &operator()(const Formula &f) const; private: - std::ostream &VisitVariable(const Expression &e); - std::ostream &VisitConstant(const Expression &e); - std::ostream &VisitAddition(const Expression &e); - std::ostream &VisitMultiplication(const Expression &e); - std::ostream &VisitDivision(const Expression &e); - std::ostream &VisitLog(const Expression &e); - std::ostream &VisitAbs(const Expression &e); - std::ostream &VisitExp(const Expression &e); - std::ostream &VisitSqrt(const Expression &e); - std::ostream &VisitPow(const Expression &e); - std::ostream &VisitSin(const Expression &e); - std::ostream &VisitCos(const Expression &e); - std::ostream &VisitTan(const Expression &e); - std::ostream &VisitAsin(const Expression &e); - std::ostream &VisitAcos(const Expression &e); - std::ostream &VisitAtan(const Expression &e); - std::ostream &VisitAtan2(const Expression &e); - std::ostream &VisitSinh(const Expression &e); - std::ostream &VisitCosh(const Expression &e); - std::ostream &VisitTanh(const Expression &e); - std::ostream &VisitMin(const Expression &e); - std::ostream &VisitMax(const Expression &e); - std::ostream &VisitIfThenElse(const Expression &e); - static std::ostream &VisitUninterpretedFunction(const Expression &e); - - std::ostream &VisitFalse(const Formula &f); - std::ostream &VisitTrue(const Formula &f); - std::ostream &VisitVariable(const Formula &f); - std::ostream &VisitEqualTo(const Formula &f); - std::ostream &VisitNotEqualTo(const Formula &f); - std::ostream &VisitGreaterThan(const Formula &f); - std::ostream &VisitGreaterThanOrEqualTo(const Formula &f); - std::ostream &VisitLessThan(const Formula &f); - std::ostream &VisitLessThanOrEqualTo(const Formula &f); - std::ostream &VisitConjunction(const Formula &f); - std::ostream &VisitDisjunction(const Formula &f); - std::ostream &VisitNegation(const Formula &f); - static std::ostream &VisitForall(const Formula &f); - - std::ostream &VisitUnaryFunction(const std::string &name, const Expression &e); - std::ostream &VisitBinaryFunction(const std::string &name, const Expression &e); - - // Makes VisitExpression a friend of this class so that it can use private - // operator()s. - friend std::ostream &drake::symbolic::VisitExpression(PrefixPrinter *, const Expression &e); - - // Makes VisitFormula a friend of this class so that it can use private - // operator()s. - friend std::ostream &drake::symbolic::VisitFormula(PrefixPrinter *, const Formula &f); - - std::ostream &os_; ///< Stream to print to. - std::streamsize old_precision_{}; ///< Original precision of the stream. + std::ostream &VisitVariable(const Expression &e) const override; + std::ostream &VisitConstant(const Expression &e) const override; + std::ostream &VisitAddition(const Expression &e) const override; + std::ostream &VisitMultiplication(const Expression &e) const override; + std::ostream &VisitDivision(const Expression &e) const override; + std::ostream &VisitLog(const Expression &e) const override; + std::ostream &VisitAbs(const Expression &e) const override; + std::ostream &VisitExp(const Expression &e) const override; + std::ostream &VisitSqrt(const Expression &e) const override; + std::ostream &VisitPow(const Expression &e) const override; + std::ostream &VisitSin(const Expression &e) const override; + std::ostream &VisitCos(const Expression &e) const override; + std::ostream &VisitTan(const Expression &e) const override; + std::ostream &VisitAsin(const Expression &e) const override; + std::ostream &VisitAcos(const Expression &e) const override; + std::ostream &VisitAtan(const Expression &e) const override; + std::ostream &VisitAtan2(const Expression &e) const override; + std::ostream &VisitSinh(const Expression &e) const override; + std::ostream &VisitCosh(const Expression &e) const override; + std::ostream &VisitTanh(const Expression &e) const override; + std::ostream &VisitMin(const Expression &e) const override; + std::ostream &VisitMax(const Expression &e) const override; + std::ostream &VisitIfThenElse(const Expression &e) const override; + std::ostream &VisitUninterpretedFunction(const Expression &e) const override; + + std::ostream &VisitFalse(const Formula &f) const override; + std::ostream &VisitTrue(const Formula &f) const override; + std::ostream &VisitVariable(const Formula &f) const override; + std::ostream &VisitEqualTo(const Formula &f) const override; + std::ostream &VisitNotEqualTo(const Formula &f) const override; + std::ostream &VisitGreaterThan(const Formula &f) const override; + std::ostream &VisitGreaterThanOrEqualTo(const Formula &f) const override; + std::ostream &VisitLessThan(const Formula &f) const override; + std::ostream &VisitLessThanOrEqualTo(const Formula &f) const override; + std::ostream &VisitConjunction(const Formula &f) const override; + std::ostream &VisitDisjunction(const Formula &f) const override; + std::ostream &VisitNegation(const Formula &f) const override; + std::ostream &VisitForall(const Formula &f) const override; + + std::ostream &VisitUnaryFunction(const std::string &name, const Expression &e) const; + std::ostream &VisitBinaryFunction(const std::string &name, const Expression &e) const; + + std::ostream &os_; ///< Stream to print to. + const std::streamsize old_precision_; ///< Original precision of the stream. }; /** diff --git a/dlinear/symbolic/TseitinCnfizer.cpp b/dlinear/symbolic/TseitinCnfizer.cpp index 4205180..129e2b1 100644 --- a/dlinear/symbolic/TseitinCnfizer.cpp +++ b/dlinear/symbolic/TseitinCnfizer.cpp @@ -33,16 +33,17 @@ void CnfizeDisjunction(const Variable &b, const Formula &f, std::vector // - It visits each node and introduce a Boolean variable `b` for // each subterm `f`, and keep the relation `b ⇔ f`. // - Then it cnfizes each `b ⇔ f` and make a conjunction of them. -std::vector TseitinCnfizer::Convert(const Formula &f) { - TimerGuard timer_guard(&stats_.m_timer(), stats_.enabled()); +std::vector TseitinCnfizer::Process(const Formula &f) const { + const TimerGuard timer_guard(&stats_.m_timer(), stats_.enabled()); stats_.Increase(); - map_.clear(); + + std::map map; std::vector ret; - const Formula head{Visit(f)}; - if (map_.empty()) { + const Formula head{VisitFormula(f, map)}; + if (map.empty()) { return {head}; } - for (auto const &p : map_) { + for (auto const &p : map) { if (get_variable(head).equal_to(p.first)) { if (is_conjunction(p.second)) { const std::set &conjuncts(get_operands(p.second)); @@ -56,8 +57,9 @@ std::vector TseitinCnfizer::Convert(const Formula &f) { } return ret; } +std::vector TseitinCnfizer::operator()(const Formula &f) const { return Process(f); } -Formula TseitinCnfizer::VisitForall(const Formula &f) { +Formula TseitinCnfizer::VisitForall(const Formula &f, std::map &map) const { // Given: f := ∀y. φ(x, y), this process CNFizes φ(x, y) and push the // universal quantifier over conjunctions: // @@ -66,7 +68,7 @@ Formula TseitinCnfizer::VisitForall(const Formula &f) { const Variables &quantified_variables{get_quantified_variables(f)}; // y const Formula &quantified_formula{get_quantified_formula(f)}; // φ(x, y) // clause₁(x, y) ∧ ... ∧ clauseₙ(x, y) - const std::set clauses{get_clauses(naive_cnfizer_.Convert(quantified_formula))}; + const std::set clauses{get_clauses(naive_cnfizer_.Process(quantified_formula))}; const std::set new_clauses{::dlinear::map(clauses, [&quantified_variables](const Formula &clause) { DLINEAR_ASSERT(is_clause(clause), "Must be a clause"); if (HaveIntersection(clause.GetFreeVariables(), quantified_variables)) { @@ -82,39 +84,39 @@ Formula TseitinCnfizer::VisitForall(const Formula &f) { } else { static std::size_t id{0}; const Variable bvar{std::string("forall") + std::to_string(id++), Variable::Type::BOOLEAN}; - map_.emplace(bvar, make_conjunction(new_clauses)); + map.emplace(bvar, make_conjunction(new_clauses)); return Formula{bvar}; } } -Formula TseitinCnfizer::VisitConjunction(const Formula &f) { +Formula TseitinCnfizer::VisitConjunction(const Formula &f, std::map &map) const { // Introduce a new Boolean variable, `bvar` for `f` and record the // relation `bvar ⇔ f`. static std::size_t id{0}; - const std::set transformed_operands{ - ::dlinear::map(get_operands(f), [this](const Formula &formula) { return this->Visit(formula); })}; + const std::set transformed_operands{::dlinear::map( + get_operands(f), [this, &map](const Formula &formula) { return this->VisitFormula(formula, map); })}; const Variable bvar{std::string("conj") + std::to_string(id++), Variable::Type::BOOLEAN}; - map_.emplace(bvar, make_conjunction(transformed_operands)); + map.emplace(bvar, make_conjunction(transformed_operands)); return Formula{bvar}; } -Formula TseitinCnfizer::VisitDisjunction(const Formula &f) { +Formula TseitinCnfizer::VisitDisjunction(const Formula &f, std::map &map) const { static std::size_t id{0}; - const std::set &transformed_operands{ - ::dlinear::map(get_operands(f), [this](const Formula &formula) { return this->Visit(formula); })}; + const std::set &transformed_operands{::dlinear::map( + get_operands(f), [this, &map](const Formula &formula) { return this->VisitFormula(formula, map); })}; const Variable bvar{std::string("disj") + std::to_string(id++), Variable::Type::BOOLEAN}; - map_.emplace(bvar, make_disjunction(transformed_operands)); + map.emplace(bvar, make_disjunction(transformed_operands)); return Formula{bvar}; } -Formula TseitinCnfizer::VisitNegation(const Formula &f) { +Formula TseitinCnfizer::VisitNegation(const Formula &f, std::map &map) const { const Formula &operand{get_operand(f)}; if (is_atomic(operand)) { return f; } else { const Variable bvar{"neg", Variable::Type::BOOLEAN}; - const Formula transformed_operand{Visit(operand)}; - map_.emplace(bvar, !transformed_operand); + const Formula transformed_operand{VisitFormula(operand, map)}; + map.emplace(bvar, !transformed_operand); return Formula{bvar}; } } diff --git a/dlinear/symbolic/TseitinCnfizer.h b/dlinear/symbolic/TseitinCnfizer.h index 1bb7efe..8e5902b 100644 --- a/dlinear/symbolic/TseitinCnfizer.h +++ b/dlinear/symbolic/TseitinCnfizer.h @@ -23,7 +23,7 @@ namespace dlinear { * The method can introduce extra Boolean variables. * Check [Wikipedia](https://en.wikipedia.org/wiki/Tseytin_transformation) for more information. */ -class TseitinCnfizer : public FormulaVisitor { +class TseitinCnfizer : public FormulaVisitor &> { public: /** * Construct a new TseitinCnfizer object with the given @p config. @@ -36,26 +36,16 @@ class TseitinCnfizer : public FormulaVisitor { * @param f formula to convert * @return vector of equi-satisfiable formulae in CNF */ - std::vector Convert(const Formula &f); - - /** - * @getter{map of temporary variables, TseitinCnfizer, @note @ref map_ is cleared at the beginning of @ref Convert } - */ - [[nodiscard]] const std::map &map() const { return map_; } + [[nodiscard]] std::vector Process(const Formula &f) const; + [[nodiscard]] std::vector operator()(const Formula &f) const; private: - Formula VisitConjunction(const Formula &f) override; - Formula VisitDisjunction(const Formula &f) override; - Formula VisitNegation(const Formula &f) override; - Formula VisitForall(const Formula &f) override; - - /** - * Map a temporary variable, which is introduced by a Tseitin transformation, to a corresponding Formula. - * @note that this map_ is cleared at the beginning of @ref Convert call. - */ - std::map map_; + [[nodiscard]] Formula VisitConjunction(const Formula &f, std::map &map) const override; + [[nodiscard]] Formula VisitDisjunction(const Formula &f, std::map &map) const override; + [[nodiscard]] Formula VisitNegation(const Formula &f, std::map &map) const override; + [[nodiscard]] Formula VisitForall(const Formula &f, std::map &map) const override; - NaiveCnfizer naive_cnfizer_; ///< Naive CNFizer. Transforms nested formulas inside universal quantification. + const NaiveCnfizer naive_cnfizer_; ///< Naive CNFizer. Transforms nested formulas inside universal quantification. }; } // namespace dlinear diff --git a/test/solver/TestBoundPreprocessor.cpp b/test/solver/TestBoundPreprocessor.cpp index 728e1e5..ff93728 100644 --- a/test/solver/TestBoundPreprocessor.cpp +++ b/test/solver/TestBoundPreprocessor.cpp @@ -39,7 +39,7 @@ class MockContextBoundPreprocessor : public BoundPreprocessor { private: Formula Flatten(const Formula &formula) { PredicateAbstractor pa{config()}; - const Variable var = get_variable(pa.Convert(formula)); + const Variable var = get_variable(pa.Process(formula)); return pa.var_to_formula_map().at(var); } }; @@ -65,7 +65,7 @@ class TestBoundPreprocessor : public ::testing::Test { void AddConstraints(std::initializer_list formulas) { for (const auto &formula : formulas) { for (const Variable &var : formula.GetFreeVariables()) bound_preprocessor_.AddVariable(var); - const Formula flattened = pa_.Convert(formula); + const Formula flattened = pa_.Process(formula); const Variable &var = is_negation(flattened) ? get_variable(get_operand(flattened)) : get_variable(flattened); const Literal lit{var, !is_negation(flattened)}; bound_preprocessor_.EnableLiteral(lit); diff --git a/test/symbolic/TestNnfizer.cpp b/test/symbolic/TestNnfizer.cpp index 5665788..0c855e0 100644 --- a/test/symbolic/TestNnfizer.cpp +++ b/test/symbolic/TestNnfizer.cpp @@ -21,64 +21,64 @@ class NnfizerTest : public ::testing::Test { const Variable b3_{"b3", Variable::Type::BOOLEAN}; const Config config_{}; - const Nnfizer converter_{config_}; + const Nnfizer nnfizer_{config_}; }; TEST_F(NnfizerTest, NNFNoChanges) { // No Changes: True - EXPECT_PRED2(FormulaEqual, converter_.Convert(Formula::True()), Formula::True()); + EXPECT_PRED2(FormulaEqual, nnfizer_(Formula::True()), Formula::True()); // No Changes: False - EXPECT_PRED2(FormulaEqual, converter_.Convert(Formula::False()), Formula::False()); + EXPECT_PRED2(FormulaEqual, nnfizer_(Formula::False()), Formula::False()); // No Changes: Variables - EXPECT_PRED2(FormulaEqual, converter_.Convert(Formula{b1_}), Formula{b1_}); - EXPECT_PRED2(FormulaEqual, converter_.Convert(!b1_), !b1_); + EXPECT_PRED2(FormulaEqual, nnfizer_(Formula{b1_}), Formula{b1_}); + EXPECT_PRED2(FormulaEqual, nnfizer_(!b1_), !b1_); // No Changes: x ≥ y ∧ y ≤ z const Formula f1{x_ >= y_ && y_ <= z_}; - EXPECT_PRED2(FormulaEqual, converter_.Convert(f1), f1); + EXPECT_PRED2(FormulaEqual, nnfizer_(f1), f1); // No Changes.: x > y ∨ y < z const Formula f2{x_ > y_ || y_ < z_}; - EXPECT_PRED2(FormulaEqual, converter_.Convert(f2), f2); + EXPECT_PRED2(FormulaEqual, nnfizer_(f2), f2); // No Changes: ∀x. x + y ≥ x const Formula f4{forall({x_}, x_ + y_ >= x_)}; - EXPECT_PRED2(FormulaEqual, converter_.Convert(f4), f4); - EXPECT_PRED2(FormulaEqual, converter_.Convert(!f4), !f4); + EXPECT_PRED2(FormulaEqual, nnfizer_(f4), f4); + EXPECT_PRED2(FormulaEqual, nnfizer_(!f4), !f4); } TEST_F(NnfizerTest, NNFRelational) { // ¬(x ≥ y) ∧ ¬(y ≤ z) ==> ¬(x ≥ y) ∧ ¬(y ≤ z) - EXPECT_PRED2(FormulaEqual, converter_.Convert(!(x_ >= y_) && !(y_ <= z_)), !(x_ >= y_) && !(y_ <= z_)); + EXPECT_PRED2(FormulaEqual, nnfizer_(!(x_ >= y_) && !(y_ <= z_)), !(x_ >= y_) && !(y_ <= z_)); // ¬(x ≥ y ∧ y ≤ z) ==> ¬(x ≥ y) ∨ ¬(y ≤ z) - EXPECT_PRED2(FormulaEqual, converter_.Convert(!(x_ >= y_ && y_ <= z_)), !(x_ >= y_) || !(y_ <= z_)); + EXPECT_PRED2(FormulaEqual, nnfizer_(!(x_ >= y_ && y_ <= z_)), !(x_ >= y_) || !(y_ <= z_)); // ¬(x > y) ∨ ¬(y < z) ==> ¬(x > y) ∨ ¬(y < z) - EXPECT_PRED2(FormulaEqual, converter_.Convert(!(x_ > y_) || !(y_ < z_)), !(x_ > y_) || !(y_ < z_)); + EXPECT_PRED2(FormulaEqual, nnfizer_(!(x_ > y_) || !(y_ < z_)), !(x_ > y_) || !(y_ < z_)); // ¬(x > y ∨ y < z) ==> ¬(x > y) ∧ ¬(y < z) - EXPECT_PRED2(FormulaEqual, converter_.Convert(!(x_ > y_ || y_ < z_)), !(x_ > y_) && !(y_ < z_)); + EXPECT_PRED2(FormulaEqual, nnfizer_(!(x_ > y_ || y_ < z_)), !(x_ > y_) && !(y_ < z_)); // ¬(x ≠ y) ∧ ¬(y = z) ==> ¬(x ≠ y) ∧ ¬(y = z) - EXPECT_PRED2(FormulaEqual, converter_.Convert(!(x_ != y_) && !(y_ == z_)), !(x_ != y_) && !(y_ == z_)); + EXPECT_PRED2(FormulaEqual, nnfizer_(!(x_ != y_) && !(y_ == z_)), !(x_ != y_) && !(y_ == z_)); // ¬(x ≠ y ∧ y = z) ==> ¬(x ≠ y) ∧ ¬(y = z) - EXPECT_PRED2(FormulaEqual, converter_.Convert(!(x_ != y_ && y_ == z_)), !(x_ != y_) || !(y_ == z_)); + EXPECT_PRED2(FormulaEqual, nnfizer_(!(x_ != y_ && y_ == z_)), !(x_ != y_) || !(y_ == z_)); } TEST_F(NnfizerTest, NNFBoolean) { // ¬(b₁ ∨ ¬(b₂ ∧ b₃)) ==> ¬b₁ ∧ b₂ ∧ b₃ - EXPECT_PRED2(FormulaEqual, converter_.Convert(!(b1_ || !(b2_ && b3_))), !b1_ && b2_ && b3_); + EXPECT_PRED2(FormulaEqual, nnfizer_(!(b1_ || !(b2_ && b3_))), !b1_ && b2_ && b3_); // ¬(b₁ ∨ ¬(b₂ ∨ b₃)) ==> ¬b₁ ∧ (b₂ ∨ b₃) - EXPECT_PRED2(FormulaEqual, converter_.Convert(!(b1_ || !(b2_ || b3_))), !b1_ && (b2_ || b3_)); + EXPECT_PRED2(FormulaEqual, nnfizer_(!(b1_ || !(b2_ || b3_))), !b1_ && (b2_ || b3_)); // ¬(b₁ ∧ ¬(b₂ ∨ b₃)) ==> ¬b₁ ∨ b₂ ∨ b₃ - EXPECT_PRED2(FormulaEqual, converter_.Convert(!(b1_ && !(b2_ || b3_))), !b1_ || b2_ || b3_); + EXPECT_PRED2(FormulaEqual, nnfizer_(!(b1_ && !(b2_ || b3_))), !b1_ || b2_ || b3_); // ¬(b₁ ∧ ¬(b₂ ∧ b₃)) ==> ¬b₁ ∨ (b₂ ∧ b₃) - EXPECT_PRED2(FormulaEqual, converter_.Convert(!(b1_ && !(b2_ && b3_))), !b1_ || (b2_ && b3_)); + EXPECT_PRED2(FormulaEqual, nnfizer_(!(b1_ && !(b2_ && b3_))), !b1_ || (b2_ && b3_)); } \ No newline at end of file diff --git a/test/symbolic/TestPlaistedGreenbaumCnfizer.cpp b/test/symbolic/TestPlaistedGreenbaumCnfizer.cpp index 1771ba2..2fedb05 100644 --- a/test/symbolic/TestPlaistedGreenbaumCnfizer.cpp +++ b/test/symbolic/TestPlaistedGreenbaumCnfizer.cpp @@ -36,7 +36,7 @@ class PlaistedGreenbaumCnfizerTest : public ::testing::Test { protected: ::testing::AssertionResult CnfChecker(const Formula &f) { - const vector clauses{cnfizer_.Convert(f)}; + const auto [clauses, aux]{cnfizer_(f)}; const Formula f_cnf{make_conjunction(set{clauses.begin(), clauses.end()})}; // Check1: f_cnf should be in CNF. if (!is_cnf(f_cnf)) { diff --git a/test/symbolic/TestPredicateAbstractor.cpp b/test/symbolic/TestPredicateAbstractor.cpp index c49ef4d..e296c1e 100644 --- a/test/symbolic/TestPredicateAbstractor.cpp +++ b/test/symbolic/TestPredicateAbstractor.cpp @@ -31,27 +31,27 @@ class TestPredicateAbstractor : public ::testing::Test { TEST_F(TestPredicateAbstractor, False) { // False <-> False - const Formula abstracted{abstractor_.Convert(Formula::False())}; + const Formula abstracted{abstractor_.Process(Formula::False())}; EXPECT_TRUE(is_false(abstracted)); } TEST_F(TestPredicateAbstractor, True) { // True <-> True - const Formula abstracted{abstractor_.Convert(Formula::True())}; + const Formula abstracted{abstractor_.Process(Formula::True())}; EXPECT_TRUE(is_true(abstracted)); } TEST_F(TestPredicateAbstractor, Variable) { // b <-> b const Formula f{b1_}; - const Formula f_abstracted{abstractor_.Convert(f)}; + const Formula f_abstracted{abstractor_.Process(f)}; EXPECT_PRED2(FormulaEqual, f, f_abstracted); } TEST_F(TestPredicateAbstractor, Eq) { // x + y == 10 <-> b const Formula f{x_ + y_ == 10}; - const Formula f_abstracted{abstractor_.Convert(f)}; + const Formula f_abstracted{abstractor_.Process(f)}; EXPECT_FALSE(is_variable(f)); ASSERT_TRUE(is_variable(f_abstracted)); @@ -65,7 +65,7 @@ TEST_F(TestPredicateAbstractor, Eq) { TEST_F(TestPredicateAbstractor, Neq) { // x + y != 10 <-> !(x + y == 10) const Formula f{x_ + y_ != 10}; - const Formula f_abstracted{abstractor_.Convert(f)}; + const Formula f_abstracted{abstractor_(f)}; EXPECT_FALSE(is_variable(f)); ASSERT_TRUE(is_negation(f_abstracted)); @@ -80,7 +80,7 @@ TEST_F(TestPredicateAbstractor, Neq) { TEST_F(TestPredicateAbstractor, Gt) { // x + y > 10 <-> !(x + y <= 10) const Formula f{x_ + y_ > 10}; - const Formula f_abstracted{abstractor_.Convert(f)}; + const Formula f_abstracted{abstractor_(f)}; EXPECT_FALSE(is_variable(f)); ASSERT_TRUE(is_negation(f_abstracted)); @@ -95,7 +95,7 @@ TEST_F(TestPredicateAbstractor, Gt) { TEST_F(TestPredicateAbstractor, Geq) { // x + y >= 10 <-> !(x + y < 10) const Formula f{x_ + y_ >= 10}; - const Formula f_abstracted{abstractor_.Convert(f)}; + const Formula f_abstracted{abstractor_(f)}; EXPECT_FALSE(is_variable(f)); ASSERT_TRUE(is_negation(f_abstracted)); @@ -110,7 +110,7 @@ TEST_F(TestPredicateAbstractor, Geq) { TEST_F(TestPredicateAbstractor, Lt) { // x + y < 10 <-> b const Formula f{x_ + y_ < 10}; - const Formula f_abstracted{abstractor_.Convert(f)}; + const Formula f_abstracted{abstractor_(f)}; EXPECT_FALSE(is_variable(f)); ASSERT_TRUE(is_variable(f_abstracted)); @@ -124,7 +124,7 @@ TEST_F(TestPredicateAbstractor, Lt) { TEST_F(TestPredicateAbstractor, Leq) { // x + y <= 10 <-> b const Formula f{x_ + y_ <= 10}; - const Formula f_abstracted{abstractor_.Convert(f)}; + const Formula f_abstracted{abstractor_(f)}; EXPECT_FALSE(is_variable(f)); ASSERT_TRUE(is_variable(f_abstracted)); @@ -144,7 +144,7 @@ TEST_F(TestPredicateAbstractor, Conjunction) { const Formula conjunction{f1 && f2 && f3 && f4}; const set operands{get_operands(conjunction)}; - const Formula conjunction_abstracted{abstractor_.Convert(conjunction)}; + const Formula conjunction_abstracted{abstractor_(conjunction)}; ASSERT_TRUE(is_conjunction(conjunction_abstracted)); const set operands_abstracted{get_operands(conjunction_abstracted)}; EXPECT_EQ(operands_abstracted.size(), operands.size()); @@ -174,7 +174,7 @@ TEST_F(TestPredicateAbstractor, Disjunction) { const Formula disjunction{f1 || f2 || f3 || f4}; const set operands{get_operands(disjunction)}; - const Formula disjunction_abstracted{abstractor_.Convert(disjunction)}; + const Formula disjunction_abstracted{abstractor_(disjunction)}; ASSERT_TRUE(is_disjunction(disjunction_abstracted)); const set operands_abstracted{get_operands(disjunction_abstracted)}; EXPECT_EQ(operands_abstracted.size(), operands.size()); @@ -192,7 +192,7 @@ TEST_F(TestPredicateAbstractor, Negation) { // !(x + y >= 10) <-> x + y < 10 const Formula f{x_ + y_ >= 10}; const Formula not_f{!f}; - const Formula not_f_abstracted{abstractor_.Convert(not_f)}; + const Formula not_f_abstracted{abstractor_(not_f)}; ASSERT_TRUE(is_variable(not_f_abstracted)); const Variable &var{get_variable(not_f_abstracted)}; @@ -204,7 +204,7 @@ TEST_F(TestPredicateAbstractor, Negation) { TEST_F(TestPredicateAbstractor, Forall) { // (∀x. x >= 0) <-> b const Formula f{forall({x_}, x_ >= 0)}; - const Formula f_abstracted{abstractor_.Convert(f)}; + const Formula f_abstracted{abstractor_(f)}; ASSERT_TRUE(is_variable(f_abstracted)); const Variable &var{get_variable(f_abstracted)}; EXPECT_EQ(var.get_type(), Variable::Type::BOOLEAN); diff --git a/test/symbolic/TestTseitinCnfizer.cpp b/test/symbolic/TestTseitinCnfizer.cpp index 5c049bc..20bfe04 100644 --- a/test/symbolic/TestTseitinCnfizer.cpp +++ b/test/symbolic/TestTseitinCnfizer.cpp @@ -36,7 +36,7 @@ class TestTseitinCnfizer : public ::testing::Test { protected: ::testing::AssertionResult CnfChecker(const Formula &f) { - const vector clauses{cnfizer_.Convert(f)}; + const vector clauses{cnfizer_.Process(f)}; const Formula f_cnf{make_conjunction(set{clauses.begin(), clauses.end()})}; // Check1: f_cnf should be in CNF. if (!is_cnf(f_cnf)) {