From 973442c2063ff6b10b7a8b23be82396ad56c5296 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 30 May 2022 18:11:40 +0200 Subject: [PATCH] Parse let bindigns of literals speciall. --- libsolutil/BooleanLP.cpp | 97 ++++++++++++++++++++++++++++++---------- libsolutil/BooleanLP.h | 17 ++++--- libsolutil/LP.cpp | 2 + 3 files changed, 86 insertions(+), 30 deletions(-) diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index 853abb8b5..090bf7b78 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -46,6 +46,8 @@ using namespace solidity::smtutil; using rational = boost::rational; +//#define DEBUG + namespace { template @@ -230,7 +232,7 @@ string BooleanLPSolver::toString() const return result; } -void BooleanLPSolver::addAssertion(Expression const& _expr, map _letBindings) +void BooleanLPSolver::addAssertion(Expression const& _expr, map _letBindings) { #ifdef DEBUG cerr << "adding assertion" << endl; @@ -239,9 +241,23 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map solAssert(_expr.sort->kind == Kind::Bool); if (_expr.arguments.empty()) { - size_t index = _letBindings.count(_expr.name) ? _letBindings.at(_expr.name) : state().variables.at(_expr.name); - solAssert(isBooleanVariable(index)); - state().clauses.emplace_back(Clause{Literal{true, index }}); + size_t varIndex = 0; + if (_letBindings.count(_expr.name)) + { + LetBinding binding = _letBindings.at(_expr.name); + if (holds_alternative(binding)) + { + addAssertion(std::get(binding), move(_letBindings)); + return; + } + else + varIndex = std::get(binding); + } + else + varIndex = state().variables.at(_expr.name); + solAssert(varIndex > 0, ""); + solAssert(isBooleanVariable(varIndex)); + state().clauses.emplace_back(Clause{Literal{true, varIndex}}); } else if (_expr.name == "let") { @@ -360,23 +376,28 @@ void BooleanLPSolver::declareVariable(string const& _name, bool _boolean) resizeAndSet(state().isBooleanVariable, index, _boolean); } -void BooleanLPSolver::addLetBindings(Expression const& _let, map& _letBindings) +void BooleanLPSolver::addLetBindings(Expression const& _let, map& _letBindings) { - map newBindings; + map newBindings; solAssert(_let.name == "let"); for (size_t i = 0; i < _let.arguments.size() - 1; i++) { Expression binding = _let.arguments.at(i); bool isBool = binding.arguments.at(0).sort->kind == Kind::Bool; - Expression var = declareInternalVariable(isBool); - newBindings.insert({binding.name, state().variables.at(var.name)}); - addAssertion(var == binding.arguments.at(0), _letBindings); + if (isLiteral(binding.arguments.at(0))) + newBindings.insert({binding.name, binding.arguments.at(0)}); + else + { + Expression var = declareInternalVariable(isBool); + newBindings.insert({binding.name, state().variables.at(var.name)}); + addAssertion(var == binding.arguments.at(0), _letBindings); + } } - for (auto&& [name, varIndex]: newBindings) - _letBindings.insert({name, varIndex}); + for (auto& [name, value]: newBindings) + _letBindings.insert({name, move(value)}); } -optional BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr, map _letBindings) +optional BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr, map _letBindings) { // TODO constanst true/false? @@ -388,9 +409,19 @@ optional BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr if (_expr.arguments.empty()) { - size_t index = _letBindings.count(_expr.name) ? _letBindings.at(_expr.name) : state().variables.at(_expr.name); - solAssert(isBooleanVariable(index)); - return Literal{true, index}; + size_t varIndex = 0; + if (_letBindings.count(_expr.name)) + { + LetBinding binding = _letBindings.at(_expr.name); + if (holds_alternative(binding)) + return parseLiteral(std::get(binding), move(_letBindings)); + else + varIndex = std::get(binding); + } + else + varIndex = state().variables.at(_expr.name); + solAssert(isBooleanVariable(varIndex)); + return Literal{true, varIndex}; } else if (_expr.name == "not") return negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0), move(_letBindings))); @@ -487,7 +518,7 @@ Literal BooleanLPSolver::negate(Literal const& _lit) return ~_lit; } -Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _expr, map _letBindings) +Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _expr, map _letBindings) { if (_expr.sort->kind != Kind::Bool) cerr << "expected bool: " << _expr.toString() << endl; @@ -503,7 +534,7 @@ Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _exp } } -optional BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr, map _letBindings) +optional BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr, map _letBindings) { if (_expr.name == "let") { @@ -577,8 +608,18 @@ optional BooleanLPSolver::parseLinearSum(smtutil::Expression c } } +bool BooleanLPSolver::isLiteral(smtutil::Expression const& _expr) const +{ + if (!_expr.arguments.empty()) + return false; + solAssert(!_expr.name.empty(), ""); + return + ('0' <= _expr.name[0] && _expr.name[0] <= '9') || + _expr.name == "true" || + _expr.name == "false"; +} -optional BooleanLPSolver::parseFactor(smtutil::Expression const& _expr, map _letBindings) const +optional BooleanLPSolver::parseFactor(smtutil::Expression const& _expr, map _letBindings) const { solAssert(_expr.arguments.empty(), ""); solAssert(!_expr.name.empty(), ""); @@ -591,11 +632,21 @@ optional BooleanLPSolver::parseFactor(smtutil::Expression cons // TODO do we want to do this? return LinearExpression::constant(0); - size_t index = _letBindings.count(_expr.name) ? _letBindings.at(_expr.name) : state().variables.at(_expr.name); - solAssert(index > 0, ""); - if (isBooleanVariable(index)) + size_t varIndex = 0; + if (_letBindings.count(_expr.name)) + { + LetBinding binding = _letBindings.at(_expr.name); + if (holds_alternative(binding)) + return parseFactor(std::get(binding), move(_letBindings)); + else + varIndex = std::get(binding); + } + else + varIndex = state().variables.at(_expr.name); + solAssert(varIndex > 0, ""); + if (isBooleanVariable(varIndex)) return nullopt; - return LinearExpression::factorForVariable(index, rational(bigint(1))); + return LinearExpression::factorForVariable(varIndex, rational(bigint(1))); } bool BooleanLPSolver::tryAddDirectBounds(Constraint const& _constraint) @@ -666,7 +717,7 @@ size_t BooleanLPSolver::addConditionalConstraint(Constraint _constraint) return index; } -void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expression const& _right, map _letBindings) +void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expression const& _right, map _letBindings) { solAssert(_right.sort->kind == Kind::Bool); if (optional right = parseLiteral(_right, _letBindings)) diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h index 186b3bd98..64883943a 100644 --- a/libsolutil/BooleanLP.h +++ b/libsolutil/BooleanLP.h @@ -52,6 +52,7 @@ struct State std::vector fixedConstraints; }; + /** * Component that satisfies the SMT SolverInterface and uses an LP solver plus the CDCL * algorithm internally. @@ -82,28 +83,29 @@ public: private: using rational = boost::rational; + using LetBinding = std::variant; void addAssertion( smtutil::Expression const& _expr, - std::map _letBindings + std::map _letBindings ); smtutil::Expression declareInternalVariable(bool _boolean); void declareVariable(std::string const& _name, bool _boolean); /// Handles a "let" expression and adds the bindings to @a _letBindings. - void addLetBindings(smtutil::Expression const& _let, std::map& _letBindings); + void addLetBindings(smtutil::Expression const& _let, std::map& _letBindings); /// Parses an expression of sort bool and returns a literal. std::optional parseLiteral( smtutil::Expression const& _expr, - std::map _letBindings + std::map _letBindings ); Literal negate(Literal const& _lit); Literal parseLiteralOrReturnEqualBoolean( smtutil::Expression const& _expr, - std::map _letBindings + std::map _letBindings ); /// Parses the expression and expects a linear sum of variables. @@ -111,8 +113,9 @@ private: /// 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, std::map _letBindings); - std::optional parseFactor(smtutil::Expression const& _expression, std::map _letBindings) const; + std::optional parseLinearSum(smtutil::Expression const& _expression, std::map _letBindings); + bool isLiteral(smtutil::Expression const& _expression) const; + std::optional parseFactor(smtutil::Expression const& _expression, std::map _letBindings) const; bool tryAddDirectBounds(Constraint const& _constraint); void addUpperBound(size_t _index, RationalWithDelta _value); @@ -120,7 +123,7 @@ private: size_t addConditionalConstraint(Constraint _constraint); - void addBooleanEquality(Literal const& _left, smtutil::Expression const& _right, std::map _letBindings); + void addBooleanEquality(Literal const& _left, smtutil::Expression const& _right, std::map _letBindings); //std::string toString(std::vector const& _bounds) const; std::string toString(Clause const& _clause) const; diff --git a/libsolutil/LP.cpp b/libsolutil/LP.cpp index 62ead4dac..8d160ec92 100644 --- a/libsolutil/LP.cpp +++ b/libsolutil/LP.cpp @@ -43,6 +43,8 @@ #include #include +//#define DEBUG + using namespace std; using namespace solidity; using namespace solidity::util;