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

#include <stdio.h>
#include "nusmv/core/dag/dag.h"
#include "nusmv/core/utils/Slist.h"
#include "nusmv/core/cinit/NuSMVEnv.h"

Go to the source code of this file.

Data Structures
struct	RbcDfsFunctions
Defines
#define	RBC_INVALID_CONVERSION_NAME   "invalid"
#define	RBC_INVALID_SUBST_VALUE   INT_MAX
#define	RBC_SHERIDAN_CONVERSION_NAME   "sheridan"
#define	RBC_TSEITIN_CONVERSION_NAME   "tseitin"
	Formula handling with Reduced Boolean Circuits (RBCs).
Typedefs
typedef int(*	Rbc_IntPtr_t )(void)
typedef void(*	Rbc_ProcPtr_t )(void)
typedef Dag_Vertex_t	Rbc_t
typedef Dag_DfsFunctions_t	RbcDfsFunctions_t
Enumerations
enum	Rbc_2CnfAlgorithm { RBC_INVALID_CONVERSION = 0, RBC_TSEITIN_CONVERSION, RBC_SHERIDAN_CONVERSION }
enum	Rbc_Bool_c { RBC_FALSE = DAG_ANNOTATION_BIT, RBC_TRUE = 0 }
Functions
const char *	Rbc_CnfConversionAlgorithm2Str (Rbc_2CnfAlgorithm algo)
	Conversion from CNF conversion algorithm enumerative to string.
Rbc_2CnfAlgorithm	Rbc_CnfConversionAlgorithmFromStr (const char *str)
	Conversion from string to CNF conversion algorithm enumerative.
const char *	Rbc_CnfGetValidRbc2CnfAlgorithms (void)
	String of valid conversion algorithms.
int	Rbc_CnfVar2RbcIndex (Rbc_Manager_t *rbcManager, int cnfVar)
	Returns the RBC index corresponding to a particular CNF var.
int	Rbc_Convert2Cnf (Rbc_Manager_t *rbcManager, Rbc_t *f, int polarity, Rbc_2CnfAlgorithm alg, Slist_ptr clauses, Slist_ptr vars, int *literalAssignedToWholeFormula)
	Translates the rbc into the corresponding (equisatisfiable) set of clauses.
void	Rbc_Dfs_clean_exported (Rbc_t *dfsRoot, Rbc_Manager_t *manager)
	Calls the internal DFS clean.
void	Rbc_Dfs_exported (Rbc_t *dfsRoot, RbcDfsFunctions_t *dfsFun, void *dfsData, Rbc_Manager_t *manager)
	Calls the internal DFS.
Rbc_t *	Rbc_GetIthVar (Rbc_Manager_t *rbcManager, int varIndex)
	Returns a variable.
Rbc_t *	Rbc_GetLeftOpnd (Rbc_t *f)
	Gets the left operand.
Rbc_t *	Rbc_GetOne (Rbc_Manager_t *rbcManager)
	Logical constant 1 (truth).
Rbc_t *	Rbc_GetRightOpnd (Rbc_t *f)
	Gets the right operand.
int	Rbc_GetVarIndex (Rbc_t *f)
	Gets the variable index.
Rbc_t *	Rbc_GetZero (Rbc_Manager_t *rbcManager)
	Logical constant 0 (falsity).
boolean	Rbc_is_and (Rbc_t *rbc)
	Check if a rbc type is RBCAND.
boolean	Rbc_is_iff (Rbc_t *rbc)
	Check if a rbc type is RBCIFF.
boolean	Rbc_is_ite (Rbc_t *rbc)
	Check if a rbc type is RBCITE.
boolean	Rbc_is_top (Rbc_t *rbc)
	Check if a rbc type is RBCTOP.
boolean	Rbc_is_var (Rbc_t *rbc)
	Check if a rbc type is RBCVAR.
boolean	Rbc_IsConstant (Rbc_Manager_t *manager, Rbc_t *f)
	Returns true if the given rbc is a constant value, such as either False or True.
