CVC3
2.4.1
|
#include <minisat_solver.h>
Public Member Functions | |
SolverStats () | |
Public Attributes | |
int64_t | starts |
int64_t | decisions |
int64_t | propagations |
int64_t | conflicts |
int64_t | theory_conflicts |
int64_t | max_level |
int64_t | clauses_literals |
int64_t | learnts_literals |
int64_t | max_literals |
int64_t | del_clauses |
int64_t | del_lemmas |
int64_t | db_simpl |
int64_t | lm_simpl |
int64_t | debug |
Definition at line 162 of file minisat_solver.h.
|
inline |
Definition at line 167 of file minisat_solver.h.
int64_t MiniSat::SolverStats::starts |
Definition at line 163 of file minisat_solver.h.
Referenced by MiniSat::Solver::search().
int64_t MiniSat::SolverStats::decisions |
Definition at line 163 of file minisat_solver.h.
Referenced by SAT::DPLLTMiniSat::search(), and MiniSat::Solver::search().
int64_t MiniSat::SolverStats::propagations |
Definition at line 163 of file minisat_solver.h.
Referenced by MiniSat::Solver::propagate(), and SAT::DPLLTMiniSat::search().
int64_t MiniSat::SolverStats::conflicts |
Definition at line 163 of file minisat_solver.h.
Referenced by SAT::DPLLTMiniSat::search(), and MiniSat::Solver::search().
int64_t MiniSat::SolverStats::theory_conflicts |
Definition at line 163 of file minisat_solver.h.
Referenced by SAT::DPLLTMiniSat::search(), and MiniSat::Solver::search().
int64_t MiniSat::SolverStats::max_level |
Definition at line 163 of file minisat_solver.h.
Referenced by MiniSat::Solver::assume(), and SAT::DPLLTMiniSat::search().
int64_t MiniSat::SolverStats::clauses_literals |
Definition at line 164 of file minisat_solver.h.
Referenced by MiniSat::Solver::insertClause(), MiniSat::Solver::remove(), SAT::DPLLTMiniSat::search(), and MiniSat::Solver::simplifyDB().
int64_t MiniSat::SolverStats::learnts_literals |
Definition at line 164 of file minisat_solver.h.
Referenced by MiniSat::Solver::insertClause(), MiniSat::Solver::insertLemma(), MiniSat::Solver::pop(), MiniSat::Solver::push(), MiniSat::Solver::remove(), SAT::DPLLTMiniSat::search(), and MiniSat::Solver::simplifyDB().
int64_t MiniSat::SolverStats::max_literals |
Definition at line 164 of file minisat_solver.h.
Referenced by MiniSat::Solver::insertClause(), and SAT::DPLLTMiniSat::search().
int64_t MiniSat::SolverStats::del_clauses |
Definition at line 164 of file minisat_solver.h.
Referenced by SAT::DPLLTMiniSat::search(), and MiniSat::Solver::simplifyDB().
int64_t MiniSat::SolverStats::del_lemmas |
Definition at line 164 of file minisat_solver.h.
Referenced by MiniSat::Solver::reduceDB(), and SAT::DPLLTMiniSat::search().
int64_t MiniSat::SolverStats::db_simpl |
Definition at line 164 of file minisat_solver.h.
Referenced by SAT::DPLLTMiniSat::search(), and MiniSat::Solver::simplifyDB().
int64_t MiniSat::SolverStats::lm_simpl |
Definition at line 164 of file minisat_solver.h.
Referenced by MiniSat::Solver::reduceDB(), and SAT::DPLLTMiniSat::search().
int64_t MiniSat::SolverStats::debug |
Definition at line 164 of file minisat_solver.h.
Referenced by MiniSat::Solver::pop(), SAT::DPLLTMiniSat::search(), and MiniSat::Solver::search().