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

debugging

Browse Source
This commit is contained in:
chriseth 2022-05-16 19:14:31 +02:00
parent 657a02771b
commit 56d5f6d926
4 changed files with 36 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
libsolutil/BooleanLP.cpp
View File

@ -670,7 +670,15 @@ void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expressi
state().clauses.emplace_back(Clause{vector<Literal>{negate(_left), a, negate(b)}}); state().clauses.emplace_back(Clause{vector<Literal>{negate(_left), a, negate(b)}});
state().clauses.emplace_back(Clause{vector<Literal>{_left, negate(a), negate(b)}}); state().clauses.emplace_back(Clause{vector<Literal>{_left, negate(a), negate(b)}});
state().clauses.emplace_back(Clause{vector<Literal>{_left, a, b}}); state().clauses.emplace_back(Clause{vector<Literal>{_left, a, b}});
} }/*
else if (_right.name == "ite")
{
// a = (c ? x : y)
// c ? a = x : a = y
// c => a = x && !c => a = y
addAssertion(!_right.arguments.at(0) || (_left == _right.arguments.at(1)), _letBindings);
addAssertion(_right.arguments.at(0) || (_left == _right.arguments.at(2)), _letBindings);
}*/
else else
solAssert(false, "Unsupported operation: " + _right.name); solAssert(false, "Unsupported operation: " + _right.name);
} }

2
libsolutil/CDCL.cpp
View File