Rbc_t *	Rbc_LogicalShift (Rbc_Manager_t *rbcManager, Rbc_t *f, int shift, const int *log2phy, const int *phy2log)
	Creates a fresh copy G(X') of the rbc F(X) by shifting each variable index of a certain amount.
Rbc_t *	Rbc_LogicalSubst (Rbc_Manager_t *rbcManager, Rbc_t *f, int *subst, const int *log2phy, const int *phy2log)
	Creates a fresh copy G(Y) of the rbc F(X) such that G(Y) = F(X)[Y/X] where X and Y are vectors of variables.
Rbc_t *	Rbc_LogicalSubstRbc (Rbc_Manager_t *rbcManager, Rbc_t *f, Rbc_t **substRbc, int *phy2log)
	Creates a fresh copy G(S) of the rbc F(X) such that G(S) = F(X)[S/X] where X is a vector of variables and S is a corresponding vector of formulas.
Rbc_t *	Rbc_MakeAnd (Rbc_Manager_t *rbcManager, Rbc_t *left, Rbc_t *right, Rbc_Bool_c sign)
	Makes the conjunction of two rbcs.
Rbc_t *	Rbc_MakeIff (Rbc_Manager_t *rbcManager, Rbc_t *left, Rbc_t *right, Rbc_Bool_c sign)
	Makes the coimplication of two rbcs.
Rbc_t *	Rbc_MakeIte (Rbc_Manager_t *rbcManager, Rbc_t *c, Rbc_t *t, Rbc_t *e, Rbc_Bool_c sign)
	Makes the if-then-else of three rbcs.
Rbc_t *	Rbc_MakeNot (Rbc_Manager_t *rbcManager, Rbc_t *left)
	Returns the complement of an rbc.
Rbc_t *	Rbc_MakeOr (Rbc_Manager_t *rbcManager, Rbc_t *left, Rbc_t *right, Rbc_Bool_c sign)
	Makes the disjunction of two rbcs.
Rbc_t *	Rbc_MakeXor (Rbc_Manager_t *rbcManager, Rbc_t *left, Rbc_t *right, Rbc_Bool_c sign)
	Makes the exclusive disjunction of two rbcs.
Rbc_Manager_t *	Rbc_ManagerAlloc (const NuSMVEnv_ptr env, int varCapacity)
	Creates a new RBC manager.
int	Rbc_ManagerCapacity (Rbc_Manager_t *rbcManager)
	Returns the current variable capacity of the rbc.
void	Rbc_ManagerFree (Rbc_Manager_t *rbcManager)
	Deallocates an RBC manager.
void	Rbc_ManagerGC (Rbc_Manager_t *rbcManager)
	Garbage collection in the RBC manager.
RbcDfsFunctions_t *	Rbc_ManagerGetDfsCleanFun (Rbc_Manager_t *rbcManager)
	Get the DAG cleaning function.
NuSMVEnv_ptr	Rbc_ManagerGetEnvironment (Rbc_Manager_t *rbcManager)
	Returns the environment instance.
void	Rbc_ManagerReserve (Rbc_Manager_t *rbcManager, int newVarCapacity)
	Reserves more space for new variables.
void	Rbc_ManagerReset (Rbc_Manager_t *rbcManager)
	Resets RBC manager.
void	Rbc_Mark (Rbc_Manager_t *rbc, Rbc_t *f)
	Makes a node permanent.
void	Rbc_OutputDaVinci (Rbc_Manager_t *rbcManager, Rbc_t *f, FILE *outFile)
	Print out an rbc using DaVinci graph format.
void	Rbc_OutputGdl (Rbc_Manager_t *rbcManager, Rbc_t *f, FILE *outFile)
	Print out an rbc using Gdl graph format.
void	Rbc_OutputSexpr (Rbc_Manager_t *rbcManager, Rbc_t *f, FILE *outFile)
	Print out an rbc using LISP S-expressions.
void	Rbc_pkg_init (void)
	Package initialization.
void	Rbc_pkg_quit (void)
	Package deinitialization.
void	Rbc_PrintStats (Rbc_Manager_t *rbcManager, int clustSz, FILE *outFile)
	Prints various statistics.
int	Rbc_RbcIndex2CnfVar (Rbc_Manager_t *rbcManager, int rbcIndex)
	Returns the associated CNF variable of a given RBC index.
Rbc_t *	Rbc_Shift (Rbc_Manager_t *rbcManager, Rbc_t *f, int shift)
	Creates a fresh copy G(X') of the rbc F(X) by shifting each variable index of a certain amount.
Rbc_t *	Rbc_Subst (Rbc_Manager_t *rbcManager, Rbc_t *f, int *subst)
	Creates a fresh copy G(Y) of the rbc F(X) such that G(Y) = F(X)[Y/X] where X and Y are vectors of variables.
Rbc_t *	Rbc_SubstRbc (Rbc_Manager_t *rbcManager, Rbc_t *f, Rbc_t **substRbc)
	Creates a fresh copy G(S) of the rbc F(X) such that G(S) = F(X)[S/X] where X is a vector of variables and S is a corresponding vector of formulas.
void	Rbc_Unmark (Rbc_Manager_t *rbc, Rbc_t *f)
	Makes a node volatile.
struct InlineResult_TAG *	RbcInline_apply_inlining (Rbc_Manager_t *rbcm, Rbc_t *f)
	Calculates the inlining of the given formula.
Slist_ptr	RbcUtils_get_dependencies (Rbc_Manager_t *rbcManager, Rbc_t *f, boolean reset_dag)
	None

---

Define Documentation

#define RBC_INVALID_CONVERSION_NAME   "invalid"

Todo:

Missing synopsis

Todo:

Missing description

#define RBC_INVALID_SUBST_VALUE   INT_MAX

Todo:

Missing synopsis

Todo:

Missing description

#define RBC_SHERIDAN_CONVERSION_NAME   "sheridan"

Todo:

Missing synopsis

Todo:

Missing description

#define RBC_TSEITIN_CONVERSION_NAME   "tseitin"

Formula handling with Reduced Boolean Circuits (RBCs).

Author:

Armando Tacchella, Marco Roveri External functions and data structures of the rbc package.

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef int(* Rbc_IntPtr_t)(void)

Todo:

Missing synopsis

Todo:

Missing description

typedef void(* Rbc_ProcPtr_t)(void)

Todo:

Missing synopsis

Todo:

Missing description

typedef Dag_Vertex_t Rbc_t

Todo:

Missing synopsis

Todo:

Missing description

typedef Dag_DfsFunctions_t RbcDfsFunctions_t

Todo:

Missing synopsis

Todo:

Missing description

---

Enumeration Type Documentation

enum Rbc_2CnfAlgorithm

RBC CNF conversion algorithm.

Enumerator:

RBC_INVALID_CONVERSION
RBC_TSEITIN_CONVERSION
RBC_SHERIDAN_CONVERSION

enum Rbc_Bool_c

RBC boolean values.

Enumerator:

RBC_FALSE
RBC_TRUE

---

Function Documentation

const char* Rbc_CnfConversionAlgorithm2Str

(

Rbc_2CnfAlgorithm

algo

)

Conversion from CNF conversion algorithm enumerative to string.

Rbc_2CnfAlgorithm Rbc_CnfConversionAlgorithmFromStr

(

const char *

str

)

Conversion from string to CNF conversion algorithm enumerative.

const char* Rbc_CnfGetValidRbc2CnfAlgorithms

(

void

)

String of valid conversion algorithms.

int Rbc_CnfVar2RbcIndex	(	Rbc_Manager_t *	rbcManager,
		int	cnfVar
	)

Returns the RBC index corresponding to a particular CNF var.

Returns -1, if there is no original RBC variable corresponding to CNF variable, this may be the case if CNF variable corresponds to an internal node (not leaf) of RBC tree. Input CNF variable should be a correct variable generated by RBC manager.

int Rbc_Convert2Cnf	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		int	polarity,
		Rbc_2CnfAlgorithm	alg,
		Slist_ptr	clauses,
		Slist_ptr	vars,
		int *	literalAssignedToWholeFormula
	)

Translates the rbc into the corresponding (equisatisfiable) set of clauses.

This calls the user's choice of translation procedure

`clauses' and `vars' are filled up. `clauses' is the empty list if `f' was true, and contains a single empty clause if `f' was false. 'polarity' is used to determine if the clauses generated should represent the RBC positively, negatively, or both (1, -1 or 0 respectively). For an RBC that is known to be true, the clauses that represent it being false are not needed (they would be removed anyway by propogating the unit literal which states that the RBC is true). Similarly for when the RBC is known to be false. This parameter is only used with the compact cnf conversion algorithm, and is ignored if the simple algorithm is used.

void Rbc_Dfs_clean_exported	(	Rbc_t *	dfsRoot,
		Rbc_Manager_t *	manager
	)

Calls the internal DFS clean.

This is an external function that call the internal DFS clean

See also:

Dag_Dfs()

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

Calls the internal DFS.

This is an external function that call the internal DFS

See also:

Dag_Dfs()

Rbc_t* Rbc_GetIthVar	(	Rbc_Manager_t *	rbcManager,
		int	varIndex
	)

Returns a variable.

Returns a pointer to an rbc node containing the requested variable. Works in three steps:

• the requested variable index exceeds the current capacity: allocated more room up to the requested index;
• the variable node does not exists: inserts it in the dag and makes it permanent;
• returns the variable node.

none

Rbc_t* Rbc_GetLeftOpnd

(

Rbc_t *

f

)

Gets the left operand.

Gets the left operand.

none

Rbc_t* Rbc_GetOne

(

Rbc_Manager_t *

rbcManager

)

Logical constant 1 (truth).

Returns the rbc that stands for logical truth.

none

Rbc_t* Rbc_GetRightOpnd

(

Rbc_t *

f

)

Gets the right operand.

Gets the right operand.

none

int Rbc_GetVarIndex

(

Rbc_t *

f

)

Gets the variable index.

Returns the variable index, -1 if the rbc is not a variable.

none

Rbc_t* Rbc_GetZero

(

Rbc_Manager_t *

rbcManager

)

Logical constant 0 (falsity).

Returns the rbc that stands for logical falsity.

none

boolean Rbc_is_and

(

Rbc_t *

rbc

)

Check if a rbc type is RBCAND.

Check if a rbc type is RBCAND

boolean Rbc_is_iff

(

Rbc_t *

rbc

)

Check if a rbc type is RBCIFF.

Check if a rbc type is RBCIFF

boolean Rbc_is_ite

(

Rbc_t *

rbc

)

Check if a rbc type is RBCITE.

Check if a rbc type is RBCITE

boolean Rbc_is_top

(

Rbc_t *

rbc

)

Check if a rbc type is RBCTOP.

Check if a rbc type is RBCTOP

boolean Rbc_is_var

(

Rbc_t *

rbc

)

Check if a rbc type is RBCVAR.

Check if a rbc type is RBCVAR

boolean Rbc_IsConstant	(	Rbc_Manager_t *	manager,
		Rbc_t *	f
	)

Returns true if the given rbc is a constant value, such as either False or True.

Rbc_t* Rbc_LogicalShift	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		int	shift,
		const int *	log2phy,
		const int *	phy2log
	)

