CVC3
|
#include <xchaff.h>
Inherits SatSolver.
Public Member Functions | |
Xchaff () | |
~Xchaff () | |
int | NumVariables () |
Var | AddVariables (int nvars) |
Var | GetVar (int varIndex) |
int | GetVarIndex (Var v) |
Var | GetFirstVar () |
Var | GetNextVar (Var var) |
Lit | MakeLit (Var var, int phase) |
Var | GetVarFromLit (Lit lit) |
int | GetPhaseFromLit (Lit lit) |
int | NumClauses () |
Clause | AddClause (std::vector< Lit > &lits) |
Clause | GetClause (int clauseIndex) |
Clause | GetFirstClause () |
Clause | GetNextClause (Clause clause) |
void | GetClauseLits (SatSolver::Clause clause, std::vector< Lit > *lits) |
SatSolver::SATStatus | Satisfiable (bool allowNewClauses) |
int | GetVarAssignment (Var var) |
SatSolver::SATStatus | Continue () |
void | Restart () |
void | Reset () |
void | RegisterDLevelHook (void(*f)(void *, int), void *cookie) |
void | RegisterDecisionHook (Lit(*f)(void *, bool *), void *cookie) |
void | RegisterAssignmentHook (void(*f)(void *, Var, int), void *cookie) |
void | RegisterDeductionHook (void(*f)(void *), void *cookie) |
bool | SetBudget (int budget) |
bool | SetMemLimit (int mem_limit) |
bool | SetRandomness (int n) |
bool | SetRandSeed (int seed) |
bool | EnableClauseDeletion () |
bool | DisableClauseDeletion () |
int | GetBudgetUsed () |
int | GetMemUsed () |
int | GetNumDecisions () |
int | GetNumConflicts () |
int | GetNumExtConflicts () |
float | GetTotalTime () |
float | GetSATTime () |
int | GetNumLiterals () |
int | GetNumDeletedClauses () |
int | GetNumDeletedLiterals () |
int | GetNumImplications () |
int | GetMaxDLevel () |
![]() | |
SatSolver () | |
virtual | ~SatSolver () |
Var | AddVariable () |
virtual Var | GetVarFromLit (Lit lit)=0 |
virtual int | GetPhaseFromLit (Lit lit)=0 |
virtual Clause | AddClause (std::vector< Lit > &lits)=0 |
virtual bool | DeleteClause (Clause clause) |
virtual void | GetClauseLits (Clause clause, std::vector< Lit > *lits)=0 |
virtual void | RegisterDecisionHook (Lit(*f)(void *, bool *), void *cookie)=0 |
void | PrintStatistics (std::ostream &os=std::cout) |
Static Public Member Functions | |
static int | TranslateDecisionHook (void *cookie, bool *done) |
static void | TranslateAssignmentHook (void *cookie, int var, int value) |
![]() | |
static SatSolver * | Create () |
Static Private Member Functions | |
static Var | mkVar (int id) |
static Lit | mkLit (int id) |
static Clause | mkClause (int id) |
Private Attributes | |
CSolver * | _solver |
Lit(* | _decision_hook )(void *, bool *) |
void(* | _assignment_hook )(void *, Var, int) |
void * | _decision_hook_cookie |
void * | _assignment_hook_cookie |
Additional Inherited Members | |
![]() | |
enum | SATStatus { UNKNOWN, UNSATISFIABLE, SATISFIABLE, BUDGET_EXCEEDED, OUT_OF_MEMORY } |
typedef enum SatSolver::SATStatus | SATStatus |
|
inlinestaticprivate |
Definition at line 24 of file xchaff.h.
References SatSolver::Var::id.
Referenced by AddVariables(), GetVar(), GetVarFromLit(), and TranslateAssignmentHook().
|
inlinestaticprivate |
Definition at line 25 of file xchaff.h.
References SatSolver::Lit::id.
Referenced by GetClauseLits(), and MakeLit().
|
inlinestaticprivate |
Definition at line 26 of file xchaff.h.
References SatSolver::Clause::id.
Referenced by AddClause().
|
inlinevirtual |
Implements SatSolver.
Definition at line 36 of file xchaff.h.
References _solver, and CDatabase::num_variables().
|
inlinevirtual |
|
inlinevirtual |
|
inlinevirtual |
|
inlinevirtual |
Implements SatSolver.
Definition at line 44 of file xchaff.h.
References _solver, SatSolver::Var::id, and CDatabase::num_variables().
Implements SatSolver.
Definition at line 46 of file xchaff.h.
References _solver, SatSolver::Var::id, and CDatabase::num_variables().
|
inlinevirtual |
Implements SatSolver.
Definition at line 49 of file xchaff.h.
References SatSolver::Var::id, and mkLit().
|
inline |
|
inlinevirtual |
Implements SatSolver.
Definition at line 55 of file xchaff.h.
References _solver, and CDatabase::num_clauses().
|
inline |
Definition at line 57 of file xchaff.h.
References _solver, CSolver::add_clause(), and mkClause().
|
virtual |
Implements SatSolver.
Definition at line 20 of file xchaff.cpp.
References _solver, CDatabase::clause(), SatSolver::Clause::id, CClause::in_use(), and CDatabase::init_num_clauses().
|
inlinevirtual |
Implements SatSolver.
Definition at line 60 of file xchaff.h.
References _solver, CDatabase::clause(), CDatabase::clauses(), SatSolver::Clause::id, and CClause::in_use().
Implements SatSolver.
Definition at line 65 of file xchaff.h.
References _solver, CDatabase::clause(), SatSolver::Clause::id, and CClause::in_use().
void Xchaff::GetClauseLits | ( | SatSolver::Clause | clause, |
std::vector< Lit > * | lits | ||
) |
Definition at line 35 of file xchaff.cpp.
References _solver, CDatabase::clause(), SatSolver::Clause::id, CClause::literal(), mkLit(), CClause::num_lits(), and CLitPoolElement::s_var().
|
virtual |
Implements SatSolver.
Definition at line 43 of file xchaff.cpp.
References _solver, SatSolver::BUDGET_EXCEEDED, MEM_OUT, SatSolver::OUT_OF_MEMORY, SatSolver::SATISFIABLE, CSolver::solve(), TIME_OUT, SatSolver::UNKNOWN, and SatSolver::UNSATISFIABLE.
|
inlinevirtual |
Implements SatSolver.
Definition at line 72 of file xchaff.h.
References _solver, SatSolver::Var::id, CVariable::value(), and CDatabase::variable().
|
virtual |
Implements SatSolver.
Definition at line 57 of file xchaff.cpp.
References _solver, SatSolver::BUDGET_EXCEEDED, CSolver::continueCheck(), MEM_OUT, SatSolver::OUT_OF_MEMORY, SatSolver::SATISFIABLE, TIME_OUT, SatSolver::UNKNOWN, and SatSolver::UNSATISFIABLE.
|
inlinevirtual |
|
inlinevirtual |
Implements SatSolver.
Definition at line 80 of file xchaff.h.
References _solver, and CSolver::RegisterDLevelHook().
|
inlinestatic |
Definition at line 83 of file xchaff.h.
References _decision_hook, _decision_hook_cookie, and SatSolver::Lit::id.
Referenced by RegisterDecisionHook().
|
inline |
Definition at line 90 of file xchaff.h.
References _decision_hook, _decision_hook_cookie, _solver, CSolver::RegisterDecisionHook(), and TranslateDecisionHook().
|
inlinestatic |
Definition at line 94 of file xchaff.h.
References _assignment_hook, _assignment_hook_cookie, and mkVar().
Referenced by RegisterAssignmentHook().
|
inlinevirtual |
Implements SatSolver.
Definition at line 100 of file xchaff.h.
References _assignment_hook, _assignment_hook_cookie, _solver, CSolver::RegisterAssignmentHook(), and TranslateAssignmentHook().
|
inlinevirtual |
Implements SatSolver.
Definition at line 103 of file xchaff.h.
References _solver, and CSolver::RegisterDeductionHook().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 105 of file xchaff.h.
References _solver, and CSolver::set_time_limit().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 107 of file xchaff.h.
References _solver, and CSolver::set_mem_limit().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 109 of file xchaff.h.
References _solver, and CSolver::set_randomness().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 111 of file xchaff.h.
References _solver, and CSolver::set_random_seed().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 113 of file xchaff.h.
References _solver, and CSolver::enable_cls_deletion().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 115 of file xchaff.h.
References _solver, and CSolver::enable_cls_deletion().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 117 of file xchaff.h.
References _solver, and CSolver::total_run_time().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 119 of file xchaff.h.
References _solver, and CSolver::estimate_mem_usage().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 121 of file xchaff.h.
References _solver, and CSolver::num_decisions().
|
inlinevirtual |
|
inlinevirtual |
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 127 of file xchaff.h.
References _solver, and CSolver::total_run_time().
|
inlinevirtual |
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 131 of file xchaff.h.
References _solver, and CDatabase::num_literals().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 133 of file xchaff.h.
References _solver, and CDatabase::num_deleted_clauses().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 135 of file xchaff.h.
References _solver, and CDatabase::num_deleted_literals().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 137 of file xchaff.h.
References _solver, and CSolver::num_implications().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 139 of file xchaff.h.
References _solver, and CSolver::max_dlevel().
|
private |
Definition at line 17 of file xchaff.h.
Referenced by AddClause(), AddVariables(), Continue(), DisableClauseDeletion(), EnableClauseDeletion(), GetBudgetUsed(), GetClause(), GetClauseLits(), GetFirstClause(), GetFirstVar(), GetMaxDLevel(), GetMemUsed(), GetNextClause(), GetNextVar(), GetNumDecisions(), GetNumDeletedClauses(), GetNumDeletedLiterals(), GetNumImplications(), GetNumLiterals(), GetTotalTime(), GetVarAssignment(), NumClauses(), NumVariables(), RegisterAssignmentHook(), RegisterDecisionHook(), RegisterDeductionHook(), RegisterDLevelHook(), Satisfiable(), SetBudget(), SetMemLimit(), SetRandomness(), SetRandSeed(), Xchaff(), and ~Xchaff().
|
private |
Definition at line 19 of file xchaff.h.
Referenced by RegisterDecisionHook(), and TranslateDecisionHook().
|
private |
Definition at line 20 of file xchaff.h.
Referenced by RegisterAssignmentHook(), and TranslateAssignmentHook().
|
private |
Definition at line 21 of file xchaff.h.
Referenced by RegisterDecisionHook(), and TranslateDecisionHook().
|
private |
Definition at line 22 of file xchaff.h.
Referenced by RegisterAssignmentHook(), and TranslateAssignmentHook().