@ -86,7 +86,7 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol
conflicts++; conflicts++;
m_sumConflicts++; m_sumConflicts++;
if (m_sumConflicts % 1000 == 999) { if (m_sumConflicts % 1000 == 999) {
cout << "c confl: " << m_sumConflicts << std::endl; cerr << "c confl: " << m_sumConflicts << std::endl;
} }
if (currentDecisionLevel() == 0) if (currentDecisionLevel() == 0)
{ {

50
libsolutil/LP.cpp
View File

@ -94,10 +94,10 @@ bool Constraint::operator<(Constraint const& _other) const
for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i) for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i)
if (rational diff = data.get(i) - _other.data.get(i)) if (rational diff = data.get(i) - _other.data.get(i))
{ {
//cout << "Exit after " << i << endl; //cerr << "Exit after " << i << endl;
return diff < 0; return diff < 0;
} }
//cout << "full traversal of " << max(data.size(), _other.data.size()) << endl; //cerr << "full traversal of " << max(data.size(), _other.data.size()) << endl;
return false; return false;
} }
@ -110,10 +110,10 @@ bool Constraint::operator==(Constraint const& _other) const
for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i) for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i)
if (data.get(i) != _other.data.get(i)) if (data.get(i) != _other.data.get(i))
{ {
//cout << "Exit after " << i << endl; //cerr << "Exit after " << i << endl;
return false; return false;
} }
//cout << "full traversal of " << max(data.size(), _other.data.size()) << endl; //cerr << "full traversal of " << max(data.size(), _other.data.size()) << endl;
return true; return true;
} }
@ -209,7 +209,7 @@ void LPSolver::addConstraint(Constraint const& _constraint, optional<size_t> _re
if (touchedProblems.empty()) if (touchedProblems.empty())
{ {
//cout << "Creating new sub problem." << endl; //cerr << "Creating new sub problem." << endl;
// TODO we could find an empty spot for the pointer. // TODO we could find an empty spot for the pointer.
m_subProblems.emplace_back(make_shared<SubProblem>()); m_subProblems.emplace_back(make_shared<SubProblem>());
solAssert(!m_subProblems.back()->sealed); solAssert(!m_subProblems.back()->sealed);
@ -218,7 +218,7 @@ void LPSolver::addConstraint(Constraint const& _constraint, optional<size_t> _re
for (size_t problemToErase: touchedProblems | ranges::views::tail | ranges::views::reverse) for (size_t problemToErase: touchedProblems | ranges::views::tail | ranges::views::reverse)
combineSubProblems(*touchedProblems.begin(), problemToErase); combineSubProblems(*touchedProblems.begin(), problemToErase);
addConstraintToSubProblem(*touchedProblems.begin(), _constraint, move(_reason)); addConstraintToSubProblem(*touchedProblems.begin(), _constraint, move(_reason));
//cout << "Added constraint:\n" << toString() << endl; //cerr << "Added constraint:\n" << toString() << endl;
} }
void LPSolver::setVariableName(size_t _variable, string _name) void LPSolver::setVariableName(size_t _variable, string _name)
@ -269,7 +269,7 @@ pair<LPResult, ReasonSet> LPSolver::check()
if (*problem->result == LPResult::Infeasible) if (*problem->result == LPResult::Infeasible)
return {LPResult::Infeasible, problem->reasons}; return {LPResult::Infeasible, problem->reasons};
} }
//cout << "Feasible:\n" << toString() << endl; //cerr << "Feasible:\n" << toString() << endl;
return {LPResult::Feasible, {}}; return {LPResult::Feasible, {}};
} }
@ -318,8 +318,8 @@ LPSolver::SubProblem& LPSolver::unsealForVariable(size_t _outerIndex)
void LPSolver::combineSubProblems(size_t _combineInto, size_t _combineFrom) void LPSolver::combineSubProblems(size_t _combineInto, size_t _combineFrom)
{ {
//cout << "Combining\n" << m_subProblems.at(_combineFrom)->toString(); //cerr << "Combining\n" << m_subProblems.at(_combineFrom)->toString();
//cout << "\ninto\n" << m_subProblems.at(_combineInto)->toString(); //cerr << "\ninto\n" << m_subProblems.at(_combineInto)->toString();
SubProblem& combineInto = unseal(_combineInto); SubProblem& combineInto = unseal(_combineInto);
SubProblem const& combineFrom = *m_subProblems[_combineFrom]; SubProblem const& combineFrom = *m_subProblems[_combineFrom];
@ -350,8 +350,8 @@ void LPSolver::combineSubProblems(size_t _combineInto, size_t _combineFrom)
item.second = _combineInto; item.second = _combineInto;
m_subProblems[_combineFrom].reset(); m_subProblems[_combineFrom].reset();
//cout << "result: \n" << m_subProblems.at(_combineInto)->toString(); //cerr << "result: \n" << m_subProblems.at(_combineInto)->toString();
//cout << "------------------------------\n"; //cerr << "------------------------------\n";
} }
// TODO move this function into the problem struct and make it erturn set of vaiables added // TODO move this function into the problem struct and make it erturn set of vaiables added
@ -469,34 +469,34 @@ LPResult LPSolver::SubProblem::check()
// is spent on "operator<" - maybe we can cache "is in bounds" for variables // is spent on "operator<" - maybe we can cache "is in bounds" for variables
// and invalidate that in the update procedures. // and invalidate that in the update procedures.
// cout << "checking..." << endl; cerr << "checking..." << endl;
// cout << toString() << endl; cerr << toString() << endl;
// cout << "----------------------------" << endl; cerr << "----------------------------" << endl;
// cout << "fixing non-basic..." << endl; cerr << "fixing non-basic..." << endl;
// Adjust the assignments so we satisfy the bounds of the non-basic variables. // Adjust the assignments so we satisfy the bounds of the non-basic variables.
if (!correctNonbasic()) if (!correctNonbasic())
return LPResult::Infeasible; return LPResult::Infeasible;
// Now try to make the basic variables happy, pivoting if necessary. // Now try to make the basic variables happy, pivoting if necessary.
// cout << "fixed non-basic." << endl; cerr << "fixed non-basic." << endl;
// cout << toString() << endl; cerr << toString() << endl;
// cout << "----------------------------" << endl; cerr << "----------------------------" << endl;
// TODO bound number of iterations // TODO bound number of iterations
while (auto bvi = firstConflictingBasicVariable()) while (auto bvi = firstConflictingBasicVariable())
{ {
Variable const& basicVar = variables[*bvi]; Variable const& basicVar = variables[*bvi];
// cout << toString() << endl; cerr << toString() << endl;
// cout << "Fixing basic " << basicVar.name << endl; cerr << "Fixing basic " << basicVar.name << endl;
// cout << "----------------------------" << endl; cerr << "----------------------------" << endl;
if (basicVar.bounds.lower && basicVar.bounds.upper) if (basicVar.bounds.lower && basicVar.bounds.upper)
solAssert(*basicVar.bounds.lower <= *basicVar.bounds.upper); solAssert(*basicVar.bounds.lower <= *basicVar.bounds.upper);
if (basicVar.bounds.lower && basicVar.value < *basicVar.bounds.lower) if (basicVar.bounds.lower && basicVar.value < *basicVar.bounds.lower)
{ {
if (auto replacementVar = firstReplacementVar(*bvi, true)) if (auto replacementVar = firstReplacementVar(*bvi, true))
{ {
// cout << "Replacing by " << variables[*replacementVar].name << endl; cerr << "Replacing by " << variables[*replacementVar].name << endl;
pivotAndUpdate(*bvi, *basicVar.bounds.lower, *replacementVar); pivotAndUpdate(*bvi, *basicVar.bounds.lower, *replacementVar);
} }
@ -507,14 +507,14 @@ LPResult LPSolver::SubProblem::check()
{ {
if (auto replacementVar = firstReplacementVar(*bvi, false)) if (auto replacementVar = firstReplacementVar(*bvi, false))
{ {
// cout << "Replacing by " << variables[*replacementVar].name << endl; cerr << "Replacing by " << variables[*replacementVar].name << endl;
pivotAndUpdate(*bvi, *basicVar.bounds.upper, *replacementVar); pivotAndUpdate(*bvi, *basicVar.bounds.upper, *replacementVar);
} }
else else
return LPResult::Infeasible; return LPResult::Infeasible;
} }
// cout << "Fixed basic " << basicVar.name << endl; cerr << "Fixed basic " << basicVar.name << endl;
// cout << toString() << endl; cerr << toString() << endl;
} }
return LPResult::Feasible; return LPResult::Feasible;

2
tools/solsmt.cpp
View File

@ -164,7 +164,7 @@ smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map<stri
solAssert(bindingElements.size() == 2); solAssert(bindingElements.size() == 2);
string_view varName = get<string_view>(bindingElements.at(0).data); string_view varName = get<string_view>(bindingElements.at(0).data);
Expression replacement = toSMTUtilExpression(bindingElements.at(1), _variableSorts); Expression replacement = toSMTUtilExpression(bindingElements.at(1), _variableSorts);
cout << "Binding " << varName << " to " << replacement.toString() << endl; cerr << "Binding " << varName << " to " << replacement.toString() << endl;
subSorts[string(varName)] = replacement.sort; subSorts[string(varName)] = replacement.sort;
arguments.emplace_back(Expression(string(varName), {move(replacement)}, replacement.sort)); arguments.emplace_back(Expression(string(varName), {move(replacement)}, replacement.sort));
} }