From 0f4cc056678f74f185ebad626d41cb6c65422177 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 30 May 2022 19:37:20 +0200 Subject: [PATCH] Copy-on-write let bindings. --- libsolutil/BooleanLP.cpp | 35 ++++++++++++++++++----------------- libsolutil/BooleanLP.h | 26 ++++++++++++-------------- libsolutil/LP.h | 2 +- 3 files changed, 31 insertions(+), 32 deletions(-) diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index 55f27acc9..22466c03f 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -232,7 +232,7 @@ string BooleanLPSolver::toString() const return result; } -void BooleanLPSolver::addAssertion(Expression const& _expr, map _letBindings) +void BooleanLPSolver::addAssertion(Expression const& _expr, LetBindings _letBindings) { #ifdef DEBUG cerr << "adding assertion" << endl; @@ -242,9 +242,9 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, mapcount(_expr.name)) { - LetBinding binding = _letBindings.at(_expr.name); + LetBinding binding = _letBindings->at(_expr.name); if (holds_alternative(binding)) { addAssertion(std::get(binding), move(_letBindings)); @@ -276,7 +276,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map>()); addBooleanEquality(newBoolean, _expr.arguments.at(0), _letBindings); addBooleanEquality(newBoolean, _expr.arguments.at(1), _letBindings); } @@ -382,7 +382,7 @@ 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, LetBindings& _letBindings) { map newBindings; solAssert(_let.name == "let"); @@ -399,11 +399,12 @@ void BooleanLPSolver::addLetBindings(Expression const& _let, map>(*_letBindings); for (auto& [name, value]: newBindings) - _letBindings.insert({name, move(value)}); + _letBindings->insert({name, move(value)}); } -optional BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr, map _letBindings) +optional BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr, LetBindings _letBindings) { // TODO constanst true/false? @@ -416,9 +417,9 @@ optional BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr if (_expr.arguments.empty()) { size_t varIndex = 0; - if (_letBindings.count(_expr.name)) + if (_letBindings->count(_expr.name)) { - LetBinding binding = _letBindings.at(_expr.name); + LetBinding binding = _letBindings->at(_expr.name); if (holds_alternative(binding)) return parseLiteral(std::get(binding), move(_letBindings)); else @@ -494,7 +495,7 @@ Literal BooleanLPSolver::negate(Literal const& _lit) gt.data *= -1; Literal gtL{true, addConditionalConstraint(gt)}; - Literal equalBoolean = *parseLiteral(declareInternalVariable(true), {}); + Literal equalBoolean = *parseLiteral(declareInternalVariable(true), make_shared>()); // a = or(x, y) <=> (-a \/ x \/ y) /\ (a \/ -x) /\ (a \/ -y) state().clauses.emplace_back(Clause{vector{negate(equalBoolean), ltL, gtL}}); state().clauses.emplace_back(Clause{vector{equalBoolean, negate(ltL)}}); @@ -524,7 +525,7 @@ Literal BooleanLPSolver::negate(Literal const& _lit) return ~_lit; } -Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _expr, map _letBindings) +Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _expr, LetBindings _letBindings) { if (_expr.sort->kind != Kind::Bool) cerr << "expected bool: " << _expr.toString() << endl; @@ -540,7 +541,7 @@ Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _exp } } -optional BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr, map _letBindings) +optional BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr, LetBindings _letBindings) { if (_expr.name == "let") { @@ -604,7 +605,7 @@ optional BooleanLPSolver::parseLinearSum(smtutil::Expression c Expression result = declareInternalVariable(false); addAssertion(!_expr.arguments.at(0) || (result == _expr.arguments.at(1)), _letBindings); addAssertion(_expr.arguments.at(0) || (result == _expr.arguments.at(2)), _letBindings); - return parseLinearSum(result, {}); + return parseLinearSum(result, make_shared>()); } else { @@ -625,7 +626,7 @@ bool BooleanLPSolver::isLiteral(smtutil::Expression const& _expr) const _expr.name == "false"; } -optional BooleanLPSolver::parseFactor(smtutil::Expression const& _expr, map _letBindings) const +optional BooleanLPSolver::parseFactor(smtutil::Expression const& _expr, LetBindings _letBindings) const { solAssert(_expr.arguments.empty(), ""); solAssert(!_expr.name.empty(), ""); @@ -639,9 +640,9 @@ optional BooleanLPSolver::parseFactor(smtutil::Expression cons return LinearExpression::constant(0); size_t varIndex = 0; - if (_letBindings.count(_expr.name)) + if (_letBindings->count(_expr.name)) { - LetBinding binding = _letBindings.at(_expr.name); + LetBinding binding = _letBindings->at(_expr.name); if (holds_alternative(binding)) return parseFactor(std::get(binding), move(_letBindings)); else @@ -723,7 +724,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, LetBindings _letBindings) { solAssert(_right.sort->kind == Kind::Bool); if (optional right = parseLiteral(_right, _letBindings)) diff --git a/libsolutil/BooleanLP.h b/libsolutil/BooleanLP.h index 64883943a..0b6163bd2 100644 --- a/libsolutil/BooleanLP.h +++ b/libsolutil/BooleanLP.h @@ -74,7 +74,10 @@ public: void declareVariable(std::string const& _name, smtutil::SortPointer const& _sort) override; - void addAssertion(smtutil::Expression const& _expr) override { addAssertion(_expr, {}); } + void addAssertion(smtutil::Expression const& _expr) override + { + addAssertion(_expr, std::make_shared>()); + } std::pair> check(std::vector const& _expressionsToEvaluate) override; @@ -84,38 +87,33 @@ public: private: using rational = boost::rational; using LetBinding = std::variant; + using LetBindings = std::shared_ptr>; void addAssertion( smtutil::Expression const& _expr, - std::map _letBindings + LetBindings _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, LetBindings& _letBindings); /// Parses an expression of sort bool and returns a literal. - std::optional parseLiteral( - smtutil::Expression const& _expr, - std::map _letBindings - ); + std::optional parseLiteral(smtutil::Expression const& _expr, LetBindings _letBindings); Literal negate(Literal const& _lit); - Literal parseLiteralOrReturnEqualBoolean( - smtutil::Expression const& _expr, - std::map _letBindings - ); + Literal parseLiteralOrReturnEqualBoolean(smtutil::Expression const& _expr, LetBindings _letBindings); /// 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, std::map _letBindings); + std::optional parseLinearSum(smtutil::Expression const& _expression, LetBindings _letBindings); bool isLiteral(smtutil::Expression const& _expression) const; - std::optional parseFactor(smtutil::Expression const& _expression, std::map _letBindings) const; + std::optional parseFactor(smtutil::Expression const& _expression, LetBindings _letBindings) const; bool tryAddDirectBounds(Constraint const& _constraint); void addUpperBound(size_t _index, RationalWithDelta _value); @@ -123,7 +121,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, LetBindings _letBindings); //std::string toString(std::vector const& _bounds) const; std::string toString(Clause const& _clause) const; diff --git a/libsolutil/LP.h b/libsolutil/LP.h index 617b483b5..d68c54697 100644 --- a/libsolutil/LP.h +++ b/libsolutil/LP.h @@ -298,7 +298,7 @@ public: void addLowerBound(size_t _variable, RationalWithDelta _bound, std::optional _reason = std::nullopt); void addUpperBound(size_t _variable, RationalWithDelta _bound, std::optional _reason = std::nullopt); - std::paircheck(); + std::pair check(); std::string toString() const; std::map model() const;