diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-02 13:01:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-02 13:01:50 -0500 |
| commit | a84b54ea155251af6254237816e449589591b33c (patch) | |
| tree | 932321bb441693d7b2fc2539047db204ee2a097b /src/prop/minisat | |
| parent | 9b9cd3a304f5830942a8b715b19e3cac0a771289 (diff) | |
Remove references to deprecated propagate as decision feature (#2258)
Diffstat (limited to 'src/prop/minisat')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index c312ac146..62496df2f 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -603,15 +603,21 @@ Lit Solver::pickBranchLit() nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest()); while (nextLit != lit_Undef) { if(value(var(nextLit)) == l_Undef) { - Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl; + Debug("theoryDecision") + << "getNextTheoryDecisionRequest(): now deciding on " << nextLit + << std::endl; decisions++; return nextLit; } else { - Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl; + Debug("theoryDecision") + << "getNextTheoryDecisionRequest(): would decide on " << nextLit + << " but it already has an assignment" << std::endl; } nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest()); } - Debug("propagateAsDecision") << "propagateAsDecision(): decide on another literal" << std::endl; + Debug("theoryDecision") + << "getNextTheoryDecisionRequest(): decide on another literal" + << std::endl; // DE requests bool stopSearch = false; |