NuSMV/code/nusmv/core/bmc/sbmc/sbmcUtils.h File Reference

#include "nusmv/core/prop/propPkg.h"
#include "nusmv/core/bmc/sbmc/sbmcStructs.h"
#include "nusmv/core/enc/enc.h"
#include "nusmv/core/enc/be/BeEnc.h"
#include "nusmv/core/trace/Trace.h"
#include "nusmv/core/trace/TraceMgr.h"
#include "nusmv/core/sat/sat.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/assoc.h"

Go to the source code of this file.

Defines
#define	sbmc_SNH_text   "%s:%d: Should not happen"
#define	sbmc_SNYI_text   "%s:%d: Something not yet implemented\n"
Typedefs
typedef struct sbmc_MetaSolver_TAG	sbmc_MetaSolver
Functions
node_ptr	sbmc_1_fresh_state_var (const NuSMVEnv_ptr env, SymbLayer_ptr layer, unsigned int *index)
	Creates a new fresh state variable.
void	sbmc_add_loop_variable (BddEnc_ptr bdd_enc, BeFsm_ptr fsm)
node_ptr	sbmc_add_new_state_variable (const NuSMVEnv_ptr env, SymbLayer_ptr layer, const char *name)
	Declare a new boolean state variable in the layer.
void	sbmc_allocate_trans_vars (const NuSMVEnv_ptr env, sbmc_node_info *info, SymbLayer_ptr layer, lsList state_vars_formula_pd0, lsList state_vars_formula_pdx, unsigned int *new_var_index)
	Creates info->pastdepth+1 new state variables for the main translation in info->trans_vars.
int	sbmc_E_state (void)
	Routines for the state indexing scheme.
lsList	sbmc_find_formula_vars (const NuSMVEnv_ptr env, node_ptr ltlspec)
	Compute the variables that occur in the formula ltlspec.
void	sbmc_find_relevant_vars (state_vars_struct *svs, BeFsm_ptr be_fsm, node_ptr bltlspec)
	Find state and input variables that occurr in the formula.
int	sbmc_get_unique_id (const NuSMVEnv_ptr env)
void	sbmc_increment_unique_id (const NuSMVEnv_ptr env)
int	sbmc_L_state (void)
	Routines for the state indexing scheme.
node_ptr	sbmc_loop_var_name_get (const NuSMVEnv_ptr env)
void	sbmc_loop_var_name_set (const NuSMVEnv_ptr env, node_ptr n)
node_ptr	sbmc_make_boolean_formula (BddEnc_ptr bdd_enc, Prop_ptr ltlprop)
	Takes a property and return the negation of the property conjoined with the big and of fairness conditions.
unsigned int	sbmc_model_k (int k)
	Routines for the state indexing scheme.
sbmc_MetaSolver *	sbmc_MS_create (BeEnc_ptr be_enc)
	Creates a meta solver wrapper.
void	sbmc_MS_create_volatile_group (sbmc_MetaSolver *ms)
	Create the volatile group in the meta solver wrapper.
void	sbmc_MS_destroy (sbmc_MetaSolver *ms)
	Destroy a meta solver wrapper.
void	sbmc_MS_destroy_volatile_group (sbmc_MetaSolver *ms)
	Destroy the volatile group of the meta solver wrapper and force use of the permanent one.
void	sbmc_MS_force_constraint_list (sbmc_MetaSolver *ms, lsList constraints, Be_CnfAlgorithm cnf_alg)
	Forces a list of BEs to be true in the solver.
void	sbmc_MS_force_true (sbmc_MetaSolver *ms, be_ptr be_constraint, Be_CnfAlgorithm cnf_alg)
	Forces a BE to be true in the solver.
Slist_ptr	sbmc_MS_get_conflicts (sbmc_MetaSolver *ms)
	Returns the underlying solver.
Slist_ptr	sbmc_MS_get_model (sbmc_MetaSolver *ms)
	Returns the model (of previous solving).
SatSolver_ptr	sbmc_MS_get_solver (sbmc_MetaSolver *ms)
	Returns the underlying solver.
void	sbmc_MS_goto_permanent_group (sbmc_MetaSolver *ms)
	Destroy the volatile group of the meta solver wrapper.
void	sbmc_MS_goto_volatile_group (sbmc_MetaSolver *ms)
	Create and force use of the volatile group of the meta solver wrapper.
SatSolverResult	sbmc_MS_solve (sbmc_MetaSolver *ms)
	Solves all groups belonging to the solver and returns the flag.
SatSolverResult	sbmc_MS_solve_assume (sbmc_MetaSolver *ms, Slist_ptr assumptions)
	Solves all groups belonging to the solver assuming the CNF assumptions and returns the flag.
