Biddy  1.7.1
An academic Binary Decision Diagrams package
biddyMain.c File Reference

File biddyMain.c contains main functions for representation and manipulation of boolean functions with ROBDDs. More...

#include "biddyInt.h"

Go to the source code of this file.

Functions

void Biddy_InitMNG (Biddy_Manager *mng, int gddtype)
 Function Biddy_InitMNG initialize a manager. More...
 
void Biddy_ExitMNG (Biddy_Manager *mng)
 Function Biddy_ExitMNG deletes a manager. More...
 
Biddy_String Biddy_About ()
 Function Biddy_About reports version of Biddy package. More...
 
int Biddy_Managed_GetManagerType (Biddy_Manager MNG)
 Function Biddy_Managed_GetManagerType reports BDD type used in the manager. More...
 
void Biddy_Managed_SetManagerParameters (Biddy_Manager MNG, float gcr, float gcrF, float gcrX, float rr, float rrF, float rrX, float st, float fst, float cst, float fcst)
 Function Biddy_Managed_SetManagerParameters set modifiable parameters. More...
 
Biddy_Edge Biddy_GetThen (Biddy_Edge fun)
 Function Biddy_GetThen returns THEN successor. More...
 
Biddy_Edge Biddy_GetElse (Biddy_Edge fun)
 Function Biddy_GetElse returns ELSE successor. More...
 
Biddy_Variable Biddy_GetTopVariable (Biddy_Edge fun)
 Function Biddy_GetTopVariable returns the top variable. More...
 
Biddy_Boolean Biddy_Managed_IsEqv (Biddy_Manager MNG1, Biddy_Edge f1, Biddy_Manager MNG2, Biddy_Edge f2)
 Function Biddy_Managed_IsEqv returns TRUE iff two BDDs are equal. More...
 