Creates a fresh copy G(X') of the rbc F(X) by shifting each variable index of a certain amount.

Given `rbcManager', the rbc `f', and the integer `shift', replaces every occurence of the variable x_i in in `f' with the variable x_(i + shift).

Notice that in this context, 'i' is a LOGICAL index, not physical, i.e. the substitution array is provided in terms of logical indices, and is related only to the logical level.

For a substitution at physical level, see Rbc_SubstRbc.

The two indices arrays log2phy and phy2log map respectively the logical level to the physical level, and the physical level to the logical levels. They allow the be encoder to freely organize the variables into a logical and a physical level. This feature has been introduced with NuSMV-2.4 that ships dynamic encodings.

none

Rbc_t* Rbc_LogicalSubst	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		int *	subst,
		const int *	log2phy,
		const int *	phy2log
	)

Creates a fresh copy G(Y) of the rbc F(X) such that G(Y) = F(X)[Y/X] where X and Y are vectors of variables.

Given `rbcManager', the rbc `f', and the array of integers `subst', replaces every occurence of the variable x_i in in `f' with the variable x_j provided that subst[i] = j.

Notice that in this context, 'i' and 'j' are LOGICAL indices, not physical, i.e. the substitution array is provided in terms of logical indices, and is related only to the logical level.

For a substitution at physical level, see Rbc_Subst.

There is no need for `subst' to contain all the variables, but it should map at least the variables in `f' in order for the substitution to work properly.

The two indices arrays log2phy and phy2log map respectively the logical level to the physical level, and the physical level to the logical levels. They allow the be encoder to freely organize the variables into a logical and a physical level. This feature has been introduced with NuSMV-2.4 that ships dynamic encodings.

none

See also:

Rbc_Subst

Rbc_t* Rbc_LogicalSubstRbc	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		Rbc_t **	substRbc,
		int *	phy2log
	)

