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

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

Copyright

Copyright (C) 2006, 2018 UM FERI, Koroska cesta 46, SI-2000 Maribor, Slovenia

Biddy is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

Biddy is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.

More info

See also: biddy.h, biddyInt.h

Definition in file 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 3815 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 4321 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 5641 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 3378 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.

Side effects

Original BDD is not changed. Implemented 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 4754 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 6154 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 6074 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 3610 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 3973 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 3089 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 3910 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_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 varaiables.

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 6250 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 set is a set containing only one subset which consist of all elements, i.e. it is a set {{x1,x2,...,xn}}.

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

Side effects

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

Side effects

Original BDD is not changed. Implemented 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 4887 of file biddyOp.c.

◆ Biddy_Managed_Subset()

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

Description

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

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

Definition at line 5826 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 not included.

More info

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

Definition at line 5027 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 4226 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.