void Biddy_Managed_SelectNode (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_SelectNode selects the top node of the given function. More...
 
void Biddy_Managed_DeselectNode (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_DeselectNode deselects the top node of the given function. More...
 
Biddy_Boolean Biddy_Managed_IsSelected (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_IsSelected returns TRUE iff the top node of the given function is selected. More...
 
void Biddy_Managed_SelectFunction (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_SelectFunction recursively selects all nodes of a given function. More...
 
void Biddy_Managed_DeselectAll (Biddy_Manager MNG)
 Function Biddy_Managed_DeselectAll deselects all nodes. More...
 
Biddy_Edge Biddy_Managed_GetTerminal (Biddy_Manager MNG)
 Function Biddy_Managed_GetTerminal returns unmarked edge pointing to the constant node 1. More...
 
Biddy_Edge Biddy_Managed_GetConstantZero (Biddy_Manager MNG)
 Function Biddy_Managed_GetConstantZero returns constant 0. More...
 
Biddy_Edge Biddy_Managed_GetConstantOne (Biddy_Manager MNG)
 Function Biddy_Managed_GetConstantOne returns constant 1. More...
 
Biddy_Edge Biddy_Managed_GetBaseSet (Biddy_Manager MNG)
 Function Biddy_Managed_GetBaseSet returns set containing only a null combination, i.e. it returns {{}}. More...
 
Biddy_Variable Biddy_Managed_GetVariable (Biddy_Manager MNG, Biddy_String x)
 Function Biddy_Managed_GetVariable returns variable with the given name. More...
 
Biddy_Variable Biddy_Managed_GetPrevVariable (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetPrevVariable returns previous variable in the global ordering (lower, topmore). More...
 
Biddy_Variable Biddy_Managed_GetNextVariable (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetNextVariable returns next variable in the global ordering (higher, bottommore). More...
 
Biddy_Edge Biddy_Managed_GetVariableEdge (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetVariableEdge returns variable's edge. More...
 
Biddy_Edge Biddy_Managed_GetElementEdge (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetElementEdge returns element's edge. More...
 
Biddy_String Biddy_Managed_GetVariableName (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetVariableName returns the name of a variable. More...
 
Biddy_Edge Biddy_Managed_GetTopVariableEdge (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_GetTopVariableEdge returns variable's edge of top variable. More...
 
Biddy_String Biddy_Managed_GetTopVariableName (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_GetTopVariableName returns the name of top variable. More...
 
char Biddy_Managed_GetTopVariableChar (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_GetTopVariableChar returns the first character in the name of top variable. More...
 
void Biddy_Managed_ResetVariablesValue (Biddy_Manager MNG)
 Function Biddy_Managed_ResetVariablesValue sets all variable's value to biddyZero. More...
 
void Biddy_Managed_SetVariableValue (Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge f)
 Function Biddy_Managed_SetVariableValue sets variable's value. More...
 
Biddy_Boolean Biddy_Managed_IsSmaller (Biddy_Manager MNG, Biddy_Variable fv, Biddy_Variable gv)
 Function Biddy_Managed_IsSmaller returns TRUE if the first variable is smaller (= lower = previous = above = topmore). More...
 
Biddy_Variable Biddy_Managed_FoaVariable (Biddy_Manager MNG, Biddy_String x, Biddy_Boolean varelem)
 Function Biddy_Managed_FoaVariable finds variable/element or adds new variable (i.e. Boolean function f = x) and new element (i.e. it creates set {{x}}). More...
 
Biddy_Edge Biddy_Managed_AddVariableByName (Biddy_Manager MNG, Biddy_String x)
 Function Biddy_Managed_AddVariableByName adds variable. More...
 
Biddy_Edge Biddy_Managed_AddElementByName (Biddy_Manager MNG, Biddy_String x)
 Function Biddy_Managed_AddElementByName adds element. More...
 
Biddy_Edge Biddy_Managed_AddVariableBelow (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_AddVariableBelow adds a numbered variable. More...
 
Biddy_Edge Biddy_Managed_AddVariableAbove (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_AddVariableAbove adds a numbered variable. More...
 
Biddy_Edge Biddy_Managed_TransferMark (Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean mark, Biddy_Boolean leftright)
 Function Biddy_Managed_TransferMark returns edge with inverted complement bit iff the second parameter is TRUE and normalization rules require this. More...
 
Biddy_Edge Biddy_Managed_IncTag (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_IncTag returns edge with an incremented tag. More...
 
Biddy_Edge Biddy_Managed_TaggedFoaNode (Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge pf, Biddy_Edge pt, Biddy_Variable ptag, Biddy_Boolean garbageAllowed)
 Function Biddy_Managed_TaggedFoaNode finds or adds new node with the given variable and successors. More...
 
Biddy_Edge Biddy_Managed_Not (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_Not calculates Boolean function NOT. More...
 
Biddy_Edge Biddy_Managed_ITE (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Edge h)
 Function Biddy_Managed_ITE calculates ITE operation of three Boolean functions. More...
 
Biddy_Edge Biddy_Managed_And (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_And calculates Boolean function AND (conjunction). More...
 
Biddy_Edge Biddy_Managed_Or (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Or calculates Boolean function OR (disjunction). More...
 
Biddy_Edge Biddy_Managed_Nand (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Nand calculates Boolean function NAND (Sheffer). More...
 
Biddy_Edge Biddy_Managed_Nor (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Nor calculates Boolean function NOR (Peirce). More...
 
Biddy_Edge Biddy_Managed_Xor (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Xor calculates Boolean function XOR. More...
 
Biddy_Edge Biddy_Managed_Xnor (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Xnor calculates Boolean function XNOR. More...
 
Biddy_Edge Biddy_Managed_Leq (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Leq calculates Boolean implication. More...
 
Biddy_Edge Biddy_Managed_Gt (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Gt calculates the negation of Boolean implication. More...
 
Biddy_Boolean Biddy_Managed_IsLeq (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_IsLeq returns TRUE iff function f is included in function g. More...
 
Biddy_Edge Biddy_Managed_SubIntersect (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Biddy_Managed_SubIntersect calculates a function included in the intersection of f and g. More...
 
Biddy_Edge Biddy_Managed_Restrict (Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v, Biddy_Boolean value)
 Function Biddy_Managed_Restrict calculates a restriction of Boolean function. More...
 
Biddy_Edge Biddy_Managed_Compose (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Variable v)
 Function Biddy_Managed_Compose calculates a composition of two Boolean functions. More...
 
Biddy_Edge Biddy_Managed_E (Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
 Function Biddy_Managed_E calculates an existential quantification of Boolean function. More...
 
Biddy_Edge Biddy_Managed_A (Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
 Function Biddy_Managed_A calculates an universal quantification of Boolean function. More...
 
Biddy_Boolean Biddy_Managed_IsVariableDependent (Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
 Function Biddy_Managed_IsVariableDependent returns TRUE iff variable is dependent on others in a function. More...
 
Biddy_Edge Biddy_Managed_ExistAbstract (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge cube)
 Function Biddy_Managed_ExistAbstract existentially abstracts all the variables in cube from f. More...
 
Biddy_Edge Biddy_Managed_UnivAbstract (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge cube)
 Function Biddy_Managed_UnivAbstract universally abstracts all the variables in cube from f. More...
 
Biddy_Edge Biddy_Managed_AndAbstract (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Edge cube)
 Function Biddy_Managed_AndAbstract calculates the AND of two BDDs and simultaneously (existentially) abstracts the variables in cube. More...
 
Biddy_Edge Biddy_Managed_Constrain (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge c)
 Function Biddy_Managed_Constrain calculates Coudert and Madre's constrain function. More...
 
Biddy_Edge Biddy_Managed_Simplify (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge c)
 Function Biddy_Managed_Simplify calculates Coudert and Madre's restrict function. More...
 
Biddy_Edge Biddy_Managed_Support (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_Support calculates a product of all dependent variables. More...
 
Biddy_Edge Biddy_Managed_Replace (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_Replace calculates BDD with one or more variables replaced. More...
 
Biddy_Edge Biddy_Managed_Change (Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
 Function Biddy_Managed_Change change the form of the given variable (positive literal becomes negative and vice versa). More...
 
Biddy_Edge Biddy_Managed_Subset (Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v, Biddy_Boolean value)
 Function Biddy_Managed_Subset calculates a division of Boolean function with a literal. More...
 
Biddy_Boolean Biddy_Managed_IsOK (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_IsOK returns TRUE iff given node is not obsolete. More...
 
void Biddy_Managed_GC (Biddy_Manager MNG, Biddy_Variable target, Biddy_Boolean purge, Biddy_Boolean total)
 Function Biddy_Managed_GC performs garbage collection. More...
 
void Biddy_Managed_Clean (Biddy_Manager MNG)
 Function Biddy_Managed_Clean performs cleaning. More...
 
void Biddy_Managed_Purge (Biddy_Manager MNG)
 Function Biddy_Managed_Purge immediately removes all nodes which were not preserved or which are not preserved anymore. More...
 
void Biddy_Managed_PurgeAndReorder (Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean converge)
 Function Biddy_Managed_PurgeAndReorder immediately removes non-preserved nodes and triggers reordering on function. More...
 
void Biddy_Managed_Refresh (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_Refresh refreshes top node in a given function. More...
 
void Biddy_Managed_AddCache (Biddy_Manager MNG, Biddy_GCFunction gc)
 Function Biddy_Managed_AddCache adds cache to the end of Cache list. More...
 
unsigned int Biddy_Managed_AddFormula (Biddy_Manager MNG, Biddy_String x, Biddy_Edge f, int c)
 Function Biddy_Managed_AddFormula adds formula to Formula table. More...
 
Biddy_Boolean Biddy_Managed_FindFormula (Biddy_Manager MNG, Biddy_String x, Biddy_Edge *f)
 Function Biddy_Managed_FindFormula find formula in Formula table. More...
 
Biddy_Boolean Biddy_Managed_DeleteFormula (Biddy_Manager MNG, Biddy_String x)
 Function Biddy_Managed_DeleteFormula delete formula from Formula table. More...
 
Biddy_Boolean Biddy_Managed_DeleteIthFormula (Biddy_Manager MNG, unsigned int i)
 Function Biddy_Managed_DeleteIthFormula deletes formula from the table. More...
 
Biddy_Edge Biddy_Managed_GetIthFormula (Biddy_Manager MNG, unsigned int i)
 Function Biddy_Managed_GetIthFormula returns ith formula in a Formula table. More...
 
Biddy_String Biddy_Managed_GetIthFormulaName (Biddy_Manager MNG, unsigned int i)
 Function Biddy_Managed_GetIthFormulaName returns name of the ith formula in a Formula table. More...
 
Biddy_Variable Biddy_Managed_SwapWithHigher (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_SwapWithHigher swaps two adjacent variables. More...
 
Biddy_Variable Biddy_Managed_SwapWithLower (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_SwapWithLower swaps two adjacent variables. More...
 
Biddy_Boolean Biddy_Managed_Sifting (Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean converge)
 Function Biddy_Managed_Sifting reorders variables to minimize node number for the whole system (if f = NULL) or for the given function (if f != NULL) using Rudell's sifting algorithm. More...
 
Biddy_Edge Biddy_Managed_Copy (Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_Edge f)
 Function Biddy_Managed_Copy copies a graph from one manager to another manager.

Description

The function takes a graph from one manager and creates the same graph in another manager. The resulting graph will represent the same Boolean function assuming the domain from the target manager. If f = biddyZero then only the domain is copied.

Side effects

If source and target manager are the same then function does nothing. The variable ordering of created BDD is adapted to the target manager.

More info

Macro Biddy_Copy(MNG2,f) is defined for use with anonymous manager.
 
void Biddy_Managed_CopyFormula (Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_String x)
 Function Biddy_Managed_CopyFormula uses Biddy_Managed_Copy to copy a graph from one manager to another manager.

Description

See Biddy_Managed_Copy.

Side effects

If source and target manager are the same then function does nothing. The variable ordering of created BDD is adapted to the target manager. The created formula is not preserved.

More info

Macro Biddy_CopyFormula(MNG2,x) is defined for use with anonymous manager.
 
Biddy_Boolean Biddy_Managed_Eval (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_Eval returns the value of a Boolean function for a given variable assignment.

Description

Side effects

More info

Macro Biddy_Eval(f) is defined for use with anonymous manager.
 
Biddy_Edge Biddy_Managed_Random (Biddy_Manager MNG, Biddy_Edge support, double r)
 Function Biddy_Managed_Random generates a random BDD. More...
 
Biddy_Edge Biddy_Managed_RandomSet (Biddy_Manager MNG, Biddy_Edge unit, double r)
 Function Biddy_Managed_RandomSet generates a random BDD. More...
 

Detailed Description

File biddyMain.c contains main functions for representation and manipulation of boolean functions with ROBDDs.

Description

PackageName [Biddy]
Synopsis    [Biddy provides data structures and algorithms for the
             representation and manipulation of Boolean functions with
             ROBDDs. A hash table is used for quick search of nodes.
             Complement edges decreases the number of nodes. An automatic
             garbage collection with a system age is implemented.
             Variable swapping and sifting are implemented.]

FileName    [biddyMain.c]
Revision    [$Revision: 253 $]
Date        [$Date: 2017-03-20 09:03:47 +0100 (pon, 20 mar 2017) $]
Authors     [Robert Meolic (robert.meolic@um.si),
             Ales Casar (ales@homemade.net)]

Copyright

Copyright (C) 2006, 2017 UM-FERI, Smetanova ulica 17, SI-2000 Maribor, Slovenia

Biddy is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

Biddy is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.

More info

See also: biddy.h, biddyInt.h

Definition in file biddyMain.c.

Function Documentation

void Biddy_InitMNG ( Biddy_Manager mng,
int  gddtype 
)

Function Biddy_InitMNG initialize a manager.

Description

Biddy_InitMNG creates and initializes a manager. Initialization consists of creating manager structure (MNG), node table (biddyNodeTable), variable table (biddyVariableTable), formula table (biddyFormulaTable), three basic caches (biddyOPCache, biddyEACache and biddyRCCache), and cache list (biddyCacheList). Biddy_InitMNG also initializes constant edges (biddyOne, biddyZero), memory management and automatic garbage collection.

Side effects

Allocates a lot of memory. Parameter gddtype is ignored.

More info

Macro Biddy_Init() will initialize anonymous manager.

Definition at line 210 of file biddyMain.c.

void Biddy_ExitMNG ( Biddy_Manager mng)

Function Biddy_ExitMNG deletes a manager.

Description

Deallocates all memory allocated by Biddy_InitMNG, Biddy_FoaVariable, Biddy_FoaNode etc.

Side effects

More info

Macro Biddy_Exit() will delete anonymous manager.

Definition at line 691 of file biddyMain.c.

Biddy_String Biddy_About ( )

Function Biddy_About reports version of Biddy package.

Description

Side effects

More info

Definition at line 886 of file biddyMain.c.

int Biddy_Managed_GetManagerType ( Biddy_Manager  MNG)

Function Biddy_Managed_GetManagerType reports BDD type used in the manager.

Description

Side effects

More info

Macro Biddy_GetManagerType() is defined for use with anonymous manager.

Definition at line 908 of file biddyMain.c.

void Biddy_Managed_SetManagerParameters ( Biddy_Manager  MNG,
float  gcr,
float  gcrF,
float  gcrX,
float  rr,
float  rrF,
float  rrX,
float  st,
float  fst,
float  cst,
float  fcst 
)

Function Biddy_Managed_SetManagerParameters set modifiable parameters.

Description

Function expect 6 float values. If the value is < 0 then the parameter is not modified. The parameters are: biddyNodeTable.gcratio (do not delete nodes if the effect is to small), biddyNodeTable.gcratioF (do not delete nodes if the effect is to small), biddyNodeTable.gcratioX (do not delete nodes if the effect is to small), biddyNodeTable.resizeratio (resize Node table if there are to many nodes), biddyNodeTable.resizeratioF (resize Node table if there are to many nodes), biddyNodeTable.resizeratioX (resize Node table if there are to many nodes), biddyNodeTable.siftingtreshold (stop sifting if the size of the system grows to much), biddyNodeTable.fsiftingtreshold (stop sifting if the size of the function grows to much), biddyNodeTable.convergesiftingtreshold (stop one step of converging sifting if the size of the system grows to much), biddyNodeTable.fconvergesiftingtreshold (stop one step of converging sifting if the size of the function grows to much).

Side effects

Initial values are given in Biddy_InitMNG.

More info

Macro Biddy_SetManagerParameters() is defined for use with anonymous manager.

Definition at line 951 of file biddyMain.c.

Biddy_Edge Biddy_GetThen ( Biddy_Edge  fun)

Function Biddy_GetThen returns THEN successor.

Description

Input mark is not transfered! External use, only.

Side effects

More info

Macro BiddyT(fun) is defined for internal use.

Definition at line 988 of file biddyMain.c.

Biddy_Edge Biddy_GetElse ( Biddy_Edge  fun)

Function Biddy_GetElse returns ELSE successor.

Description

Input mark is not transfered! External use, only.

Side effects

More info

Macro BiddyE(fun) is defined for internal use.

Definition at line 1024 of file biddyMain.c.

Biddy_Variable Biddy_GetTopVariable ( Biddy_Edge  fun)

Function Biddy_GetTopVariable returns the top variable.

Description

External use, only.

Side effects

More info

Macro BiddyV(fun) is defined for internal use.

Definition at line 1060 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Boolean Biddy_Managed_IsEqv ( Biddy_Manager  MNG1,
Biddy_Edge  f1,
Biddy_Manager  MNG2,
Biddy_Edge  f2 
)

Function Biddy_Managed_IsEqv returns TRUE iff two BDDs are equal.

Description

It is assumed that f1 and f2 have the same ordering.

Side effects

More info

Macro Biddy_IsEqv(f1,MNG2,f2) is defined for use with anonymous manager.

Definition at line 1084 of file biddyMain.c.

void Biddy_Managed_SelectNode ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_SelectNode selects the top node of the given function.

Description

Side effects

More info

Macro Biddy_SelectNode(f) is defined for use with anonymous manager.

Definition at line 1119 of file biddyMain.c.

Here is the caller graph for this function:

void Biddy_Managed_DeselectNode ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_DeselectNode deselects the top node of the given function.

Description

Side effects

More info

Macro Biddy_DeselectNode(f) is defined for use with anonymous manager.

Definition at line 1145 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Boolean Biddy_Managed_IsSelected ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_IsSelected returns TRUE iff the top node of the given function is selected.

Description

Side effects

More info

Macro Biddy_IsSelected(f) is defined for use with anonymous manager.

Definition at line 1171 of file biddyMain.c.

Here is the caller graph for this function:

void Biddy_Managed_SelectFunction ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_SelectFunction recursively selects all nodes of a given function.

Description

Side effects

Constant node must be selected before starting this function!

More info

Macro Biddy_SelectFunction(f) is defined for use with anonymous manager.

Definition at line 1198 of file biddyMain.c.

void Biddy_Managed_DeselectAll ( Biddy_Manager  MNG)

Function Biddy_Managed_DeselectAll deselects all nodes.

Description

Deselect all nodes.

Side effects

More info

Macro Biddy_DeselectAll() is defined for use with anonymous manager.

Definition at line 1255 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_GetTerminal ( Biddy_Manager  MNG)

Function Biddy_Managed_GetTerminal returns unmarked edge pointing to the constant node 1.

Description

Terminal node depends on a manager.

Side effects

More info

Internally, use macro biddyTerminal. Macro Biddy_GetTerminal() is defined for use with anonymous manager.

Definition at line 1289 of file biddyMain.c.

Biddy_Edge Biddy_Managed_GetConstantZero ( Biddy_Manager  MNG)

Function Biddy_Managed_GetConstantZero returns constant 0.

Description

Constants 0 and 1 depend on a manager. For combination sets, constant 0 coincides with empty set.

Side effects

More info

Internally, use macro biddyZero. Macro Biddy_GetConstantZero() is defined for use with anonymous manager. Macros Biddy_Managed_GetEmptySet(MNG) and Biddy_GetEmptySet() are defined for manipulation of combination sets.

Definition at line 1319 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_GetConstantOne ( Biddy_Manager  MNG)

Function Biddy_Managed_GetConstantOne returns constant 1.

Description

Constants 0 and 1 depend on a manager. For combination sets, constant 1 coincides with universal set.

Side effects

More info

Internally, use macro biddyOne. Macro Biddy_GetConstantOne() is defined for use with anonymous manager. Macros Biddy_Managed_GetUniversalSet(MNG) and Biddy_GetUniversalSet() are defined for manipulation of combination sets.

Definition at line 1349 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_GetBaseSet ( Biddy_Manager  MNG)

Function Biddy_Managed_GetBaseSet returns set containing only a null combination, i.e. it returns {{}}.

Description

Side effects

More info

Macro Biddy_GetBaseSet() is defined for use with anonymous manager.

Definition at line 1375 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Variable Biddy_Managed_GetVariable ( Biddy_Manager  MNG,
Biddy_String  x 
)

Function Biddy_Managed_GetVariable returns variable with the given name.

Description

Side effects

If variable is not found function returns 0!

More info

Macro Biddy_GetVariable(x) is defined for use with anonymous manager.

Definition at line 1410 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Variable Biddy_Managed_GetPrevVariable ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Function Biddy_Managed_GetPrevVariable returns previous variable in the global ordering (lower, topmore).

Description

Side effects

More info

Macro Biddy_GetPrevVariable(v) is defined for use with anonymous manager.

Definition at line 1455 of file biddyMain.c.

Biddy_Variable Biddy_Managed_GetNextVariable ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Function Biddy_Managed_GetNextVariable returns next variable in the global ordering (higher, bottommore).

Description

Side effects

More info

Macro Biddy_GetNextVariable(v) is defined for use with anonymous manager.

Definition at line 1485 of file biddyMain.c.

Biddy_Edge Biddy_Managed_GetVariableEdge ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Function Biddy_Managed_GetVariableEdge returns variable's edge.

Description

Side effects

More info

Macro Biddy_GetVariableEdge(v) is defined for use with anonymous manager.

Definition at line 1514 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_GetElementEdge ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Function Biddy_Managed_GetElementEdge returns element's edge.

Description

Side effects

More info

Macro Biddy_GetElementEdge(v) is defined for use with anonymous manager.

Definition at line 1539 of file biddyMain.c.

Biddy_String Biddy_Managed_GetVariableName ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Function Biddy_Managed_GetVariableName returns the name of a variable.

Description

Side effects

More info

Macro Biddy_GetVariableName(v) is defined for use with anonymous manager.

Definition at line 1563 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_GetTopVariableEdge ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_GetTopVariableEdge returns variable's edge of top variable.

Description

Side effects

TO DO: For ZBDDs, element edge is sometimes preffered over variable edge.

More info

Macro Biddy_GetTopVariableEdge(f) is defined for use with anonymous manager.

Definition at line 1591 of file biddyMain.c.

Biddy_String Biddy_Managed_GetTopVariableName ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_GetTopVariableName returns the name of top variable.

Description

Side effects

More info

Macro Biddy_GetTopVariableName(f) is defined for use with anonymous manager.

Definition at line 1619 of file biddyMain.c.

Here is the caller graph for this function:

char Biddy_Managed_GetTopVariableChar ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_GetTopVariableChar returns the first character in the name of top variable.

Description

Side effects

More info

Macro Biddy_GetTopVariableChar(f) is defined for use with anonymous manager.

Definition at line 1647 of file biddyMain.c.

void Biddy_Managed_ResetVariablesValue ( Biddy_Manager  MNG)

Function Biddy_Managed_ResetVariablesValue sets all variable's value to biddyZero.

Description

Side effects

Only active (used) variables are reinitialized.

More info

Macro Biddy_ResetVariablesValue() is defined for use with anonymous manager.

Definition at line 1676 of file biddyMain.c.

Here is the caller graph for this function:

void Biddy_Managed_SetVariableValue ( Biddy_Manager  MNG,
Biddy_Variable  v,
Biddy_Edge  f 
)

Function Biddy_Managed_SetVariableValue sets variable's value.

Description

Side effects

More info

Macro Biddy_SetVariableValue(v,f) is defined for use with anonymous manager.

Definition at line 1705 of file biddyMain.c.

Biddy_Boolean Biddy_Managed_IsSmaller ( Biddy_Manager  MNG,
Biddy_Variable  fv,
Biddy_Variable  gv 
)

Function Biddy_Managed_IsSmaller returns TRUE if the first variable is smaller (= lower = previous = above = topmore).

Description

Side effects

More info

Macro Biddy_IsSmaller(fv,gv) is defined for use with anonymous manager.

Definition at line 1731 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Variable Biddy_Managed_FoaVariable ( Biddy_Manager  MNG,
Biddy_String  x,
Biddy_Boolean  varelem 
)

Function Biddy_Managed_FoaVariable finds variable/element or adds new variable (i.e. Boolean function f = x) and new element (i.e. it creates set {{x}}).

Description

If variable/element already exists, function returns the existing one. If x == NULL then numbered variable/element is added. Numbered variables/elements have only digits in its name. The current number of numbered variables/elements is stored in numnum. If numbered variable/element is requested then function increments numnum and creates a new (non-existing) variable/element. Parameter varelem is used to determine how to adapt the existing BDD base to keep the current formula valid (use varelem = TRUE if formulae represent Boolean functions and varelem = FALSE if they represent combination sets). The ordering of the new variable/element is determined in Biddy_InitMNG. Function always returns variable.

Side effects

Adding new variable/element may change the meaning of the existing BDDs. Variables and elements are repaired. Moreover, formulae are repaired with regards to the parameter varelem. For OBDDs, it is safe to add new variables/elements if BDDs are used to represent Boolean functions. User should not add numbered variables/elements with some other function. TO DO: Formulae in user's formula tables are not repaired, yet!

More info

Macro Biddy_FoaVariable(x) is defined for use with anonymous manager.

Definition at line 1776 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_AddVariableByName ( Biddy_Manager  MNG,
Biddy_String  x 
)

Function Biddy_Managed_AddVariableByName adds variable.

Description

Biddy_Managed_AddVariableByName uses Biddy_Managed_FoaVariable to find or add variable. Function returns variable edge. If variable already exists, function returns the existing variable edge. For more details see Biddy_Managed_FoaVariable.

Side effects

See Biddy_Managed_FoaVariable.

More info

Macro Biddy_AddVariableByName(x) is defined for use with anonymous manager. Macros Biddy_Managed_AddVariable(MNG) and Biddy_AddVariable() are defined for creating numbered variables.

Definition at line 1892 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_AddElementByName ( Biddy_Manager  MNG,
Biddy_String  x 
)

Function Biddy_Managed_AddElementByName adds element.

Description

Biddy_Managed_AddElementByName uses Biddy_Managed_FoaVariable to find or add element. Function returns element edge. If element already exists, function returns the existing element edge. For more details see Biddy_Managed_FoaVariable.

Side effects

See Biddy_Managed_FoaVariable.

More info

Macro Biddy_AddElementByName(x) is defined for use with anonymous manager. Macros Biddy_Managed_AddElement(MNG) and Biddy_AddElement() are defined for creating numbered elements.

Definition at line 1927 of file biddyMain.c.

Biddy_Edge Biddy_Managed_AddVariableBelow ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Function Biddy_Managed_AddVariableBelow adds a numbered variable.

Description

Biddy_Managed_AddVariableBelow uses Biddy_Managed_AddVariableByName to add numbered variable. Then, the order of the new variable is changed to become immediately below the given variable (below = next = bottommore in BDD) Function returns variable edge.

Side effects

More info

Macro Biddy_AddVariableBelow(v) is defined for use with anonymous manager.

Definition at line 1959 of file biddyMain.c.

Biddy_Edge Biddy_Managed_AddVariableAbove ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Function Biddy_Managed_AddVariableAbove adds a numbered variable.

Description

Biddy_Managed_AddVariableAbove uses Biddy_Managed_AddVariableByName to add numbered variable. Then, the order of the new variable is changed to become immediately above the given variable (above = previous = topmore in BDD) Function returns variable edge.

Side effects

More info

Macro Biddy_AddVariableAbove(v) is defined for use with anonymous manager.

Definition at line 2026 of file biddyMain.c.

Biddy_Edge Biddy_Managed_TransferMark ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Boolean  mark,
Biddy_Boolean  leftright 
)

Function Biddy_Managed_TransferMark returns edge with inverted complement bit iff the second parameter is TRUE and normalization rules require this.

Description

It is better to use macro Biddy_InvCond. Parameter leftright is ignored.

Side effects

More info

Macro Biddy_TransferMark() is defined for use with anonymous manager.

Definition at line 2089 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_IncTag ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_IncTag returns edge with an incremented tag.

Description

This function is not used for OBDDs.

Side effects

More info

Macro Biddy_IncTag() is defined for use with anonymous manager.

Definition at line 2117 of file biddyMain.c.

Biddy_Edge Biddy_Managed_TaggedFoaNode ( Biddy_Manager  MNG,
Biddy_Variable  v,
Biddy_Edge  pf,
Biddy_Edge  pt,
Biddy_Variable  ptag,
Biddy_Boolean  garbageAllowed 
)

Function Biddy_Managed_TaggedFoaNode finds or adds new node with the given variable and successors.

Description

If such node already exists, function returns it and does not create the new one. If pf = pt = NULL then new variable is created. This function should not be called directly to add new variables, you must use Biddy_Managed_FoaVariable and Biddy_Managed_AddVariableByName.

Side effects

Parameter ptag is ignored. Using Biddy_Managed_FoaNode you can create node with arbitrary ordering. It is much more safe to use Biddy_Managed_ITE. To enable efficient implementation of sifting the function started with the returned node is not refreshed!

More info

Macro Biddy_Managed_FoaNode(MNG,v,pf,pt,garbageAllowed) is defined for use without tags. Macros Biddy_TaggedFoaNode(v,pf,pt,tag,garbageAllowed) and Biddy_FoaNode(v,pf,pt,garbageAllowed) are defined for use with anonymous manager.

Definition at line 2155 of file biddyMain.c.

Biddy_Edge Biddy_Managed_Not ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_Not calculates Boolean function NOT.

Description

It is better to use macro Biddy_Inv.

Side effects

More info

Macro Biddy_Not() is defined for use with anonymous manager.

Definition at line 2371 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_ITE ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g,
Biddy_Edge  h 
)

Function Biddy_Managed_ITE calculates ITE operation of three Boolean functions.

Description

Side Effects

More info

Macro Biddy_ITE(f,g,h) is defined for use with anonymous manager.

Definition at line 2405 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_And ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g 
)

Function Biddy_Managed_And calculates Boolean function AND (conjunction).

Description

For combination sets, this function coincides with Intersection.

Side Effects

Used by ITE.

More Info

Macro Biddy_And(f,g) is defined for use with anonymous manager. Macros Biddy_Managed_Intersect(MNG,f,g) and Biddy_Intersect(f,g) are defined for manipulation of combination sets.

Definition at line 2699 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_Or ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g 
)

Function Biddy_Managed_Or calculates Boolean function OR (disjunction).

Description

For combination sets, this function coincides with Union.

Side Effects

More Info

Macro Biddy_Or(f,g) is defined for use with anonymous manager. Macros Biddy_Managed_Union(MNG,f,g) and Biddy_Union(f,g) are defined for manipulation of combination sets.

Definition at line 2915 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_Nand ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g 
)

Function Biddy_Managed_Nand calculates Boolean function NAND (Sheffer).

Description

Side Effects

More Info

Macro Biddy_Nand(f,g) is defined for use with anonymous manager.

Definition at line 2970 of file biddyMain.c.

Biddy_Edge Biddy_Managed_Nor ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g 
)

Function Biddy_Managed_Nor calculates Boolean function NOR (Peirce).

Description

Side Effects

More Info

Macro Biddy_Nor(f,g) is defined for use with anonymous manager.

Definition at line 3018 of file biddyMain.c.

Biddy_Edge Biddy_Managed_Xor ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g 
)

Function Biddy_Managed_Xor calculates Boolean function XOR.

Description

Side Effects

Used by ITE.

More Info

Macro Biddy_Xor(f,g) is defined for use with anonymous manager.

Definition at line 3066 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_Xnor ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g 
)

Function Biddy_Managed_Xnor calculates Boolean function XNOR.

Description

Side Effects

More Info

Macro Biddy_Xnor(f,g) is defined for use with anonymous manager.

Definition at line 3292 of file biddyMain.c.

Biddy_Edge Biddy_Managed_Leq ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g 
)

Function Biddy_Managed_Leq calculates Boolean implication.

Description

Side Effects

More Info

Macro Biddy_Leq(f,g) is defined for use with anonymous manager.

Definition at line 3339 of file biddyMain.c.

Biddy_Edge Biddy_Managed_Gt ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g 
)

Function Biddy_Managed_Gt calculates the negation of Boolean implication.

Description

For combination sets, this function coincides with Diff.

Side Effects

More Info

Macro Biddy_Gt(f,g) is defined for use with anonymous manager. Macros Biddy_Managed_Diff(MNG,f,g) and Biddy_Diff(f,g) are defined for manipulation of combination sets.

Definition at line 3388 of file biddyMain.c.

Biddy_Boolean Biddy_Managed_IsLeq ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g 
)

Function Biddy_Managed_IsLeq returns TRUE iff function f is included in function g.

Description

Side Effects

Implemented by calculating full implication which is less efficient as implementation in CUDD.

More Info

Macro Biddy_IsLeq(f,g) is defined for use with anonymous manager.

Definition at line 3437 of file biddyMain.c.

Biddy_Edge Biddy_Managed_SubIntersect ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g 
)

Biddy_Managed_SubIntersect calculates a function included in the intersection of f and g.

Description

If the result is not constant 0 then it is a witness that the intersection is not empty. The result should be calculated with as few new nodes as possible, and the result may not be the same as conjunction between functions! If the only result of interest is whether f and g intersect, Biddy_IsLeq should be used (which returns TRUE iff f*g' == 0).

Side Effects

Implemented by calculating full conjunction which is less efficient as implementation in CUDD.

More Info

Macro Biddy_SubIntersect(f,g) is defined for use with anonymous manager.

Definition at line 3474 of file biddyMain.c.

Biddy_Edge Biddy_Managed_Restrict ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Variable  v,
Biddy_Boolean  value 
)

Function Biddy_Managed_Restrict calculates a restriction of Boolean function.

Description

Original BDD is not changed. This is not Coudert and Madre's restrict function (use Biddy_Simplify if you need that one).

Side effects

Recursive calls use optimization: F(a=x) == NOT((NOT F)(a=x)).

More info

Macro Biddy_Restrict(f,v,value) is defined for use with anonymous manager.

Definition at line 3508 of file biddyMain.c.

Biddy_Edge Biddy_Managed_Compose ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g,
Biddy_Variable  v 
)

Function Biddy_Managed_Compose calculates a composition of two Boolean functions.

Description

Original BDDs are not changed.

Side effects

It uses optimization: F(a=G) == NOT((NOT F)(a=G)).

More info

Macro Biddy_Compose(f,g,v) is defined for use with anonymous manager.

Definition at line 3599 of file biddyMain.c.

Biddy_Edge Biddy_Managed_E ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Variable  v 
)

Function Biddy_Managed_E calculates an existential quantification of Boolean function.

Description

Original BDD is not changed.

Side effects

Be careful: ExA F != NOT(ExA (NOT F)). Counterexample: Exb (AND (NOT a) b c).

More info

Macro Biddy_E(f,v) is defined for use with anonymous manager.

Definition at line 3692 of file biddyMain.c.

Biddy_Edge Biddy_Managed_A ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Variable  v 
)

Function Biddy_Managed_A calculates an universal quantification of Boolean function.

Description

Original BDD is not changed.

Side effects

Be careful: AxA F != NOT(AxA (NOT F)). Counterexample: Axb (AND (NOT a) b c).

More info

Macro Biddy_A(f,v) is defined for use with anonymous manager.

Definition at line 3785 of file biddyMain.c.

Biddy_Boolean Biddy_Managed_IsVariableDependent ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Variable  v 
)

Function Biddy_Managed_IsVariableDependent returns TRUE iff variable is dependent on others in a function.

Description

A variable is dependent on others in a function iff universal quantification of this variable returns constant FALSE.

Side effects

Implemented by calculating full universal quantification which is less efficient as direct implementation in CUDD.

More info

Macro Biddy_IsVariableDependent(f,v) is defined for use with anonymous manager.

Definition at line 3842 of file biddyMain.c.

Biddy_Edge Biddy_Managed_ExistAbstract ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  cube 
)

Function Biddy_Managed_ExistAbstract existentially abstracts all the variables in cube from f.

Description

Original BDD is not changed.

Side effects

More info

Macro Biddy_ExistAbstract(f,cube) is defined for use with anonymous manager.

Definition at line 3873 of file biddyMain.c.

Biddy_Edge Biddy_Managed_UnivAbstract ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  cube 
)

Function Biddy_Managed_UnivAbstract universally abstracts all the variables in cube from f.

Description

Original BDD is not changed.

Side effects

More info

Macro Biddy_UnivAbstract(f,cube) is defined for use with anonymous manager.

Definition at line 3978 of file biddyMain.c.

Biddy_Edge Biddy_Managed_AndAbstract ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  g,
Biddy_Edge  cube 
)

Function Biddy_Managed_AndAbstract calculates the AND of two BDDs and simultaneously (existentially) abstracts the variables in cube.

Description

Side effects

More info

Macro Biddy_AndAbstract(f,g,cube) is defined for use with anonymous manager.

Definition at line 4033 of file biddyMain.c.

Biddy_Edge Biddy_Managed_Constrain ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  c 
)

Function Biddy_Managed_Constrain calculates Coudert and Madre's constrain function.

Description

Coudert and Madre's constrain function is also called a generalized cofactor of function f with respect to function c.

Side effects

Cache table is not implemented, yet.

More info

Macro Biddy_Constrain(f,c) is defined for use with anonymous manager.

Definition at line 4192 of file biddyMain.c.

Biddy_Edge Biddy_Managed_Simplify ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Edge  c 
)

Function Biddy_Managed_Simplify calculates Coudert and Madre's restrict function.

Description

Coudert and Madre's restrict function tries to simplify function f by restricting it to the domain covered by function c. No checks are done to see if the result is actually smaller than the input.

Side effects

Cache table is not implemented, yet.

More info

Macro Biddy_Simplify(f,c) is defined for use with anonymous manager.

Definition at line 4285 of file biddyMain.c.

Biddy_Edge Biddy_Managed_Support ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_Support calculates a product of all dependent variables.

Description

Side effects

More info

Macro Biddy_Support(f) is defined for use with anonymous manager.

Definition at line 4378 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_Replace ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_Replace calculates BDD with one or more variables replaced.

Description

Original BDD is not changed. Replacing is controlled by variable's values (which are edges!). Use Biddy_Managed_ResetVariablesValue and Biddy_Managed_SetVariableValue to prepare replacing. Current and new variables should be disjoint sets.

Side effects

Cache table is not implemented, yet.

More info

Macro Biddy_Replace(f) is defined for use with anonymous manager.

Definition at line 4448 of file biddyMain.c.

Biddy_Edge Biddy_Managed_Change ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Variable  v 
)

Function Biddy_Managed_Change change the form of the given variable (positive literal becomes negative and vice versa).

Description

Side effects

More info

Macro Biddy_Change() is defined for use with anonymous manager.

Definition at line 4516 of file biddyMain.c.

Biddy_Edge Biddy_Managed_Subset ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Variable  v,
Biddy_Boolean  value 
)

Function Biddy_Managed_Subset calculates a division of Boolean function with a literal.

Description

Original BDD is not changed. For combination sets, this function coincides with Subset0 and Subset1.

Side effects

More info

Macro Biddy_Subset(f,v,value) is defined for use with anonymous manager. Macros Biddy_Managed_Subset0(MNG,f,v), Biddy_Subset0(f,v), Biddy_Managed_Subset1(MNG,f,v), and Biddy_Subset1(f,v) are defined for manipulation of combination sets.

Definition at line 4585 of file biddyMain.c.

Biddy_Boolean Biddy_Managed_IsOK ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_IsOK returns TRUE iff given node is not obsolete.

Description

This is needed for implementation of user caches.

Side effects

More info

Macro BiddyIsOK(f) is defined for debugging. It will check more properties and not only the expiry value. Macro Biddy_IsOK(f) is defined for use with anonymous manager.

Definition at line 4691 of file biddyMain.c.

void Biddy_Managed_GC ( Biddy_Manager  MNG,
Biddy_Variable  target,
Biddy_Boolean  purge,
Biddy_Boolean  total 
)

Function Biddy_Managed_GC performs garbage collection.

Description

All obsolete nodes are deleted. Parameter target is used during sifting. If parameter total is true than all obsolete nodes are deleted, otherwise nodes are deleted only if there are enough obsolete nodes. Nodes from deleted non-obsolete formulae are immediately removed only if parameter purge is true (this should not be used during the automatic garbage collection), otherwise these nodes only become fresh.

Side effects

The first element of each chain in a node table should have a special value for its 'prev' element to allow tricky but efficient deleting. Moreover, 'prev' and 'next' should be the first and the second element in the structure BiddyNode, respectively. Garbage collecion is reported by biddyNodeTable.garbage only if some bad nodes are purged!

More info

Macro Biddy_GC(target,purge,total) is defined for use with anonymous manager. Macros Biddy_Managed_AutoGC(MNG) and Biddy_AutoGC() are useful variants with target = 0, purge = FALSE, and total = FALSE.

Definition at line 4731 of file biddyMain.c.

Here is the caller graph for this function:

void Biddy_Managed_Clean ( Biddy_Manager  MNG)

Function Biddy_Managed_Clean performs cleaning.

Description

Discard all nodes which are not preserved or which are not preserved anymore. Obsolete nodes are not immediately removed, they will be removed during the first garbage collection.

Side effects

Tag deleted is not considered and thus no fortified node and no prolonged node is discarded. Constants and variables should be fortified! Restoring elements is not implemented, yet.

More info

Macro Biddy_Clean() is defined for use with anonymous manager.

Definition at line 5074 of file biddyMain.c.

Here is the caller graph for this function:

void Biddy_Managed_Purge ( Biddy_Manager  MNG)

Function Biddy_Managed_Purge immediately removes all nodes which were not preserved or which are not preserved anymore.

Description

All fresh and obsolete nodes are immediatelly removed. Moreover, nodes from deleted prolonged formulae and nodes from deleted fortified formulae are removed if they are not needed by other formulae. Call to Biddy_Purge does not count as clearing and thus all preserved formulae remains preserved for the same number of clearings.

Side effects

Removes all fresh nodes!

More info

Macro Biddy_Purge(f) is defined for use with anonymous manager.

Definition at line 5108 of file biddyMain.c.

Here is the caller graph for this function:

void Biddy_Managed_PurgeAndReorder ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Boolean  converge 
)

Function Biddy_Managed_PurgeAndReorder immediately removes non-preserved nodes and triggers reordering on function.

Description

All obsolete nodes are immediatelly removed. Moreover, nodes from deleted prolonged formulae and nodes from deleted fortified formulae are removed if they are not needed by other formulae. If BDD is given (f != NULL), reordering on function is used. Otherwise (f == NULL) global reordering is used. Call to Biddy_PurgeAndReorder does not count as clearing and thus all preserved formulae remains preserved for the same number of clearings.

Side effects

Removes all fresh nodes.

More info

Macro Biddy_PurgeAndReorder(f) is defined for use with anonymous manager.

Definition at line 5144 of file biddyMain.c.

void Biddy_Managed_Refresh ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Function Biddy_Managed_Refresh refreshes top node in a given function.

Description

This is an external variant of internal macro BiddyRefresh This is needed for implementing user caches.

Side effects

More info

Macro Biddy_Refresh(f) is defined for use with anonymous manager.

Definition at line 5173 of file biddyMain.c.

void Biddy_Managed_AddCache ( Biddy_Manager  MNG,
Biddy_GCFunction  gc 
)

Function Biddy_Managed_AddCache adds cache to the end of Cache list.

Description

If Cache list does not exist, function creates it.

Side effects

More info

Macro Biddy_AddCache(gc) is defined for use with anonymous manager.

Definition at line 5199 of file biddyMain.c.

Here is the caller graph for this function:

unsigned int Biddy_Managed_AddFormula ( Biddy_Manager  MNG,
Biddy_String  x,
Biddy_Edge  f,
int  c 
)

Function Biddy_Managed_AddFormula adds formula to Formula table.

Description

Nodes of the given BDD will be preserved for the given number of clearings. If (x != NULL) then formula is accessible by its name. If (c == -1) then formula is not preserved. If (c == 0) then formula is persistently preserved and you have to use Biddy_DeleteFormula to remove its nodes. There are two macros defined to simplify formulae management. Macro Biddy_Managed_AddTmpFormula(mng,bdd,c) is defined as Biddy_Managed_AddFormula(mng,NULL,bdd,c) and macro Biddy_Managed_AddPersistentFormula(mng,name,bdd) is defined as Biddy_Managed_AddFormula(mng,name,bdd,0).

Side effects

Function is prolonged or fortified. Formulae with name are ordered by name. If formula with the same name already exists, it will be overwritten (preserved and persistently preserved formulae, too)!

More info

Macros Biddy_AddFormula(x,f), Biddy_AddTmpFormula(f,c), and Biddy_AddPersistentFormula(x,f) are defined for use with anonymous manager.

Definition at line 5260 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Boolean Biddy_Managed_FindFormula ( Biddy_Manager  MNG,
Biddy_String  x,
Biddy_Edge f 
)

Function Biddy_Managed_FindFormula find formula in Formula table.

Description

Side effects

More info

Macro Biddy_FindFormula(x,f) is defined for use with anonymous manager.

Definition at line 5453 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Boolean Biddy_Managed_DeleteFormula ( Biddy_Manager  MNG,
Biddy_String  x 
)

Function Biddy_Managed_DeleteFormula delete formula from Formula table.

Description

Formula is labelled but not immediately removed. Nodes of the given formula are not immediately removed.

Side effects

Formula is not accessible by its name anymore. Formulae representing constants and variables will not be deleted.

More info

Macro Biddy_DeleteFormula(x) is defined for use with anonymous manager.

Definition at line 5554 of file biddyMain.c.

Biddy_Boolean Biddy_Managed_DeleteIthFormula ( Biddy_Manager  MNG,
unsigned int  i 
)

Function Biddy_Managed_DeleteIthFormula deletes formula from the table.

Description

Formula is labelled but not immediately removed. Nodes of the given formula are not immediately removed.

Side effects

Formula is not accessible by its name anymore. The first two formulae ("0" and "1") will not be deleted. Formulae representing variables will not be deleted.

More info

Macro Biddy_DeleteIthFormula(x) is defined for use with anonymous manager.

Definition at line 5617 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_GetIthFormula ( Biddy_Manager  MNG,
unsigned int  i 
)

Function Biddy_Managed_GetIthFormula returns ith formula in a Formula table.

Description

Return biddyNull if ith formulae does not exist.

Side effects

After addding new formula the index of others may change!

More info

Macro Biddy_GetIthFormula(i) is defined for use with anonymous manager.

Definition at line 5677 of file biddyMain.c.

Biddy_String Biddy_Managed_GetIthFormulaName ( Biddy_Manager  MNG,
unsigned int  i 
)

Function Biddy_Managed_GetIthFormulaName returns name of the ith formula in a Formula table.

Description

Return NULL if ith formulae does not exist.

Side effects

After addding new formula the index of others may change!

More info

Macro Biddy_GetIthFormulaName(i) is defined for use with anonymous manager.

Definition at line 5708 of file biddyMain.c.

Biddy_Variable Biddy_Managed_SwapWithHigher ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Function Biddy_Managed_SwapWithHigher swaps two adjacent variables.

Description

Higher (greater) variable is the bottommore one! The highest element is constant "1". Constant '1' has global ordering numUsedVariables (not smaller than anyone). Global ordering is the number of zeros in corresponding line of orderingTable.

Side effects

All obsolete nodes will be removed.

More info

Macro Biddy_SwapWithHigher(v) is defined for use with anonymous manager.

Definition at line 5749 of file biddyMain.c.

Biddy_Variable Biddy_Managed_SwapWithLower ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Function Biddy_Managed_SwapWithLower swaps two adjacent variables.

Description

Lower (smaller) variable is the topmore one! The lowest (topmost) element is not fixed. Topmost variable has global ordering 1 (smaller than all except itself). Global ordering is the number of zeros in corresponding line of orderingTable.

Side effects

All obsolete nodes will be removed.

More info

Macro Biddy_SwapWithLower(v) is defined for use with anonymous manager.

Definition at line 5787 of file biddyMain.c.

Biddy_Boolean Biddy_Managed_Sifting ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Boolean  converge 
)

Function Biddy_Managed_Sifting reorders variables to minimize node number for the whole system (if f = NULL) or for the given function (if f != NULL) using Rudell's sifting algorithm.

Description

Variables are reordered globally. All obsolete nodes will be removed.

Side effects

More info

Macro Biddy_Sifting(f) is defined for use with anonymous manager.

Definition at line 5824 of file biddyMain.c.

Here is the caller graph for this function:

Biddy_Edge Biddy_Managed_Random ( Biddy_Manager  MNG,
Biddy_Edge  support,
double  r 
)

Function Biddy_Managed_Random generates a random BDD.

Description

The represented Boolean function depends on the variables given with parameter support whilst the parameter r determines the ratio between the number of function's minterms and the number of all possible minterms. Parameter support is a product of positive varaiables.

Side effects

Parameter r must be a number from [0,1]. Otherwise, function returns biddyNull.

More info

Macro Biddy_Random(support,r) is defined for use with anonymous manager.

Definition at line 6918 of file biddyMain.c.

Biddy_Edge Biddy_Managed_RandomSet ( Biddy_Manager  MNG,
Biddy_Edge  unit,
double  r 
)

Function Biddy_Managed_RandomSet generates a random BDD.

Description

The represented set is a random combination set determined by the parameter unit whilst the parameter r determines the ratio between the number of set's subsets and the number of all possible subsets. Parameter set is a set containing only one subset which consist of all elements, i.e. it is a set {{x1,x2,...,xn}}.

Side effects

Parameter r must be a number from [0,1]. Otherwise, function returns biddyNull.

More info

Macro Biddy_RandomSet(unit,r) is defined for use with anonymous manager.

Definition at line 7030 of file biddyMain.c.