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 output

Browse Source
This commit is contained in:
chriseth 2022-05-18 15:50:51 +02:00
parent 56d5f6d926
commit 77d1ebae3b
3 changed files with 34 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
libsolutil/BooleanLP.cpp
View File

@ -101,13 +101,17 @@ void BooleanLPSolver::declareVariable(string const& _name, SortPointer const& _s
pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> const&) pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> const&)
{ {
#ifdef DEBUG
cerr << "Solving boolean constraint system" << endl; cerr << "Solving boolean constraint system" << endl;
cerr << toString() << endl; cerr << toString() << endl;
cerr << "--------------" << endl; cerr << "--------------" << endl;
#endif
if (state().infeasible) if (state().infeasible)
{ {
#ifdef DEBUG
cerr << "----->>>>> unsatisfiable" << endl; cerr << "----->>>>> unsatisfiable" << endl;
#endif
return make_pair(CheckResult::UNSATISFIABLE, vector<string>{}); return make_pair(CheckResult::UNSATISFIABLE, vector<string>{});
} }
@ -142,7 +146,9 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
if (lpSolver.check().first == LPResult::Infeasible) if (lpSolver.check().first == LPResult::Infeasible)
{ {
#ifdef DEBUG
cerr << "----->>>>> unsatisfiable" << endl; cerr << "----->>>>> unsatisfiable" << endl;
#endif
return {CheckResult::UNSATISFIABLE, {}}; return {CheckResult::UNSATISFIABLE, {}};
} }
@ -180,12 +186,16 @@ pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> cons
auto optionalModel = CDCL{move(booleanVariables), clauses, theorySolver, backtrackNotify}.solve(); auto optionalModel = CDCL{move(booleanVariables), clauses, theorySolver, backtrackNotify}.solve();
if (!optionalModel) if (!optionalModel)
{ {
#ifdef DEBUG
cerr << "==============> CDCL final result: unsatisfiable." << endl; cerr << "==============> CDCL final result: unsatisfiable." << endl;
#endif
return {CheckResult::UNSATISFIABLE, {}}; return {CheckResult::UNSATISFIABLE, {}};
} }
else else
{ {
#ifdef DEBUG
cerr << "==============> CDCL final result: SATisfiable / UNKNOWN." << endl; cerr << "==============> CDCL final result: SATisfiable / UNKNOWN." << endl;
#endif
// TODO should be "unknown" later on // TODO should be "unknown" later on
return {CheckResult::SATISFIABLE, {}}; return {CheckResult::SATISFIABLE, {}};
//return {CheckResult::UNKNOWN, {}}; //return {CheckResult::UNKNOWN, {}};
@ -219,8 +229,10 @@ string BooleanLPSolver::toString() const
void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, size_t> _letBindings) void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, size_t> _letBindings)
{ {
#ifdef DEBUG
cerr << "adding assertion" << endl; cerr << "adding assertion" << endl;
cerr << " - " << _expr.toString() << endl; cerr << " - " << _expr.toString() << endl;
#endif
solAssert(_expr.sort->kind == Kind::Bool); solAssert(_expr.sort->kind == Kind::Bool);
if (_expr.arguments.empty()) if (_expr.arguments.empty())
{ {
@ -262,10 +274,14 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map<string, size_t>
Constraint c{move(data), Constraint::EQUAL}; Constraint c{move(data), Constraint::EQUAL};
if (!tryAddDirectBounds(c)) if (!tryAddDirectBounds(c))
state().fixedConstraints.emplace_back(move(c)); state().fixedConstraints.emplace_back(move(c));
#ifdef DEBUG
cerr << "Added as fixed constraint" << endl; cerr << "Added as fixed constraint" << endl;
#endif
} }
else else
{ {
cerr << _expr.toString() << endl;
cerr << "Expected linear arguments." << endl;
solAssert(false); solAssert(false);
} }
} }
@ -521,6 +537,7 @@ optional<LinearExpression> BooleanLPSolver::parseLinearSum(smtutil::Expression c
} }
else else
{ {
cerr << _expr.toString() << endl;
cerr << "Invalid operator " << _expr.name << endl; cerr << "Invalid operator " << _expr.name << endl;
return std::nullopt; return std::nullopt;
} }

12
libsolutil/LP.cpp
View File

@ -469,34 +469,42 @@ 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.
#ifdef DEBUG
cerr << "checking..." << endl; cerr << "checking..." << endl;
cerr << toString() << endl; cerr << toString() << endl;
cerr << "----------------------------" << endl; cerr << "----------------------------" << endl;
cerr << "fixing non-basic..." << endl; cerr << "fixing non-basic..." << endl;
#endif
// 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.
#ifdef DEBUG
cerr << "fixed non-basic." << endl; cerr << "fixed non-basic." << endl;
cerr << toString() << endl; cerr << toString() << endl;
cerr << "----------------------------" << endl; cerr << "----------------------------" << endl;
#endif
// 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];
#ifdef DEBUG
cerr << toString() << endl; cerr << toString() << endl;
cerr << "Fixing basic " << basicVar.name << endl; cerr << "Fixing basic " << basicVar.name << endl;
cerr << "----------------------------" << endl; cerr << "----------------------------" << endl;
#endif
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))
{ {
#ifdef DEBUG
cerr << "Replacing by " << variables[*replacementVar].name << endl; cerr << "Replacing by " << variables[*replacementVar].name << endl;
#endif
pivotAndUpdate(*bvi, *basicVar.bounds.lower, *replacementVar); pivotAndUpdate(*bvi, *basicVar.bounds.lower, *replacementVar);
} }
@ -507,14 +515,18 @@ LPResult LPSolver::SubProblem::check()
{ {
if (auto replacementVar = firstReplacementVar(*bvi, false)) if (auto replacementVar = firstReplacementVar(*bvi, false))
{ {
#ifdef DEBUG
cerr << "Replacing by " << variables[*replacementVar].name << endl; cerr << "Replacing by " << variables[*replacementVar].name << endl;
#endif
pivotAndUpdate(*bvi, *basicVar.bounds.upper, *replacementVar); pivotAndUpdate(*bvi, *basicVar.bounds.upper, *replacementVar);
} }
else else
return LPResult::Infeasible; return LPResult::Infeasible;
} }
#ifdef DEBUG
cerr << "Fixed basic " << basicVar.name << endl; cerr << "Fixed basic " << basicVar.name << endl;
cerr << toString() << endl; cerr << toString() << endl;
#endif
} }
return LPResult::Feasible; return LPResult::Feasible;