void	sbmc_MS_switch_to_permanent_group (sbmc_MetaSolver *ms)
	Force use of the permanent group of the meta solver wrapper.
void	sbmc_MS_switch_to_volatile_group (sbmc_MetaSolver *ms)
	Force use of the volatile group of the meta solver wrapper.
array_t *	sbmc_n_fresh_state_vars (const NuSMVEnv_ptr env, SymbLayer_ptr layer, const unsigned int n, unsigned int *index)
	Creates N new fresh state variables.
void	sbmc_print_Fvarmap (const NuSMVEnv_ptr env, FILE *out, node_ptr var, node_ptr formula)
	Prints some of the information associated to a F formula.
void	sbmc_print_Gvarmap (const NuSMVEnv_ptr env, FILE *out, node_ptr var, node_ptr formula)
	Prints some of the information associated to a G formula.
void	sbmc_print_node (const NuSMVEnv_ptr env, FILE *out, const char *prefix, node_ptr node, const char *postfix)
	Print a node_ptr expression by prefixing and suffixing it.
void	sbmc_print_node_list (const NuSMVEnv_ptr env, FILE *out, lsList l)
	Prints a lsList of node_ptr.
void	sbmc_print_varmap (const NuSMVEnv_ptr env, FILE *out, node_ptr node, sbmc_node_info *info)
	Prints some of the information associated to a subformula.
int	sbmc_real_k (int k)
	Routines for the state indexing scheme.
char *	sbmc_real_k_string (const unsigned int k_real)
	Routines for the state indexing scheme.
void	sbmc_remove_loop_variable (BddEnc_ptr bdd_enc, BeFsm_ptr fsm)
void	sbmc_reset_unique_id (const NuSMVEnv_ptr env)
Trace_ptr	Sbmc_Utils_fill_cntexample (BeEnc_ptr be_enc, sbmc_MetaSolver *solver, node_ptr l_var, const int k, Trace_ptr trace)
	Fills the given trace using the given sat assignment.
Trace_ptr	Sbmc_Utils_generate_and_print_cntexample (BeEnc_ptr be_enc, TraceMgr_ptr tm, sbmc_MetaSolver *solver, node_ptr l_var, const int k, const char *trace_name, NodeList_ptr symbols)
	Extracts a trace from a sat assignment, and prints it.
Trace_ptr	Sbmc_Utils_generate_cntexample (BeEnc_ptr be_enc, sbmc_MetaSolver *solver, node_ptr l_var, const int k, const char *trace_name, NodeList_ptr symbols)
	Extracts a trace from a sat assignment.

---

Define Documentation

#define sbmc_SNH_text   "%s:%d: Should not happen"

Todo:

Missing synopsis

Todo:

Missing description

#define sbmc_SNYI_text   "%s:%d: Something not yet implemented\n"

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef struct sbmc_MetaSolver_TAG sbmc_MetaSolver

---

Function Documentation

node_ptr sbmc_1_fresh_state_var	(	const NuSMVEnv_ptr	env,
		SymbLayer_ptr	layer,
		unsigned int *	index
	)

Creates a new fresh state variable.

Creates a new fresh state variable. The name is according to the pattern LTL_tu, being u an unsigned integer. The index is incremented by one.

index is incremented by one.

void sbmc_add_loop_variable	(	BddEnc_ptr	bdd_enc,
		BeFsm_ptr	fsm
	)

Declares a new layer to contain the loop variable.

node_ptr sbmc_add_new_state_variable	(	const NuSMVEnv_ptr	env,
		SymbLayer_ptr	layer,
		const char *	name
	)

Declare a new boolean state variable in the layer.

Declare a new boolean state variable in the layer. The name is specified as a string. If the variable already exists, then an error is generated.

None

void sbmc_allocate_trans_vars	(	const NuSMVEnv_ptr	env,
		sbmc_node_info *	info,
		SymbLayer_ptr	layer,
		lsList	state_vars_formula_pd0,
		lsList	state_vars_formula_pdx,
		unsigned int *	new_var_index
	)

Creates info->pastdepth+1 new state variables for the main translation in info->trans_vars.

Creates info->pastdepth+1 new state variables for the main translation in info->trans_vars. state_vars_formula_pd0, state_vars_formula_pdx and new_var_index are updated accordingly.

new_var_index is incremented accordingly to the number of variables created. state_vars_formula_pd0, state_vars_formula_pdx and new_var_index are updated accordingly.

int sbmc_E_state

(

void

)

Routines for the state indexing scheme.

State 1 is the E state

None

See also:

sbmc_L_state sbmc_real_k sbmc_model_k sbmc_real_k_string

lsList sbmc_find_formula_vars	(	const NuSMVEnv_ptr	env,
		node_ptr	ltlspec
	)

Compute the variables that occur in the formula ltlspec.