Creates a fresh copy G(S) of the rbc F(X) such that G(S) = F(X)[S/X] where X is a vector of variables and S is a corresponding vector of formulas.

Given `rbcManager', the rbc `f', and the array of rbcs `substRbc', replaces every occurence of the variable x_i in in `f' with the rbc r_i provided that substRbc[i] = r_i.

Notice that in this context, 'i' is a LOGICAL index, not physical.

There is no need for `substRbc' to contain all the variables, but it should map at least the variables in `f' in order for the substitution to work properly.

The two indices arrays log2phy and phy2log map respectively the logical level to the physical level, and the physical level to the logical levels. They allow the be encoder to freely organize the variables into a logical and a physical level. This feature has been introduced with NuSMV-2.4 that ships dynamic encodings.

none

Rbc_t* Rbc_MakeAnd	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	left,
		Rbc_t *	right,
		Rbc_Bool_c	sign
	)

Makes the conjunction of two rbcs.

Makes the conjunction of two rbcs. Works in three steps:

• performs boolean simplification: if successfull, returns the result of the simplification;
• orders left and right son pointers;
• looks up the formula in the dag and returns it.

If RBC_ENABLE_LOCAL_MINIMIZATION_WITHOUT_BLOWUP is defined, applies all the rules proposed in R. Brummayer and A. Biere. Local Two-Level And-Inverter Graph Minimization without Blowup. In Proc. MEMICS 2006. The expressions o1, o2, o3, o4 refers to the four level of optimization proposed in the paper. The rules are implemented as macros in order to avoid repetitions

