#include <xchaff.h>

Inheritance diagram for Xchaff:

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 SatSolver *	Create ()

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.

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 CDatabase::num_variables().

Var Xchaff::AddVariables ( int nvars )

inlinevirtual

Implements SatSolver.

Definition at line 38 of file xchaff.h.

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

Var Xchaff::GetNextVar ( Var var )

inlinevirtual

Implements SatSolver.

Definition at line 46 of file xchaff.h.

References 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 CDatabase::num_clauses().

Clause Xchaff::AddClause ( std::vector< Lit > & lits )

inline

Definition at line 57 of file xchaff.h.

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

inlinevirtual

Implements SatSolver.

Definition at line 60 of file xchaff.h.

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

inlinevirtual

Implements SatSolver.

Definition at line 72 of file xchaff.h.

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

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

Definition at line 90 of file xchaff.h.

References _decision_hook, CSolver::RegisterDecisionHook(), and TranslateDecisionHook().

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

Implements SatSolver.

Definition at line 100 of file xchaff.h.

References _assignment_hook, CSolver::RegisterAssignmentHook(), and TranslateAssignmentHook().

void Xchaff::RegisterDeductionHook	(	void()(void )	f,
		void *	cookie
	)

inlinevirtual

Implements SatSolver.

Definition at line 103 of file xchaff.h.

References CSolver::RegisterDeductionHook().

bool Xchaff::SetBudget ( int budget )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 105 of file xchaff.h.

References CSolver::set_time_limit().

bool Xchaff::SetMemLimit ( int mem_limit )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 107 of file xchaff.h.

References CSolver::set_mem_limit().

bool Xchaff::SetRandomness ( int n )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 109 of file xchaff.h.

References CSolver::set_randomness().

bool Xchaff::SetRandSeed ( int seed )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 111 of file xchaff.h.

References CSolver::set_random_seed().

bool Xchaff::EnableClauseDeletion ( )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 113 of file xchaff.h.

References CSolver::enable_cls_deletion().

bool Xchaff::DisableClauseDeletion ( )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 115 of file xchaff.h.

References CSolver::enable_cls_deletion().

int Xchaff::GetBudgetUsed ( )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 117 of file xchaff.h.

References CSolver::total_run_time().

int Xchaff::GetMemUsed ( )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 119 of file xchaff.h.

References CSolver::estimate_mem_usage().

int Xchaff::GetNumDecisions ( )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 121 of file xchaff.h.

References 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 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 CDatabase::num_literals().

int Xchaff::GetNumDeletedClauses ( )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 133 of file xchaff.h.

References CDatabase::num_deleted_clauses().

int Xchaff::GetNumDeletedLiterals ( )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 135 of file xchaff.h.

References CDatabase::num_deleted_literals().

int Xchaff::GetNumImplications ( )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 137 of file xchaff.h.

References CSolver::num_implications().

int Xchaff::GetMaxDLevel ( )

inlinevirtual

Reimplemented from SatSolver.

Definition at line 139 of file xchaff.h.

References CSolver::max_dlevel().

Member Data Documentation

CSolver* Xchaff::_solver

private

Definition at line 17 of file xchaff.h.

Referenced by Continue(), GetClause(), GetClauseLits(), Satisfiable(), 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 TranslateDecisionHook().

void* Xchaff::_assignment_hook_cookie

private

Definition at line 22 of file xchaff.h.

Referenced by TranslateAssignmentHook().

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

Public Member Functions

Static Public Member Functions

Static Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation