SatSolver Struct Reference

The private interface of class SatSolver. More...

#include <SatSolver_private.h>

Public Member Functions
	INHERITS_FROM (EnvObject)
Data Fields
VIRTUAL void(*	add )(const SatSolver_ptr self, const Be_Cnf_ptr cnfProb, SatSolverGroup group)
VIRTUAL void(*	clear_preferred_variables )(const SatSolver_ptr self)
Slist_ptr	conflicts
VIRTUAL SatSolverItpGroup(*	curr_itp_group )(SatSolver_ptr self)
Olist_ptr	existingGroups
VIRTUAL Term(*	extract_interpolant )(SatSolver_ptr self, int nof_ga_groups, SatSolverItpGroup *ga_groups, TermFactoryCallbacks_ptr callbacks, TermFactoryCallbacksUserData_ptr user_data)
VIRTUAL int(*	get_cnf_var )(const SatSolver_ptr self, int lit)
VIRTUAL Slist_ptr(*	get_conflicts )(const SatSolver_ptr self)
VIRTUAL int(*	get_polarity_mode )(const SatSolver_ptr self)
boolean	interpolation
VIRTUAL Slist_ptr(*	make_model )(const SatSolver_ptr self)
Slist_ptr	model
char *	name
VIRTUAL SatSolverItpGroup(*	new_itp_group )(SatSolver_ptr self)
VIRTUAL void(*	set_polarity )(const SatSolver_ptr self, const Be_Cnf_ptr cnfProb, int polarity, SatSolverGroup group)
VIRTUAL void(*	set_polarity_mode )(SatSolver_ptr self, int mode)
VIRTUAL void(*	set_preferred_variables )(const SatSolver_ptr self, const Slist_ptr cnfVars)
VIRTUAL void(*	set_random_mode )(SatSolver_ptr self, double seed)
VIRTUAL SatSolverResult(*	solve_all_groups )(const SatSolver_ptr self)
VIRTUAL SatSolverResult(*	solve_all_groups_assume )(const SatSolver_ptr self, Slist_ptr assumption)
long	solvingTime
Olist_ptr	unsatisfiableGroups
Related Functions
(Note that these are not member functions.)
void	sat_solver_add (const SatSolver_ptr self, const Be_Cnf_ptr cnfClause, SatSolverGroup group)
void	sat_solver_clear_preferred_variables (const SatSolver_ptr self)
void	sat_solver_deinit (SatSolver_ptr self)
int	sat_solver_get_cnf_var (const SatSolver_ptr self, int lit)
int	sat_solver_get_polarity_mode (const SatSolver_ptr self)
void	sat_solver_init (SatSolver_ptr self, const NuSMVEnv_ptr env, const char *name)
Slist_ptr	sat_solver_make_model (const SatSolver_ptr self)
void	sat_solver_set_polarity (const SatSolver_ptr self, const Be_Cnf_ptr cnfClause, int polarity, SatSolverGroup group)
void	sat_solver_set_polarity_mode (SatSolver_ptr self, int mode)
void	sat_solver_set_preferred_variables (const SatSolver_ptr self, const Slist_ptr cnfVars)
void	sat_solver_set_random_mode (SatSolver_ptr self, double seed)
SatSolverResult	sat_solver_solve_all_groups (const SatSolver_ptr self)
SatSolverResult	sat_solver_solve_all_groups_assume (const SatSolver_ptr self, Slist_ptr assumptions)
VIRTUAL void	SatSolver_add (const SatSolver_ptr self, const Be_Cnf_ptr cnfProb, SatSolverGroup group)
	Adds a CNF formula to a group.
VIRTUAL void	SatSolver_clear_preferred_variables (const SatSolver_ptr self)
	Clear preferred variables in the solver.
SatSolverItpGroup	SatSolver_curr_itp_group (const SatSolver_ptr self)
	Returns current itp group.
void	SatSolver_destroy (SatSolver_ptr self)
	Destoys an instance of a SAT solver.
Term	SatSolver_extract_interpolant (const SatSolver_ptr self, int nof_ga_groups, SatSolverItpGroup *ga_groups, TermFactoryCallbacks_ptr callbacks, TermFactoryCallbacksUserData_ptr user_data)
	Returns the time of last solving.
VIRTUAL int	SatSolver_get_cnf_var (const SatSolver_ptr self, int var)
VIRTUAL Slist_ptr	SatSolver_get_conflicts (const SatSolver_ptr self)
	Returns the conflicts resulting from a previous call to solving under assumptions.
long	SatSolver_get_last_solving_time (const SatSolver_ptr self)
	Returns the time of last solving.
VIRTUAL Slist_ptr	SatSolver_get_model (const SatSolver_ptr self)
	Returns the model (of previous solving).
const char *	SatSolver_get_name (const SatSolver_ptr self)
	Returns the name of the solver.
SatSolverGroup	SatSolver_get_permanent_group (const SatSolver_ptr self)
	Returns the permanent group of this class instance.
VIRTUAL int	SatSolver_get_polarity_mode (const SatSolver_ptr self)
	Gets the current polarity mode.
