From 77d1ebae3b553ac1d4ab831737135e83daabd5c6 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 18 May 2022 15:50:51 +0200 Subject: [PATCH] debugging output --- libsolutil/BooleanLP.cpp | 17 +++++++++++++++++ libsolutil/LP.cpp | 12 ++++++++++++ tools/solsmt.cpp | 6 +++++- 3 files changed, 34 insertions(+), 1 deletion(-) diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index 963cb34ef..bb22153ef 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -101,13 +101,17 @@ void BooleanLPSolver::declareVariable(string const& _name, SortPointer const& _s pair> BooleanLPSolver::check(vector const&) { +#ifdef DEBUG cerr << "Solving boolean constraint system" << endl; cerr << toString() << endl; cerr << "--------------" << endl; +#endif if (state().infeasible) { +#ifdef DEBUG cerr << "----->>>>> unsatisfiable" << endl; +#endif return make_pair(CheckResult::UNSATISFIABLE, vector{}); } @@ -142,7 +146,9 @@ pair> BooleanLPSolver::check(vector cons if (lpSolver.check().first == LPResult::Infeasible) { +#ifdef DEBUG cerr << "----->>>>> unsatisfiable" << endl; +#endif return {CheckResult::UNSATISFIABLE, {}}; } @@ -180,12 +186,16 @@ pair> BooleanLPSolver::check(vector cons auto optionalModel = CDCL{move(booleanVariables), clauses, theorySolver, backtrackNotify}.solve(); if (!optionalModel) { +#ifdef DEBUG cerr << "==============> CDCL final result: unsatisfiable." << endl; +#endif return {CheckResult::UNSATISFIABLE, {}}; } else { +#ifdef DEBUG cerr << "==============> CDCL final result: SATisfiable / UNKNOWN." << endl; +#endif // TODO should be "unknown" later on return {CheckResult::SATISFIABLE, {}}; //return {CheckResult::UNKNOWN, {}}; @@ -219,8 +229,10 @@ string BooleanLPSolver::toString() const void BooleanLPSolver::addAssertion(Expression const& _expr, map _letBindings) { +#ifdef DEBUG cerr << "adding assertion" << endl; cerr << " - " << _expr.toString() << endl; +#endif solAssert(_expr.sort->kind == Kind::Bool); if (_expr.arguments.empty()) { @@ -262,10 +274,14 @@ void BooleanLPSolver::addAssertion(Expression const& _expr, map Constraint c{move(data), Constraint::EQUAL}; if (!tryAddDirectBounds(c)) state().fixedConstraints.emplace_back(move(c)); +#ifdef DEBUG cerr << "Added as fixed constraint" << endl; +#endif } else { + cerr << _expr.toString() << endl; + cerr << "Expected linear arguments." << endl; solAssert(false); } } @@ -521,6 +537,7 @@ optional BooleanLPSolver::parseLinearSum(smtutil::Expression c } else { + cerr << _expr.toString() << endl; cerr << "Invalid operator " << _expr.name << endl; return std::nullopt; } diff --git a/libsolutil/LP.cpp b/libsolutil/LP.cpp index 4e039feed..62ead4dac 100644 --- a/libsolutil/LP.cpp +++ b/libsolutil/LP.cpp @@ -469,34 +469,42 @@ LPResult LPSolver::SubProblem::check() // is spent on "operator<" - maybe we can cache "is in bounds" for variables // and invalidate that in the update procedures. +#ifdef DEBUG cerr << "checking..." << endl; cerr << toString() << endl; cerr << "----------------------------" << endl; cerr << "fixing non-basic..." << endl; +#endif // Adjust the assignments so we satisfy the bounds of the non-basic variables. if (!correctNonbasic()) return LPResult::Infeasible; // Now try to make the basic variables happy, pivoting if necessary. +#ifdef DEBUG cerr << "fixed non-basic." << endl; cerr << toString() << endl; cerr << "----------------------------" << endl; +#endif // TODO bound number of iterations while (auto bvi = firstConflictingBasicVariable()) { Variable const& basicVar = variables[*bvi]; +#ifdef DEBUG cerr << toString() << endl; cerr << "Fixing basic " << basicVar.name << endl; cerr << "----------------------------" << endl; +#endif if (basicVar.bounds.lower && basicVar.bounds.upper) solAssert(*basicVar.bounds.lower <= *basicVar.bounds.upper); if (basicVar.bounds.lower && basicVar.value < *basicVar.bounds.lower) { if (auto replacementVar = firstReplacementVar(*bvi, true)) { +#ifdef DEBUG cerr << "Replacing by " << variables[*replacementVar].name << endl; +#endif pivotAndUpdate(*bvi, *basicVar.bounds.lower, *replacementVar); } @@ -507,14 +515,18 @@ LPResult LPSolver::SubProblem::check() { if (auto replacementVar = firstReplacementVar(*bvi, false)) { +#ifdef DEBUG cerr << "Replacing by " << variables[*replacementVar].name << endl; +#endif pivotAndUpdate(*bvi, *basicVar.bounds.upper, *replacementVar); } else return LPResult::Infeasible; } +#ifdef DEBUG cerr << "Fixed basic " << basicVar.name << endl; cerr << toString() << endl; +#endif } return LPResult::Feasible; diff --git a/tools/solsmt.cpp b/tools/solsmt.cpp index c3707eb72..e4617b8ea 100644 --- a/tools/solsmt.cpp +++ b/tools/solsmt.cpp @@ -164,7 +164,9 @@ smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map(bindingElements.at(0).data); Expression replacement = toSMTUtilExpression(bindingElements.at(1), _variableSorts); +#ifdef DEBUG cerr << "Binding " << varName << " to " << replacement.toString() << endl; +#endif subSorts[string(varName)] = 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); SMTLib2Expression expr = parser.parseExpression(); auto newInputToParse = parser.remainingInput(); +#ifdef DEBUG cerr << "got : " << string(inputToParse.begin(), newInputToParse.begin()) << endl; - inputToParse = move(newInputToParse); cerr << " -> " << expr.toString() << endl; +#endif + inputToParse = move(newInputToParse); vector const& items = get>(expr.data); string_view cmd = command(expr); if (cmd == "set-info")