CVC3
2.4.1
|
#include <xchaff.h>
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 CDatabase::num_variables().
|
inlinevirtual |
Implements SatSolver.
Definition at line 38 of file xchaff.h.
References CSolver::add_variables(), and mkVar().
|
inlinevirtual |
|
inlinevirtual |
|
inlinevirtual |
Implements SatSolver.
Definition at line 44 of file xchaff.h.
References SatSolver::Var::id, and CDatabase::num_variables().
Implements SatSolver.
Definition at line 46 of file xchaff.h.
References 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 |
|
inline |
Definition at line 57 of file xchaff.h.
References 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 CDatabase::clause(), CDatabase::clauses(), SatSolver::Clause::id, and CClause::in_use().
Implements SatSolver.
Definition at line 65 of file xchaff.h.
References 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 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 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, 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, CSolver::RegisterAssignmentHook(), and TranslateAssignmentHook().
|
inlinevirtual |
Implements SatSolver.
Definition at line 103 of file xchaff.h.
References CSolver::RegisterDeductionHook().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 105 of file xchaff.h.
References CSolver::set_time_limit().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 107 of file xchaff.h.
References CSolver::set_mem_limit().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 109 of file xchaff.h.
References CSolver::set_randomness().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 111 of file xchaff.h.
References CSolver::set_random_seed().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 113 of file xchaff.h.
References CSolver::enable_cls_deletion().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 115 of file xchaff.h.
References CSolver::enable_cls_deletion().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 117 of file xchaff.h.
References CSolver::total_run_time().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 119 of file xchaff.h.
References CSolver::estimate_mem_usage().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 121 of file xchaff.h.
References CSolver::num_decisions().
|
inlinevirtual |
|
inlinevirtual |
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 127 of file xchaff.h.
References CSolver::total_run_time().
|
inlinevirtual |
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 131 of file xchaff.h.
References CDatabase::num_literals().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 133 of file xchaff.h.
References CDatabase::num_deleted_clauses().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 135 of file xchaff.h.
References CDatabase::num_deleted_literals().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 137 of file xchaff.h.
References CSolver::num_implications().
|
inlinevirtual |
Reimplemented from SatSolver.
Definition at line 139 of file xchaff.h.
References CSolver::max_dlevel().
|
private |
Definition at line 17 of file xchaff.h.
Referenced by Continue(), GetClause(), GetClauseLits(), Satisfiable(), 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 TranslateDecisionHook().
|
private |
Definition at line 22 of file xchaff.h.
Referenced by TranslateAssignmentHook().