Compute the variables that occur in the formula ltlspec. The formula ltlspec must be in NNF.

None

void sbmc_find_relevant_vars	(	state_vars_struct *	svs,
		BeFsm_ptr	be_fsm,
		node_ptr	bltlspec
	)

Find state and input variables that occurr in the formula.

Find state and input variables that occurr in the formula. Build the list of system variables for simple path constraints.

• state_vars->formula_state_vars will have the state vars occurring in the formula bltlspec
• state_vars->formula_input_vars will have the input vars occurring in the formula bltlspec
• state_vars->simple_path_system_vars will be the union of state_vars->transition_state_vars, state_vars->formula_state_vars, and state_vars->formula_input_vars

Note: frozen variables are not collected since they do no paticipate in state equality formulas.

svs is modified to store retrieved information.

int sbmc_get_unique_id

(

const NuSMVEnv_ptr

env

)

AutomaticStart

Todo:

Missing synopsis

Todo:

Missing description

void sbmc_increment_unique_id

(

const NuSMVEnv_ptr

env

)

Todo:

Missing synopsis

Todo:

Missing description

int sbmc_L_state

(

void

)

Routines for the state indexing scheme.

State 0 is the L state

None

See also:

sbmc_E_state sbmc_real_k sbmc_model_k sbmc_real_k_string

node_ptr sbmc_loop_var_name_get

(

const NuSMVEnv_ptr

env

)

Gets the name of the loop variable.

void sbmc_loop_var_name_set	(	const NuSMVEnv_ptr	env,
		node_ptr	n
	)

Sets the name of the loop variable.

node_ptr sbmc_make_boolean_formula	(	BddEnc_ptr	bdd_enc,
		Prop_ptr	ltlprop
	)

Takes a property and return the negation of the property conjoined with the big and of fairness conditions.

Takes a property and return the negation of the property conjoined with the big and of fairness conditions.

None

unsigned int sbmc_model_k

(

int

k

)

Routines for the state indexing scheme.

Given a real k return the corresponding model k (real - 2)

None

See also:

sbmc_L_state sbmc_E_state sbmc_real_k sbmc_real_k_string

sbmc_MetaSolver* sbmc_MS_create

(

BeEnc_ptr

be_enc

)

Creates a meta solver wrapper.

Creates a meta solver wrapper

None

void sbmc_MS_create_volatile_group

(

sbmc_MetaSolver *

ms

)

Create the volatile group in the meta solver wrapper.

Create the volatile group in the meta solver wrapper. Use of the volatile group is not forced

None

void sbmc_MS_destroy

(

sbmc_MetaSolver *

ms

)

Destroy a meta solver wrapper.

Destroy a meta solver wrapper

None

void sbmc_MS_destroy_volatile_group

(

sbmc_MetaSolver *

ms

)

Destroy the volatile group of the meta solver wrapper and force use of the permanent one.

Destroy the volatile group of the meta solver wrapper and force use of the permanent one

None

void sbmc_MS_force_constraint_list	(	sbmc_MetaSolver *	ms,
		lsList	constraints,
		Be_CnfAlgorithm	cnf_alg
	)

Forces a list of BEs to be true in the solver.

Forces a list of BEs to be true in the solver. Each is converted to CNF, the CNF is then forced in the group in use, i.e. in the permanent or in the volatile group.

None

See also:

sbmc_MS_force_true

void sbmc_MS_force_true	(	sbmc_MetaSolver *	ms,
		be_ptr	be_constraint,
		Be_CnfAlgorithm	cnf_alg
	)

Forces a BE to be true in the solver.

Forces a BE to be true in the solver. The BE converted to CNF, the CNF is then forced in the group in use, i.e. in the permanent or in the volatile group.

None

Slist_ptr sbmc_MS_get_conflicts

(

sbmc_MetaSolver *

ms

)

Returns the underlying solver.

Returns the solver

Slist_ptr sbmc_MS_get_model

(

sbmc_MetaSolver *

ms

)

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 must be NOT destroyed.

SatSolver_ptr sbmc_MS_get_solver

(

sbmc_MetaSolver *

ms

)

Returns the underlying solver.

Returns the solver

void sbmc_MS_goto_permanent_group

(

sbmc_MetaSolver *

ms

)

Destroy the volatile group of the meta solver wrapper.

Destroy the volatile group of the meta solver wrapper, thus only considering the permanent group.

None

void sbmc_MS_goto_volatile_group

(

sbmc_MetaSolver *

ms

)

Create and force use of the volatile group of the meta solver wrapper.

Create and force use of the volatile group of the meta solver wrapper.

None

SatSolverResult sbmc_MS_solve

(

sbmc_MetaSolver *

ms

)

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

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

None

See also:

SatSolver_solve_all_groups

