diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index dad12da7f..963cb34ef 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -670,7 +670,15 @@ void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expressi state().clauses.emplace_back(Clause{vector{negate(_left), a, negate(b)}}); state().clauses.emplace_back(Clause{vector{_left, negate(a), negate(b)}}); state().clauses.emplace_back(Clause{vector{_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 solAssert(false, "Unsupported operation: " + _right.name); } diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp index ad79a11b0..8e60dab2b 100644 --- a/libsolutil/CDCL.cpp +++ b/libsolutil/CDCL.cpp @@ -86,7 +86,7 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol conflicts++; m_sumConflicts++; if (m_sumConflicts % 1000 == 999) { - cout << "c confl: " << m_sumConflicts << std::endl; + cerr << "c confl: " << m_sumConflicts << std::endl; } if (currentDecisionLevel() == 0) { diff --git a/libsolutil/LP.cpp b/libsolutil/LP.cpp index 4058163d8..4e039feed 100644 --- a/libsolutil/LP.cpp +++ b/libsolutil/LP.cpp @@ -94,10 +94,10 @@ bool Constraint::operator<(Constraint const& _other) const for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i) if (rational diff = data.get(i) - _other.data.get(i)) { - //cout << "Exit after " << i << endl; + //cerr << "Exit after " << i << endl; 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; } @@ -110,10 +110,10 @@ bool Constraint::operator==(Constraint const& _other) const for (size_t i = 0; i < max(data.size(), _other.data.size()); ++i) if (data.get(i) != _other.data.get(i)) { - //cout << "Exit after " << i << endl; + //cerr << "Exit after " << i << endl; 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; } @@ -209,7 +209,7 @@ void LPSolver::addConstraint(Constraint const& _constraint, optional _re 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. m_subProblems.emplace_back(make_shared()); solAssert(!m_subProblems.back()->sealed); @@ -218,7 +218,7 @@ void LPSolver::addConstraint(Constraint const& _constraint, optional _re for (size_t problemToErase: touchedProblems | ranges::views::tail | ranges::views::reverse) combineSubProblems(*touchedProblems.begin(), problemToErase); 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) @@ -269,7 +269,7 @@ pair LPSolver::check() if (*problem->result == LPResult::Infeasible) return {LPResult::Infeasible, problem->reasons}; } - //cout << "Feasible:\n" << toString() << endl; + //cerr << "Feasible:\n" << toString() << endl; return {LPResult::Feasible, {}}; } @@ -318,8 +318,8 @@ LPSolver::SubProblem& LPSolver::unsealForVariable(size_t _outerIndex) void LPSolver::combineSubProblems(size_t _combineInto, size_t _combineFrom) { - //cout << "Combining\n" << m_subProblems.at(_combineFrom)->toString(); - //cout << "\ninto\n" << m_subProblems.at(_combineInto)->toString(); + //cerr << "Combining\n" << m_subProblems.at(_combineFrom)->toString(); + //cerr << "\ninto\n" << m_subProblems.at(_combineInto)->toString(); SubProblem& combineInto = unseal(_combineInto); SubProblem const& combineFrom = *m_subProblems[_combineFrom]; @@ -350,8 +350,8 @@ void LPSolver::combineSubProblems(size_t _combineInto, size_t _combineFrom) item.second = _combineInto; m_subProblems[_combineFrom].reset(); - //cout << "result: \n" << m_subProblems.at(_combineInto)->toString(); - //cout << "------------------------------\n"; + //cerr << "result: \n" << m_subProblems.at(_combineInto)->toString(); + //cerr << "------------------------------\n"; } // 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 // and invalidate that in the update procedures. -// cout << "checking..." << endl; -// cout << toString() << endl; -// cout << "----------------------------" << endl; -// cout << "fixing non-basic..." << endl; + cerr << "checking..." << endl; + cerr << toString() << endl; + cerr << "----------------------------" << endl; + cerr << "fixing non-basic..." << endl; // 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. -// cout << "fixed non-basic." << endl; -// cout << toString() << endl; -// cout << "----------------------------" << endl; + cerr << "fixed non-basic." << endl; + cerr << toString() << endl; + cerr << "----------------------------" << endl; // TODO bound number of iterations while (auto bvi = firstConflictingBasicVariable()) { Variable const& basicVar = variables[*bvi]; -// cout << toString() << endl; -// cout << "Fixing basic " << basicVar.name << endl; -// cout << "----------------------------" << endl; + cerr << toString() << endl; + cerr << "Fixing basic " << basicVar.name << endl; + cerr << "----------------------------" << endl; 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)) { -// cout << "Replacing by " << variables[*replacementVar].name << endl; + cerr << "Replacing by " << variables[*replacementVar].name << endl; pivotAndUpdate(*bvi, *basicVar.bounds.lower, *replacementVar); } @@ -507,14 +507,14 @@ LPResult LPSolver::SubProblem::check() { 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); } else return LPResult::Infeasible; } -// cout << "Fixed basic " << basicVar.name << endl; -// cout << toString() << endl; + cerr << "Fixed basic " << basicVar.name << endl; + cerr << toString() << endl; } return LPResult::Feasible; diff --git a/tools/solsmt.cpp b/tools/solsmt.cpp index 9cb0e8de2..c3707eb72 100644 --- a/tools/solsmt.cpp +++ b/tools/solsmt.cpp @@ -164,7 +164,7 @@ smtutil::Expression toSMTUtilExpression(SMTLib2Expression const& _expr, map(bindingElements.at(0).data); 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; arguments.emplace_back(Expression(string(varName), {move(replacement)}, replacement.sort)); }