NuSMV/code/nusmv/core/rbc/rbcInt.h File Reference

#include "nusmv/core/rbc/rbc.h"
#include "nusmv/core/rbc/InlineResult.h"
#include "nusmv/core/opt/opt.h"
#include "nusmv/core/utils/LRUCache.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/assoc.h"

Go to the source code of this file.

Data Structures
struct	Rbc_Manager_t
	RBC manager. More...
Defines
#define	RBC_ENABLE_IFF_CONNECTIVE   1
#define	RBC_ENABLE_ITE_CONNECTIVE   1
	Formula handling with Reduced Boolean Circuits (RBCs).
#define	RBC_GET_LEFTMOST_CHILD(rbc)   (rbc->outList[0])
	Control the way compact CNF conversion is performed.
#define	RBC_GET_SECOND_CHILD(rbc)   (rbc->outList[1])
#define	Rbc_get_type(rbc)   rbc->symbol
#define	RBCAND   (int) 2
#define	RbcClear(p)   Dag_VertexClear(p)
#define	RBCDUMMY   ((Rbc_t*) 4)
#define	RbcGetRef(p)   Dag_VertexGetRef(p)
	Rbc interface to underlying package.
#define	RbcId(r, s)   DagId(r,s)
#define	RBCIFF   (int) 3
#define	RbcIsSet(p)   Dag_VertexIsSet(p)
#define	RBCITE   (int) 4
#define	RBCMAX_STAT   (int) 1
#define	RbcSet(p)   Dag_VertexSet(p)
#define	RBCTOP   (int) 0
#define	RBCVAR   (int) 1
#define	RBCVAR_NO   (int) 0
Functions
int	Rbc_Convert2CnfCompact (Rbc_Manager_t *rbcManager, Rbc_t *f, int polarity, Slist_ptr clauses, Slist_ptr vars, int *literalAssignedToWholeFormula)
int	Rbc_Convert2CnfSimple (Rbc_Manager_t *rbcManager, Rbc_t *f, Slist_ptr clauses, Slist_ptr vars, int *literalAssignedToWholeFormula)
void	Rbc_Dfs (Rbc_t *dfsRoot, RbcDfsFunctions_t *dfsFun, void *dfsData, Rbc_Manager_t *manager)
void	Rbc_Dfs_clean (Rbc_t *dfsRoot, Rbc_Manager_t *manager)
void	Rbc_Dfs_do_only_last_visit (Rbc_t *dfsRoot, RbcDfsFunctions_t *dfsFun, void *dfsData, Rbc_Manager_t *manager)
int	Rbc_get_node_cnf (Rbc_Manager_t *rbcm, Rbc_t *f, int *maxvar)
void	rbc_inlining_cache_init (Rbc_Manager_t *)
InlineResult_ptr	rbc_inlining_cache_lookup_result (Rbc_Manager_t *rbcm, Rbc_t *f)
	Inline caching private service to retrieve a value.
void	rbc_inlining_cache_quit (Rbc_Manager_t *)

---

Define Documentation

#define RBC_ENABLE_IFF_CONNECTIVE   1

Todo:

Missing synopsis

Todo:

Missing description

#define RBC_ENABLE_ITE_CONNECTIVE   1

Formula handling with Reduced Boolean Circuits (RBCs).

Author:

Armando Tacchella and Tommi Junttila Internal functions and data structures of the rbc package.

Todo:

Missing synopsis

Todo:

Missing description

#define RBC_GET_LEFTMOST_CHILD

(

rbc

)

(rbc->outList[0])

Control the way compact CNF conversion is performed.

none

Get the leftmost child. Get the leftmost child.

#define RBC_GET_SECOND_CHILD

(

rbc

)

(rbc->outList[1])

Get the right children.

#define Rbc_get_type

(

rbc

)

rbc->symbol

Todo:

Missing synopsis

Todo:

Missing description

#define RBCAND   (int) 2

Todo:

Missing synopsis

Todo:

Missing description

#define RbcClear

(

p

)

Dag_VertexClear(p)

Todo:

Missing synopsis

Todo:

Missing description

#define RBCDUMMY   ((Rbc_t*) 4)

Todo:

Missing synopsis

Todo:

Missing description

#define RbcGetRef

(

p

)

Dag_VertexGetRef(p)

Rbc interface to underlying package.

Rbc interface to underlying package

#define RbcId	(	r,
		s		)	DagId(r,s)

Todo:

Missing synopsis

Todo:

Missing description

#define RBCIFF   (int) 3

Todo:

Missing synopsis

Todo:

Missing description

#define RbcIsSet

(

p

)

Dag_VertexIsSet(p)

Todo:

Missing synopsis

Todo:

Missing description

#define RBCITE   (int) 4

Todo:

Missing synopsis

Todo:

Missing description

#define RBCMAX_STAT   (int) 1

Todo:

Missing synopsis

Todo:

Missing description

#define RbcSet

(

p

)

Dag_VertexSet(p)

Todo:

Missing synopsis

Todo:

Missing description

#define RBCTOP   (int) 0

Todo:

Missing synopsis

Todo:

Missing description

#define RBCVAR   (int) 1

Todo:

Missing synopsis

Todo:

Missing description

#define RBCVAR_NO   (int) 0

Todo:

Missing synopsis

Todo:

Missing description

---

Function Documentation

int Rbc_Convert2CnfCompact	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		int	polarity,
		Slist_ptr	clauses,
		Slist_ptr	vars,
		int *	literalAssignedToWholeFormula
	)

int Rbc_Convert2CnfSimple	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		Slist_ptr	clauses,
		Slist_ptr	vars,
		int *	literalAssignedToWholeFormula
	)

AutomaticStart

void Rbc_Dfs	(	Rbc_t *	dfsRoot,
		RbcDfsFunctions_t *	dfsFun,
		void *	dfsData,
		Rbc_Manager_t *	manager
	)

void Rbc_Dfs_clean	(	Rbc_t *	dfsRoot,
		Rbc_Manager_t *	manager
	)

void Rbc_Dfs_do_only_last_visit	(	Rbc_t *	dfsRoot,
		RbcDfsFunctions_t *	dfsFun,
		void *	dfsData,
		Rbc_Manager_t *	manager
	)

int Rbc_get_node_cnf	(	Rbc_Manager_t *	rbcm,
		Rbc_t *	f,
		int *	maxvar
	)

void rbc_inlining_cache_init

(

Rbc_Manager_t *

)

InlineResult_ptr rbc_inlining_cache_lookup_result	(	Rbc_Manager_t *	rbcm,
		Rbc_t *	f
	)

Inline caching private service to retrieve a value.

Returned instance is NOT referenced, do not destroy it as it belongs to the cache.

void rbc_inlining_cache_quit

(

Rbc_Manager_t *

)