SatSolverItpGroup	SatSolver_new_itp_group (const SatSolver_ptr self)
	Returns the time of last solving.
VIRTUAL void	SatSolver_set_polarity (const SatSolver_ptr self, const Be_Cnf_ptr cnfProb, int polarity, SatSolverGroup group)
	Sets the polarity of a CNF formula in a group.
VIRTUAL void	SatSolver_set_polarity_mode (SatSolver_ptr self, int mode)
	Sets the current polarity mode.
VIRTUAL void	SatSolver_set_preferred_variables (const SatSolver_ptr self, const Slist_ptr cnfVars)
	Sets preferred variables in the solver.
VIRTUAL void	SatSolver_set_random_mode (SatSolver_ptr self, double seed)
	Enables or disables random mode for polarity.
VIRTUAL SatSolverResult	SatSolver_solve_all_groups (const SatSolver_ptr self)
	Solves all groups belonging to the solver and returns the flag.
VIRTUAL SatSolverResult	SatSolver_solve_all_groups_assume (const SatSolver_ptr self, Slist_ptr assumptions)
	Solves all groups belonging to the solver assuming the cnf assumptions, and returns the flag.

Detailed Description

The private interface of class SatSolver.

Author:: Andrei Tchaltsev Private definition to be used by derived classes

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

Todo:: Missing synopsis

Todo:: Missing description

Member Function Documentation

SatSolver::INHERITS_FROM ( EnvObject )

Friends And Related Function Documentation

void sat_solver_add	(	const SatSolver_ptr	self,
		const Be_Cnf_ptr	cnfClause,
		SatSolverGroup	group
	)			`[related]`

Todo:

void sat_solver_clear_preferred_variables ( const SatSolver_ptr self ) [related]

Todo:

void sat_solver_deinit ( SatSolver_ptr self ) [related]

Todo:

int sat_solver_get_cnf_var	(	const SatSolver_ptr	self,
		int	lit
	)			`[related]`

Todo:

int sat_solver_get_polarity_mode ( const SatSolver_ptr self ) [related]

Todo:

void sat_solver_init	(	SatSolver_ptr	self,
		const NuSMVEnv_ptr	env,
		const char *	name
	)			`[related]`

AutomaticStart

Todo:

Slist_ptr sat_solver_make_model ( const SatSolver_ptr self ) [related]

Todo:

void sat_solver_set_polarity	(	const SatSolver_ptr	self,
		const Be_Cnf_ptr	cnfClause,
		int	polarity,
		SatSolverGroup	group
	)			`[related]`

Todo:

void sat_solver_set_polarity_mode	(	SatSolver_ptr	self,
		int	mode
	)			`[related]`

Todo:

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

Todo:

void sat_solver_set_random_mode	(	SatSolver_ptr	self,
		double	seed
	)			`[related]`

Todo:

SatSolverResult sat_solver_solve_all_groups ( const SatSolver_ptr self ) [related]

Todo:

SatSolverResult sat_solver_solve_all_groups_assume	(	const SatSolver_ptr	self,
		Slist_ptr	assumptions
	)			`[related]`

Todo:

VIRTUAL void SatSolver_add	(	const SatSolver_ptr	self,
		const Be_Cnf_ptr	cnfProb,
		SatSolverGroup	group
	)			`[related]`

Adds a CNF formula to a group.

The function does not specify the polarity of the formula. This should be done by SatSolver_set_polarity. In general, if polarity is not set any value can be assigned to the formula and its variables (this may potentially slow down the solver because there is a number of variables whose value can be any and solver will try to assign values to them though it is not necessary). Moreover, some solver (such as ZChaff) can deal with non-redundent clauses only, so the input clauses must be non-redundent: no variable can be in the same clause twice. CNF formular may be a constant.

See also:: SatSolver_set_polarity

VIRTUAL void SatSolver_clear_preferred_variables ( const SatSolver_ptr self ) [related]

Clear preferred variables in the solver.

Clear preferred variables in the solver

See also:: SatSolver_set_preferred_variables

SatSolverItpGroup SatSolver_curr_itp_group ( const SatSolver_ptr self ) [related]

Returns current itp group.

void SatSolver_destroy ( SatSolver_ptr self ) [related]

Destoys an instance of a SAT solver.

AutomaticStart

Term SatSolver_extract_interpolant	(	const SatSolver_ptr	self,
		int	nof_ga_groups,
		SatSolverItpGroup *	ga_groups,
		TermFactoryCallbacks_ptr	callbacks,
		TermFactoryCallbacksUserData_ptr	user_data
	)			`[related]`

Returns the time of last solving.

VIRTUAL int SatSolver_get_cnf_var	(	const SatSolver_ptr	self,
		int	var
	)			`[related]`

VIRTUAL Slist_ptr SatSolver_get_conflicts ( const SatSolver_ptr self ) [related]

Returns the conflicts resulting from a previous call to solving under assumptions.

See also:: SatSolverResult

long SatSolver_get_last_solving_time ( const SatSolver_ptr self ) [related]

Returns the time of last solving.

