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

true/false literals.

Browse Source
This commit is contained in:
chriseth 2022-06-01 23:31:33 +02:00
parent 5c1ecce2a3
commit 0e06440153
2 changed files with 17 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
libsolutil/BooleanLP.cpp
View File

@ -241,6 +241,11 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, LetBindings _letBind
solAssert(_expr.sort->kind == Kind::Bool);
if (_expr.arguments.empty())
{
if (_expr.name == "true")
return;
else if (_expr.name == "false")
solAssert(false, "Adding false as top-level assertion.");
size_t varIndex = 0;
if (_letBindings->count(_expr.name))
{
@ -430,8 +435,16 @@ optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr
}
else if (_expr.name == "true" || _expr.name == "false")
{
// TODO handle this better
solAssert(false, "True/false literals not implemented");
// TODO handle this better, we can introduce some shortcuts if we propagate this up.
// Also we should maybe not create a new variable each time.
if (!state().trueConstant)
{
Expression var = declareInternalVariable(true);
addAssertion(var, make_shared<map<string, LetBinding>>());
state().trueConstant = parseLiteral(var, make_shared<map<string, LetBinding>>())->variable;
}
return Literal{_expr.name == "true", *state().trueConstant};
}
else
varIndex = state().variables.at(_expr.name);

2
libsolutil/BooleanLP.h
View File

@ -39,6 +39,8 @@ struct State
// Potential constraints, referenced through clauses
std::map<size_t, Constraint> conditionalConstraints;
std::vector<Clause> clauses;
/// The variable index of a bool variable that is always true.
std::optional<size_t> trueConstant;
struct Bounds
{