Xchaff Class Reference

#include <xchaff.h>

Inheritance diagram for Xchaff:

[legend]Collaboration diagram for Xchaff:

[legend]List of all members.

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 (vector< Lit > &lits)
Clause GetClause (int clauseIndex)
Clause GetFirstClause ()
Clause GetNextClause (Clause clause)
void GetClauseLits (Clause clause, 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 ()

Static Public Member Functions

static int TranslateDecisionHook (void *cookie, bool *done)
static void TranslateAssignmentHook (void *cookie, int var, int value)

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

Detailed Description

Definition at line 18 of file xchaff.h.

Constructor & Destructor Documentation

Xchaff::Xchaff ( ) [inline]

Definition at line 31 of file xchaff.h.
References _solver.

Xchaff::~Xchaff ( ) [inline]

Definition at line 32 of file xchaff.h.
References _solver.

Member Function Documentation

static Var Xchaff::mkVar ( int id ) [inline, static, private]

Definition at line 26 of file xchaff.h.
Referenced by AddVariables(), GetVar(), GetVarFromLit(), and TranslateAssignmentHook().

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

Definition at line 27 of file xchaff.h.
Referenced by MakeLit().

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

Definition at line 28 of file xchaff.h.
Referenced by AddClause().

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

Implements SatSolver.
Definition at line 38 of file xchaff.h.
References _solver, and CDatabase::num_variables().

Var Xchaff::AddVariables ( int nvars ) [inline, virtual]

Implements SatSolver.
Definition at line 40 of file xchaff.h.
References _solver, CSolver::add_variables(), and mkVar().

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

Implements SatSolver.
Definition at line 42 of file xchaff.h.
References mkVar().

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

Definition at line 44 of file xchaff.h.

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

Implements SatSolver.
Definition at line 46 of file xchaff.h.
References _solver, and CDatabase::num_variables().

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

Definition at line 48 of file xchaff.h.
References _solver, and CDatabase::num_variables().

Lit Xchaff::MakeLit ( Var var,

int phase

) [inline]

Definition at line 51 of file xchaff.h.
References mkLit().

Var Xchaff::GetVarFromLit ( Lit lit ) [inline]

Definition at line 53 of file xchaff.h.
References mkVar().

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

Definition at line 55 of file xchaff.h.

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

Implements SatSolver.
Definition at line 57 of file xchaff.h.
References _solver, and CDatabase::num_clauses().

Clause Xchaff::AddClause ( vector< Lit > & lits ) [inline]

Definition at line 59 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 62 of file xchaff.h.
References _solver, CDatabase::clause(), and CClause::in_use().

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

Definition at line 67 of file xchaff.h.
References _solver, CDatabase::clause(), and CClause::in_use().

void Xchaff::GetClauseLits ( Clause clause,

vector< Lit > * lits

)

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 74 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 79 of file xchaff.h.

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

Implements SatSolver.
Definition at line 80 of file xchaff.h.

void Xchaff::RegisterDLevelHook ( void(*)(void *, int) f,

void * cookie

) [inline, virtual]

Implements SatSolver.
Definition at line 82 of file xchaff.h.
References _solver, and CSolver::RegisterDLevelHook().

static int Xchaff::TranslateDecisionHook ( void * cookie,

bool * done

) [inline, static]

Definition at line 85 of file xchaff.h.
References _decision_hook, _decision_hook_cookie, and b.
Referenced by RegisterDecisionHook().

void Xchaff::RegisterDecisionHook ( Lit(*)(void *, bool *) f,

void * cookie

) [inline]

Definition at line 92 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 96 of file xchaff.h.
References _assignment_hook, _assignment_hook_cookie, b, and mkVar().
Referenced by RegisterAssignmentHook().

void Xchaff::RegisterAssignmentHook ( void(*)(void *, Var, int) f,

void * cookie

) [inline]

Definition at line 102 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 105 of file xchaff.h.
References _solver, and CSolver::RegisterDeductionHook().

bool Xchaff::SetBudget ( int budget ) [inline, virtual]

Reimplemented from SatSolver.
Definition at line 107 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 109 of file xchaff.h.
References _solver, and CSolver::set_mem_limit().

bool Xchaff::SetRandomness ( int n ) [inline, virtual]

Reimplemented from SatSolver.
Definition at line 111 of file xchaff.h.
References _solver, and CSolver::set_randomness().

bool Xchaff::SetRandSeed ( int seed ) [inline, virtual]

Reimplemented from SatSolver.
Definition at line 113 of file xchaff.h.
References _solver, and CSolver::set_random_seed().

bool Xchaff::EnableClauseDeletion ( ) [inline, virtual]

Reimplemented from SatSolver.
Definition at line 115 of file xchaff.h.
References _solver, and CSolver::enable_cls_deletion().

bool Xchaff::DisableClauseDeletion ( ) [inline, virtual]

Reimplemented from SatSolver.
Definition at line 117 of file xchaff.h.
References _solver, and CSolver::enable_cls_deletion().

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

Reimplemented from SatSolver.
Definition at line 119 of file xchaff.h.
References _solver, and CSolver::total_run_time().

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

Reimplemented from SatSolver.
Definition at line 121 of file xchaff.h.
References _solver, and CSolver::estimate_mem_usage().

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

Reimplemented from SatSolver.
Definition at line 123 of file xchaff.h.
References _solver, and CSolver::num_decisions().

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

Reimplemented from SatSolver.
Definition at line 125 of file xchaff.h.

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

Reimplemented from SatSolver.
Definition at line 127 of file xchaff.h.

float Xchaff::GetTotalTime ( ) [inline, virtual]

Reimplemented from SatSolver.
Definition at line 129 of file xchaff.h.
References _solver, and CSolver::total_run_time().

float Xchaff::GetSATTime ( ) [inline, virtual]

Reimplemented from SatSolver.
Definition at line 131 of file xchaff.h.

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

Reimplemented from SatSolver.
Definition at line 133 of file xchaff.h.
References _solver, and CDatabase::num_literals().

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

Reimplemented from SatSolver.
Definition at line 135 of file xchaff.h.
References _solver, and CDatabase::num_deleted_clauses().

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

Reimplemented from SatSolver.
Definition at line 137 of file xchaff.h.
References _solver, and CDatabase::num_deleted_literals().

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

Reimplemented from SatSolver.
Definition at line 139 of file xchaff.h.
References _solver, and CSolver::num_implications().

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

Reimplemented from SatSolver.
Definition at line 141 of file xchaff.h.
References _solver, and CSolver::max_dlevel().

Member Data Documentation

CSolver* Xchaff::_solver [private]

Definition at line 19 of file xchaff.h.
Referenced by AddClause(), AddVariables(), Continue(), DisableClauseDeletion(), EnableClauseDeletion(), GetBudgetUsed(), GetClause(), 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 23 of file xchaff.h.
Referenced by RegisterDecisionHook(), and TranslateDecisionHook().

void* Xchaff::_assignment_hook_cookie [private]

Definition at line 24 of file xchaff.h.
Referenced by RegisterAssignmentHook(), and TranslateAssignmentHook().

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

Generated on Thu Apr 13 16:57:37 2006 for CVC Lite by

1.4.4