diff options
Diffstat (limited to 'src/prop/minisat/simp/SimpSolver.h')
| -rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 129 |
1 files changed, 82 insertions, 47 deletions
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index c13ee5583..f952aee1e 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -43,41 +43,66 @@ class SimpSolver : public Solver { public: // Constructor/Destructor: // - SimpSolver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enableIncremental = false); - CVC4_PUBLIC ~SimpSolver(); - - // Problem specification: - // - Var newVar (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); - bool addClause (const vec<Lit>& ps, bool removable, ClauseId& id); - bool addEmptyClause(bool removable); // Add the empty clause to the solver. - bool addClause (Lit p, bool removable, ClauseId& id); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver. - bool addClause_(vec<Lit>& ps, bool removable, ClauseId& id); - bool substitute(Var v, Lit x); // Replace all occurrences of v with x (may cause a contradiction). - - // Variable mode: - // - void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated. - bool isEliminated(Var v) const; - - // Solving: - // - lbool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false); - lbool solveLimited(const vec<Lit>& 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: - // - void garbageCollect() override; - - // Generate a (possibly simplified) DIMACS file: - // + SimpSolver(CVC4::prop::TheoryProxy* proxy, + CVC4::context::Context* context, + CVC4::context::UserContext* userContext, + ProofNodeManager* pnm, + bool enableIncremental = false); + CVC4_PUBLIC ~SimpSolver(); + + // Problem specification: + // + Var newVar(bool polarity = true, + bool dvar = true, + bool isTheoryAtom = false, + bool preRegister = false, + bool canErase = true); + bool addClause(const vec<Lit>& ps, bool removable, ClauseId& id); + bool addEmptyClause(bool removable); // Add the empty clause to the solver. + bool addClause(Lit p, + bool removable, + ClauseId& id); // Add a unit clause to the solver. + bool addClause(Lit p, + Lit q, + bool removable, + ClauseId& id); // Add a binary clause to the solver. + bool addClause(Lit p, + Lit q, + Lit r, + bool removable, + ClauseId& id); // Add a ternary clause to the solver. + bool addClause_(vec<Lit>& ps, bool removable, ClauseId& id); + bool substitute(Var v, Lit x); // Replace all occurrences of v with x (may + // cause a contradiction). + + // Variable mode: + // + void setFrozen(Var v, + bool b); // If a variable is frozen it will not be eliminated. + bool isEliminated(Var v) const; + + // Solving: + // + lbool solve(const vec<Lit>& assumps, + bool do_simp = true, + bool turn_off_simp = false); + lbool solveLimited(const vec<Lit>& 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: + // + void garbageCollect() override; + + // Generate a (possibly simplified) DIMACS file: + // #if 0 void toDimacs (const char* file, const vec<Lit>& assumps); void toDimacs (const char* file); @@ -118,11 +143,13 @@ class SimpSolver : public Solver { // old ordering function // bool operator()(Var x, Var y) const { return cost(x) < cost(y); } - - bool operator()(Var x, Var y) const { - int c_x = cost(x); - int c_y = cost(y); - return c_x < c_y || (c_x == c_y && x < y); } + + bool operator()(Var x, Var y) const + { + int c_x = cost(x); + int c_y = cost(y); + return c_x < c_y || (c_x == c_y && x < y); + } }; struct ClauseDeleted { @@ -200,14 +227,14 @@ inline lbool SimpSolver::solve ( bool do_simp, bool t 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(); @@ -215,7 +242,7 @@ inline lbool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool t 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(); @@ -225,16 +252,24 @@ inline lbool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool t return solve_(do_simp, turn_off_simp); } - inline lbool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ + inline lbool SimpSolver::solve(const vec<Lit>& 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<Lit>& assumps, bool do_simp, bool turn_off_simp){ - assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); } + inline lbool SimpSolver::solveLimited(const vec<Lit>& assumps, + bool do_simp, + bool turn_off_simp) + { + assumps.copyTo(assumptions); + return solve_(do_simp, turn_off_simp); + } -//================================================================================================= + //================================================================================================= } /* CVC4::Minisat namespace */ } /* CVC4 namespace */ |