CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Static Private Member Functions | Private Attributes
Xchaff Class Reference

#include <xchaff.h>

Inheritance diagram for Xchaff:
SatSolver

List of all members.

Public Member Functions

Static Public Member Functions

Static Private Member Functions

Private Attributes


Constructor & Destructor Documentation

Xchaff::Xchaff ( ) [inline]

Definition at line 29 of file xchaff.h.

References _solver.

Xchaff::~Xchaff ( ) [inline]

Definition at line 30 of file xchaff.h.

References _solver.


Member Function Documentation

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]

Implements SatSolver.

Definition at line 38 of file xchaff.h.

References mkVar(), _solver, and CSolver::add_variables().

Var Xchaff::GetVar ( int  varIndex) [inline, virtual]

Implements SatSolver.

Definition at line 40 of file xchaff.h.

References mkVar().

int Xchaff::GetVarIndex ( Var  v) [inline, virtual]

Implements SatSolver.

Definition at line 42 of file xchaff.h.

References SatSolver::Var::id.

Var Xchaff::GetFirstVar ( ) [inline, virtual]

Implements SatSolver.

Definition at line 44 of file xchaff.h.

References _solver, CDatabase::num_variables(), and SatSolver::Var::id.

Var Xchaff::GetNextVar ( Var  var) [inline, virtual]

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]

Definition at line 51 of file xchaff.h.

References mkVar().

int Xchaff::GetPhaseFromLit ( Lit  lit) [inline]

Definition at line 53 of file xchaff.h.

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]
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.

Clause Xchaff::GetNextClause ( Clause  clause) [inline, virtual]

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 
)
SatSolver::SATStatus Xchaff::Satisfiable ( bool  allowNewClauses) [virtual]
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]
void Xchaff::Restart ( ) [inline, virtual]

Implements SatSolver.

Definition at line 77 of file xchaff.h.

void Xchaff::Reset ( ) [inline, virtual]

Implements SatSolver.

Definition at line 78 of file xchaff.h.

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]
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]
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]

Reimplemented from SatSolver.

Definition at line 123 of file xchaff.h.

int Xchaff::GetNumExtConflicts ( ) [inline, virtual]

Reimplemented from SatSolver.

Definition at line 125 of file xchaff.h.

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]

Reimplemented from SatSolver.

Definition at line 129 of file xchaff.h.

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().


Member Data Documentation

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().

Definition at line 21 of file xchaff.h.

Referenced by TranslateDecisionHook(), and RegisterDecisionHook().

Definition at line 22 of file xchaff.h.

Referenced by TranslateAssignmentHook(), and RegisterAssignmentHook().


The documentation for this class was generated from the following files: