SatMinisat Struct Reference

The private interface of class SatMinisat. More...

#include <SatMinisat_private.h>

Public Member Functions
	INHERITS_FROM (SatIncSolver)
Data Fields
hash_ptr	cnfVar2minisatVar
Slist_ptr	conflict
Stack_ptr	minisat_itp_groups
int *	minisatClause
unsigned int	minisatClauseSize
MiniSat_ptr	minisatSolver
hash_ptr	minisatVar2cnfVar
Related Functions
(Note that these are not member functions.)
void	sat_minisat_add (const SatSolver_ptr self, const Be_Cnf_ptr cnfProb, SatSolverGroup group)
void	sat_minisat_clear_preferred_variables (const SatSolver_ptr self)
int	sat_minisat_cnfLiteral2minisatLiteral (SatMinisat_ptr self, int cnfLitaral)
SatSolverGroup	sat_minisat_create_group (const SatIncSolver_ptr self)
void	sat_minisat_deinit (SatMinisat_ptr self)
void	sat_minisat_destroy_group (const SatIncSolver_ptr self, SatSolverGroup group)
void	sat_minisat_enlarge_minisatClause (const SatMinisat_ptr self, unsigned int minSize)
int *	sat_minisat_get_minisatClause (const SatMinisat_ptr self)
int	sat_minisat_get_minisatClauseSize (const SatMinisat_ptr self)
int	sat_minisat_get_polarity_mode (const SatSolver_ptr self)
void	sat_minisat_init (SatMinisat_ptr self, const NuSMVEnv_ptr env, const char *name, boolean enable_proof_logging)
Slist_ptr	sat_minisat_make_conflicts (const SatMinisat_ptr self)
Slist_ptr	sat_minisat_make_model (const SatSolver_ptr self)
int	sat_minisat_minisatLiteral2cnfLiteral (SatMinisat_ptr self, int minisatLiteral)
void	sat_minisat_move_to_permanent_and_destroy_group (const SatIncSolver_ptr self, SatSolverGroup group)
void	sat_minisat_set_polarity (const SatSolver_ptr self, const Be_Cnf_ptr cnfProb, int polarity, SatSolverGroup group)
void	sat_minisat_set_polarity_mode (SatSolver_ptr self, int mode)
void	sat_minisat_set_preferred_variables (const SatSolver_ptr self, const Slist_ptr cnfVars)
void	sat_minisat_set_random_mode (SatSolver_ptr self, double seed)
SatSolverResult	sat_minisat_solve_all_groups (const SatSolver_ptr self)
SatSolverResult	sat_minisat_solve_groups (const SatIncSolver_ptr self, const Olist_ptr groups)
SatSolverResult	sat_minisat_solve_permanent_group_assume (const SatSolver_ptr self, Slist_ptr assumption)
SatSolverResult	sat_minisat_solve_without_groups (const SatIncSolver_ptr self, const Olist_ptr groups)
SatMinisat_ptr	SatMinisat_create (const NuSMVEnv_ptr env, const char *name, boolean enable_proof_logging)
	Creates a Minisat SAT solver and initializes it.
void	SatMinisat_destroy (SatMinisat_ptr self)
	Destroys an instance of a MiniSat SAT solver.

---

Detailed Description

The private interface of class SatMinisat.

The header file for the SatMinisat class.

Author:

Andrei Tchaltsev Private definition to be used by derived classes

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

Author:

Andrei Tchaltsev Minisat is an incremental SAT solver. SatMinisat inherits the SatIncSolver (interface) class

Todo:

Missing synopsis

Todo:

Missing description

---

Member Function Documentation

SatMinisat::INHERITS_FROM

(

SatIncSolver

)

---

Friends And Related Function Documentation

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

Todo:

void sat_minisat_clear_preferred_variables

(

const SatSolver_ptr

self

)

[related]

Todo:

int sat_minisat_cnfLiteral2minisatLiteral	(	SatMinisat_ptr	self,
		int	cnfLitaral
	)			[related]

Todo:

SatSolverGroup sat_minisat_create_group

(

const SatIncSolver_ptr

self

)

[related]

Todo:

void sat_minisat_deinit

(

SatMinisat_ptr

self

)

[related]

Todo:

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

Todo:

void sat_minisat_enlarge_minisatClause	(	const SatMinisat_ptr	self,
		unsigned int	minSize
	)			[related]

Todo:

int * sat_minisat_get_minisatClause

(

const SatMinisat_ptr

self

)

[related]

Todo:

int sat_minisat_get_minisatClauseSize

(

const SatMinisat_ptr

self

)

[related]

Todo:

int sat_minisat_get_polarity_mode

(

const SatSolver_ptr

self

)

[related]

Todo:

void sat_minisat_init	(	SatMinisat_ptr	self,
		const NuSMVEnv_ptr	env,
		const char *	name,
		boolean	enable_proof_logging
	)			[related]

AutomaticStart

Todo:

Slist_ptr sat_minisat_make_conflicts

(

const SatMinisat_ptr

self

)

[related]

Todo:

Slist_ptr sat_minisat_make_model

(

const SatSolver_ptr

self

)

[related]

Todo:

int sat_minisat_minisatLiteral2cnfLiteral	(	SatMinisat_ptr	self,
		int	minisatLiteral
	)			[related]

Todo:

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

Todo:

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

Todo:

void sat_minisat_set_polarity_mode	(	SatSolver_ptr	self,
		int	mode
	)			[related]

Todo:

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

Todo:

void sat_minisat_set_random_mode	(	SatSolver_ptr	self,
		double	seed
	)			[related]

Todo:

SatSolverResult sat_minisat_solve_all_groups

(

const SatSolver_ptr

self

)

[related]

Todo:

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

Todo:

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

Todo:

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

Todo:

SatMinisat_ptr SatMinisat_create	(	const NuSMVEnv_ptr	env,
		const char *	name,
		boolean	enable_proof_logging
	)			[related]

Creates a Minisat SAT solver and initializes it.

AutomaticStart

The first parameter is the name of the solver.

void SatMinisat_destroy

(

SatMinisat_ptr

self

)

[related]

Destroys an instance of a MiniSat SAT solver.

---

Field Documentation

hash_ptr SatMinisat::cnfVar2minisatVar

Slist_ptr SatMinisat::conflict

Stack_ptr SatMinisat::minisat_itp_groups

int* SatMinisat::minisatClause

unsigned int SatMinisat::minisatClauseSize

MiniSat_ptr SatMinisat::minisatSolver

hash_ptr SatMinisat::minisatVar2cnfVar

---

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

• NuSMV/code/nusmv/core/sat/solvers/SatMinisat_private.h
• NuSMV/code/nusmv/core/sat/solvers/SatMinisat.h