Biddy  1.8.2
An academic Binary Decision Diagrams package
biddyOp.c File Reference

File biddyOp.c contains functions for operations on various types of Binary Decision Diagrams. More...

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

Go to the source code of this file.

Functions

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_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 (a slightly) modified 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 (OBDDs and TZBDDs) or the combination set containing a single subset which includes all dependent variables (ZBDDs). More...
 
Biddy_Edge Biddy_Managed_ReplaceByKeyword (Biddy_Manager MNG, Biddy_Edge f, Biddy_String keyword)
 Function Biddy_Managed_ReplaceByKeyword calculates Boolean function 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_VarSubset (Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v, Biddy_Boolean value)
 Function Biddy_Managed_VarSubset calculates a division of Boolean function with a literal. More...
 
Biddy_Edge Biddy_Managed_ElementAbstract (Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
 Function Biddy_Managed_ElementAbstract remove element from all combinations in the set. More...
 
Biddy_Edge Biddy_Managed_Product (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Product calculates operation product defined over combination sets. More...
 
Biddy_Edge Biddy_Managed_SelectiveProduct (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Edge cube)
 Function Biddy_Managed_SelectiveProduct calculates operation selective product defined over combination sets. More...
 
Biddy_Edge Biddy_Managed_Supset (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Supset calculates Coudert and Madre's operation SupSet. More...
 
Biddy_Edge Biddy_Managed_Subset (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Subset calculates Coudert and Madre's operation SubSet. More...
 
Biddy_Edge Biddy_Managed_Permitsym (Biddy_Manager MNG, Biddy_Edge f, unsigned int n)
 Function Biddy_Managed_Permitsym return a subset of f where only combinations with up to n elements are included. More...
 
Biddy_Edge Biddy_Managed_Stretch (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_Stretch calculates minimal combination set such that all elements in the original set has at least one superset in the new set. More...
 
Biddy_Edge Biddy_Managed_CreateMinterm (Biddy_Manager MNG, Biddy_Edge support, long long unsigned int x)
 Function Biddy_Managed_CreateMinterm generates one minterm. More...
 
Biddy_Edge Biddy_Managed_CreateFunction (Biddy_Manager MNG, Biddy_Edge support, long long unsigned int x)
 Function Biddy_Managed_CreateFunction generates one Boolean function. More...
 
Biddy_Edge Biddy_Managed_RandomFunction (Biddy_Manager MNG, Biddy_Edge support, double r)
 Function Biddy_Managed_RandomFunction 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...
 
Biddy_Edge Biddy_Managed_ExtractMinterm (Biddy_Manager MNG, Biddy_Edge support, Biddy_Edge f)
 Function Biddy_Managed_ExtractMinterm ... More...
 

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    [biddyOp.c]
Revision    [$Revision: 545 $]
Date        [$Date: 2019-02-11 14:07:50 +0100 (pon, 11 feb 2019) $]
Authors     [Robert Meolic (robert@meolic.com)]

Copyright

Copyright (C) 2006, 2019 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 biddyOp.c.

Function Documentation

◆ Biddy_Managed_A()

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

Description

Side effects

Original BDD is not changed. Implemented for OBDDC. Prototyped for OBDD. Prototyped for ZBDD, ZBDDC and TZBDD. 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 3826 of file biddyOp.c.

◆ Biddy_Managed_And()

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

Description

For combination sets, this function coincides with Intersection.

Side Effects

Used by ITE (for OBDD). Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. For OBDDC, results are cached as parameters to ITE(F,G,H)= F*G XOR F'*H. For all other BDD types, results are cached as (f,g,biddyZero).

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 812 of file biddyOp.c.

◆ Biddy_Managed_AndAbstract()

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

Description

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD.

More info

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

Definition at line 4335 of file biddyOp.c.

◆ Biddy_Managed_Change()

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

Description

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. RC Cache is used with parameters (f,biddyNull,v).

More info

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

Definition at line 5692 of file biddyOp.c.

◆ Biddy_Managed_Compose()

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

Description

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. For OBDDs, recursive calls use 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 3383 of file biddyOp.c.

◆ Biddy_Managed_Constrain()

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

Description

Coudert and Madre's constrain function is also called a generalized cofactor of function f with respect to function c. Here is an explanation from http://gauss.ececs.uc.edu/Courses/c626/lectures/BDD/bdd-desc.pdf "BDD g is a generalized co-factor of f and c if for any truth assignment t, g(t) has the same value as f(t') where t' is the “nearest” truth assignment to t that maps c to 1. By definition, the result of this operation depends on the underlying BDD variable ordering so it cannot be regarded as a logical operation."

Side effects

Original BDD is not changed. Implemented only for OBDD and OBDDC. Cache table is not used.

More info

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

Definition at line 4775 of file biddyOp.c.

◆ Biddy_Managed_CreateFunction()

Biddy_Edge Biddy_Managed_CreateFunction ( Biddy_Manager  MNG,
Biddy_Edge  support,
long long unsigned int  x 
)

Description

The represented Boolean function depends on the variables given with parameter support whilst the parameter n determines the generated function.

Side effects

Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD.

More info

Macro Biddy_CreateFunction(support,x) is defined for use with anonymous manager.

Definition at line 7670 of file biddyOp.c.

◆ Biddy_Managed_CreateMinterm()

Biddy_Edge Biddy_Managed_CreateMinterm ( Biddy_Manager  MNG,
Biddy_Edge  support,
long long unsigned int  x 
)

Description

The represented Boolean function depends on the variables given with parameter support whilst the parameter n determines the generated minterm.

Side effects

Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD.

More info

Macro Biddy_CreateMinterm(support,x) is defined for use with anonymous manager.

Definition at line 7590 of file biddyOp.c.

◆ Biddy_Managed_E()

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

Description

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. 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 3618 of file biddyOp.c.

◆ Biddy_Managed_ElementAbstract()

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

Description

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD.

More info

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

Definition at line 6141 of file biddyOp.c.

◆ Biddy_Managed_ExistAbstract()

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

Description

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD.

More info

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

Definition at line 3987 of file biddyOp.c.

◆ Biddy_Managed_ExtractMinterm()

Biddy_Edge Biddy_Managed_ExtractMinterm ( Biddy_Manager  MNG,
Biddy_Edge  support,
Biddy_Edge  f 
)

Description

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. Cache table is not used.

More info

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

Definition at line 8067 of file biddyOp.c.

◆ Biddy_Managed_Gt()

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

Description

Boolean function gt(f,g) = and(f,not(g)) = not(leq(f,g)). For combination sets, this function coincides with Diff.

Side Effects

Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. For OBDDC, results are cached as parameters to ITE(F,G,H)= F*G XOR F'*H. For all other BDD types, results are cached as (f,g,g).

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 2767 of file biddyOp.c.

◆ Biddy_Managed_IsLeq()

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

Description

Side Effects

Prototyped for OBDDs, ZBDDs, and TZBDDs (via calculating full implication, this is less efficient as implementation in CUDD).

More Info

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

Definition at line 3091 of file biddyOp.c.

◆ Biddy_Managed_IsVariableDependent()

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

Description

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

Side effects

Prototyped for OBDDs (via xA, calculating full universal quantification 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 3924 of file biddyOp.c.

◆ Biddy_Managed_ITE()

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

Description

Side Effects

Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. For OBDDC, results are cached as parameters to ITE(F,G,H)= F*G XOR F'*H. For all other BDD types, results are cached as (f,g,h) where f,g,h != 0, f != g, f != h, and g != h.

More info

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

Definition at line 370 of file biddyOp.c.

◆ Biddy_Managed_Leq()

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

Description

Boolean function leq(f,g) = or(not(f),g) = not(gt(f,g)). This function coincides with implication f->g.

Side Effects

Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. For OBDDC, results are cached as parameters to ITE(F,G,H)= F*G XOR F'*H. For all other BDD types, results are cached as (f,f,g).

More Info

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

Definition at line 2452 of file biddyOp.c.

◆ Biddy_Managed_Nand()

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

Description

Side Effects

Implemented for OBDDC. Prototyped for OBDD. Prototyped for ZBDD, ZBDDC and TZBDD (via and-not). For OBDDC, results are cached as parameters to ITE(F,G,H)= F*G XOR F'*H. For OBDD, ZBDD, ZBDDC and TZBDD, results could be cached as (f,g,biddyNull).

More Info

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

Definition at line 1718 of file biddyOp.c.

◆ Biddy_Managed_Nor()

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

Description

Side Effects

Implemented for OBDDC. Prototyped for OBDD. Prototyped for ZBDD, ZBDDC and TZBDD (via or-not). For OBDDC, results are cached as parameters to ITE(F,G,H)= F*G XOR F'*H. For OBDD, ZBDD, ZBDDC and TZBDD, results could be cached as (biddyNull,f,g).

More Info

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

Definition at line 1816 of file biddyOp.c.

◆ Biddy_Managed_Not()

Biddy_Edge Biddy_Managed_Not ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. For OBDDC and OFDDC, it is better to use macro Biddy_Inv. For OBDDC, cache table is not needed. For ZBDD and ZBDDC, recursive calls are via Xor, its cache table is used. For OBDD and TZBDD, results are cached as (f,biddyZero,biddyOne).

More info

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

Definition at line 100 of file biddyOp.c.

◆ Biddy_Managed_Or()

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

Description

For combination sets, this function coincides with Union.

Side Effects

Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. For OBDDC, results are cached as parameters to ITE(F,G,H)= F*G XOR F'*H. For all other BDD types, results are cached as (biddyZero,f,g).

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 1243 of file biddyOp.c.

◆ Biddy_Managed_Permitsym()

Biddy_Edge Biddy_Managed_Permitsym ( Biddy_Manager  MNG,
Biddy_Edge  f,
unsigned int  n 
)

Description

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. Cache table is not used.

More info

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

Definition at line 7261 of file biddyOp.c.

◆ Biddy_Managed_Product()

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

Description

Product is also called Multiplication.

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. RC Cache is used with parameters (f,g,biddyTerminal).

More info

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

Definition at line 6307 of file biddyOp.c.

◆ Biddy_Managed_RandomFunction()

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

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 variables - it can be generated with function Biddy_Support.

Side effects

Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. Parameter r must be a number from [0,1]. Otherwise, function returns biddyNull.

More info

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

Definition at line 7767 of file biddyOp.c.

◆ Biddy_Managed_RandomSet()

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

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 unit is a set containing a sigle subset which consist of all elements, i.e. it is a set {{x1,x2,...,xn}} - this is encoded as a product of positive variables and can be generated with function Biddy_Support.

Side effects

Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. 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 7908 of file biddyOp.c.

◆ Biddy_Managed_ReplaceByKeyword()

Biddy_Edge Biddy_Managed_ReplaceByKeyword ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_String  keyword 
)

Description

Original BDD is not changed. Implemented for OBDD, OBDDC, and TZBDD. Prototyped for ZBDD and ZBDDC (via And-Xor-Not-Restrict). Replacing is controlled by variable's values (which are edges!). For OBDDs and TZBDDs control values must be variables, but for ZBDDs they must be elements! Use Biddy_ResetVariablesValue and Biddy_SetVariableValue to prepare control values. Parameter keyword is used to maintain cache table. If (keyword == NULL) then entries in the cache table from previous calculations are deleted.

Side effects

For ZBDD and ZBDDC the function is prototyped and not implemented, yet. Therefore, for ZBDD and ZBDDC, the sets of current and new variables should be disjoint.

More info

Macro Biddy_ReplaceByKeyword(f,keyword) is defined for use with anonymous manager. Macros Biddy_Managed_Replace(MNG,f) and Biddy_Replace(f) are variants with less effective cache table.

Definition at line 5265 of file biddyOp.c.

◆ Biddy_Managed_Restrict()

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

Description

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

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. For OBDDs, 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 3163 of file biddyOp.c.

◆ Biddy_Managed_SelectiveProduct()

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

Description

Selective product is also called Selective multiplication. Combinations are composed only if they agree on variables from cube. This is a non-commutatitve operation. Variables in Boolean function cube, which are presented in g, must exist in f while, viceversa, this is not required. Moreover, variables which are missing in Boolean function cube and are presented in g must not exist in f (they will be included in the result!) while, viceversa, this is not required. Combinations from f, which are not composed with any combination from g are not included in the result.

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. RC Cache is used with parameters (f,g,cube). Because the usage of RC Cache coincide with functions Biddy_Restrict and Biddy_Compose they should not be used together with Biddy_SelectiveProduct in the same manager (the allowed exception is Restrict to zero).

More info

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

Definition at line 6614 of file biddyOp.c.

◆ Biddy_Managed_Simplify()

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

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. Here is an explanation from http://gauss.ececs.uc.edu/Courses/c626/lectures/BDD/bdd-desc.pdf "Consider the truth tables corresponding to two BDDs f and c over the union of variable sets of both f and c. Build a new BDD g with variable set no larger than the union of the variable sets of f and c and with a truth table such that on rows which c maps to 1 g maps to the same value that f maps to, and on other rows g maps to any value, independent of f. It should be clear that (f AND c) and (g AND c) are identical so g can replace f in a collection of BDDs without changing its solution space."

Side effects

Original BDD is not changed. Implemented only for OBDD and OBDDC. Cache table is not used.

More info

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

Definition at line 4925 of file biddyOp.c.

◆ Biddy_Managed_Stretch()

Biddy_Edge Biddy_Managed_Stretch ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. RC Cache is used with parameters (f,biddyNull,biddyNull).

More info

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

Definition at line 7432 of file biddyOp.c.

◆ Biddy_Managed_Subset()

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

Description

The set SubSet(F,G) is the set of products of F that is contained in at least one product of G. For combination sets, function Subset coincides with a function which is called a Permission operation. It extracts the product terms from F such that the item combination is a subset of at least one item combination in G.

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. RC Cache is used with parameters (f,g,biddyNull).

More info

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

Definition at line 7076 of file biddyOp.c.

◆ Biddy_Managed_Support()

Biddy_Edge Biddy_Managed_Support ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. For OBDDs, dependent variables are exactly those variables existing in the graph. For ZBDDs and TZBDDs, this is not true.

Side effects

For ZBDDs and ZFDDs, variables above the top variable (which are always all dependent) are also included.

More info

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

Definition at line 5065 of file biddyOp.c.

◆ Biddy_Managed_Supset()

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

Description

The set SupSet(F,G) is the set of products of F that contain at least one product of G. For combination sets, function Supset coincides with a function which is called a Restriction operation. It extracts the product terms from F such that the item combination is a superset of at least one item combination in G.

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. RC Cache is used with parameters (biddyNull,f,g).

More info

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

Definition at line 6855 of file biddyOp.c.

◆ Biddy_Managed_UnivAbstract()

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

Description

Side effects

Original BDD is not changed. Implemented for OBDDC. Prototyped for OBDD. Prototyped for ZBDD, ZBDDC and TZBDD.

More info

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

Definition at line 4240 of file biddyOp.c.

◆ Biddy_Managed_VarSubset()

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

Description

If (value == FALSE) then calculates (f|_{v=0})*(NOT v). If (value == TRUE) then calculates (f|_{v=1})*v. This is NOT a Coudert and Madre's SubSet operation (which is also called a Permission operation and is a counterpart of a SupSet operation). For combination sets, function Subset coincides with functions Subset0 and Subset1. Moreover, function Offset (also called Modulo or Remainder) is the same as function Subset0, while function Onset (also called Division or Quotient) can be calculated as Change(Subset1(f,v),v).

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. Cache table for AND is used.

More info

Macro Biddy_VarSubset(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. Macros Biddy_Managed_Quotient(MNG,f,v), Biddy_Quotient(f,v), Biddy_Managed_Remainder(MNG,f,v), and Biddy_Remainder(f,v) are defined for manipulation of combination sets. Using the provided macros, Biddy_Managed_Quotient and Biddy_Quotient are not implemented optimally.

Definition at line 5891 of file biddyOp.c.

◆ Biddy_Managed_Xnor()

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

Description

Side Effects

Implemented for OBDDC. Prototyped for OBDD. Prototyped for ZBDD, ZBDDC and TZBDD (via xor-not). For OBDDC, results are cached as parameters to ITE(F,G,H)= F*G XOR F'*H. For OBDD, ZBDD, ZBDDC and TZBDD, results could be cached as (f,biddyNull,g).

More Info

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

Definition at line 2354 of file biddyOp.c.

◆ Biddy_Managed_Xor()

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

Description

Side Effects

Used by ITE (for OBDDC). Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. For OBDDC, results are cached as parameters to ITE(F,G,H)= F*G XOR F'*H. For all other BDD types, results are cached as (f,biddyZero,g).

More Info

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

Definition at line 1913 of file biddyOp.c.