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... | |

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 (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.

See also: biddy.h, biddyInt.h

Definition in file biddyOp.c.

Biddy_Edge Biddy_Managed_A | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Variable | v |
||

) |

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).

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

Biddy_Edge Biddy_Managed_And | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g |
||

) |

For combination sets, this function coincides with Intersection.

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).

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.

Biddy_Edge Biddy_Managed_AndAbstract | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g, |
||

Biddy_Edge | cube |
||

) |

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

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

Biddy_Edge Biddy_Managed_Change | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Variable | v |
||

) |

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

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

Biddy_Edge Biddy_Managed_Compose | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g, |
||

Biddy_Variable | v |
||

) |

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)).

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

Biddy_Edge Biddy_Managed_Constrain | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | c |
||

) |

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."

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

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

Biddy_Edge Biddy_Managed_CreateFunction | ( | Biddy_Manager | MNG, |

Biddy_Edge | support, |
||

long long unsigned int | x |
||

) |

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

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

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

Biddy_Edge Biddy_Managed_CreateMinterm | ( | Biddy_Manager | MNG, |

Biddy_Edge | support, |
||

long long unsigned int | x |
||

) |

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

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

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

Biddy_Edge Biddy_Managed_E | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Variable | v |
||

) |

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).

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

Biddy_Edge Biddy_Managed_ElementAbstract | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Variable | v |
||

) |

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.

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

Biddy_Edge Biddy_Managed_ExistAbstract | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | cube |
||

) |

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

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

Biddy_Edge Biddy_Managed_ExtractMinterm | ( | Biddy_Manager | MNG, |

Biddy_Edge | f |
||

) |

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

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

Biddy_Edge Biddy_Managed_Gt | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g |
||

) |

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

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).

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.

Biddy_Boolean Biddy_Managed_IsLeq | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g |
||

) |

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

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

Biddy_Boolean Biddy_Managed_IsVariableDependent | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Variable | v |
||

) |

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

Prototyped for OBDDs (via xA, calculating full universal quantification is less efficient as direct implementation in CUDD).

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

Biddy_Edge Biddy_Managed_ITE | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g, |
||

Biddy_Edge | h |
||

) |

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.

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

Biddy_Edge Biddy_Managed_Leq | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g |
||

) |

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

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).

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

Biddy_Edge Biddy_Managed_Nand | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g |
||

) |

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).

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

Biddy_Edge Biddy_Managed_Nor | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g |
||

) |

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).

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

Biddy_Edge Biddy_Managed_Not | ( | Biddy_Manager | MNG, |

Biddy_Edge | f |
||

) |

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).

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

Biddy_Edge Biddy_Managed_Or | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g |
||

) |

For combination sets, this function coincides with Union.

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).

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.

Biddy_Edge Biddy_Managed_Permitsym | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

unsigned int | n |
||

) |

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

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

Biddy_Edge Biddy_Managed_Product | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g |
||

) |

Product is also called Multiplication.

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

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

Biddy_Edge Biddy_Managed_RandomFunction | ( | Biddy_Manager | MNG, |

Biddy_Edge | support, |
||

double | ratio |
||

) |

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.

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

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

Biddy_Edge Biddy_Managed_RandomSet | ( | Biddy_Manager | MNG, |

Biddy_Edge | unit, |
||

double | ratio |
||

) |

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.

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

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

Biddy_Edge Biddy_Managed_ReplaceByKeyword | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_String | keyword |
||

) |

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.

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.

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.

Biddy_Edge Biddy_Managed_Restrict | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Variable | v, |
||

Biddy_Boolean | value |
||

) |

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

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)).

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

Biddy_Edge Biddy_Managed_SelectiveProduct | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g, |
||

Biddy_Edge | pncube |
||

) |

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.

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).

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

Biddy_Edge Biddy_Managed_Simplify | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | c |
||

) |

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."

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

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

Biddy_Edge Biddy_Managed_Stretch | ( | Biddy_Manager | MNG, |

Biddy_Edge | f |
||

) |

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.

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.

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

Biddy_Edge Biddy_Managed_Subset | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g |
||

) |

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.

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

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

Biddy_Edge Biddy_Managed_Support | ( | Biddy_Manager | MNG, |

Biddy_Edge | f |
||

) |

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.

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

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

Biddy_Edge Biddy_Managed_Supset | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g |
||

) |

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.

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

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

Biddy_Edge Biddy_Managed_UnivAbstract | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | cube |
||

) |

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

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

Biddy_Edge Biddy_Managed_VarSubset | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Variable | v, |
||

Biddy_Boolean | value |
||

) |

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).

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

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.

Biddy_Edge Biddy_Managed_Xnor | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g |
||

) |

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).

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

Biddy_Edge Biddy_Managed_Xor | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Edge | g |
||

) |

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).

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