Xchaff Class Reference

#include <xchaff.h>

Inherits SatSolver.

Collaboration 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

---

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.

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 _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, 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, SatSolver::Var::id, and CDatabase::num_variables().

Var Xchaff::GetNextVar

(

Var

var

)

[inline, virtual]

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
	)		[inline, virtual]

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

(

)

[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(), SatSolver::Clause::id, and CClause::in_use().

Clause Xchaff::GetNextClause

(

Clause

clause

)

[inline, virtual]

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
	)

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

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]

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

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:

• xchaff.h
• xchaff.cpp