SatZchaff Struct Reference

The private interface of class SatZchaff. More...

#include <SatZchaff_private.h>

Public Member Functions
	INHERITS_FROM (SatIncSolver)
Data Fields
hash_ptr	cnfVar2zchaffVar
Slist_ptr	conflict
SAT_Manager	zchaffSolver
hash_ptr	zchaffVar2cnfVar
Related Functions
(Note that these are not member functions.)
void	sat_zchaff_add (const SatSolver_ptr self, const Be_Cnf_ptr cnfProb, SatSolverGroup group)
void	sat_zchaff_clear_preferred_variables (const SatSolver_ptr self)
int	sat_zchaff_cnfLiteral2zchaffLiteral (SatZchaff_ptr self, int cnfLitaral)
SatSolverGroup	sat_zchaff_create_group (const SatIncSolver_ptr self)
void	sat_zchaff_deinit (SatZchaff_ptr self)
void	sat_zchaff_destroy_group (const SatIncSolver_ptr self, SatSolverGroup group)
void	sat_zchaff_init (SatZchaff_ptr self, const NuSMVEnv_ptr env, const char *name)
Slist_ptr	sat_zchaff_make_conflicts (const SatZchaff_ptr self)
	Obtains the set of conflicting assumptions from zCahdd.
Slist_ptr	sat_zchaff_make_model (const SatSolver_ptr self)
void	sat_zchaff_move_to_permanent_and_destroy_group (const SatIncSolver_ptr self, SatSolverGroup group)
void	sat_zchaff_set_polarity (const SatSolver_ptr self, const Be_Cnf_ptr cnfProb, int polarity, SatSolverGroup group)
void	sat_zchaff_set_preferred_variables (const SatSolver_ptr self, const Slist_ptr cnfVars)
SatSolverResult	sat_zchaff_solve_all_groups (const SatSolver_ptr self)
SatSolverResult	sat_zchaff_solve_groups (const SatIncSolver_ptr self, const Olist_ptr groups)
SatSolverResult	sat_zchaff_solve_permanent_group_assume (const SatSolver_ptr self, Slist_ptr assumption)
SatSolverResult	sat_zchaff_solve_without_groups (const SatIncSolver_ptr self, const Olist_ptr groups)
int	sat_zchaff_zchaffLiteral2cnfLiteral (SatZchaff_ptr self, int zchaffLiteral)
SatZchaff_ptr	SatZchaff_create (const NuSMVEnv_ptr env, const char *name)
	Creates a Zchaff SAT solver and initializes it.
void	SatZchaff_destroy (SatZchaff_ptr self)
	Destroys a Zchaff SAT solver instence.

---

Detailed Description

The private interface of class SatZchaff.

The header file for the SatZchaff class.

Author:

Andrei Tchaltsev Private definition to be used by derived classes

SatZchaff Class This class defines a prototype for a generic SatZchaff. This class is virtual and must be specialized.

Author:

Andrei Tchaltsev Zchaff is an incremental SAT solver. SatZchaff inherits the SatIncSolver (interface) class

Todo:

Missing synopsis

Todo:

Missing description

---

Member Function Documentation

SatZchaff::INHERITS_FROM

(

SatIncSolver

)

---

Friends And Related Function Documentation

void sat_zchaff_add	(	const SatSolver_ptr	self,
		const Be_Cnf_ptr	cnfProb,
		SatSolverGroup	group
	)			[related]

Todo:

void sat_zchaff_clear_preferred_variables

(

const SatSolver_ptr

self

)

[related]

Todo:

int sat_zchaff_cnfLiteral2zchaffLiteral	(	SatZchaff_ptr	self,
		int	cnfLitaral
	)			[related]

Todo:

SatSolverGroup sat_zchaff_create_group

(

const SatIncSolver_ptr

self

)

[related]

Todo:

void sat_zchaff_deinit

(

SatZchaff_ptr

self

)

[related]

Todo:

void sat_zchaff_destroy_group	(	const SatIncSolver_ptr	self,
		SatSolverGroup	group
	)			[related]

Todo:

void sat_zchaff_init	(	SatZchaff_ptr	self,
		const NuSMVEnv_ptr	env,
		const char *	name
	)			[related]

AutomaticStart

Todo:

Slist_ptr sat_zchaff_make_conflicts

(

const SatZchaff_ptr

self

)

[related]

Obtains the set of conflicting assumptions from zCahdd.

See also:

sat_zchaff_solve_permanent_group_assume, sat_zchaff_get_conflict

Slist_ptr sat_zchaff_make_model

(

const SatSolver_ptr

self

)

[related]

Todo:

void sat_zchaff_move_to_permanent_and_destroy_group	(	const SatIncSolver_ptr	self,
		SatSolverGroup	group
	)			[related]

Todo:

void sat_zchaff_set_polarity	(	const SatSolver_ptr	self,
		const Be_Cnf_ptr	cnfProb,
		int	polarity,
		SatSolverGroup	group
	)			[related]

Todo:

void sat_zchaff_set_preferred_variables	(	const SatSolver_ptr	self,
		const Slist_ptr	cnfVars
	)			[related]

Todo:

SatSolverResult sat_zchaff_solve_all_groups

(

const SatSolver_ptr

self

)

[related]

Todo:

SatSolverResult sat_zchaff_solve_groups	(	const SatIncSolver_ptr	self,
		const Olist_ptr	groups
	)			[related]

Todo:

SatSolverResult sat_zchaff_solve_permanent_group_assume	(	const SatSolver_ptr	self,
		Slist_ptr	assumption
	)			[related]

Todo:

SatSolverResult sat_zchaff_solve_without_groups	(	const SatIncSolver_ptr	self,
		const Olist_ptr	groups
	)			[related]

Todo:

int sat_zchaff_zchaffLiteral2cnfLiteral	(	SatZchaff_ptr	self,
		int	zchaffLiteral
	)			[related]

Todo:

SatZchaff_ptr SatZchaff_create	(	const NuSMVEnv_ptr	env,
		const char *	name
	)			[related]

Creates a Zchaff SAT solver and initializes it.

AutomaticStart

The first parameter is the name of the solver.

void SatZchaff_destroy

(

SatZchaff_ptr

self

)

[related]

Destroys a Zchaff SAT solver instence.

The first parameter is the name of the solver.

---

Field Documentation

hash_ptr SatZchaff::cnfVar2zchaffVar

Slist_ptr SatZchaff::conflict

SAT_Manager SatZchaff::zchaffSolver

hash_ptr SatZchaff::zchaffVar2cnfVar

---

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

• NuSMV/code/nusmv/core/sat/solvers/SatZchaff_private.h
• NuSMV/code/nusmv/core/sat/solvers/SatZchaff.h