none

Rbc_t* Rbc_MakeIff	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	left,
		Rbc_t *	right,
		Rbc_Bool_c	sign
	)

Makes the coimplication of two rbcs.

Makes the coimplication of two rbcs. Works in four steps:

• performs boolean simplification: if successfull, returns the result of the simplification;
• orders left and right son pointers;
• re-encodes the negation

• looks up the formula in the dag and returns it.

• If the coimplication mode is disable, expands the connective in three AND nodes.

none

Rbc_t* Rbc_MakeIte	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	c,
		Rbc_t *	t,
		Rbc_t *	e,
		Rbc_Bool_c	sign
	)

Makes the if-then-else of three rbcs.

Makes the if-then-else of three rbcs: expands the connective into the corresponding product-of-sums.

If the if-then-else mode is disable, expands the connective in three AND nodes

none

Rbc_t* Rbc_MakeNot	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	left
	)

Returns the complement of an rbc.

Returns the complement of an rbc.

none

Rbc_t* Rbc_MakeOr	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	left,
		Rbc_t *	right,
		Rbc_Bool_c	sign
	)

Makes the disjunction of two rbcs.

Makes the disjunction of two rbcs: casts the connective to the negation of a conjunction using De Morgan's law.

none

Rbc_t* Rbc_MakeXor	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	left,
		Rbc_t *	right,
		Rbc_Bool_c	sign
	)

Makes the exclusive disjunction of two rbcs.

Makes the exclusive disjunction of two rbcs: casts the connective as the negation of a coimplication.

none

Rbc_Manager_t* Rbc_ManagerAlloc	(	const NuSMVEnv_ptr	env,
		int	varCapacity
	)

Creates a new RBC manager.

Creates a new RBC manager:

• varCapacity how big is the variable index (this number must be strictly greater than 0)

Returns the allocated manager if varCapacity is greater than 0, and NIL(Rbc_Manager_t) otherwise.

none

See also:

Rbc_ManagerFree

int Rbc_ManagerCapacity

(

Rbc_Manager_t *

rbcManager

)

Returns the current variable capacity of the rbc.

This number is the maximum number of variables (starting from 0) that can be requested without causing any memory allocation.

none

void Rbc_ManagerFree

(

Rbc_Manager_t *

rbcManager

)

Deallocates an RBC manager.

Frees the variable index and the internal dag manager.

none

void Rbc_ManagerGC

(

Rbc_Manager_t *

rbcManager

)

Garbage collection in the RBC manager.

Relies on the internal DAG garbage collector.

None

RbcDfsFunctions_t* Rbc_ManagerGetDfsCleanFun

(

Rbc_Manager_t *

rbcManager

)

Get the DAG cleaning function.

Get the DAG cleaning function

NuSMVEnv_ptr Rbc_ManagerGetEnvironment

(

Rbc_Manager_t *

rbcManager

)

Returns the environment instance.

void Rbc_ManagerReserve	(	Rbc_Manager_t *	rbcManager,
		int	newVarCapacity
	)

Reserves more space for new variables.

If the requested space is bigger than the current one makes room for more variables in the varTable.

none

void Rbc_ManagerReset

(

Rbc_Manager_t *

rbcManager

)

Resets RBC manager.

none

void Rbc_Mark	(	Rbc_Manager_t *	rbc,
		Rbc_t *	f
	)

Makes a node permanent.

Marks the vertex in the internal dag. This saves the rbc from being wiped out during garbage collection.

none

void Rbc_OutputDaVinci	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		FILE *	outFile
	)

Print out an rbc using DaVinci graph format.

