Biddy  1.8.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 various types of Binary Decision Diagrams. More...

#include "biddyInt.h"
Include dependency graph for biddyMain.c:

Go to the source code of this file.

Macros

#define TINY_SIZE   1023
 
#define SMALL_SIZE   65535
 
#define MEDIUM_SIZE   262143
 
#define LARGE_SIZE   1048575
 
#define XLARGE_SIZE   2097151
 
#define XXLARGE_SIZE   4194303
 
#define XXXLARGE_SIZE   8388607
 
#define HUGE_SIZE   16777215
 
#define SYSTEMREPORTVERBOSE
 
#define SYSTEMREPORTDETAILS
 
#define FUNCTIONREPORTVERBOSE
 
#define FUNCTIONREPORTDETAILS
 

Functions

void Biddy_InitMNG (Biddy_Manager *mng, int bddtype)
 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...
 
Biddy_String Biddy_Managed_GetManagerName (Biddy_Manager MNG)
 Function Biddy_Managed_GetManagerName reports the name of the 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 cst)
 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 and untagged edge pointing to terminal 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_GetLowestVariable (Biddy_Manager MNG)
 Function Biddy_Managed_GetLowestVariable returns the lowest variable in the current ordering. More...
 
Biddy_Variable Biddy_Managed_GetIthVariable (Biddy_Manager MNG, Biddy_Variable i)
 Function Biddy_Managed_GetIthVariable returns ith variable in the current global ordering. 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_Edge Biddy_Managed_GetVariableValue (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetVariableValue gets variable's value. More...
 
void Biddy_Managed_ClearVariablesData (Biddy_Manager MNG)
 Function Biddy_Managed_ClearVariablesData free memory used for all variable's data. More...
 
void Biddy_Managed_SetVariableData (Biddy_Manager MNG, Biddy_Variable v, void *x)
 Function Biddy_Managed_SetVariableData sets variable's data. More...
 
void * Biddy_Managed_GetVariableData (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetVariableData gets variable's data. More...
 
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

Variables must have values assigned. Variable is considered to be FALSE iff variable.value == biddyZero, whilst it is considered to be TRUE, otherwise.

More info

Macro Biddy_Eval(f) is defined for use with anonymous manager.
 
double Biddy_Managed_EvalProbability (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_EvalProbability evaluates BDD. 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_Boolean Biddy_Managed_IsLowest (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_IsLowest returns TRUE if the variable is the lowest one (lowest == topmost). More...
 
Biddy_Boolean Biddy_Managed_IsHighest (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_IsHighest returns TRUE if the variable is the highest one if terminal node is ignored (highest == bottommost). 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...
 
void Biddy_Managed_ChangeVariableName (Biddy_Manager MNG, Biddy_Variable v, Biddy_String x)
 Function Biddy_Managed_ChangeVariableName set new name to the given variable/element. More...
 
Biddy_Variable Biddy_Managed_AddVariableByName (Biddy_Manager MNG, Biddy_String x)
 Function Biddy_Managed_AddVariableByName adds variable. More...
 
Biddy_Variable 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 variable. More...
 
Biddy_Edge Biddy_Managed_AddVariableAbove (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_AddVariableAbove adds 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_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 targetLT, Biddy_Variable targetGEQ, 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, unsigned int *idx, 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...
 
void Biddy_Managed_SetAlphabeticOrdering (Biddy_Manager MNG)
 Function Biddy_Managed_SetAlphabeticOrdering use variable swapping to create an alphabetic ordering. 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...
 
void Biddy_Managed_MinimizeBDD (Biddy_Manager MNG, Biddy_String name)
 Function Biddy_Managed_MinimizeBDD reorders variables to minimize the node number of the given formula using an exhaustive search over all possible orderings. More...
 
void Biddy_Managed_MaximizeBDD (Biddy_Manager MNG, Biddy_String name)
 Function Biddy_Managed_MaximizeBDD reorders variables to maximize the node number of the given function using an exhaustive search over all possible orderings. 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 which can use the same or different BDD type.

Description

The function takes a graph from one manager and creates the same graph in another manager. If the managers do not use the same BDD type then a graph is converted. The resulting graph will represent the same Boolean function assuming the domain from the target manager. If (f == biddyZero) then only the complete domain (all variables) is copied.

Side effects

If source and target manager are the same then function does nothing. The variable ordering of the created BDD is trying to follow the original ordering, but if some variables already exist in the target manager then the final ordering is adapted to the target manager. Please note, that indices of variables in the target manager may not be the same as in the source manager (for example, if source managet does not use initial ordering the indices in the target manager will follow the variable's ordering and not variable's original indices)

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 which can use the same or different BDD type.

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 refreshed but not preserved.

More info

Macro Biddy_CopyFormula(MNG2,x) is defined for use with anonymous manager.
 
Biddy_Edge Biddy_Managed_ConstructBDD (Biddy_Manager MNG, int numV, Biddy_String varlist, int numN, Biddy_String nodelist)
 

Variables

Biddy_Manager biddyAnonymousManager = NULL
 
BiddyLocalInfo * biddyLocalInfo = NULL
 

Detailed Description

Description

PackageName [Biddy]
Synopsis    [Biddy provides data structures and algorithms for the
             representation and manipulation of Boolean functions with
             ROBDDs, 0-sup-BDDs, and TZBDDs. 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: 458 $]
Date        [$Date: 2018-07-18 13:53:04 +0200 (sre, 18 jul 2018) $]
Authors     [Robert Meolic (robert.meolic@um.si)]

Copyright

Copyright (C) 2006, 2018 UM FERI, Koroska cesta 46, 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

◆ Biddy_About()

Biddy_String Biddy_About ( )

Description

Side effects

More info

Definition at line 1106 of file biddyMain.c.

◆ Biddy_ExitMNG()

void Biddy_ExitMNG ( Biddy_Manager mng)

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 883 of file biddyMain.c.

◆ Biddy_GetElse()

Biddy_Edge Biddy_GetElse ( Biddy_Edge  fun)

Description

Input mark is not transfered! External use, only.

Side effects

For terminal nodes, function returns the same node.

More info

Macro BiddyE(fun) is defined for internal use.

Definition at line 1282 of file biddyMain.c.

◆ Biddy_GetThen()

Biddy_Edge Biddy_GetThen ( Biddy_Edge  fun)

Description

Input mark is not transfered! External use, only.

Side effects

For terminal nodes, function returns the same node.

More info

Macro BiddyT(fun) is defined for internal use.

Definition at line 1243 of file biddyMain.c.

◆ Biddy_GetTopVariable()

Biddy_Variable Biddy_GetTopVariable ( Biddy_Edge  fun)

Description

External use, only.

Side effects

More info

Macro BiddyV(fun) is defined for internal use.

Definition at line 1320 of file biddyMain.c.

◆ Biddy_InitMNG()

void Biddy_InitMNG ( Biddy_Manager mng,
int  bddtype 
)

Description

Biddy_InitMNG creates and initializes a manager. Initialization consists of creating manager structure (MNG), node table (biddyNodeTable), variable table (biddyVariableTable), formula table (biddyFormulaTable), four basic caches (biddyOPCache, biddyEACache, biddyRCCache, and biddyReplaceCache), 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.

More info

Macro Biddy_InitAnonymous() will initialize anonymous manager. Macro Biddy_Init() will initialize anonymous manager for ROBDDs.

Definition at line 177 of file biddyMain.c.

◆ Biddy_Managed_AddCache()

void Biddy_Managed_AddCache ( Biddy_Manager  MNG,
Biddy_GCFunction  gc 
)

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 4406 of file biddyMain.c.

◆ Biddy_Managed_AddElementByName()

Biddy_Variable Biddy_Managed_AddElementByName ( Biddy_Manager  MNG,
Biddy_String  x 
)

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 2903 of file biddyMain.c.

◆ Biddy_Managed_AddFormula()

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

Description

Given BDD becomes a formula. If (x != NULL) then formula is accessible by its name. If (x != NULL) then index of the formula in the Formulae Table is returned, otherwise function returns 0. Nodes of the given BDD will be preserved for the given number of clearings. If (c == -1) then formula is refreshed but not preserved. If (c == 0) then formula is persistently preserved. You have to use Biddy_DeleteFormula and Biddy_Purge to remove nodes of persistently preserved formulae. There are five macros defined to simplify formulae management: Biddy_Managed_AddTmpFormula(mng,name,bdd) := Biddy_Managed_AddFormula(mng,name,bdd,-1) Biddy_Managed_AddPersistentFormula(mng,name,bdd) := Biddy_Managed_AddFormula(mng,name,bdd,0) Biddy_Managed_KeepFormula(mng,bdd) := Biddy_Managed_AddFormula(mng,NULL,bdd,1) Biddy_Managed_KeepFormulaProlonged(mng,bdd,c) := Biddy_Managed_AddFormula(mng,NULL,bdd,c) Biddy_Managed_KeepFormulaUntilPurge(mng,bdd) := Biddy_Managed_AddFormula(mng,NULL,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 (i.e. not obsolete and not fresh) and persistently preserved formulae will be deleted at the original index and recreated at new index!

More info

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

Definition at line 4480 of file biddyMain.c.

◆ Biddy_Managed_AddVariableAbove()

Biddy_Edge Biddy_Managed_AddVariableAbove ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Biddy_Managed_AddVariableAbove uses Biddy_Managed_AddVariableByName to add new 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 3015 of file biddyMain.c.

◆ Biddy_Managed_AddVariableBelow()

Biddy_Edge Biddy_Managed_AddVariableBelow ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Biddy_Managed_AddVariableBelow uses Biddy_Managed_AddVariableByName to add new 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 2932 of file biddyMain.c.

◆ Biddy_Managed_AddVariableByName()

Biddy_Variable Biddy_Managed_AddVariableByName ( Biddy_Manager  MNG,
Biddy_String  x 
)

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 2871 of file biddyMain.c.

◆ Biddy_Managed_ChangeVariableName()

void Biddy_Managed_ChangeVariableName ( Biddy_Manager  MNG,
Biddy_Variable  v,
Biddy_String  x 
)

Description

Side effects

It is not checked that the same variable/element does not already exist. The ordering of the variable is not changed.

More info

Macro Biddy_ChangeVariableName(v,x) is defined for use with anonymous manager.

Definition at line 2835 of file biddyMain.c.

◆ Biddy_Managed_Clean()

void Biddy_Managed_Clean ( Biddy_Manager  MNG)

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

Field deleted is not considered and thus no fortified node and no prolonged node is discarded.

More info

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

Definition at line 4252 of file biddyMain.c.

◆ Biddy_Managed_ClearVariablesData()

void Biddy_Managed_ClearVariablesData ( Biddy_Manager  MNG)

Description

Side effects

Only active (used) variables are considered.

More info

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

Definition at line 2147 of file biddyMain.c.

◆ Biddy_Managed_ConstructBDD()

Biddy_Edge Biddy_Managed_ConstructBDD ( Biddy_Manager  MNG,
int  numV,
Biddy_String  varlist,
int  numN,
Biddy_String  nodelist 
)

Function**************************************************************** Synopsis [Function Biddy_Managed_ConstructBDD.] Description [Biddy_Managed_ConstructBDD constructs BDD from lists of nodes and edges. In both lists, elements are separated with spaces. Elements of node list has the following format: terminal node zero = (type=0,l=-1,r=-1), terminal node one = (type=1,l=-1,r=-1), regular label = (type=2,r=-1), complemented label = (type=3,r=-1), regular node = (type=4), node with complemented successor(s) = (type=5) The first element in nodelist is ignored. An example node list is: 'Biddy 0 Biddy 2 1 -1 1 B 4 2 3 2 0 0 -1 -1 3 i 4 4 9 4 d 4 5 6 5 0 0 -1 -1 6 y 4 7 8 7 0 0 -1 -1 8 1 1 -1 -1 9 d 4 6 10 10 1 1 -1 -1' which is constructed as: '{Biddy} {0 Biddy 2 1 -1} {1 B 4 2 3} {2 0 0 -1 -1} {3 i 4 4 9} {4 d 4 5 6} {5 0 0 -1 -1} {6 y 4 7 8} {7 0 0 -1 -1} {8 1 1 -1 -1} {9 d 4 6 10} {10 1 1 -1 -1}'. ] SideEffects [If variable ordering in the file is not compatible with the active ordering then the result will be wrong.] SeeAlso []

Definition at line 6044 of file biddyMain.c.

◆ Biddy_Managed_DeleteFormula()

Biddy_Boolean Biddy_Managed_DeleteFormula ( Biddy_Manager  MNG,
Biddy_String  x 
)

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 4933 of file biddyMain.c.

◆ Biddy_Managed_DeleteIthFormula()

Biddy_Boolean Biddy_Managed_DeleteIthFormula ( Biddy_Manager  MNG,
unsigned int  i 
)

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 4997 of file biddyMain.c.

◆ Biddy_Managed_DeselectAll()

void Biddy_Managed_DeselectAll ( Biddy_Manager  MNG)

Description

Deselect all nodes.

Side effects

More info

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

Definition at line 1515 of file biddyMain.c.

◆ Biddy_Managed_DeselectNode()

void Biddy_Managed_DeselectNode ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

More info

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

Definition at line 1405 of file biddyMain.c.

◆ Biddy_Managed_EvalProbability()

double Biddy_Managed_EvalProbability ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Each variable should be associated with a probability q (0-1) via data element in BiddyVariable. For each 1-path a product of variable's probability is calculated (q for 'then' successor and (1-q) for 'else' successor). The result of the function is the sum of all such products.

Side effects

Implemented for OBDD, ZBDD, and TZBDD.

More info

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

Definition at line 2366 of file biddyMain.c.

◆ Biddy_Managed_FindFormula()

Biddy_Boolean Biddy_Managed_FindFormula ( Biddy_Manager  MNG,
Biddy_String  x,
unsigned int *  idx,
Biddy_Edge f 
)

Description

Return TRUE/FALSE, index, and the formula. If formula is constant or variable then idx = 0 and f != biddyNull. If formula is not found then idx is a position where the formulae should exist and f == biddyNull.

Side effects

More info

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

Definition at line 4759 of file biddyMain.c.

◆ Biddy_Managed_FoaVariable()

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

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 always repaired. Formulae are repaired with regards to the parameter varelem. BDDs without external references are not repaired. For OBDDs, OFDDs, TZBDDS, and TZFDDs, it is safe to add new variables/elements if BDDs are used to represent Boolean functions. For ZBDDs and ZFDDs, it is safe to add new variables/elements if BDDs are used to represent combination sets. User should not add numbered variables/elements with some other function. TO DO: Formulae in user's formula tables are not repaired, yet! TO DO: Variables cannot be deleted, yet!

More info

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

Definition at line 2551 of file biddyMain.c.

◆ Biddy_Managed_GC()

void Biddy_Managed_GC ( Biddy_Manager  MNG,
Biddy_Variable  targetLT,
Biddy_Variable  targetGEQ,
Biddy_Boolean  purge,
Biddy_Boolean  total 
)

Description

All obsolete nodes are deleted. Iff parameter purge is true then all formulae without name are deleted. Iff parameter purge is true then all nodes which are not part of non-obsolete non-deleted formulae are removed even if they are fresh or fortified (this should not be used during automatic garbage collection!). If parameter total is true than all unnecessary nodes are immediately deleted, otherwise they are deleted only when there are enough of them. If (targetLT != 0) then node table resizing is disabled. If (targetLT != 0) then there should not exist obsolete formulae. If (targetLT != 0) then there should not exist obsolete nodes which are not part of any non-obsolete non-deleted formulae. If (targetLT != 0) then there should not exist obsolete nodes with variable equal or higher (bottom-more) than target and smaller (top-more) than targetGEQ.

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! Parameters targetLT and targetGEQ are used during sifting, only, in all other cases 0 is used.

More info

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

Definition at line 3762 of file biddyMain.c.

◆ Biddy_Managed_GetBaseSet()

Biddy_Edge Biddy_Managed_GetBaseSet ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 1647 of file biddyMain.c.

◆ Biddy_Managed_GetConstantOne()

Biddy_Edge Biddy_Managed_GetConstantOne ( Biddy_Manager  MNG)

Description

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

Side effects

For ZBDDs and ZFDDs, you should always obtain constant 1 through the call of this function!

More info

Internally, use macro biddyOne (also for ZBDDs and ZFDDs!). 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 1621 of file biddyMain.c.

◆ Biddy_Managed_GetConstantZero()

Biddy_Edge Biddy_Managed_GetConstantZero ( Biddy_Manager  MNG)

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 1589 of file biddyMain.c.

◆ Biddy_Managed_GetElementEdge()

Biddy_Edge Biddy_Managed_GetElementEdge ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

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

Definition at line 1926 of file biddyMain.c.

◆ Biddy_Managed_GetIthFormula()

Biddy_Edge Biddy_Managed_GetIthFormula ( Biddy_Manager  MNG,
unsigned int  i 
)

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 5057 of file biddyMain.c.

◆ Biddy_Managed_GetIthFormulaName()

Biddy_String Biddy_Managed_GetIthFormulaName ( Biddy_Manager  MNG,
unsigned int  i 
)

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 5088 of file biddyMain.c.

◆ Biddy_Managed_GetIthVariable()

Biddy_Variable Biddy_Managed_GetIthVariable ( Biddy_Manager  MNG,
Biddy_Variable  i 
)

Description

The lowest (topmost) variable has global ordering 1. The highest (bottommost) variable is '1' and has global ordering equal to numUsedVariables.

Side effects

If argument is 0, function returns 0. If argument is larger than the number of variables, function returns 0.

More info

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

Definition at line 1804 of file biddyMain.c.

◆ Biddy_Managed_GetLowestVariable()

Biddy_Variable Biddy_Managed_GetLowestVariable ( Biddy_Manager  MNG)

Description

The lowest variable is the tompost variable.

Side effects

More info

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

Definition at line 1766 of file biddyMain.c.

◆ Biddy_Managed_GetManagerName()

Biddy_String Biddy_Managed_GetManagerName ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 1155 of file biddyMain.c.

◆ Biddy_Managed_GetManagerType()

int Biddy_Managed_GetManagerType ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 1129 of file biddyMain.c.

◆ Biddy_Managed_GetNextVariable()

Biddy_Variable Biddy_Managed_GetNextVariable ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

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

Definition at line 1872 of file biddyMain.c.

◆ Biddy_Managed_GetPrevVariable()

Biddy_Variable Biddy_Managed_GetPrevVariable ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

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

Definition at line 1842 of file biddyMain.c.

◆ Biddy_Managed_GetTerminal()

Biddy_Edge Biddy_Managed_GetTerminal ( Biddy_Manager  MNG)

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 1559 of file biddyMain.c.

◆ Biddy_Managed_GetTopVariableChar()

char Biddy_Managed_GetTopVariableChar ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

More info

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

Definition at line 2035 of file biddyMain.c.

◆ Biddy_Managed_GetTopVariableEdge()

Biddy_Edge Biddy_Managed_GetTopVariableEdge ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

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 1979 of file biddyMain.c.

◆ Biddy_Managed_GetTopVariableName()

Biddy_String Biddy_Managed_GetTopVariableName ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

More info

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

Definition at line 2007 of file biddyMain.c.

◆ Biddy_Managed_GetVariable()

Biddy_Variable Biddy_Managed_GetVariable ( Biddy_Manager  MNG,
Biddy_String  x 
)

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 1712 of file biddyMain.c.

◆ Biddy_Managed_GetVariableData()

void* Biddy_Managed_GetVariableData ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

It is not checked that the given variable is valid.

More info

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

Definition at line 2206 of file biddyMain.c.

◆ Biddy_Managed_GetVariableEdge()

Biddy_Edge Biddy_Managed_GetVariableEdge ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

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

Definition at line 1901 of file biddyMain.c.

◆ Biddy_Managed_GetVariableName()

Biddy_String Biddy_Managed_GetVariableName ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

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

Definition at line 1951 of file biddyMain.c.

◆ Biddy_Managed_GetVariableValue()

Biddy_Edge Biddy_Managed_GetVariableValue ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

It is not checked that the given variable is valid.

More info

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

Definition at line 2120 of file biddyMain.c.

◆ Biddy_Managed_IncTag()

Biddy_Edge Biddy_Managed_IncTag ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Used for TZBDDs and TZFDDs, only.

Side effects

It is not checked, that the resulting tag is not greater than top variable. Function may return non-fresh node even if f is fresh.

More info

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

Definition at line 3162 of file biddyMain.c.

◆ Biddy_Managed_IsEqv()

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

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 1344 of file biddyMain.c.

◆ Biddy_Managed_IsHighest()

Biddy_Boolean Biddy_Managed_IsHighest ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

Macro BiddyIsHighest(v) is defined for internal use. Macro Biddy_IsHighest(v) is defined for use with anonymous manager.

Definition at line 2493 of file biddyMain.c.

◆ Biddy_Managed_IsLowest()

Biddy_Boolean Biddy_Managed_IsLowest ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

Macro BiddyIsLowest(v) is defined for internal use. Macro Biddy_IsLowest(v) is defined for use with anonymous manager.

Definition at line 2456 of file biddyMain.c.

◆ Biddy_Managed_IsOK()

Biddy_Boolean Biddy_Managed_IsOK ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

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 3711 of file biddyMain.c.

◆ Biddy_Managed_IsSelected()

Biddy_Boolean Biddy_Managed_IsSelected ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

More info

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

Definition at line 1431 of file biddyMain.c.

◆ Biddy_Managed_IsSmaller()

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

Description

Side effects

More info

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

Definition at line 2429 of file biddyMain.c.

◆ Biddy_Managed_MaximizeBDD()

void Biddy_Managed_MaximizeBDD ( Biddy_Manager  MNG,
Biddy_String  name 
)

Description

Steinhaus–Johnson–Trotter algorithm is used to generate all possible permutations. An optimized version of Bubble Sort is used to setup the final ordering. Variables are reordered globally. All obsolete nodes will be removed.

Side effects

Indeed, this function may take a lot of time! For TZBDD, all unreferenced nodes (not part of registered formulae) will be removed. For TZBDD, this function may change top edge or even a top node of any function/formula - this is a problem, because functions referenced by local variables only may become wrong. Consequently, for TZBDDs, sifting is not safe to start automatically!

More info

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

Definition at line 5576 of file biddyMain.c.

◆ Biddy_Managed_MinimizeBDD()

void Biddy_Managed_MinimizeBDD ( Biddy_Manager  MNG,
Biddy_String  name 
)

Description

Steinhaus–Johnson–Trotter algorithm is used to generate all possible permutations. An optimized version of Bubble Sort is used to setup the final ordering. Variables are reordered globally. All obsolete nodes will be removed.

Side effects

Indeed, this function may take a lot of time! For TZBDD, all unreferenced nodes (not part of registered formulae) will be removed. For TZBDD, this function may change top edge or even a top node of any function/formula - this is a problem, because functions referenced by local variables only may become wrong. Consequently, for TZBDDs, sifting is not safe to start automatically!

More info

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

Definition at line 5481 of file biddyMain.c.

◆ Biddy_Managed_Purge()

void Biddy_Managed_Purge ( Biddy_Manager  MNG)

Description

All formulae without name are deleted. All deleted formulae (including prolonged/fortified formulae) are removed. All fresh and obsolete nodes are immediatelly removed. Moreover, all prolonged and fortified nodes are removed if they are not needed by some of the remaining formula. 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 4303 of file biddyMain.c.

◆ Biddy_Managed_PurgeAndReorder()

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

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 4351 of file biddyMain.c.

◆ Biddy_Managed_Refresh()

void Biddy_Managed_Refresh ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

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 4380 of file biddyMain.c.

◆ Biddy_Managed_ResetVariablesValue()

void Biddy_Managed_ResetVariablesValue ( Biddy_Manager  MNG)

Description

Side effects

Only active (used) variables are reinitialized.

More info

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

Definition at line 2064 of file biddyMain.c.

◆ Biddy_Managed_SelectFunction()

void Biddy_Managed_SelectFunction ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

Terminal node must be selected before starting this function!

More info

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

Definition at line 1458 of file biddyMain.c.

◆ Biddy_Managed_SelectNode()

void Biddy_Managed_SelectNode ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

More info

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

Definition at line 1379 of file biddyMain.c.

◆ Biddy_Managed_SetAlphabeticOrdering()

void Biddy_Managed_SetAlphabeticOrdering ( Biddy_Manager  MNG)

Description

Named variables are ordered according to their names. Numbered variables are ordered according to their numbers and are always smaller (topmore) as any named variable.

Side effects

More info

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

Definition at line 5129 of file biddyMain.c.

◆ Biddy_Managed_SetManagerParameters()

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

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 1198 of file biddyMain.c.

◆ Biddy_Managed_SetVariableData()

void Biddy_Managed_SetVariableData ( Biddy_Manager  MNG,
Biddy_Variable  v,
void *  x 
)

Description

Side effects

It is not checked that the given variable is valid.

More info

Macro Biddy_SetVariableData(v,x) is defined for use with anonymous manager.

Definition at line 2180 of file biddyMain.c.

◆ Biddy_Managed_SetVariableValue()

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

Description

Side effects

It is not checked that the given variable is valid.

More info

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

Definition at line 2094 of file biddyMain.c.

◆ Biddy_Managed_Sifting()

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

Description

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

Side effects

For TZBDD, all unreferenced nodes (not part of registered formulae) will be removed. For TZBDD, sifting may change top edge or even a top node of any function/formula - this is a problem, because functions referenced by local variables only may become wrong. Consequently, for TZBDDs, sifting is not safe to start automatically!

More info

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

Definition at line 5298 of file biddyMain.c.

◆ Biddy_Managed_SwapWithHigher()

Biddy_Variable Biddy_Managed_SwapWithHigher ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

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

Side effects

All obsolete nodes will be removed.

More info

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

Definition at line 5162 of file biddyMain.c.

◆ Biddy_Managed_SwapWithLower()

Biddy_Variable Biddy_Managed_SwapWithLower ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

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 5228 of file biddyMain.c.

◆ Biddy_Managed_TaggedFoaNode()

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

Description

If such node already exists, function returns it and does not create the new one. For OBDDs, ZBDDs, OFDDs, and ZFDDs, the returned edge is not tagged (i.e. tag == 0). For TZBDDs and TZFDDs, the returned edge is tagged with the given ptag. There are two special cases:

  1. If (pf == pt == NULL) then new variable (for OBDDs, OFDDs, TZBDDs, and TZFDDs) or new element (for ZBDDs and ZFDDs) is created.
  2. (If ptag == 0) then the reduction rule and the normalization of complemented edges is not used and the node is added exactly as specified (be careful, this may create a wrong node!).

    Side effects

This function should not be called directly to add new variables and elements, you must use Biddy_Managed_FoaVariable, Biddy_Managed_AddVariableByName, or Biddy_Managed_AddElementByName. Using Biddy_Managed_TaggedFoaNode you can create node with an arbitrary ordering. It is much more safe to use Boolean operators, e.g. Biddy_Managed_ITE.

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 3244 of file biddyMain.c.

◆ Biddy_Managed_TransferMark()

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

Description

Parameter leftright should be TRUE for left and FALSE for right. For OBDDC, it is better to use macro Biddy_InvCond. For OBDDC, parameter leftright is ignored.

Side effects

TO DO: swap the meaning of parameter leftright (left should be FALSE)

More info

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

Definition at line 3096 of file biddyMain.c.