Xchaff Class Reference

#include <xchaff.h>

Inheritance diagram for Xchaff:

Inheritance graph
[legend]
Collaboration diagram for Xchaff:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Static Public Member Functions

Static Private Member Functions

Private Attributes


Detailed Description

Definition at line 16 of file xchaff.h.


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.

Referenced by AddVariables(), GetVar(), GetVarFromLit(), and TranslateAssignmentHook().

static Lit Xchaff::mkLit ( int  id  )  [inline, static, private]

Definition at line 25 of file xchaff.h.

Referenced by GetClauseLits(), and MakeLit().

static Clause Xchaff::mkClause ( int  id  )  [inline, static, private]

Definition at line 26 of file xchaff.h.

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 _solver, CSolver::add_variables(), and mkVar().

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]

Definition at line 42 of file xchaff.h.

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

Implements SatSolver.

Definition at line 44 of file xchaff.h.

References _solver, and CDatabase::num_variables().

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

Definition at line 46 of file xchaff.h.

References _solver, and CDatabase::num_variables().

Lit Xchaff::MakeLit ( Var  var,
int  phase 
) [inline]

Definition at line 49 of file xchaff.h.

References mkLit().

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 _solver, CSolver::add_clause(), and mkClause().

SatSolver::Clause Xchaff::GetClause ( int  clauseIndex  )  [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().

Clause Xchaff::GetFirstClause (  )  [inline, virtual]

Implements SatSolver.

Definition at line 60 of file xchaff.h.

References _solver, CDatabase::clause(), CDatabase::clauses(), and CClause::in_use().

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

Definition at line 65 of file xchaff.h.

References _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::literal(), mkLit(), CClause::num_lits(), and CLitPoolElement::s_var().

SatSolver::SATStatus Xchaff::Satisfiable ( bool  allowNewClauses  )  [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.

int Xchaff::GetVarAssignment ( Var  var  )  [inline]

Definition at line 72 of file xchaff.h.

References _solver, CVariable::value(), and CDatabase::variable().

SatSolver::SATStatus Xchaff::Continue (  )  [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.

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, and _decision_hook_cookie.

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]

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]

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

CSolver* Xchaff::_solver [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().

Lit(* Xchaff::_decision_hook)(void *, bool *) [private]

Referenced by RegisterDecisionHook(), and TranslateDecisionHook().

void(* Xchaff::_assignment_hook)(void *, Var, int) [private]

Referenced by RegisterAssignmentHook(), and TranslateAssignmentHook().

void* Xchaff::_decision_hook_cookie [private]

Definition at line 21 of file xchaff.h.

Referenced by RegisterDecisionHook(), and TranslateDecisionHook().

void* Xchaff::_assignment_hook_cookie [private]

Definition at line 22 of file xchaff.h.

Referenced by RegisterAssignmentHook(), and TranslateAssignmentHook().


The documentation for this class was generated from the following files:
Generated on Tue Jul 3 14:35:24 2007 for CVC3 by  doxygen 1.5.1