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 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 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_Subset (Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v, Biddy_Boolean value) |

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

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

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: 457 $] Date [$Date: 2018-07-17 11:43:13 +0200 (tor, 17 jul 2018) $] Authors [Robert Meolic (robert.meolic@um.si)]

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.

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.

Original BDD is not changed. Implemented 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_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_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_RandomFunction | ( | Biddy_Manager | MNG, |

Biddy_Edge | support, |
||

double | r |
||

) |

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

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

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

Biddy_Edge Biddy_Managed_RandomSet | ( | Biddy_Manager | MNG, |

Biddy_Edge | unit, |
||

double | r |
||

) |

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

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, ZBDD, and TZBDD. Prototyped for ZBDD and ZBDDC (via And-Xor-Not-Restrict). For ZBDD and ZBDDC, the sets of current and new variables should be disjoint. 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.

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

Original BDD is not changed. Implemented 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_Subset | ( | Biddy_Manager | MNG, |

Biddy_Edge | f, |
||

Biddy_Variable | v, |
||

Biddy_Boolean | value |
||

) |

For combination sets, this function coincides with Subset0 and Subset1.

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

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

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

Macro Biddy_Support(f) 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_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.