CVC3  2.4.1
Public Member Functions | Public Attributes | List of all members
MiniSat::SolverStats Struct Reference

#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
 

Detailed Description

Definition at line 162 of file minisat_solver.h.

Constructor & Destructor Documentation

MiniSat::SolverStats::SolverStats ( )
inline

Definition at line 167 of file minisat_solver.h.

Member Data Documentation

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
int64_t MiniSat::SolverStats::learnts_literals
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

The documentation for this struct was generated from the following file: