diff options
| author | lianah <lianahady@gmail.com> | 2014-11-18 14:35:02 -0500 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2014-11-18 14:35:02 -0500 |
| commit | fb6326517ce661d4d9bb1c593cce2a8b91eb51b3 (patch) | |
| tree | 6da2859de50b7bbfbbaf3b45dd0c551323bce08e /src/prop/minisat/core | |
| parent | ba02a5247204abc3b6d38a61f5f7d31f23e765ac (diff) | |
All Minisat solve calls now return lbool (fixes bug 599)
Diffstat (limited to 'src/prop/minisat/core')
| -rw-r--r-- | src/prop/minisat/core/Solver.h | 23 |
1 files changed, 10 insertions, 13 deletions
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<Lit>& assumps); // Search for a model that respects a given set of assumptions. + lbool solve (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions. lbool solveLimited (const vec<Lit>& 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<Lit>& 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<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_(); } inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); } inline bool Solver::okay () const { return ok; } |