cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Parse let bindigns of literals speciall.

Browse Source
This commit is contained in:
chriseth 2022-05-30 18:11:40 +02:00
parent e655f53813
commit 973442c206
3 changed files with 86 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

91
libsolutil/BooleanLP.cpp
View File

@ -46,6 +46,8 @@ using namespace solidity::smtutil;
using rational = boost::rational<bigint>;
//#define DEBUG
namespace
{
template <class T>
@ -230,7 +232,7 @@ string BooleanLPSolver::toString() const
return result;
}
void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, size_t> _letBindings)
void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, LetBinding> _letBindings)
{
#ifdef DEBUG
cerr << "adding assertion" << endl;
@ -239,9 +241,23 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, size_t>
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<smtutil::Expression>(binding))
{
addAssertion(std::get<smtutil::Expression>(binding), move(_letBindings));
return;
}
else
varIndex = std::get<size_t>(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<string, size_t>& _letBindings)
void BooleanLPSolver::addLetBindings(Expression const& _let, map<string, LetBinding>& _letBindings)
{
map<string, size_t> newBindings;
map<string, LetBinding> 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;
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<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr, map<string, size_t> _letBindings)
optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr, map<string, LetBinding> _letBindings)
{
// TODO constanst true/false?
@ -388,9 +409,19 @@ optional<Literal> 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<smtutil::Expression>(binding))
return parseLiteral(std::get<smtutil::Expression>(binding), move(_letBindings));
else
varIndex = std::get<size_t>(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<string, size_t> _letBindings)
Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _expr, map<string, LetBinding> _letBindings)
{
if (_expr.sort->kind != Kind::Bool)
cerr << "expected bool: " << _expr.toString() << endl;
@ -503,7 +534,7 @@ Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _exp
}
}
optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr, map<string, size_t> _letBindings)
optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression const& _expr, map<string, LetBinding> _letBindings)
{
if (_expr.name == "let")
{
@ -577,8 +608,18 @@ optional<LinearExpression> 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<LinearExpression> BooleanLPSolver::parseFactor(smtutil::Expression const& _expr, map<string, size_t> _letBindings) const
optional<LinearExpression> BooleanLPSolver::parseFactor(smtutil::Expression const& _expr, map<string, LetBinding> _letBindings) const
{
solAssert(_expr.arguments.empty(), "");
solAssert(!_expr.name.empty(), "");
@ -591,11 +632,21 @@ optional<LinearExpression> 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<smtutil::Expression>(binding))
return parseFactor(std::get<smtutil::Expression>(binding), move(_letBindings));
else
varIndex = std::get<size_t>(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<string, size_t> _letBindings)
void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expression const& _right, map<string, LetBinding> _letBindings)
{
solAssert(_right.sort->kind == Kind::Bool);
if (optional<Literal> right = parseLiteral(_right, _letBindings))

17
libsolutil/BooleanLP.h
View File

@ -52,6 +52,7 @@ struct State
std::vector<Constraint> 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<bigint>;
using LetBinding = std::variant<size_t, smtutil::Expression>;
void addAssertion(
smtutil::Expression const& _expr,
std::map<std::string, size_t> _letBindings
std::map<std::string, LetBinding> _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<std::string, size_t>& _letBindings);
void addLetBindings(smtutil::Expression const& _let, std::map<std::string, LetBinding>& _letBindings);
/// Parses an expression of sort bool and returns a literal.
std::optional<Literal> parseLiteral(
smtutil::Expression const& _expr,
std::map<std::string, size_t> _letBindings
std::map<std::string, LetBinding> _letBindings
);
Literal negate(Literal const& _lit);
Literal parseLiteralOrReturnEqualBoolean(
smtutil::Expression const& _expr,
std::map<std::string, size_t> _letBindings
std::map<std::string, LetBinding> _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<LinearExpression> parseLinearSum(smtutil::Expression const& _expression, std::map<std::string, size_t> _letBindings);
std::optional<LinearExpression> parseFactor(smtutil::Expression const& _expression, std::map<std::string, size_t> _letBindings) const;
std::optional<LinearExpression> parseLinearSum(smtutil::Expression const& _expression, std::map<std::string, LetBinding> _letBindings);
bool isLiteral(smtutil::Expression const& _expression) const;
std::optional<LinearExpression> parseFactor(smtutil::Expression const& _expression, std::map<std::string, LetBinding> _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<std::string, size_t> _letBindings);
void addBooleanEquality(Literal const& _left, smtutil::Expression const& _right, std::map<std::string, LetBinding> _letBindings);
//std::string toString(std::vector<SolvingState::Bounds> const& _bounds) const;
std::string toString(Clause const& _clause) const;

2
libsolutil/LP.cpp
View File

@ -43,6 +43,8 @@
#include <optional>
#include <stack>
//#define DEBUG
using namespace std;
using namespace solidity;
using namespace solidity::util;