sat_solvers/minisat/Solver.C

0 /****************************************************************************************[Solver.C]
20 #include "Solver.h"
62 void Solver::newClause(const vec<Lit>& ps_, bool learnt, ClauseId id)
151 void Solver::remove(Clause* c, bool just_dealloc)
171 bool Solver::simplify(Clause* c) const
189 Var Solver::newVar() {
207 bool Solver::assume(Lit p) {
213 void Solver::cancelUntil(int level) {
254 void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
372 bool Solver::analyze_removable(Lit p, uint min_level)
413 void Solver::analyzeFinal(Clause* confl, bool skip_first)
472 bool Solver::enqueue(Lit p, Clause* from)
501 Clause* Solver::propagate()
583 void Solver::reduceDB()
613 void Solver::simplifyDB()
664 lbool Solver::search(int nof_conflicts, int nof_learnts, const SearchParams& params)
731 double Solver::progressEstimate()
744 void Solver::varRescaleActivity()
754 void Solver::claRescaleActivity()
775 bool Solver::solve(const vec<Lit>& assumps)