VIRTUAL Slist_ptr SatSolver_get_model ( const SatSolver_ptr self ) [related]

Returns the model (of previous solving).

The previous solving call should have returned SATISFIABLE. The returned list is a list of values in dimac form (positive literal is included as the variable index, negative literal as the negative variable index, if a literal has not been set its value is not included).

Returned list belongs to self and must be not destroyed or changed.

const char * SatSolver_get_name ( const SatSolver_ptr self ) [related]

Returns the name of the solver.

SatSolverGroup SatSolver_get_permanent_group ( const SatSolver_ptr self ) [related]

Returns the permanent group of this class instance.

Every solver has one permanent group that can not be destroyed. This group may has more efficient representation and during invocations of any 'solve' functions, the permanent group will always be included into the groups to be solved.

VIRTUAL int SatSolver_get_polarity_mode ( const SatSolver_ptr self ) [related]

Gets the current polarity mode.

SatSolverItpGroup SatSolver_new_itp_group ( const SatSolver_ptr self ) [related]

Returns the time of last solving.

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

Sets the polarity of a CNF formula in a group.

Polarity 1 means the formula will be considered in this group as positive. Polarity -1 means the formula will be considered in this group as negative. The formula is not added to the group, just the formula's polarity. The formula can be added to a group with SatSolver_add. The formula and its polarity can be added to different groups. CNF formular may be a constant.

See also:: SatSolver_add

VIRTUAL void SatSolver_set_polarity_mode	(	SatSolver_ptr	self,
		int	mode
	)			`[related]`

Sets the current polarity mode.

VIRTUAL void SatSolver_set_preferred_variables	(	const SatSolver_ptr	self,
		const Slist_ptr	cnfVars
	)			`[related]`

Sets preferred variables in the solver.

Sets preferred variables in the solver

See also:: SatSolver_clear_preferred_variables

VIRTUAL void SatSolver_set_random_mode	(	SatSolver_ptr	self,
		double	seed
	)			`[related]`

Enables or disables random mode for polarity.

If given seed is != 0, then random polarity mode is enabled with given seed, otherwise random mode is disabled

VIRTUAL SatSolverResult SatSolver_solve_all_groups ( const SatSolver_ptr self ) [related]

Solves all groups belonging to the solver and returns the flag.

See also:: SatSolverResult

VIRTUAL SatSolverResult SatSolver_solve_all_groups_assume	(	const SatSolver_ptr	self,
		Slist_ptr	assumptions
	)			`[related]`

Solves all groups belonging to the solver assuming the cnf assumptions, and returns the flag.

See also:: SatSolverResult

Field Documentation

VIRTUAL void(* SatSolver::add)(const SatSolver_ptr self, const Be_Cnf_ptr cnfProb, SatSolverGroup group)

VIRTUAL void(* SatSolver::clear_preferred_variables)(const SatSolver_ptr self)

Slist_ptr SatSolver::conflicts

VIRTUAL SatSolverItpGroup(* SatSolver::curr_itp_group)(SatSolver_ptr self)

Olist_ptr SatSolver::existingGroups

VIRTUAL Term(* SatSolver::extract_interpolant)(SatSolver_ptr self, int nof_ga_groups, SatSolverItpGroup *ga_groups, TermFactoryCallbacks_ptr callbacks, TermFactoryCallbacksUserData_ptr user_data)

VIRTUAL int(* SatSolver::get_cnf_var)(const SatSolver_ptr self, int lit)

VIRTUAL Slist_ptr(* SatSolver::get_conflicts)(const SatSolver_ptr self)

VIRTUAL int(* SatSolver::get_polarity_mode)(const SatSolver_ptr self)

boolean SatSolver::interpolation

VIRTUAL Slist_ptr(* SatSolver::make_model)(const SatSolver_ptr self)

Slist_ptr SatSolver::model

char* SatSolver::name

VIRTUAL SatSolverItpGroup(* SatSolver::new_itp_group)(SatSolver_ptr self)

VIRTUAL void(* SatSolver::set_polarity)(const SatSolver_ptr self, const Be_Cnf_ptr cnfProb, int polarity, SatSolverGroup group)

VIRTUAL void(* SatSolver::set_polarity_mode)(SatSolver_ptr self, int mode)

VIRTUAL void(* SatSolver::set_preferred_variables)(const SatSolver_ptr self, const Slist_ptr cnfVars)

VIRTUAL void(* SatSolver::set_random_mode)(SatSolver_ptr self, double seed)

VIRTUAL SatSolverResult(* SatSolver::solve_all_groups)(const SatSolver_ptr self)

VIRTUAL SatSolverResult(* SatSolver::solve_all_groups_assume)(const SatSolver_ptr self, Slist_ptr assumption)

long SatSolver::solvingTime

Olist_ptr SatSolver::unsatisfiableGroups

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

NuSMV/code/nusmv/core/sat/SatSolver_private.h
NuSMV/code/nusmv/core/sat/SatSolver.h

SatSolver Struct Reference

Public Member Functions

Data Fields

Related Functions

Detailed Description

Member Function Documentation

Friends And Related Function Documentation

Field Documentation