diff options
Diffstat (limited to 'src/prop/bvminisat/simp/SimpSolver.h')
| -rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 85 |
1 files changed, 49 insertions, 36 deletions
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 246bb7152..9d3a51c02 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -37,42 +37,55 @@ class SimpSolver : public Solver { public: // Constructor/Destructor: // - SimpSolver(CVC4::context::Context* c); - ~SimpSolver(); - - // Problem specification: - // - Var newVar (bool polarity = true, bool dvar = true, bool freeze = false); - bool addClause (const vec<Lit>& ps, ClauseId& id); - bool addEmptyClause(); // Add the empty clause to the solver. - bool addClause (Lit p, ClauseId& id); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, ClauseId& id); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, ClauseId& id); // Add a ternary clause to the solver. - bool addClause_( vec<Lit>& ps, ClauseId& id); - bool substitute(Var v, Lit x); // Replace all occurences 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 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: - // - void garbageCollect() override; - - // Generate a (possibly simplified) DIMACS file: - // + SimpSolver(CVC4::context::Context* context); + ~SimpSolver(); + + // Problem specification: + // + Var newVar(bool polarity = true, bool dvar = true, bool freeze = false); + bool addClause(const vec<Lit>& ps, ClauseId& id); + bool addEmptyClause(); // Add the empty clause to the solver. + bool addClause(Lit p, ClauseId& id); // Add a unit clause to the solver. + bool addClause(Lit p, + Lit q, + ClauseId& id); // Add a binary clause to the solver. + bool addClause(Lit p, + Lit q, + Lit r, + ClauseId& id); // Add a ternary clause to the solver. + bool addClause_(vec<Lit>& ps, ClauseId& id); + bool substitute(Var v, Lit x); // Replace all occurences 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 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: + // + 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); |