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

some more debugging output

Browse Source
This commit is contained in:
chriseth 2022-03-03 19:50:27 +01:00
parent c8c9067c9b
commit fe15610ba4
3 changed files with 12 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
libsmtutil/SolverInterface.h
View File

@ -497,7 +497,10 @@ public:
std::vector<std::string> argsAsString;
for (auto const& arg: arguments)
argsAsString.emplace_back(arg.toString());
return name + "(" + util::joinHumanReadable(argsAsString) + ")";
if (arguments.size() == 2)
return "(" + argsAsString[0] + " " + name + " " + argsAsString[1] + ")";
else
return name + "(" + util::joinHumanReadable(argsAsString) + ")";
}
private:
/// Manual constructors, should only be used by SolverInterface and this class itself.

1
libsolutil/BooleanLP.cpp
View File

@ -135,6 +135,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
Constraint c{move(data), _expr.name == "=", {}};
if (!tryAddDirectBounds(c))
state().fixedConstraints.emplace_back(move(c));
cout << "Added as fixed constraint" << endl;
}
else
{

7
libyul/optimiser/ReasoningBasedSimplifier.cpp
View File

@ -67,25 +67,31 @@ void ReasoningBasedSimplifier::operator()(If& _if)
if (!SideEffectsCollector{m_dialect, *_if.condition}.movable())
return;
cout << "Checking if condition can be false" << endl;
smtutil::Expression condition = encodeExpression(*_if.condition);
m_solver->push();
m_solver->addAssertion(condition == constantValue(0));
cout << " running check" << endl;
CheckResult result = m_solver->check({}).first;
m_solver->pop();
if (result == CheckResult::UNSATISFIABLE)
{
cout << " unsat => cannot be false!" << endl;
Literal trueCondition = m_dialect.trueLiteral();
trueCondition.debugData = debugDataOf(*_if.condition);
_if.condition = make_unique<yul::Expression>(move(trueCondition));
}
else
{
cout << "Checking if condition can be true" << endl;
m_solver->push();
m_solver->addAssertion(condition != constantValue(0));
cout << " running check" << endl;
CheckResult result2 = m_solver->check({}).first;
m_solver->pop();
if (result2 == CheckResult::UNSATISFIABLE)
{
cout << " unsat => cannot be true!" << endl;
Literal falseCondition = m_dialect.zeroLiteralForType(m_dialect.boolType);
falseCondition.debugData = debugDataOf(*_if.condition);
_if.condition = make_unique<yul::Expression>(move(falseCondition));
@ -96,6 +102,7 @@ void ReasoningBasedSimplifier::operator()(If& _if)
}
m_solver->push();
cout << "Setting condition true inside body" << endl;
m_solver->addAssertion(condition != constantValue(0));
ASTModifier::operator()(_if.body);