Xchaff Class Reference

#include <xchaff.h>

Inheritance diagram for Xchaff:

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

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

---

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]

Implements SatSolver.

Definition at line 20 of file xchaff.cpp.

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

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
	)

Definition at line 35 of file xchaff.cpp.

References _solver, CDatabase::clause(), SatSolver::Clause::id, CClause::num_lits(), mkLit(), CClause::literal(), and CLitPoolElement::s_var().

SatSolver::SATStatus Xchaff::Satisfiable

(

bool

allowNewClauses

)

[virtual]

Implements SatSolver.

Definition at line 43 of file xchaff.cpp.

References _solver, CSolver::solve(), SatSolver::UNSATISFIABLE, SatSolver::SATISFIABLE, TIME_OUT, SatSolver::BUDGET_EXCEEDED, MEM_OUT, SatSolver::OUT_OF_MEMORY, and SatSolver::UNKNOWN.

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]

Implements SatSolver.

Definition at line 57 of file xchaff.cpp.

References _solver, CSolver::continueCheck(), SatSolver::UNSATISFIABLE, SatSolver::SATISFIABLE, TIME_OUT, SatSolver::BUDGET_EXCEEDED, MEM_OUT, SatSolver::OUT_OF_MEMORY, and SatSolver::UNKNOWN.

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]

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

Implements SatSolver.

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 GetClause(), GetClauseLits(), Satisfiable(), Continue(), Xchaff(), ~Xchaff(), NumVariables(), AddVariables(), GetFirstVar(), GetNextVar(), NumClauses(), AddClause(), GetFirstClause(), GetNextClause(), GetVarAssignment(), RegisterDLevelHook(), RegisterDecisionHook(), RegisterAssignmentHook(), RegisterDeductionHook(), SetBudget(), SetMemLimit(), SetRandomness(), SetRandSeed(), EnableClauseDeletion(), DisableClauseDeletion(), GetBudgetUsed(), GetMemUsed(), GetNumDecisions(), GetTotalTime(), GetNumLiterals(), GetNumDeletedClauses(), GetNumDeletedLiterals(), GetNumImplications(), and GetMaxDLevel().

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

void* Xchaff::_decision_hook_cookie [private]

Definition at line 21 of file xchaff.h.

Referenced by TranslateDecisionHook(), and RegisterDecisionHook().

void* Xchaff::_assignment_hook_cookie [private]

Definition at line 22 of file xchaff.h.

Referenced by TranslateAssignmentHook(), and RegisterAssignmentHook().

---

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

• xchaff.h
• xchaff.cpp