From fb6326517ce661d4d9bb1c593cce2a8b91eb51b3 Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 18 Nov 2014 14:35:02 -0500 Subject: [PATCH] All Minisat solve calls now return lbool (fixes bug 599) --- src/prop/bvminisat/bvminisat.cpp | 5 --- src/prop/bvminisat/bvminisat.h | 1 - src/prop/bvminisat/core/Solver.h | 23 ++++++------ src/prop/bvminisat/simp/SimpSolver.h | 44 ++++++++++++++++------- src/prop/minisat/core/Solver.h | 23 ++++++------ src/prop/minisat/minisat.cpp | 5 --- src/prop/minisat/minisat.h | 1 - src/prop/minisat/simp/SimpSolver.h | 54 +++++++++++++++++++++------- src/util/resource_manager.cpp | 6 ++-- 9 files changed, 96 insertions(+), 66 deletions(-) diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index aceb0f2e9..ab157844a 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -182,11 +182,6 @@ SatLiteral BVMinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) { BVMinisat::sign(lit)); } -SatValue BVMinisatSatSolver::toSatLiteralValue(bool res) { - if(res) return SAT_VALUE_TRUE; - else return SAT_VALUE_FALSE; -} - SatValue BVMinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) { if(res == (BVMinisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE; if(res == (BVMinisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN; diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index e163ddcfd..6246e6885 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -108,7 +108,6 @@ public: static SatVariable toSatVariable(BVMinisat::Var var); static BVMinisat::Lit toMinisatLit(SatLiteral lit); static SatLiteral toSatLiteral(BVMinisat::Lit lit); - static SatValue toSatLiteralValue(bool res); static SatValue toSatLiteralValue(BVMinisat::lbool res); static void toMinisatClause(SatClause& clause, BVMinisat::vec& minisat_clause); diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index a7a55208d..3fcf34185 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -99,12 +99,12 @@ public: // Solving: // bool simplify (); // Removes already satisfied clauses. - bool solve (const vec& assumps); // Search for a model that respects a given set of assumptions. + lbool solve (const vec& assumps); // Search for a model that respects a given set of assumptions. lbool solveLimited (const vec& assumps); // Search for a model that respects a given set of assumptions (With resource constraints). - bool solve (); // Search without assumptions. - bool solve (Lit p); // Search for a model that respects a single assumption. - bool solve (Lit p, Lit q); // Search for a model that respects two assumptions. - bool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions. + lbool solve (); // Search without assumptions. + lbool solve (Lit p); // Search for a model that respects a single assumption. + lbool solve (Lit p, Lit q); // Search for a model that respects two assumptions. + lbool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions. bool okay () const; // FALSE means solver is in a conflicting state lbool assertAssumption(Lit p, bool propagate); // Assert a new assumption, start BCP if propagate = true lbool propagateAssumptions(); // Do BCP over asserted assumptions @@ -421,14 +421,11 @@ inline bool Solver::withinBudget() const { (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) && (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); } -// FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a -// pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or -// all calls to solve must return an 'lbool'. I'm not yet sure which I prefer. -inline bool Solver::solve () { budgetOff(); return solve_() == l_True; } -inline bool Solver::solve (Lit p) { budgetOff(); assumptions.push(p); return solve_() == l_True; } -inline bool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; } -inline bool Solver::solve (Lit p, Lit q, Lit r) { budgetOff(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; } -inline bool Solver::solve (const vec& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; } +inline lbool Solver::solve () { budgetOff(); return solve_(); } +inline lbool Solver::solve (Lit p) { budgetOff(); assumptions.push(p); return solve_(); } +inline lbool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.push(p); assumptions.push(q); return solve_(); } +inline lbool Solver::solve (Lit p, Lit q, Lit r) { budgetOff(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(); } +inline lbool Solver::solve (const vec& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_(); } inline lbool Solver::solveLimited (const vec& assumps){ assumps.copyTo(assumptions); return solve_(); } inline bool Solver::okay () const { return ok; } diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index d808daa22..4ff17d3ab 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -56,13 +56,13 @@ class SimpSolver : public Solver { // Solving: // - bool solve (const vec& assumps, bool do_simp = true, bool turn_off_simp = false); - lbool solveLimited(const vec& assumps, bool do_simp = true, bool turn_off_simp = false); - lbool solveLimited(bool do_simp = true, bool turn_off_simp = false); - bool solve ( bool do_simp = true, bool turn_off_simp = false); - bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); - bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); - bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); + lbool solve (const vec& assumps, bool do_simp = true, bool turn_off_simp = false); + lbool solveLimited(const vec& assumps, bool do_simp = true, bool turn_off_simp = false); + lbool solveLimited(bool do_simp = true, bool turn_off_simp = false); + lbool solve ( bool do_simp = true, bool turn_off_simp = false); + lbool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); + lbool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); + lbool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification. // Memory managment: @@ -184,13 +184,31 @@ inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); } inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } -inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); return solve_(do_simp, turn_off_simp) == l_True; } -inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; } -inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; } -inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; } -inline bool SimpSolver::solve (const vec& assumps, bool do_simp, bool turn_off_simp){ +inline lbool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { + budgetOff(); + return solve_(do_simp, turn_off_simp); + } +inline lbool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { + budgetOff(); + assumptions.push(p); + return solve_(do_simp, turn_off_simp); + } +inline lbool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { + budgetOff(); + assumptions.push(p); + assumptions.push(q); + return solve_(do_simp, turn_off_simp); + } +inline lbool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { + budgetOff(); + assumptions.push(p); + assumptions.push(q); + assumptions.push(r); + return solve_(do_simp, turn_off_simp); + } +inline lbool SimpSolver::solve (const vec& assumps, bool do_simp, bool turn_off_simp){ budgetOff(); assumps.copyTo(assumptions); - return solve_(do_simp, turn_off_simp) == l_True; + return solve_(do_simp, turn_off_simp); } inline lbool SimpSolver::solveLimited (const vec& assumps, bool do_simp, bool turn_off_simp){ diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 3ec19b026..ecebb086d 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -169,12 +169,12 @@ public: // Solving: // bool simplify (); // Removes already satisfied clauses. - bool solve (const vec& assumps); // Search for a model that respects a given set of assumptions. + lbool solve (const vec& assumps); // Search for a model that respects a given set of assumptions. lbool solveLimited (const vec& assumps); // Search for a model that respects a given set of assumptions (With resource constraints). - bool solve (); // Search without assumptions. - bool solve (Lit p); // Search for a model that respects a single assumption. - bool solve (Lit p, Lit q); // Search for a model that respects two assumptions. - bool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions. + lbool solve (); // Search without assumptions. + lbool solve (Lit p); // Search for a model that respects a single assumption. + lbool solve (Lit p, Lit q); // Search for a model that respects two assumptions. + lbool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions. bool okay () const; // FALSE means solver is in a conflicting state void toDimacs (); @@ -535,14 +535,11 @@ inline void Solver::interrupt(){ asynch_interrupt = true; } inline void Solver::clearInterrupt(){ asynch_interrupt = false; } inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; } -// FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a -// pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or -// all calls to solve must return an 'lbool'. I'm not yet sure which I prefer. -inline bool Solver::solve () { budgetOff(); assumptions.clear(); return solve_() == l_True; } -inline bool Solver::solve (Lit p) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; } -inline bool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; } -inline bool Solver::solve (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; } -inline bool Solver::solve (const vec& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; } +inline lbool Solver::solve () { budgetOff(); assumptions.clear(); return solve_(); } +inline lbool Solver::solve (Lit p) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(); } +inline lbool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(); } +inline lbool Solver::solve (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(); } +inline lbool Solver::solve (const vec& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_(); } inline lbool Solver::solveLimited (const vec& assumps){ assumps.copyTo(assumptions); return solve_(); } inline bool Solver::okay () const { return ok; } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index b9fa37230..b896b03fb 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -59,11 +59,6 @@ SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) { Minisat::sign(lit)); } -SatValue MinisatSatSolver::toSatLiteralValue(bool res) { - if(res) return SAT_VALUE_TRUE; - else return SAT_VALUE_FALSE; -} - SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE; if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN; diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 7c6e10170..a355702bc 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -42,7 +42,6 @@ public: static SatVariable toSatVariable(Minisat::Var var); static Minisat::Lit toMinisatLit(SatLiteral lit); static SatLiteral toSatLiteral(Minisat::Lit lit); - static SatValue toSatLiteralValue(bool res); static SatValue toSatLiteralValue(Minisat::lbool res); static Minisat::lbool toMinisatlbool(SatValue val); //(Commented because not in use) static bool tobool(SatValue val); diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 041309546..e1dfeb95e 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -62,12 +62,12 @@ class SimpSolver : public Solver { // Solving: // - bool solve (const vec& assumps, bool do_simp = true, bool turn_off_simp = false); - lbool solveLimited(const vec& assumps, bool do_simp = true, bool turn_off_simp = false); - bool solve ( bool do_simp = true, bool turn_off_simp = false); - bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); - bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); - bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); + lbool solve (const vec& assumps, bool do_simp = true, bool turn_off_simp = false); + lbool solveLimited(const vec& assumps, bool do_simp = true, bool turn_off_simp = false); + lbool solve ( bool do_simp = true, bool turn_off_simp = false); + lbool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); + lbool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); + lbool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification. // Memory managment: @@ -193,12 +193,42 @@ inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable, uint6 { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); } inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } -inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; } -inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; } -inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; } -inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; } -inline bool SimpSolver::solve (const vec& assumps, bool do_simp, bool turn_off_simp){ - budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; } +// the solver can always return unknown due to resource limiting +inline lbool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { + budgetOff(); + assumptions.clear(); + return solve_(do_simp, turn_off_simp); + } + +inline lbool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { + budgetOff(); + assumptions.clear(); + assumptions.push(p); + return solve_(do_simp, turn_off_simp); + } + +inline lbool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { + budgetOff(); + assumptions.clear(); + assumptions.push(p); + assumptions.push(q); + return solve_(do_simp, turn_off_simp); + } + +inline lbool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { + budgetOff(); + assumptions.clear(); + assumptions.push(p); + assumptions.push(q); + assumptions.push(r); + return solve_(do_simp, turn_off_simp); + } + + inline lbool SimpSolver::solve (const vec& assumps, bool do_simp, bool turn_off_simp){ + budgetOff(); + assumps.copyTo(assumptions); + return solve_(do_simp, turn_off_simp); + } inline lbool SimpSolver::solveLimited (const vec& assumps, bool do_simp, bool turn_off_simp){ assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); } diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 2aca55616..b0fd37fd2 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -184,10 +184,10 @@ void ResourceManager::spendResource() throw (UnsafeInterruptException) { Trace("limit") << "ResourceManager::spendResource: elapsed time" << d_cumulativeTimer.elapsed() << std::endl; } - if (smt::smtEngineInScope()) { - theory::Rewriter::clearCaches(); - } if (d_isHardLimit) { + if (smt::smtEngineInScope()) { + theory::Rewriter::clearCaches(); + } throw UnsafeInterruptException(); } -- 2.30.2