diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index a5b40b6c0..52adc329f 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -178,9 +178,9 @@ void BooleanLPSolver::addAssertion(Expression const& _expr) pair> BooleanLPSolver::check(vector const&) { - cout << "Solving boolean constraint system" << endl; - cout << toString() << endl; - cout << "--------------" << endl; + //cout << "Solving boolean constraint system" << endl; + //cout << toString() << endl; + //cout << "--------------" << endl; if (state().infeasible) return make_pair(CheckResult::UNSATISFIABLE, vector{}); @@ -200,8 +200,8 @@ pair> BooleanLPSolver::check(vector cons else resizeAndSet(lpState.variableNames, index, name); - cout << "Boolean variables:" << joinHumanReadable(booleanVariables) << endl; - cout << "Running LP solver on fixed constraints." << endl; + //cout << "Boolean variables:" << joinHumanReadable(booleanVariables) << endl; + //cout << "Running LP solver on fixed constraints." << endl; if (m_lpSolver.check(lpState).first == LPResult::Infeasible) return {CheckResult::UNSATISFIABLE, {}}; @@ -239,12 +239,12 @@ pair> BooleanLPSolver::check(vector cons auto optionalModel = CDCL{move(booleanVariables), clauses, theorySolver}.solve(); if (!optionalModel) { - cout << "==============> CDCL final result: unsatisfiable." << endl; + //cout << "==============> CDCL final result: unsatisfiable." << endl; return {CheckResult::UNSATISFIABLE, {}}; } else { - cout << "==============> CDCL final result: SATisfiable / UNKNON." << endl; + //cout << "==============> CDCL final result: SATisfiable / UNKNON." << endl; // TODO should be "unknown" later on return {CheckResult::SATISFIABLE, {}}; } diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp index 42aadda10..a2ba3ba29 100644 --- a/libsolutil/CDCL.cpp +++ b/libsolutil/CDCL.cpp @@ -45,24 +45,24 @@ CDCL::CDCL( optional CDCL::solve() { - cout << "====" << endl; - for (unique_ptr const& c: m_clauses) - cout << toString(*c) << endl; - cout << "====" << endl; +// cout << "====" << endl; +// for (unique_ptr const& c: m_clauses) +// cout << toString(*c) << endl; +// cout << "====" << endl; while (true) { optional conflictClause = propagate(); if (!conflictClause && m_theorySolver) { conflictClause = m_theorySolver(m_assignments); - if (conflictClause) - cout << "Theory gave us conflict: " << toString(*conflictClause) << endl; +// if (conflictClause) +// cout << "Theory gave us conflict: " << toString(*conflictClause) << endl; } if (conflictClause) { if (currentDecisionLevel() == 0) { - cout << "Unsatisfiable" << endl; +// cout << "Unsatisfiable" << endl; return nullopt; } auto&& [learntClause, backtrackLevel] = analyze(move(*conflictClause)); @@ -80,14 +80,14 @@ optional CDCL::solve() if (auto variable = nextDecisionVariable()) { m_decisionPoints.emplace_back(m_assignmentTrail.size()); - cout << "Deciding on " << m_variables.at(*variable) << " @" << currentDecisionLevel() << endl; +// cout << "Deciding on " << m_variables.at(*variable) << " @" << currentDecisionLevel() << endl; enqueue(Literal{false, *variable}, nullptr); } else { - cout << "satisfiable." << endl; - for (auto&& [var, value]: m_assignments) - cout << " " << m_variables.at(var) << ": " << (value ? "true" : "false") << endl; + //cout << "satisfiable." << endl; + //for (auto&& [i, value]: m_assignments | ranges::view::enumerate()) + // cout << " " << m_variables.at(i) << ": " << value.toString() << endl; return m_assignments; } } @@ -102,12 +102,12 @@ void CDCL::setupWatches(Clause& _clause) optional CDCL::propagate() { - cout << "Propagating." << endl; + //cout << "Propagating." << endl; for (; m_assignmentQueuePointer < m_assignmentTrail.size(); m_assignmentQueuePointer++) { Literal toPropagate = m_assignmentTrail.at(m_assignmentQueuePointer); Literal falseLiteral = ~toPropagate; - cout << "Propagating " << toString(toPropagate) << endl; + //cout << "Propagating " << toString(toPropagate) << endl; // Go through all watched clauses where this assignment makes the literal false. vector watchReplacement; auto it = m_watches[falseLiteral].begin(); @@ -115,7 +115,7 @@ optional CDCL::propagate() for (; it != end; ++it) { Clause& clause = **it; - cout << " watch clause: " << toString(clause) << endl; + //cout << " watch clause: " << toString(clause) << endl; solAssert(!clause.empty()); if (clause.front() != falseLiteral) @@ -124,7 +124,7 @@ optional CDCL::propagate() if (clause.size() >= 2 && isAssignedTrue(clause[1])) { // Clause is already satisfied, keezp the watch. - cout << " -> already satisfied by " << toString(clause[1]) << endl; + //cout << " -> already satisfied by " << toString(clause[1]) << endl; watchReplacement.emplace_back(&clause); continue; } @@ -133,7 +133,7 @@ optional CDCL::propagate() for (size_t i = 2; i < clause.size(); i++) if (isUnknownOrAssignedTrue(clause[i])) { - cout << " -> swapping " << toString(clause.front()) << " with " << toString(clause[i]) << endl; + //cout << " -> swapping " << toString(clause.front()) << " with " << toString(clause[i]) << endl; swap(clause.front(), clause[i]); m_watches[clause.front()].emplace_back(&clause); break; @@ -145,10 +145,10 @@ optional CDCL::propagate() // are false, thus clause[1] has to be true (if it exists) if (clause.size() == 1 || isAssignedFalse(clause[1])) { - if (clause.size() >= 2) - cout << " - Propagate resulted in conflict because " << toString(clause[1]) << " is also false." << endl; - else - cout << " - Propagate resulted in conflict since clause is single-literal." << endl; +// if (clause.size() >= 2) +// cout << " - Propagate resulted in conflict because " << toString(clause[1]) << " is also false." << endl; +// else +// cout << " - Propagate resulted in conflict since clause is single-literal." << endl; // Copy over the remaining watches and replace. while (it != end) watchReplacement.emplace_back(move(*it++)); m_watches[falseLiteral] = move(watchReplacement); @@ -158,7 +158,7 @@ optional CDCL::propagate() } else { - cout << " - resulted in new assignment: " << toString(clause[1]) << endl; +// cout << " - resulted in new assignment: " << toString(clause[1]) << endl; watchReplacement.emplace_back(&clause); enqueue(clause[1], &clause); } @@ -172,7 +172,7 @@ optional CDCL::propagate() std::pair CDCL::analyze(Clause _conflictClause) { solAssert(!_conflictClause.empty()); - cout << "Analyzing conflict." << endl; + //cout << "Analyzing conflict." << endl; Clause learntClause; size_t backtrackLevel = 0; @@ -183,7 +183,7 @@ std::pair CDCL::analyze(Clause _conflictClause) optional resolvingLiteral; do { - cout << " conflict clause: " << toString(_conflictClause) << endl; + //cout << " conflict clause: " << toString(_conflictClause) << endl; for (Literal literal: _conflictClause) if ((!resolvingLiteral || literal != *resolvingLiteral) && !seenVariables.count(literal.variable)) { @@ -191,31 +191,31 @@ std::pair CDCL::analyze(Clause _conflictClause) size_t variableLevel = m_levelForVariable.at(literal.variable); if (variableLevel == currentDecisionLevel()) { - cout << " ignoring " << toString(literal) << " at current decision level." << endl; + //cout << " ignoring " << toString(literal) << " at current decision level." << endl; // ignore variable, we will apply resolution with its reason. pathCount++; } else { - cout << " adding " << toString(literal) << " @" << variableLevel << " to learnt clause." << endl; + //cout << " adding " << toString(literal) << " @" << variableLevel << " to learnt clause." << endl; learntClause.push_back(literal); backtrackLevel = max(backtrackLevel, variableLevel); } - } + }/* else - cout << " already seen " << toString(literal) << endl; + cout << " already seen " << toString(literal) << endl;*/ solAssert(pathCount > 0); pathCount--; while (!seenVariables.count(m_assignmentTrail[trailIndex--].variable)); resolvingLiteral = m_assignmentTrail[trailIndex + 1]; - cout << " resolving literal: " << toString(*resolvingLiteral) << endl; + //cout << " resolving literal: " << toString(*resolvingLiteral) << endl; seenVariables.erase(resolvingLiteral->variable); // TODO Is there always a reason? Not if it's a decision variable. if (pathCount > 0) { _conflictClause = *m_reason.at(*resolvingLiteral); - cout << " reason: " << toString(_conflictClause) << endl; + //cout << " reason: " << toString(_conflictClause) << endl; } } while (pathCount > 0); @@ -224,7 +224,7 @@ std::pair CDCL::analyze(Clause _conflictClause) // Move to front so we can directly propagate. swap(learntClause.front(), learntClause.back()); - cout << "-> learnt clause: " << toString(learntClause) << " backtrack to " << backtrackLevel << endl; + //cout << "-> learnt clause: " << toString(learntClause) << " backtrack to " << backtrackLevel << endl; return {move(learntClause), backtrackLevel}; @@ -238,9 +238,11 @@ void CDCL::addClause(Clause _clause) void CDCL::enqueue(Literal const& _literal, Clause const* _reason) { + /* cout << "Enqueueing " << toString(_literal) << " @" << currentDecisionLevel() << endl; if (_reason) cout << " because of " << toString(*_reason) << endl; +*/ // TODO assert that assignmnets was unknown m_assignments[_literal.variable] = _literal.positive; m_levelForVariable[_literal.variable] = currentDecisionLevel(); @@ -252,13 +254,13 @@ void CDCL::enqueue(Literal const& _literal, Clause const* _reason) void CDCL::cancelUntil(size_t _backtrackLevel) { // TODO what if we backtrack to zero? - cout << "Canceling until " << _backtrackLevel << endl; + //cout << "Canceling until " << _backtrackLevel << endl; solAssert(m_assignmentQueuePointer == m_assignmentTrail.size()); size_t assignmentsToUndo = m_assignmentTrail.size() - m_decisionPoints.at(_backtrackLevel); for (size_t i = 0; i < assignmentsToUndo; i++) { Literal l = m_assignmentTrail.back(); - cout << " undoing " << toString(l) << endl; + //cout << " undoing " << toString(l) << endl; m_assignmentTrail.pop_back(); m_assignments.erase(l.variable); m_reason.erase(l); diff --git a/libsolutil/LP.cpp b/libsolutil/LP.cpp index dd60db5ee..c3350bbd2 100644 --- a/libsolutil/LP.cpp +++ b/libsolutil/LP.cpp @@ -778,13 +778,13 @@ LPSolver::LPSolver(bool _supportModels): pair> LPSolver::check(SolvingState _state) { normalizeRowLengths(_state); - cout << "Running LP on:\n" << _state.toString() << endl; + //cout << "Running LP on:\n" << _state.toString() << endl; auto&& [simplificationResult, modelOrReasonSet] = SolvingStateSimplifier{_state}.simplify(); switch (simplificationResult) { case LPResult::Infeasible: - cout << "-> LP infeasible." << endl; + //cout << "-> LP infeasible." << endl; return {LPResult::Infeasible, modelOrReasonSet}; case LPResult::Feasible: case LPResult::Unbounded: @@ -808,7 +808,7 @@ pair> LPSolver::check(SolvingState _state) if (auto conflict = boundsToConstraints(split)) { - cout << "-> LP infeasible." << endl; + //cout << "-> LP infeasible." << endl; return {LPResult::Infeasible, move(*conflict)}; } @@ -839,7 +839,7 @@ pair> LPSolver::check(SolvingState _state) set reasons; for (auto const& constraint: split.constraints) reasons += constraint.reasons; - cout << "-> LP infeasible." << endl; + //cout << "-> LP infeasible." << endl; return {LPResult::Infeasible, move(reasons)}; } case LPResult::Unknown: @@ -854,11 +854,11 @@ pair> LPSolver::check(SolvingState _state) if (canOnlyBeUnknown) { - cout << "-> LP unknown." << endl; + //cout << "-> LP unknown." << endl; return {LPResult::Unknown, Model{}}; } - cout << "-> LP feasible." << endl; + //cout << "-> LP feasible." << endl; return {LPResult::Feasible, move(model)}; }