SatSolverResult sbmc_MS_solve_assume	(	sbmc_MetaSolver *	ms,
		Slist_ptr	assumptions
	)

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

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

None

See also:

SatSolver_solve_all_groups_assume

void sbmc_MS_switch_to_permanent_group

(

sbmc_MetaSolver *

ms

)

Force use of the permanent group of the meta solver wrapper.

Force use of the permanent group of the meta solver wrapper. Volatile group is left in place, if existing

None

void sbmc_MS_switch_to_volatile_group

(

sbmc_MetaSolver *

ms

)

Force use of the volatile group of the meta solver wrapper.

Force use of the volatile group of the meta solver wrapper. The volatile group must have been previously created

None

array_t* sbmc_n_fresh_state_vars	(	const NuSMVEnv_ptr	env,
		SymbLayer_ptr	layer,
		const unsigned int	n,
		unsigned int *	index
	)

Creates N new fresh state variables.

Creates N new fresh state variables. The name is according to the pattern LTL_tu, being u an unsigned integer. The index is incremented by N. The new variables are stroed into an array of node_ptr

index is incremented by N.

void sbmc_print_Fvarmap	(	const NuSMVEnv_ptr	env,
		FILE *	out,
		node_ptr	var,
		node_ptr	formula
	)

Prints some of the information associated to a F formula.

Prints some of the information associated to a F formula.

None

void sbmc_print_Gvarmap	(	const NuSMVEnv_ptr	env,
		FILE *	out,
		node_ptr	var,
		node_ptr	formula
	)

Prints some of the information associated to a G formula.

Prints some of the information associated to a G formula.

None

void sbmc_print_node	(	const NuSMVEnv_ptr	env,
		FILE *	out,
		const char *	prefix,
		node_ptr	node,
		const char *	postfix
	)

Print a node_ptr expression by prefixing and suffixing it.

Prints a node_ptr expression in a file stream by prefixing and suffixing it with a string. If the prefix and suffix strings are NULL they are not printed out.

None

void sbmc_print_node_list	(	const NuSMVEnv_ptr	env,
		FILE *	out,
		lsList	l
	)

Prints a lsList of node_ptr.

Prints a lsList of node_ptr in a file stream.

None

void sbmc_print_varmap	(	const NuSMVEnv_ptr	env,
		FILE *	out,
		node_ptr	node,
		sbmc_node_info *	info
	)

Prints some of the information associated to a subformula.

Prints some of the information associated to a subformula.

None

int sbmc_real_k

(

int

k

)

Routines for the state indexing scheme.

The first real state is 2

None

See also:

sbmc_L_state sbmc_E_state sbmc_model_k sbmc_real_k_string

char* sbmc_real_k_string

(

const unsigned int

k_real

)

Routines for the state indexing scheme.

Returns a string correspondingg to the state considered. E, L, Real

The returned value must be freed

See also:

sbmc_L_state sbmc_E_state sbmc_real_k sbmc_model_k

void sbmc_remove_loop_variable	(	BddEnc_ptr	bdd_enc,
		BeFsm_ptr	fsm
	)

Remove the new layer to contain the loop variable.

void sbmc_reset_unique_id

(

const NuSMVEnv_ptr

env

)

Todo:

Missing synopsis

Todo:

Missing description

Trace_ptr Sbmc_Utils_fill_cntexample	(	BeEnc_ptr	be_enc,
		sbmc_MetaSolver *	solver,
		node_ptr	l_var,
		const int	k,
		Trace_ptr	trace
	)

Fills the given trace using the given sat assignment.

Fills the given trace using the given sat assignment.

The \"res\" trace is filled

See also:

Bmc_Utils_generate_cntexample

Trace_ptr Sbmc_Utils_generate_and_print_cntexample	(	BeEnc_ptr	be_enc,
		TraceMgr_ptr	tm,
		sbmc_MetaSolver *	solver,
		node_ptr	l_var,
		const int	k,
		const char *	trace_name,
		NodeList_ptr	symbols
	)

Extracts a trace from a sat assignment, and prints it.

Extracts a trace from a sat assignment, registers it in the TraceMgr and prints it using the default plugin.

None

See also:

Bmc_Utils_generate_and_print_cntexample Sbmc_Utils_generate_cntexample Sbmc_Utils_fill_cntexample

Trace_ptr Sbmc_Utils_generate_cntexample	(	BeEnc_ptr	be_enc,
		sbmc_MetaSolver *	solver,
		node_ptr	l_var,
		const int	k,
		const char *	trace_name,
		NodeList_ptr	symbols
	)

Extracts a trace from a sat assignment.

Extracts a trace from a sat assignment. The generated trace is non-volatile

None

See also:

Bmc_Utils_generate_cntexample Sbmc_Utils_fill_cntexample