SatIncSolver Struct Reference

The private interface of class SatIncSolver. More...

#include <SatIncSolver_private.h>

Public Member Functions
	INHERITS_FROM (SatSolver)
Data Fields
VIRTUAL SatSolverGroup(*	create_group )(const SatIncSolver_ptr self)
VIRTUAL void(*	destroy_group )(const SatIncSolver_ptr self, SatSolverGroup group)
VIRTUAL void(*	move_to_permanent_and_destroy_group )(const SatIncSolver_ptr self, SatSolverGroup group)
VIRTUAL SatSolverResult(*	solve_groups )(const SatIncSolver_ptr self, const Olist_ptr groups)
VIRTUAL SatSolverResult(*	solve_without_groups )(const SatIncSolver_ptr self, const Olist_ptr groups)
Related Functions
(Note that these are not member functions.)
SatSolverGroup	sat_inc_solver_create_group (const SatIncSolver_ptr self)
void	sat_inc_solver_deinit (SatIncSolver_ptr self)
void	sat_inc_solver_destroy_group (const SatIncSolver_ptr self, SatSolverGroup group)
void	sat_inc_solver_init (SatIncSolver_ptr self, const NuSMVEnv_ptr env, const char *name)
void	sat_inc_solver_move_to_permanent_and_destroy_group (const SatIncSolver_ptr self, SatSolverGroup group)
SatSolverResult	sat_inc_solver_solve_groups (const SatIncSolver_ptr self, const Olist_ptr groups)
SatSolverResult	sat_inc_solver_solve_without_groups (const SatIncSolver_ptr self, const Olist_ptr groups)
VIRTUAL SatSolverGroup	SatIncSolver_create_group (const SatIncSolver_ptr self)
	Creates a new group and returns its ID. To destroy a group use SatIncSolver_destroy_group or SatIncSolver_move_to_permanent_and_destroy_group.
void	SatIncSolver_destroy (SatIncSolver_ptr self)
	Destroys an instance of a SAT incremental solver.
VIRTUAL void	SatIncSolver_destroy_group (const SatIncSolver_ptr self, SatSolverGroup group)
	Destroy an existing group (which has been returned by SatIncSolver_create_group) and all formulas in it.
VIRTUAL void	SatIncSolver_move_to_permanent_and_destroy_group (const SatIncSolver_ptr self, SatSolverGroup group)
	Moves all formulas from a group into the permanent group of the solver and then destroy the given group. (Permanent group may have more efficient implementation, but it can not be destroyed).
VIRTUAL SatSolverResult	SatIncSolver_solve_groups (const SatIncSolver_ptr self, const Olist_ptr groups)
	Tries to solve formulas from the groups in the list.
VIRTUAL SatSolverResult	SatIncSolver_solve_without_groups (const SatIncSolver_ptr self, const Olist_ptr groups)
	Tries to solve formulas in groups belonging to the solver except the groups in the list.

Detailed Description

The private interface of class SatIncSolver.

The header file for the SatIncSolver class.

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

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

Author:: Andrei Tchaltsev An incremental SAT solver interface. SatIncSolver inherits the SatSolver class

Todo:: Missing synopsis

Todo:: Missing description

Member Function Documentation

SatIncSolver::INHERITS_FROM ( SatSolver )

Friends And Related Function Documentation

SatSolverGroup sat_inc_solver_create_group ( const SatIncSolver_ptr self ) [related]

Todo:

void sat_inc_solver_deinit ( SatIncSolver_ptr self ) [related]

Todo:

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

Todo:

void sat_inc_solver_init	(	SatIncSolver_ptr	self,
		const NuSMVEnv_ptr	env,
		const char *	name
	)			`[related]`

AutomaticStart

Todo:

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

Todo:

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

Todo:

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

Todo:

VIRTUAL SatSolverGroup SatIncSolver_create_group ( const SatIncSolver_ptr self ) [related]

Creates a new group and returns its ID. To destroy a group use SatIncSolver_destroy_group or SatIncSolver_move_to_permanent_and_destroy_group.

See also:: SatIncSolver_destroy_group, SatIncSolver_move_to_permanent_and_destroy_group

void SatIncSolver_destroy ( SatIncSolver_ptr self ) [related]

Destroys an instance of a SAT incremental solver.

AutomaticStart

VIRTUAL void SatIncSolver_destroy_group	(	const SatIncSolver_ptr	self,
		SatSolverGroup	group
	)			`[related]`

Destroy an existing group (which has been returned by SatIncSolver_create_group) and all formulas in it.

See also:: SatIncSolver_create_group

VIRTUAL void SatIncSolver_move_to_permanent_and_destroy_group	(	const SatIncSolver_ptr	self,
		SatSolverGroup	group
	)			`[related]`

Moves all formulas from a group into the permanent group of the solver and then destroy the given group. (Permanent group may have more efficient implementation, but it can not be destroyed).

See also:: SatIncSolver_create_group, SatSolver_get_permanent_group

VIRTUAL SatSolverResult SatIncSolver_solve_groups	(	const SatIncSolver_ptr	self,
		const Olist_ptr	groups
	)			`[related]`

Tries to solve formulas from the groups in the list.

The permanent group is automatically added to the list. Returns a flag whether the solving was successful. If it was successful only then SatSolver_get_model may be invoked to obtain the model

See also:: SatSolverResult,SatSolver_get_permanent_group, SatIncSolver_create_group, SatSolver_get_model

VIRTUAL SatSolverResult SatIncSolver_solve_without_groups	(	const SatIncSolver_ptr	self,
		const Olist_ptr	groups
	)			`[related]`

Tries to solve formulas in groups belonging to the solver except the groups in the list.

The permanent group must not be in the list. Returns a flag whether the solving was successful. If it was successful only then SatSolver_get_model may be invoked to obtain the model

See also:: SatSolverResult,SatSolver_get_permanent_group, SatIncSolver_create_group, SatSolver_get_model

Field Documentation

VIRTUAL SatSolverGroup(* SatIncSolver::create_group)(const SatIncSolver_ptr self)

VIRTUAL void(* SatIncSolver::destroy_group)(const SatIncSolver_ptr self, SatSolverGroup group)

VIRTUAL void(* SatIncSolver::move_to_permanent_and_destroy_group)(const SatIncSolver_ptr self, SatSolverGroup group)

VIRTUAL SatSolverResult(* SatIncSolver::solve_groups)(const SatIncSolver_ptr self, const Olist_ptr groups)

VIRTUAL SatSolverResult(* SatIncSolver::solve_without_groups)(const SatIncSolver_ptr self, const Olist_ptr groups)

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

NuSMV/code/nusmv/core/sat/SatIncSolver_private.h
NuSMV/code/nusmv/core/sat/SatIncSolver.h

SatIncSolver Struct Reference

Public Member Functions

Data Fields

Related Functions

Detailed Description

Member Function Documentation

Friends And Related Function Documentation

Field Documentation