Print out an rbc using DaVinci graph format.

None

void Rbc_OutputGdl	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		FILE *	outFile
	)

Print out an rbc using Gdl graph format.

Print out an rbc using Gdl graph format.

None

void Rbc_OutputSexpr	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		FILE *	outFile
	)

Print out an rbc using LISP S-expressions.

Print out an rbc using LISP S-exrpressions.

None

void Rbc_pkg_init

(

void

)

Package initialization.

void Rbc_pkg_quit

(

void

)

Package deinitialization.

void Rbc_PrintStats	(	Rbc_Manager_t *	rbcManager,
		int	clustSz,
		FILE *	outFile
	)

Prints various statistics.

Prints various statistics.

None

int Rbc_RbcIndex2CnfVar	(	Rbc_Manager_t *	rbcManager,
		int	rbcIndex
	)

Returns the associated CNF variable of a given RBC index.

Returns 0, if there is no original RBC variable corresponding to CNF variable. This may be the case if particular RBC node (of the given variable) has never been converted into CNF

Rbc_t* Rbc_Shift	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		int	shift
	)

Creates a fresh copy G(X') of the rbc F(X) by shifting each variable index of a certain amount.

Given `rbcManager', the rbc `f', and the integer `shift', replaces every occurence of the variable x_i in in `f' with the variable x_(i + shift).

!!!!!! WARNING WARNING WARNING WARNING WARNING WARNING !!!!! !! !! !! This function cannot be used with the new encoding BeEnc, !! !! with NuSMV-2.4. As shifting involves the traversal of the !! !! logical layer within the !! !! BeEnc, simple shifting is no longer usable, and will produce !! !! unpredictable results if used on variables handled by a BeEnc !! !! instance. !! !! !! !! Use Rbc_LogicalShiftVar instead. !! !! !! !!!!!! WARNING WARNING WARNING WARNING WARNING WARNING !!!!!

none

Rbc_t* Rbc_Subst	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		int *	subst
	)

Creates a fresh copy G(Y) of the rbc F(X) such that G(Y) = F(X)[Y/X] where X and Y are vectors of variables.

Given `rbcManager', the rbc `f', and the array of integers `subst', replaces every occurence of the variable x_i in in `f' with the variable x_j provided that subst[i] = j. There is no need for `subst' to contain all the variables, but it should map at least the variables in `f' in order for the substitution to work properly.

Here the substitution is performed completely at physical level (i.e. at the level of pure rbc indices). For a substitution at logical level, see Rbc_LogicalSubst.

!!!!!! WARNING WARNING WARNING WARNING WARNING WARNING !!!!! !! !! !! This function cannot be used with the new encoding BeEnc. As !! !! substitution involves the traversal of the logical layer within !! !! the BeEnc, simple shifting is no longer usable, and will !! !! produce unpredictable results if used on variables handled by !! !! a BeEnc instance. !! !! !! !! Use Rbc_LogicalSubst instead. !! !! !! !!!!!! WARNING WARNING WARNING WARNING WARNING WARNING !!!!!

none

See also:

Rbc_LogicalSubst

Rbc_t* Rbc_SubstRbc	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		Rbc_t **	substRbc
	)

Creates a fresh copy G(S) of the rbc F(X) such that G(S) = F(X)[S/X] where X is a vector of variables and S is a corresponding vector of formulas.

Given `rbcManager', the rbc `f', and the array of rbcs `substRbc', replaces every occurence of the variable x_i in in `f' with the rbc r_i provided that substRbc[i] = r_i. There is no need for `substRbc' to contain all the variables, but it should map at least the variables in `f' in order for the substitution to work properly.

Here the substitution is performed completely at physical level (i.e. at the level of pure rbc indices). For a substitution at logical level, see Rbc_LogicalSubstRbc.

none

void Rbc_Unmark	(	Rbc_Manager_t *	rbc,
		Rbc_t *	f
	)

Makes a node volatile.

Unmarks the vertex in the internal dag. This exposes the rbc to garbage collection.

none

struct InlineResult_TAG* RbcInline_apply_inlining	(	Rbc_Manager_t *	rbcm,
		Rbc_t *	f
	)			[read]

Calculates the inlining of the given formula.

Returned InlineResult instance is cached and must be _NOT_ destroyed by the caller

None

See also:

InlineResult

Slist_ptr RbcUtils_get_dependencies	(	Rbc_Manager_t *	rbcManager,
		Rbc_t *	f,
		boolean	reset_dag
	)

None