6
tools/solsmt.cpp
View File

@ -164,7 +164,9 @@ 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);
#ifdef DEBUG
cerr << "Binding " << varName << " to " << replacement.toString() << endl; cerr << "Binding " << varName << " to " << replacement.toString() << endl;
#endif
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));
} }
@ -231,9 +233,11 @@ int main(int argc, char** argv)
SMTLib2Parser parser(inputToParse); SMTLib2Parser parser(inputToParse);
SMTLib2Expression expr = parser.parseExpression(); SMTLib2Expression expr = parser.parseExpression();
auto newInputToParse = parser.remainingInput(); auto newInputToParse = parser.remainingInput();
#ifdef DEBUG
cerr << "got : " << string(inputToParse.begin(), newInputToParse.begin()) << endl; cerr << "got : " << string(inputToParse.begin(), newInputToParse.begin()) << endl;
inputToParse = move(newInputToParse);
cerr << " -> " << expr.toString() << endl; cerr << " -> " << expr.toString() << endl;
#endif
inputToParse = move(newInputToParse);
vector<SMTLib2Expression> const& items = get<vector<SMTLib2Expression>>(expr.data); vector<SMTLib2Expression> const& items = get<vector<SMTLib2Expression>>(expr.data);
string_view cmd = command(expr); string_view cmd = command(expr);
if (cmd == "set-info") if (cmd == "set-info")