Biddy  2.1.1
A multi-platform 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 pncube)
 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 subset of the given set such that all elements in the original set has at least one element in the new set that is a superset of it. 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 ratio)
 Function Biddy_Managed_RandomFunction generates a random BDD. More...
 
Biddy_Edge Biddy_Managed_RandomSet (Biddy_Manager MNG, Biddy_Edge unit, double ratio)
 Function Biddy_Managed_RandomSet generates a random BDD. More...
 
Biddy_Edge Biddy_Managed_ExtractMinterm (Biddy_Manager MNG, 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: 652 $]
Date        [$Date: 2021-08-28 09:52:46 +0200 (sob, 28 avg 2021) $]
Authors     [Robert Meolic (robert@meolic.com)]

Copyright

Copyright (C) 2006, 2019 UM FERI, Koroska cesta 46, SI-2000 Maribor, Slovenia. Copyright (C) 2019, 2021 Robert Meolic, 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 1264 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 270 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 1565 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 2056 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 1102 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 1662 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 2948 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 2871 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 1184 of file biddyOp.c.

◆ Biddy_Managed_ElementAbstract()

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

Description

Side effects

Biddy_Managed_ElementAbstract is similar as Biddy_Managed_E but the abstracted element is added as negative literal. 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 2229 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 1410 of file biddyOp.c.

◆ Biddy_Managed_ExtractMinterm()

Biddy_Edge Biddy_Managed_ExtractMinterm ( Biddy_Manager  MNG,
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) is defined for use with anonymous manager.

Definition at line 3186 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 871 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 948 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 1344 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 184 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 790 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 474 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 553 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 103 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 353 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 2691 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 2308 of file biddyOp.c.

◆ Biddy_Managed_RandomFunction()

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

Description

The represented Boolean function depends on the variables given with parameter support whilst the parameter ratio 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 ratio must be a number from [0,1]. Otherwise, function returns biddyNull.

More info

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

Definition at line 3029 of file biddyOp.c.

◆ Biddy_Managed_RandomSet()

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

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 3111 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 1944 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 1023 of file biddyOp.c.

◆ Biddy_Managed_SelectiveProduct()

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

Description

Selective product is also called Selective multiplication. Combinations are composed only if they agree on all variables from cube. This is a non-commutatitve operation. For OBDD and TZBDD, variables included as positive literals in cube are from positive set, while variables included as negative literals are from negative set. For ZBDD, variables included as positive literals in cube, are from positive set, while don't care variables are from negative set. Variables that are from positive set and are presented in g, must exist in f, while, viceversa, this is not required. Variables that are from negative set and are presented in g, must not exist in f, while, viceversa, this is not required.

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. As a consequence of the given rules, variables that are in negative set and are presented in g, will exist in the result in those combinations where they do not exist in f. As a consequence of the given rules, variables that are in negative set and are not presented in g, will exist in the result in those combinations where they exist in f. As a consequence of the given rules, the result may contain combinations without any variable from positive set. As a consequence of the given rules, combinations from f, which are not composed with any combination from g (because they do not agree on cube with any combination from g) are not included in the result. 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 2413 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 1754 of file biddyOp.c.

◆ Biddy_Managed_Stretch()

Biddy_Edge Biddy_Managed_Stretch ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Each combination is a superset of itself. All non-empty combinations are a superset of an empty combination. If one combination is a superset of another one then the smaller combination is removed.

Side effects

Original BDD is not changed. Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. RC Cache is used with parameters (f,biddyNull,biddyNull). This function should be called Shrink but because of my bad English I made mistake and mixed up these words.

More info

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

Definition at line 2777 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 2603 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 1829 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 2509 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 1488 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) = f*(NOT v). If (value == TRUE) then calculates (f|_{v=1})*v = f*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 VarSubset 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 2149 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 711 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 631 of file biddyOp.c.