NuSMV/code/nusmv/core/enc/bdd/BddEnc.h File Reference

#include "nusmv/core/enc/bdd/bdd.h"
#include "nusmv/core/enc/base/BoolEncClient.h"
#include "nusmv/core/enc/bool/BoolEnc.h"
#include "nusmv/core/enc/utils/OrdGroups.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/wff/ExprMgr.h"
#include "nusmv/core/fsm/bdd/bdd.h"
#include "nusmv/core/dd/dd.h"
#include "nusmv/core/dd/VarsHandler.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/object.h"
#include "nusmv/core/utils/assoc.h"
#include "nusmv/core/utils/OStream.h"
#include "nusmv/core/enc/utils/AddArray.h"

Go to the source code of this file.

Defines
#define	__BDDENC_LAZY_COMMIT_LAYER__   1
	Set to 1 if you want to enable the LAZY commit of layers within the BDD Enc.
#define	BDD_ENC(self)   ((BddEnc_ptr) self)
	To cast and check instances of class BddEnc.
#define	BDD_ENC_CHECK_INSTANCE(self)   (nusmv_assert(BDD_ENC(self) != BDD_ENC(NULL)))
Typedefs
typedef struct BddEnc_TAG *	BddEnc_ptr
typedef void(*	VPFBEFNNV )(BddEnc_ptr, OStream_ptr, node_ptr, node_ptr, void *)
typedef void(*	VPFNNF )(FILE *, node_ptr, node_ptr)
Enumerations
enum	t_format { DUMP_FORMAT_INVALID, DUMP_FORMAT_DOT, DUMP_FORMAT_DAVINCI }
enum	VarOrderingType { DUMP_DEFAULT, DUMP_BITS, DUMP_SCALARS_ONLY }
	Used when dumping ordering file. More...
Functions
void	BddEnc_print_formula (const NuSMVEnv_ptr env, node_ptr constr, const boolean verbose, const boolean formula)

---

Define Documentation

#define __BDDENC_LAZY_COMMIT_LAYER__   1

Set to 1 if you want to enable the LAZY commit of layers within the BDD Enc.

Set to 1 if you want to enable the LAZY commit of layers within the BDD Enc

#define BDD_ENC

(

self

)

((BddEnc_ptr) self)

To cast and check instances of class BddEnc.

These macros must be used respectively to cast and to check instances of class BddEnc

#define BDD_ENC_CHECK_INSTANCE

(

self

)

(nusmv_assert(BDD_ENC(self) != BDD_ENC(NULL)))

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef struct BddEnc_TAG* BddEnc_ptr

typedef void(* VPFBEFNNV)(BddEnc_ptr, OStream_ptr, node_ptr, node_ptr, void *)

typedef void(* VPFNNF)(FILE *, node_ptr, node_ptr)

Todo:

Missing synopsis

Todo:

Missing description

---

Enumeration Type Documentation

enum t_format

Todo:

Missing synopsis

Todo:

Missing description

Enumerator:

DUMP_FORMAT_INVALID
DUMP_FORMAT_DOT
DUMP_FORMAT_DAVINCI

enum VarOrderingType

Used when dumping ordering file.

Used when dumping ordering file

Enumerator:

DUMP_DEFAULT
DUMP_BITS
DUMP_SCALARS_ONLY

---

Function Documentation

void BddEnc_print_formula	(	const NuSMVEnv_ptr	env,
		node_ptr	constr,
		const boolean	verbose,
		const boolean	formula
	)

Prints a formula in canonical format.