CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Static Private Member Functions | Private Attributes | List of all members
Xchaff Class Reference

#include <xchaff.h>

Inheritance diagram for Xchaff:
SatSolver

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 ()
- Public Member Functions inherited from SatSolver
 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 Public Member Functions inherited from SatSolver
static SatSolverCreate ()

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

- Public Types inherited from SatSolver
enum  SATStatus {
  UNKNOWN, UNSATISFIABLE, SATISFIABLE, BUDGET_EXCEEDED,
  OUT_OF_MEMORY
}
typedef enum SatSolver::SATStatus SATStatus

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)
inlinestaticprivate

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)
inlinestaticprivate

Definition at line 25 of file xchaff.h.

References SatSolver::Lit::id.

Referenced by GetClauseLits(), and MakeLit().

static Clause Xchaff::mkClause ( int  id)
inlinestaticprivate

Definition at line 26 of file xchaff.h.

References SatSolver::Clause::id.

Referenced by AddClause().

int Xchaff::NumVariables ( )
inlinevirtual

Implements SatSolver.

Definition at line 36 of file xchaff.h.

References _solver, and CDatabase::num_variables().

Var Xchaff::AddVariables ( int  nvars)
inlinevirtual

Implements SatSolver.

Definition at line 38 of file xchaff.h.

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

Var Xchaff::GetVar ( int  varIndex)
inlinevirtual

Implements SatSolver.

Definition at line 40 of file xchaff.h.

References mkVar().

int Xchaff::GetVarIndex ( Var  v)
inlinevirtual

Implements SatSolver.

Definition at line 42 of file xchaff.h.

References SatSolver::Var::id.

Var Xchaff::GetFirstVar ( )
inlinevirtual

Implements SatSolver.

Definition at line 44 of file xchaff.h.

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

Var Xchaff::GetNextVar ( Var  var)
inlinevirtual

Implements SatSolver.

Definition at line 46 of file xchaff.h.

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

Lit Xchaff::MakeLit ( Var  var,
int  phase 
)
inlinevirtual

Implements SatSolver.

Definition at line 49 of file xchaff.h.

References SatSolver::Var::id, and 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 ( )
inlinevirtual

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
Clause Xchaff::GetFirstClause ( )
inlinevirtual

Implements SatSolver.

Definition at line 60 of file xchaff.h.

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

Clause Xchaff::GetNextClause ( Clause  clause)
inlinevirtual

Implements SatSolver.

Definition at line 65 of file xchaff.h.

References _solver, CDatabase::clause(), SatSolver::Clause::id, 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)
inlinevirtual

Implements SatSolver.

Definition at line 72 of file xchaff.h.

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

SatSolver::SATStatus Xchaff::Continue ( )
virtual
void Xchaff::Restart ( )
inlinevirtual

Implements SatSolver.

Definition at line 77 of file xchaff.h.

void Xchaff::Reset ( )
inlinevirtual

Implements SatSolver.

Definition at line 78 of file xchaff.h.

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

Implements SatSolver.

Definition at line 80 of file xchaff.h.

References _solver, and CSolver::RegisterDLevelHook().

static int Xchaff::TranslateDecisionHook ( void *  cookie,
bool *  done 
)
inlinestatic

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 
)
inlinestatic

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 
)
inlinevirtual
void Xchaff::RegisterDeductionHook ( void(*)(void *)  f,
void *  cookie 
)
inlinevirtual

Implements SatSolver.

Definition at line 103 of file xchaff.h.

References _solver, and CSolver::RegisterDeductionHook().

bool Xchaff::SetBudget ( int  budget)
inlinevirtual

Reimplemented from SatSolver.

Definition at line 105 of file xchaff.h.

References _solver, and CSolver::set_time_limit().

bool Xchaff::SetMemLimit ( int  mem_limit)
inlinevirtual

Reimplemented from SatSolver.

Definition at line 107 of file xchaff.h.

References _solver, and CSolver::set_mem_limit().

bool Xchaff::SetRandomness ( int  n)
inlinevirtual

Reimplemented from SatSolver.

Definition at line 109 of file xchaff.h.

References _solver, and CSolver::set_randomness().

bool Xchaff::SetRandSeed ( int  seed)
inlinevirtual

Reimplemented from SatSolver.

Definition at line 111 of file xchaff.h.

References _solver, and CSolver::set_random_seed().

bool Xchaff::EnableClauseDeletion ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 113 of file xchaff.h.

References _solver, and CSolver::enable_cls_deletion().

bool Xchaff::DisableClauseDeletion ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 115 of file xchaff.h.

References _solver, and CSolver::enable_cls_deletion().

int Xchaff::GetBudgetUsed ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 117 of file xchaff.h.

References _solver, and CSolver::total_run_time().

int Xchaff::GetMemUsed ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 119 of file xchaff.h.

References _solver, and CSolver::estimate_mem_usage().

int Xchaff::GetNumDecisions ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 121 of file xchaff.h.

References _solver, and CSolver::num_decisions().

int Xchaff::GetNumConflicts ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 123 of file xchaff.h.

int Xchaff::GetNumExtConflicts ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 125 of file xchaff.h.

float Xchaff::GetTotalTime ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 127 of file xchaff.h.

References _solver, and CSolver::total_run_time().

float Xchaff::GetSATTime ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 129 of file xchaff.h.

int Xchaff::GetNumLiterals ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 131 of file xchaff.h.

References _solver, and CDatabase::num_literals().

int Xchaff::GetNumDeletedClauses ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 133 of file xchaff.h.

References _solver, and CDatabase::num_deleted_clauses().

int Xchaff::GetNumDeletedLiterals ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 135 of file xchaff.h.

References _solver, and CDatabase::num_deleted_literals().

int Xchaff::GetNumImplications ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 137 of file xchaff.h.

References _solver, and CSolver::num_implications().

int Xchaff::GetMaxDLevel ( )
inlinevirtual

Reimplemented from SatSolver.

Definition at line 139 of file xchaff.h.

References _solver, and CSolver::max_dlevel().

Member Data Documentation

CSolver* Xchaff::_solver
private
Lit(* Xchaff::_decision_hook)(void *, bool *)
private

Definition at line 19 of file xchaff.h.

Referenced by RegisterDecisionHook(), and TranslateDecisionHook().

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

Definition at line 20 of file xchaff.h.

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: