From a84b54ea155251af6254237816e449589591b33c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 2 Aug 2018 13:01:50 -0500 Subject: [PATCH] Remove references to deprecated propagate as decision feature (#2258) --- src/prop/minisat/core/Solver.cc | 12 +++++++++--- src/theory/theory_engine.h | 6 ------ src/theory/uf/theory_uf_strong_solver.cpp | 3 --- 3 files changed, 9 insertions(+), 12 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; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 25520c1cc..9eafe2598 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -413,12 +413,6 @@ class TheoryEngine { */ void propagate(theory::Theory::Effort effort); - /** - * Called by the output channel to request decisions "as soon as - * possible." - */ - void propagateAsDecision(TNode literal, theory::TheoryId theory); - /** * A variable to mark if we added any lemmas. */ diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 6161710f2..65f7238c9 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1172,9 +1172,6 @@ void SortModel::allocateCardinality( OutputChannel* out ){ } //require phase out->requirePhase( d_cardinality_literal[ d_aloc_cardinality ], true ); - //add the appropriate lemma, propagate as decision - //Trace("uf-ss-prop-as-dec") << "Propagate as decision " << lem[0] << " " << d_type << std::endl; - //out->propagateAsDecision( lem[0] ); d_thss->d_statistics.d_max_model_size.maxAssign( d_aloc_cardinality ); if( applyTotality( d_aloc_cardinality ) ){ -- 2.30.2