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

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/prop/Prop.h"

Go to the source code of this file.

Functions
int	Sbmc_zigzag_incr (NuSMVEnv_ptr env, Prop_ptr ltlprop, const int max_k, const int opt_do_virtual_unrolling, const int opt_do_completeness_check)
	High level functionalities for Incrememntal SBMC.
int	Sbmc_zigzag_incr_assume (NuSMVEnv_ptr env, Prop_ptr ltlprop, const int max_k, const int opt_do_virtual_unrolling, const int opt_do_completeness_check, Slist_ptr assumptions, Slist_ptr *conflict)
	High level function that performs incremental sbmc under assumptions. Currently this routine requires MiniSAT being used as SAT solver.

---

Function Documentation

int Sbmc_zigzag_incr	(	NuSMVEnv_ptr	env,
		Prop_ptr	ltlprop,
		const int	max_k,
		const int	opt_do_virtual_unrolling,
		const int	opt_do_completeness_check
	)

High level functionalities for Incrememntal SBMC.

Author:

Tommi Junttila, Marco Roveri User-commands directly use function defined in this module. This is the highest level in the Incrememntal SBMC API architecture.AutomaticStart

High level function that performs incremental sbmc optional

required

See also:

optional

int Sbmc_zigzag_incr_assume	(	NuSMVEnv_ptr	env,
		Prop_ptr	ltlprop,
		const int	max_k,
		const int	opt_do_virtual_unrolling,
		const int	opt_do_completeness_check,
		Slist_ptr	assumptions,
		Slist_ptr *	conflict
	)

High level function that performs incremental sbmc under assumptions. Currently this routine requires MiniSAT being used as SAT solver.

optional

required

See also:

optional