From c8c9067c9b5ab1d7a9c17cdefee78b4fa392df00 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 2 Mar 2022 18:56:37 +0100 Subject: [PATCH] more code --- libsmtutil/SolverInterface.h | 10 +++++++ libsolutil/BooleanLP.cpp | 55 ++++++++++++------------------------ libsolutil/BooleanLP.h | 3 +- 3 files changed, 29 insertions(+), 39 deletions(-) diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index ca4c497de..4eaebf46a 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -24,6 +24,7 @@ #include #include #include +#include #include #include @@ -489,6 +490,15 @@ public: std::vector arguments; SortPointer sort; + std::string toString() const + { + if (arguments.empty()) + return name; + std::vector argsAsString; + for (auto const& arg: arguments) + argsAsString.emplace_back(arg.toString()); + return name + "(" + util::joinHumanReadable(argsAsString) + ")"; + } private: /// Manual constructors, should only be used by SolverInterface and this class itself. Expression(std::string _name, std::vector _arguments, Kind _kind): diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index efc731915..6f424b505 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -97,6 +97,7 @@ void BooleanLPSolver::declareVariable(string const& _name, SortPointer const& _s void BooleanLPSolver::addAssertion(Expression const& _expr) { + cout << " - " << _expr.toString() << endl; solAssert(_expr.sort->kind == Kind::Bool); if (_expr.arguments.empty()) { @@ -137,9 +138,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr) } else { - Expression left = parseLinearSumOrReturnEqualVariable(_expr.arguments.at(0)); - Expression right = parseLinearSumOrReturnEqualVariable(_expr.arguments.at(1)); - addAssertion(left == right); + solAssert(false); } } else @@ -184,9 +183,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr) } else { - Expression left = parseLinearSumOrReturnEqualVariable(_expr.arguments.at(0)); - Expression right = parseLinearSumOrReturnEqualVariable(_expr.arguments.at(1)); - addAssertion(left <= right); + solAssert(false); } } else if (_expr.name == ">=") @@ -202,9 +199,9 @@ void BooleanLPSolver::addAssertion(Expression const& _expr) pair> BooleanLPSolver::check(vector const&) { - //cout << "Solving boolean constraint system" << endl; - //cout << toString() << endl; - //cout << "--------------" << endl; + cout << "Solving boolean constraint system" << endl; + cout << toString() << endl; + cout << "--------------" << endl; if (state().infeasible) return make_pair(CheckResult::UNSATISFIABLE, vector{}); @@ -270,7 +267,8 @@ pair> BooleanLPSolver::check(vector cons { //cout << "==============> CDCL final result: SATisfiable / UNKNOWN." << endl; // TODO should be "unknown" later on - return {CheckResult::SATISFIABLE, {}}; + //return {CheckResult::SATISFIABLE, {}}; + return {CheckResult::UNKNOWN, {}}; } } @@ -374,6 +372,8 @@ Literal BooleanLPSolver::negate(Literal const& _lit) Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _expr) { + if (_expr.sort->kind != Kind::Bool) + cout << "expected bool: " << _expr.toString() << endl; solAssert(_expr.sort->kind == Kind::Bool); // TODO when can this fail? if (optional literal = parseLiteral(_expr)) @@ -386,31 +386,7 @@ Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _exp } } -Expression BooleanLPSolver::parseLinearSumOrReturnEqualVariable(Expression const& _expr) -{ - solAssert(_expr.sort->kind == Kind::Int); - if (_expr.name == "ite") - { - Literal condition = parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0)); - // TODO this adds too many variables - Expression conditionBoolean = declareInternalVariable(true); - addBooleanEquality(condition, conditionBoolean); - Expression trueValue = parseLinearSumOrReturnEqualVariable(_expr.arguments.at(1)); - Expression falseValue = parseLinearSumOrReturnEqualVariable(_expr.arguments.at(2)); - Expression result = declareInternalVariable(false); - addAssertion(conditionBoolean || (result == trueValue)); - addAssertion(!conditionBoolean || (result == falseValue)); - return result; - } - if (_expr.arguments.empty()) - return _expr; - solAssert(parseLinearSum(_expr)); - Expression result = declareInternalVariable(false); - addAssertion(result == _expr); - return result; -} - -optional BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr) const +optional BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr) { if (_expr.arguments.empty() || _expr.name == "*") return parseProduct(_expr); @@ -422,10 +398,15 @@ optional BooleanLPSolver::parseLinearSum(smtutil::Expression c return std::nullopt; return _expr.name == "+" ? *left + *right : *left - *right; } + else if (_expr.name == "ite") + { + Expression result = declareInternalVariable(false); + addAssertion(_expr.arguments.at(0) || (result == _expr.arguments.at(1))); + addAssertion(!_expr.arguments.at(0) || (result == _expr.arguments.at(2))); + return parseLinearSum(result); + } else { - // TOOD This should just resort to parseLinearSumOrReturn... - // and then use that variable cout << "Invalid operator " << _expr.name << endl; return std::nullopt; } diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h index 6d1fc8b05..c207657b0 100644 --- a/libsolutil/BooleanLP.h +++ b/libsolutil/BooleanLP.h @@ -87,14 +87,13 @@ private: Literal negate(Literal const& _lit); Literal parseLiteralOrReturnEqualBoolean(smtutil::Expression const& _expr); - smtutil::Expression parseLinearSumOrReturnEqualVariable(smtutil::Expression const& _expr); /// Parses the expression and expects a linear sum of variables. /// Returns a vector with the first element being the constant and the /// other elements the factors for the respective variables. /// If the expression cannot be properly parsed or is not linear, /// returns an empty vector. - std::optional parseLinearSum(smtutil::Expression const& _expression) const; + std::optional parseLinearSum(smtutil::Expression const& _expression); std::optional parseProduct(smtutil::Expression const& _expression) const; std::optional parseFactor(smtutil::Expression const& _expression) const;