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