Biddy  1.8.1
An academic Binary Decision Diagrams package
biddy.h File Reference

File biddy.h contains declaration of all external data structures. More...

#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
#include <stdarg.h>
#include <time.h>
Include dependency graph for biddy.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define TRUE   (0 == 0)
 
#define FALSE   !TRUE
 
#define BIDDYTYPEOBDD   1
 
#define BIDDYTYPENAMEOBDD   "ROBDD"
 
#define BIDDYTYPEOBDDC   2
 
#define BIDDYTYPENAMEOBDDC   "ROBDD WITH COMPLEMENTED EDGES"
 
#define BIDDYTYPEZBDD   3
 
#define BIDDYTYPENAMEZBDD   "ZBDD"
 
#define BIDDYTYPEZBDDC   4
 
#define BIDDYTYPENAMEZBDDC   "ZBDD WITH COMPLEMENTED EDGES"
 
#define BIDDYTYPETZBDD   5
 
#define BIDDYTYPENAMETZBDD   "TAGGED ZBDD"
 
#define BIDDYTYPETZBDDC   6
 
#define BIDDYTYPENAMETZBDDC   "TAGGED ZBDD WITH COMPLEMENTED EDGES"
 
#define BIDDYTYPEOFDD   7
 
#define BIDDYTYPENAMEOFDD   "ROFDD"
 
#define BIDDYTYPEOFDDC   8
 
#define BIDDYTYPENAMEOFDDC   "ROFDD WITH COMPLEMENTED EDGES"
 
#define BIDDYTYPEZFDD   9
 
#define BIDDYTYPENAMEZFDD   "ZFDD"
 
#define BIDDYTYPEZFDDC   10
 
#define BIDDYTYPENAMEZFDDC   "ZFDD WITH COMPLEMENTED EDGES"
 
#define BIDDYTYPETZFDD   11
 
#define BIDDYTYPENAMETZFDD   "TZFDD"
 
#define BIDDYTYPETZFDDC   12
 
#define BIDDYTYPENAMETZFDDC   "TZFDD WITH COMPLEMENTED EDGES"
 
#define Biddy_IsNull(f)   (f == NULL)
 
#define Biddy_IsTerminal(f)   ((((void**)((uintptr_t) f & ~((uintptr_t) 1)))[2] == NULL) && (((void**)((uintptr_t) f & ~((uintptr_t) 1)))[3] == NULL))
 
#define Biddy_IsEqvPointer(f, g)   (((uintptr_t) f & ~((uintptr_t) 1)) == ((uintptr_t) g & ~((uintptr_t) 1)))
 
#define Biddy_GetMark(f)   (((uintptr_t) f & (uintptr_t) 1) != 0)
 
#define Biddy_SetMark(f)   (f = (Biddy_Edge) ((uintptr_t) f | (uintptr_t) 1))
 
#define Biddy_ClearMark(f)   (f = (Biddy_Edge) ((uintptr_t) f & ~((uintptr_t) 1)))
 
#define Biddy_InvertMark(f)   (f = (Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1))
 
#define Biddy_Inv(f)   ((Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1))
 
#define Biddy_InvCond(f, c)   (c ? ((Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1)) : f)
 
#define Biddy_Regular(f)   ((Biddy_Edge) ((uintptr_t) f & ~((uintptr_t) 1)))
 
#define Biddy_Complement(f)   ((Biddy_Edge) ((uintptr_t) f | (uintptr_t) 1))
 
#define Biddy_GetTag(f)   0
 
#define Biddy_SetTag(f, t)   0
 
#define Biddy_ClearTag(f)   0
 
#define Biddy_Untagged(f)   0
 
#define Biddy_Init()   Biddy_InitMNG(NULL,BIDDYTYPEOBDDC)
 
#define Biddy_InitAnonymous(bddtype)   Biddy_InitMNG(NULL,bddtype)
 
#define Biddy_Exit()   Biddy_ExitMNG(NULL)
 
#define Biddy_GetManagerType()   Biddy_Managed_GetManagerType(NULL)
 
#define Biddy_GetManagerName()   Biddy_Managed_GetManagerName(NULL)
 
#define Biddy_SetManagerParameters(gcr, gcrF, gcrX, rr, rrF, rrX, st, cst)   Biddy_Managed_SetManagerParameters(NULL,gcr,gcrF,gcrX,rr,rrF,rrX,st,cst)
 
#define Biddy_Managed_GetThen(MNG, f)   Biddy_GetThen(f)
 
#define Biddy_Managed_GetElse(MNG, f)   Biddy_GetElse(f)
 
#define Biddy_Managed_GetTopVariable(MNG, f)   Biddy_GetTopVariable(f)
 
#define Biddy_IsEqv(f1, MNG2, f2)   Biddy_Managed_IsEqv(NULL,f1,MNG2,f2)
 
#define Biddy_SelectNode(f)   Biddy_Managed_SelectNode(NULL,f)
 
#define Biddy_DeselectNode(f)   Biddy_Managed_DeselectNode(NULL,f)
 
#define Biddy_IsSelected(f)   Biddy_Managed_IsSelected(NULL,f)
 
#define Biddy_SelectFunction(f)   Biddy_Managed_SelectFunction(NULL,f)
 
#define Biddy_DeselectAll()   Biddy_Managed_DeselectAll(NULL)
 
#define Biddy_GetTerminal()   Biddy_Managed_GetTerminal(NULL)
 
#define Biddy_GetConstantZero()   Biddy_Managed_GetConstantZero(NULL)
 
#define Biddy_Managed_GetEmptySet(MNG)   Biddy_Managed_GetConstantZero(MNG)
 
#define Biddy_GetEmptySet()   Biddy_Managed_GetConstantZero(NULL)
 
#define Biddy_GetConstantOne()   Biddy_Managed_GetConstantOne(NULL)
 
#define Biddy_Managed_GetUniversalSet(MNG)   Biddy_Managed_GetConstantOne(MNG)
 
#define Biddy_GetUniversalSet()   Biddy_Managed_GetConstantOne(NULL)
 
#define Biddy_GetBaseSet()   Biddy_Managed_GetBaseSet(NULL)
 
#define Biddy_GetVariable(x)   Biddy_Managed_GetVariable(NULL,x)
 
#define Biddy_GetLowestVariable()   Biddy_Managed_GetLowestVariable(NULL)
 
#define Biddy_GetIthVariable(i)   Biddy_Managed_GetIthVariable(NULL,i)
 
#define Biddy_GetPrevVariable(v)   Biddy_Managed_GetPrevVariable(NULL,v)
 
#define Biddy_GetNextVariable(v)   Biddy_Managed_GetNextVariable(NULL,v)
 
#define Biddy_GetVariableEdge(v)   Biddy_Managed_GetVariableEdge(NULL,v)
 
#define Biddy_GetElementEdge(v)   Biddy_Managed_GetElementEdge(NULL,v)
 
#define Biddy_GetVariableName(v)   Biddy_Managed_GetVariableName(NULL,v)
 
#define Biddy_GetTopVariableEdge(f)   Biddy_Managed_GetTopVariableEdge(NULL,f)
 
#define Biddy_GetTopVariableName(f)   Biddy_Managed_GetTopVariableName(NULL,f)
 
#define Biddy_GetTopVariableChar(f)   Biddy_Managed_GetTopVariableChar(NULL,f)
 
#define Biddy_ResetVariablesValue()   Biddy_Managed_ResetVariablesValue(NULL)
 
#define Biddy_SetVariableValue(v, f)   Biddy_Managed_SetVariableValue(NULL,v,f)
 
#define Biddy_GetVariableValue(v)   Biddy_Managed_GetVariableValue(NULL,v)
 
#define Biddy_ClearVariablesData()   Biddy_Managed_ClearVariablesData(NULL)
 
#define Biddy_SetVariableData(v, x)   Biddy_Managed_SetVariableData(NULL,v,x)
 
#define Biddy_GetVariableData(v)   Biddy_Managed_GetVariableData(NULL,v)
 
#define Biddy_Eval(f)   Biddy_Managed_Eval(NULL,f)
 
#define Biddy_EvalProbability(f)   Biddy_Managed_EvalProbability(NULL,f)
 
#define Biddy_IsSmaller(fv, gv)   Biddy_Managed_IsSmaller(NULL,fv,gv)
 
#define Biddy_IsLowest(v)   Biddy_Managed_IsLowest(NULL,v)
 
#define Biddy_IsHighest(v)   Biddy_Managed_IsHighest(NULL,v)
 
#define Biddy_FoaVariable(x, varelem)   Biddy_Managed_FoaVariable(NULL,x,varelem)
 
#define Biddy_ChangeVariableName(v, x)   Biddy_Managed_ChangeVariableName(NULL,v,x)
 
#define Biddy_AddVariableByName(x)   Biddy_Managed_AddVariableByName(NULL,x)
 
#define Biddy_Managed_AddVariable(MNG)   Biddy_Managed_AddVariableByName(MNG,NULL)
 
#define Biddy_AddVariable()   Biddy_Managed_AddVariableByName(NULL,NULL)
 
#define Biddy_Managed_AddVariableEdge(MNG)   Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_AddVariableByName(MNG,NULL))
 
#define Biddy_AddVariableEdge()   Biddy_Managed_GetVariableEdge(NULL,Biddy_Managed_AddVariableByName(NULL,NULL))
 
#define Biddy_AddElementByName(x)   Biddy_Managed_AddElementByName(NULL,x)
 
#define Biddy_Managed_AddElement(MNG)   Biddy_Managed_AddElementByName(MNG,NULL)
 
#define Biddy_AddElement()   Biddy_Managed_AddElementByName(NULL,NULL)
 
#define Biddy_AddVariableBelow(v)   Biddy_Managed_AddVariableBelow(NULL,v)
 
#define Biddy_AddVariableAbove(v)   Biddy_Managed_AddVariableAbove(NULL,v)
 
#define Biddy_TransferMark(f, mark, leftright)   Biddy_Managed_TransferMark(NULL,f,mark,leftright)
 
#define Biddy_IncTag(f)   Biddy_Managed_IncTag(NULL,f)
 
#define Biddy_TaggedFoaNode(v, pf, pt, ptag, garbageAllowed)   Biddy_Managed_TaggedFoaNode(NULL,v,pf,pt,ptag,garbageAllowed)
 
#define Biddy_Managed_FoaNode(MNG, v, pf, pt, garbageAllowed)   Biddy_Managed_TaggedFoaNode(MNG,v,pf,pt,v,garbageAllowed)
 
#define Biddy_FoaNode(v, pf, pt, garbageAllowed)   Biddy_Managed_TaggedFoaNode(NULL,v,pf,pt,v,garbageAllowed)
 
#define Biddy_IsOK(f)   Biddy_Managed_IsOK(NULL,f)
 
#define Biddy_GC(targetLT, targetGEQ, purge, total)   Biddy_Managed_GC(NULL,targetLT,targetGEQ,purge,total)
 
#define Biddy_Managed_AutoGC(MNG)   Biddy_Managed_GC(MNG,0,0,FALSE,FALSE)
 
#define Biddy_AutoGC()   Biddy_Managed_GC(NULL,0,0,FALSE,FALSE)
 
#define Biddy_Managed_ForceGC(MNG)   Biddy_Managed_GC(MNG,0,0,FALSE,TRUE)
 
#define Biddy_ForceGC()   Biddy_Managed_GC(NULL,0,0,FALSE,TRUE)
 
#define Biddy_Clean()   Biddy_Managed_Clean(NULL)
 
#define Biddy_Purge()   Biddy_Managed_Purge(NULL)
 
#define Biddy_PurgeAndReorder(f, c)   Biddy_Managed_PurgeAndReorder(NULL,f,c)
 
#define Biddy_Refresh(f)   Biddy_Managed_Refresh(NULL,f)
 
#define Biddy_AddCache(gc)   Biddy_Managed_AddCache(NULL,gc)
 
#define Biddy_AddFormula(x, f, c)   Biddy_Managed_AddFormula(NULL,x,f,c)
 
#define Biddy_Managed_AddTmpFormula(mng, x, f)   Biddy_Managed_AddFormula(mng,x,f,-1)
 
#define Biddy_Managed_AddPersistentFormula(mng, x, f)   Biddy_Managed_AddFormula(mng,x,f,0)
 
#define Biddy_Managed_KeepFormula(mng, f)   Biddy_Managed_AddFormula(mng,NULL,f,1)
 
#define Biddy_Managed_KeepFormulaProlonged(mng, f, c)   Biddy_Managed_AddFormula(mng,NULL,f,c)
 
#define Biddy_Managed_KeepFormulaUntilPurge(mng, f)   Biddy_Managed_AddFormula(mng,NULL,f,0)
 
#define Biddy_AddTmpFormula(x, f)   Biddy_Managed_AddFormula(NULL,x,f,-1)
 
#define Biddy_AddPersistentFormula(x, f)   Biddy_Managed_AddFormula(NULL,x,f,0)
 
#define Biddy_KeepFormula(f)   Biddy_Managed_AddFormula(NULL,NULL,f,1)
 
#define Biddy_KeepFormulaProlonged(f, c)   Biddy_Managed_AddFormula(NULL,NULL,f,c)
 
#define Biddy_KeepFormulaUntilPurge(f)   Biddy_Managed_AddFormula(NULL,NULL,f,0)
 
#define Biddy_FindFormula(x, idx, f)   Biddy_Managed_FindFormula(NULL,x,idx,f)
 
#define Biddy_DeleteFormula(x)   Biddy_Managed_DeleteFormula(NULL,x)
 
#define Biddy_DeleteIthFormula(x)   Biddy_Managed_DeleteIthFormula(NULL,x)
 
#define Biddy_GetIthFormula(i)   Biddy_Managed_GetIthFormula(NULL,i)
 
#define Biddy_GetIthFormulaName(i)   Biddy_Managed_GetIthFormulaName(NULL,i)
 
#define Biddy_SetAlphabeticOrdering()   Biddy_Managed_SetAlphabeticOrdering(NULL)
 
#define Biddy_SwapWithHigher(v)   Biddy_Managed_SwapWithHigher(NULL,v)
 
#define Biddy_SwapWithLower(v)   Biddy_Managed_SwapWithLower(NULL,v)
 
#define Biddy_Sifting(f, c)   Biddy_Managed_Sifting(NULL,f,c)
 
#define Biddy_MinimizeBDD(f)   Biddy_Managed_MinimizeBDD(NULL,f)
 
#define Biddy_MaximizeBDD(f)   Biddy_Managed_MaximizeBDD(NULL,f)
 
#define Biddy_Copy(MNG2, f)   Biddy_Managed_Copy(NULL,MNG2,f)
 
#define Biddy_CopyFormula(MNG2, x)   Biddy_Managed_CopyFormula(NULL,MNG2,x)
 
#define Biddy_ConstructBDD(numV, varlist, numN, nodelist)   Biddy_Managed_ConstructBDD(NULL,numV,varlist,numV,nodelist)
 
#define Biddy_Not(f)   Biddy_Managed_Not(NULL,f)
 
#define Biddy_ITE(f, g, h)   Biddy_Managed_ITE(NULL,f,g,h)
 
#define Biddy_And(f, g)   Biddy_Managed_And(NULL,f,g)
 
#define Biddy_Managed_Intersect(MNG, f, g)   Biddy_Managed_And(MNG,f,g)
 
#define Biddy_Intersect(f, g)   Biddy_Managed_And(NULL,f,g)
 
#define Biddy_Or(f, g)   Biddy_Managed_Or(NULL,f,g)
 
#define Biddy_Managed_Union(MNG, f, g)   Biddy_Managed_Or(MNG,f,g)
 
#define Biddy_Union(f, g)   Biddy_Managed_Or(NULL,f,g)
 
#define Biddy_Nand(f, g)   Biddy_Managed_Nand(NULL,f,g)
 
#define Biddy_Nor(f, g)   Biddy_Managed_Nor(NULL,f,g)
 
#define Biddy_Xor(f, g)   Biddy_Managed_Xor(NULL,f,g)
 
#define Biddy_Xnor(f, g)   Biddy_Managed_Xnor(NULL,f,g)
 
#define Biddy_Leq(f, g)   Biddy_Managed_Leq(NULL,f,g)
 
#define Biddy_Gt(f, g)   Biddy_Managed_Gt(NULL,f,g)
 
#define Biddy_Managed_Diff(MNG, f, g)   Biddy_Managed_Gt(MNG,f,g)
 
#define Biddy_Diff(f, g)   Biddy_Managed_Gt(NULL,f,g)
 
#define Biddy_IsLeq(f, g)   Biddy_Managed_IsLeq(NULL,f,g)
 
#define Biddy_Restrict(f, v, value)   Biddy_Managed_Restrict(NULL,f,v,value)
 
#define Biddy_Compose(f, g, v)   Biddy_Managed_Compose(NULL,f,g,v)
 
#define Biddy_E(f, v)   Biddy_Managed_E(NULL,f,v)
 
#define Biddy_A(f, v)   Biddy_Managed_A(NULL,f,v)
 
#define Biddy_IsVariableDependent(f, v)   Biddy_Managed_IsVariableDependent(NULL,f,v)
 
#define Biddy_ExistAbstract(f, cube)   Biddy_Managed_ExistAbstract(NULL,f,cube)
 
#define Biddy_UnivAbstract(f, cube)   Biddy_Managed_UnivAbstract(NULL,f,cube)
 
#define Biddy_AndAbstract(f, g, cube)   Biddy_Managed_AndAbstract(NULL,f,g,cube)
 
#define Biddy_Constrain(f, c)   Biddy_Managed_Constrain(NULL,f,c)
 
#define Biddy_Simplify(f, c)   Biddy_Managed_Simplify(NULL,f,c)
 
#define Biddy_Support(f)   Biddy_Managed_Support(NULL,f)
 
#define Biddy_ReplaceByKeyword(f, keyword)   Biddy_Managed_ReplaceByKeyword(NULL,f,keyword)
 
#define Biddy_Managed_Replace(MNG, f)   Biddy_Managed_ReplaceByKeyword(MNG,f,NULL)
 
#define Biddy_Replace(f)   Biddy_Managed_ReplaceByKeyword(NULL,f,NULL)
 
#define Biddy_Change(f, v)   Biddy_Managed_Change(NULL,f,v)
 
#define Biddy_Subset(f, v, value)   Biddy_Managed_Subset(NULL,f,v,value)
 
#define Biddy_Managed_Subset0(MNG, f, v)   Biddy_Managed_Subset(MNG,f,v,FALSE)
 
#define Biddy_Subset0(f, v)   Biddy_Managed_Subset(NULL,f,v,FALSE)
 
#define Biddy_Managed_Subset1(MNG, f, v)   Biddy_Managed_Subset(MNG,f,v,TRUE)
 
#define Biddy_Subset1(f, v)   Biddy_Managed_Subset(NULL,f,v,TRUE)
 
#define Biddy_CreateMinterm(support, x)   Biddy_Managed_CreateMinterm(NULL,support,x)
 
#define Biddy_CreateFunction(support, x)   Biddy_Managed_CreateFunction(NULL,support,x)
 
#define Biddy_RandomFunction(support, r)   Biddy_Managed_RandomFunction(NULL,support,r)
 
#define Biddy_RandomSet(unit, r)   Biddy_Managed_RandomSet(NULL,unit,r)
 
#define Biddy_CountNodes(f)   Biddy_Managed_CountNodes(NULL,f)
 
#define Biddy_Managed_MaxLevel(MNG, f)   Biddy_MaxLevel(f)
 
#define Biddy_Managed_AvgLevel(MNG, f)   Biddy_AvgLevel(f)
 
#define Biddy_VariableTableNum()   Biddy_Managed_VariableTableNum(NULL)
 
#define Biddy_NodeTableSize()   Biddy_Managed_NodeTableSize(NULL)
 
#define Biddy_NodeTableBlockNumber()   Biddy_Managed_NodeTableBlockNumber(NULL)
 
#define Biddy_NodeTableGenerated()   Biddy_Managed_NodeTableGenerated(NULL)
 
#define Biddy_NodeTableMax()   Biddy_Managed_NodeTableMax(NULL)
 
#define Biddy_NodeTableNum()   Biddy_Managed_NodeTableNum(NULL)
 
#define Biddy_NodeTableNumVar(v)   Biddy_Managed_NodeTableNumVar(NULL,v)
 
#define Biddy_NodeTableResizeNumber()   Biddy_Managed_NodeTableResizeNumber(NULL)
 
#define Biddy_NodeTableFoaNumber()   Biddy_Managed_NodeTableFoaNumber(NULL)
 
#define Biddy_NodeTableFindNumber()   Biddy_Managed_NodeTableFindNumber(NULL)
 
#define Biddy_NodeTableCompareNumber()   Biddy_Managed_NodeTableCompareNumber(NULL)
 
#define Biddy_NodeTableAddNumber()   Biddy_Managed_NodeTableAddNumber(NULL)
 
#define Biddy_NodeTableGCNumber()   Biddy_Managed_NodeTableGCNumber(NULL)
 
#define Biddy_NodeTableGCTime()   Biddy_Managed_NodeTableGCTime(NULL)
 
#define Biddy_NodeTableGCObsoleteNumber()   Biddy_Managed_NodeTableGCObsoleteNumber(NULL)
 
#define Biddy_NodeTableSwapNumber()   Biddy_Managed_NodeTableSwapNumber(NULL)
 
#define Biddy_NodeTableSiftingNumber()   Biddy_Managed_NodeTableSiftingNumber(NULL)
 
#define Biddy_NodeTableDRTime()   Biddy_Managed_NodeTableDRTime(NULL)
 
#define Biddy_NodeTableITENumber()   Biddy_Managed_NodeTableITENumber(NULL)
 
#define Biddy_NodeTableITERecursiveNumber()   Biddy_Managed_NodeTableITERecursiveNumber(NULL)
 
#define Biddy_NodeTableANDORNumber()   Biddy_Managed_NodeTableANDORNumber(NULL)
 
#define Biddy_NodeTableANDORRecursiveNumber()   Biddy_Managed_NodeTableANDORRecursiveNumber(NULL)
 
#define Biddy_NodeTableXORNumber()   Biddy_Managed_NodeTableXORNumber(NULL)
 
#define Biddy_NodeTableXORRecursiveNumber()   Biddy_Managed_NodeTableXORRecursiveNumber(NULL)
 
#define Biddy_FormulaTableNum()   Biddy_Managed_FormulaTableNum(NULL)
 
#define Biddy_ListUsed()   Biddy_Managed_ListUsed(NULL)
 
#define Biddy_ListMaxLength()   Biddy_Managed_ListMaxLength(NULL)
 
#define Biddy_ListAvgLength()   Biddy_Managed_ListAvgLength(NULL)
 
#define Biddy_OPCacheSearch()   Biddy_Managed_OPCacheSearch(NULL)
 
#define Biddy_OPCacheFind()   Biddy_Managed_OPCacheFind(NULL)
 
#define Biddy_OPCacheInsert()   Biddy_Managed_OPCacheInsert(NULL)
 
#define Biddy_OPCacheOverwrite()   Biddy_Managed_OPCacheOverwrite(NULL)
 
#define Biddy_CountNodesPlain(f)   Biddy_Managed_CountNodesPlain(NULL,f)
 
#define Biddy_DependentVariableNumber(f, select)   Biddy_Managed_DependentVariableNumber(NULL,f,select)
 
#define Biddy_CountComplementedEdges(f)   Biddy_Managed_CountComplementedEdges(NULL,f)
 
#define Biddy_CountPaths(f)   Biddy_Managed_CountPaths(NULL,f)
 
#define Biddy_CountMinterms(f, nvars)   Biddy_Managed_CountMinterms(NULL,f,nvars)
 
#define Biddy_Managed_CountCombinations(MNG, f, nvars)   Biddy_Managed_CountMinterms(MNG,f,nvars)
 
#define Biddy_CountCombinations(f)   Biddy_Managed_CountMinterms(NULL,f,nvars)
 
#define Biddy_DensityOfFunction(f, nvars)   Biddy_Managed_DensityOfFunction(NULL,f,nvars)
 
#define Biddy_DensityOfBDD(f, nvars)   Biddy_Managed_DensityOfBDD(NULL,f,nvars)
 
#define Biddy_MinNodes(f)   Biddy_Managed_MinNodes(NULL,f)
 
#define Biddy_MaxNodes(f)   Biddy_Managed_MaxNodes(NULL,f)
 
#define Biddy_ReadMemoryInUse()   Biddy_Managed_ReadMemoryInUse(NULL)
 
#define Biddy_PrintInfo(f)   Biddy_Managed_PrintInfo(NULL,f)
 
#define Biddy_Eval0(s)   Biddy_Managed_Eval0(NULL,s)
 
#define Biddy_Eval1x(s, lf)   Biddy_Managed_Eval1x(NULL,s,lf)
 
#define Biddy_Managed_Eval1(MNG, s)   Biddy_Managed_Eval1x(MNG,s,NULL)
 
#define Biddy_Eval1(s)   Biddy_Managed_Eval1x(NULL,s,NULL)
 
#define Biddy_Eval2(boolFunc)   Biddy_Managed_Eval2(NULL,boolFunc)
 
#define Biddy_ReadBddview(filename, name)   Biddy_Managed_ReadBddview(NULL,filename,name)
 
#define Biddy_ReadVerilogFile(filename, prefix)   Biddy_Managed_ReadVerilogFile(NULL,filename,prefix)
 
#define Biddy_PrintfBDD(f)   Biddy_Managed_PrintfBDD(NULL,f)
 
#define Biddy_WriteBDD(filename, f, label)   Biddy_Managed_WriteBDD(NULL,filename,f,label)
 
#define Biddy_PrintfTable(f)   Biddy_Managed_PrintfTable(NULL,f)
 
#define Biddy_WriteTable(filename, f)   Biddy_Managed_WriteTable(NULL,filename,f)
 
#define Biddy_PrintfSOP(f)   Biddy_Managed_PrintfSOP(NULL,f)
 
#define Biddy_WriteSOP(filename, f)   Biddy_Managed_WriteSOP(NULL,filename,f)
 
#define Biddy_WriteDot(filename, f, label, id, cudd)   Biddy_Managed_WriteDot(NULL,filename,f,label,id,cudd);
 
#define Biddy_WriteBddview(filename, f, label, table)   Biddy_Managed_WriteBddview(NULL,filename,f,label,table);
 

Typedefs

typedef char Biddy_Boolean
 
typedef char * Biddy_String
 
typedef void ** Biddy_Manager
 
typedef void * Biddy_Cache
 
typedef unsigned short int Biddy_Variable
 
typedef void * Biddy_Edge
 
typedef void(* Biddy_GCFunction) (Biddy_Manager)
 
typedef Biddy_Boolean(* Biddy_LookupFunction) (Biddy_String, Biddy_Edge *)
 

Functions

EXTERN void Biddy_InitMNG (Biddy_Manager *mng, int bddtype)
 Function Biddy_InitMNG initialize a manager. More...
 
EXTERN void Biddy_ExitMNG (Biddy_Manager *mng)
 Function Biddy_ExitMNG deletes a manager. More...
 
EXTERN Biddy_String Biddy_About ()
 Function Biddy_About reports version of Biddy package. More...
 
EXTERN int Biddy_Managed_GetManagerType (Biddy_Manager MNG)
 Function Biddy_Managed_GetManagerType reports BDD type used in the manager. More...
 
EXTERN Biddy_String Biddy_Managed_GetManagerName (Biddy_Manager MNG)
 Function Biddy_Managed_GetManagerName reports the name of the BDD type used in the manager. More...
 
EXTERN void Biddy_Managed_SetManagerParameters (Biddy_Manager MNG, float gcr, float gcrF, float gcrX, float rr, float rrF, float rrX, float st, float cst)
 Function Biddy_Managed_SetManagerParameters set modifiable parameters. More...
 
EXTERN Biddy_Edge Biddy_GetThen (Biddy_Edge f)
 Function Biddy_GetThen returns THEN successor. More...
 
EXTERN Biddy_Edge Biddy_GetElse (Biddy_Edge f)
 Function Biddy_GetElse returns ELSE successor. More...
 
EXTERN Biddy_Variable Biddy_GetTopVariable (Biddy_Edge f)
 Function Biddy_GetTopVariable returns the top variable. More...
 
EXTERN Biddy_Boolean Biddy_Managed_IsEqv (Biddy_Manager MNG1, Biddy_Edge f1, Biddy_Manager MNG2, Biddy_Edge f2)
 Function Biddy_Managed_IsEqv returns TRUE iff two BDDs are equal. More...
 
EXTERN void Biddy_Managed_SelectNode (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_SelectNode selects the top node of the given function. More...
 
EXTERN void Biddy_Managed_DeselectNode (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_DeselectNode deselects the top node of the given function. More...
 
EXTERN Biddy_Boolean Biddy_Managed_IsSelected (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_IsSelected returns TRUE iff the top node of the given function is selected. More...
 
EXTERN void Biddy_Managed_SelectFunction (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_SelectFunction recursively selects all nodes of a given function. More...
 
EXTERN void Biddy_Managed_DeselectAll (Biddy_Manager MNG)
 Function Biddy_Managed_DeselectAll deselects all nodes. More...
 
EXTERN Biddy_Edge Biddy_Managed_GetTerminal (Biddy_Manager MNG)
 Function Biddy_Managed_GetTerminal returns unmarked and untagged edge pointing to terminal node 1. More...
 
EXTERN Biddy_Edge Biddy_Managed_GetConstantZero (Biddy_Manager MNG)
 Function Biddy_Managed_GetConstantZero returns constant 0. More...
 
EXTERN Biddy_Edge Biddy_Managed_GetConstantOne (Biddy_Manager MNG)
 Function Biddy_Managed_GetConstantOne returns constant 1. More...
 
EXTERN Biddy_Edge Biddy_Managed_GetBaseSet (Biddy_Manager MNG)
 Function Biddy_Managed_GetBaseSet returns set containing only a null combination, i.e. it returns {{}}. More...
 
EXTERN Biddy_Variable Biddy_Managed_GetVariable (Biddy_Manager MNG, Biddy_String x)
 Function Biddy_Managed_GetVariable returns variable with the given name. More...
 
EXTERN Biddy_Variable Biddy_Managed_GetLowestVariable (Biddy_Manager MNG)
 Function Biddy_Managed_GetLowestVariable returns the lowest variable in the current ordering. More...
 
EXTERN Biddy_Variable Biddy_Managed_GetIthVariable (Biddy_Manager MNG, Biddy_Variable i)
 Function Biddy_Managed_GetIthVariable returns ith variable in the current global ordering. More...
 
EXTERN Biddy_Variable Biddy_Managed_GetPrevVariable (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetPrevVariable returns previous variable in the global ordering (lower, topmore). More...
 
EXTERN Biddy_Variable Biddy_Managed_GetNextVariable (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetNextVariable returns next variable in the global ordering (higher, bottommore). More...
 
EXTERN Biddy_Edge Biddy_Managed_GetVariableEdge (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetVariableEdge returns variable's edge. More...
 
EXTERN Biddy_Edge Biddy_Managed_GetElementEdge (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetElementEdge returns element's edge. More...
 
EXTERN Biddy_String Biddy_Managed_GetVariableName (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetVariableName returns the name of a variable. More...
 
EXTERN Biddy_Edge Biddy_Managed_GetTopVariableEdge (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_GetTopVariableEdge returns variable's edge of top variable. More...
 
EXTERN Biddy_String Biddy_Managed_GetTopVariableName (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_GetTopVariableName returns the name of top variable. More...
 
EXTERN char Biddy_Managed_GetTopVariableChar (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_GetTopVariableChar returns the first character in the name of top variable. More...
 
EXTERN void Biddy_Managed_ResetVariablesValue (Biddy_Manager MNG)
 Function Biddy_Managed_ResetVariablesValue sets all variable's value to biddyZero. More...
 
EXTERN void Biddy_Managed_SetVariableValue (Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge f)
 Function Biddy_Managed_SetVariableValue sets variable's value. More...
 
EXTERN Biddy_Edge Biddy_Managed_GetVariableValue (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetVariableValue gets variable's value. More...
 
EXTERN void Biddy_Managed_ClearVariablesData (Biddy_Manager MNG)
 Function Biddy_Managed_ClearVariablesData free memory used for all variable's data. More...
 
EXTERN void Biddy_Managed_SetVariableData (Biddy_Manager MNG, Biddy_Variable v, void *x)
 Function Biddy_Managed_SetVariableData sets variable's data. More...
 
EXTERN void * Biddy_Managed_GetVariableData (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_GetVariableData gets variable's data. More...
 
EXTERN Biddy_Boolean Biddy_Managed_Eval (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_Eval returns the value of a Boolean function for a given variable assignment.

Description

Side effects

Variables must have values assigned. Variable is considered to be FALSE iff variable.value == biddyZero, whilst it is considered to be TRUE, otherwise.

More info

Macro Biddy_Eval(f) is defined for use with anonymous manager.
 
EXTERN double Biddy_Managed_EvalProbability (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_EvalProbability evaluates BDD. More...
 
EXTERN Biddy_Boolean Biddy_Managed_IsSmaller (Biddy_Manager MNG, Biddy_Variable fv, Biddy_Variable gv)
 Function Biddy_Managed_IsSmaller returns TRUE if the first variable is smaller (= lower = previous = above = topmore). More...
 
EXTERN Biddy_Boolean Biddy_Managed_IsLowest (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_IsLowest returns TRUE if the variable is the lowest one (lowest == topmost). More...
 
EXTERN Biddy_Boolean Biddy_Managed_IsHighest (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_IsHighest returns TRUE if the variable is the highest one if terminal node is ignored (highest == bottommost). More...
 
EXTERN Biddy_Variable Biddy_Managed_FoaVariable (Biddy_Manager MNG, Biddy_String x, Biddy_Boolean varelem)
 Function Biddy_Managed_FoaVariable finds variable/element or adds new variable (i.e. Boolean function f = x) and new element (i.e. it creates set {{x}}). More...
 
EXTERN void Biddy_Managed_ChangeVariableName (Biddy_Manager MNG, Biddy_Variable v, Biddy_String x)
 Function Biddy_Managed_ChangeVariableName set new name to the given variable/element. More...
 
EXTERN Biddy_Variable Biddy_Managed_AddVariableByName (Biddy_Manager MNG, Biddy_String x)
 Function Biddy_Managed_AddVariableByName adds variable. More...
 
EXTERN Biddy_Variable Biddy_Managed_AddElementByName (Biddy_Manager MNG, Biddy_String x)
 Function Biddy_Managed_AddElementByName adds element. More...
 
EXTERN Biddy_Edge Biddy_Managed_AddVariableBelow (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_AddVariableBelow adds variable. More...
 
EXTERN Biddy_Edge Biddy_Managed_AddVariableAbove (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_AddVariableAbove adds variable. More...
 
EXTERN Biddy_Edge Biddy_Managed_TransferMark (Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean mark, Biddy_Boolean leftright)
 Function Biddy_Managed_TransferMark returns edge with inverted complement bit iff the second parameter is TRUE and normalization rules require this. More...
 
EXTERN Biddy_Edge Biddy_Managed_IncTag (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_IncTag returns edge with an incremented tag. More...
 
EXTERN Biddy_Edge Biddy_Managed_TaggedFoaNode (Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge pf, Biddy_Edge pt, Biddy_Variable ptag, Biddy_Boolean garbageAllowed)
 Function Biddy_Managed_TaggedFoaNode finds or adds new node with the given variable and successors. More...
 
EXTERN Biddy_Boolean Biddy_Managed_IsOK (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_IsOK returns TRUE iff given node is not obsolete. More...
 
EXTERN void Biddy_Managed_GC (Biddy_Manager MNG, Biddy_Variable targetLT, Biddy_Variable targetGEQ, Biddy_Boolean purge, Biddy_Boolean total)
 Function Biddy_Managed_GC performs garbage collection. More...
 
EXTERN void Biddy_Managed_Clean (Biddy_Manager MNG)
 Function Biddy_Managed_Clean performs cleaning. More...
 
EXTERN void Biddy_Managed_Purge (Biddy_Manager MNG)
 Function Biddy_Managed_Purge immediately removes all nodes which were not preserved or which are not preserved anymore. More...
 
EXTERN void Biddy_Managed_PurgeAndReorder (Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean converge)
 Function Biddy_Managed_PurgeAndReorder immediately removes non-preserved nodes and triggers reordering on function. More...
 
EXTERN void Biddy_Managed_Refresh (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_Refresh refreshes top node in a given function. More...
 
EXTERN void Biddy_Managed_AddCache (Biddy_Manager MNG, Biddy_GCFunction gc)
 Function Biddy_Managed_AddCache adds cache to the end of Cache list. More...
 
EXTERN unsigned int Biddy_Managed_AddFormula (Biddy_Manager MNG, Biddy_String x, Biddy_Edge f, int c)
 Function Biddy_Managed_AddFormula adds formula to Formula table. More...
 
EXTERN Biddy_Boolean Biddy_Managed_FindFormula (Biddy_Manager MNG, Biddy_String x, unsigned int *idx, Biddy_Edge *f)
 Function Biddy_Managed_FindFormula find formula in Formula table. More...
 
EXTERN Biddy_Boolean Biddy_Managed_DeleteFormula (Biddy_Manager MNG, Biddy_String x)
 Function Biddy_Managed_DeleteFormula delete formula from Formula table. More...
 
EXTERN Biddy_Boolean Biddy_Managed_DeleteIthFormula (Biddy_Manager MNG, unsigned int i)
 Function Biddy_Managed_DeleteIthFormula deletes formula from the table. More...
 
EXTERN Biddy_Edge Biddy_Managed_GetIthFormula (Biddy_Manager MNG, unsigned int i)
 Function Biddy_Managed_GetIthFormula returns ith formula in a Formula table. More...
 
EXTERN Biddy_String Biddy_Managed_GetIthFormulaName (Biddy_Manager MNG, unsigned int i)
 Function Biddy_Managed_GetIthFormulaName returns name of the ith formula in a Formula table. More...
 
EXTERN void Biddy_Managed_SetAlphabeticOrdering (Biddy_Manager MNG)
 Function Biddy_Managed_SetAlphabeticOrdering use variable swapping to create an alphabetic ordering. More...
 
EXTERN Biddy_Variable Biddy_Managed_SwapWithHigher (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_SwapWithHigher swaps two adjacent variables. More...
 
EXTERN Biddy_Variable Biddy_Managed_SwapWithLower (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_SwapWithLower swaps two adjacent variables. More...
 
EXTERN Biddy_Boolean Biddy_Managed_Sifting (Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean converge)
 Function Biddy_Managed_Sifting reorders variables to minimize node number for the whole system (if f = NULL) or for the given function (if f != NULL) using Rudell's sifting algorithm. More...
 
EXTERN void Biddy_Managed_MinimizeBDD (Biddy_Manager MNG, Biddy_String name)
 Function Biddy_Managed_MinimizeBDD reorders variables to minimize the node number of the given formula using an exhaustive search over all possible orderings. More...
 
EXTERN void Biddy_Managed_MaximizeBDD (Biddy_Manager MNG, Biddy_String name)
 Function Biddy_Managed_MaximizeBDD reorders variables to maximize the node number of the given function using an exhaustive search over all possible orderings. More...
 
EXTERN Biddy_Edge Biddy_Managed_Copy (Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_Edge f)
 Function Biddy_Managed_Copy copies a graph from one manager to another manager which can use the same or different BDD type.

Description

The function takes a graph from one manager and creates the same graph in another manager. If the managers do not use the same BDD type then a graph is converted. The resulting graph will represent the same Boolean function assuming the domain from the target manager. If (f == biddyZero) then only the complete domain (all variables) is copied.

Side effects

If source and target manager are the same then function does nothing. The variable ordering of the created BDD is trying to follow the original ordering, but if some variables already exist in the target manager then the final ordering is adapted to the target manager. Please note, that indices of variables in the target manager may not be the same as in the source manager (for example, if source managet does not use initial ordering the indices in the target manager will follow the variable's ordering and not variable's original indices)

More info

Macro Biddy_Copy(MNG2,f) is defined for use with anonymous manager.
 
EXTERN void Biddy_Managed_CopyFormula (Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_String x)
 Function Biddy_Managed_CopyFormula uses Biddy_Managed_Copy to copy a graph from one manager to another manager which can use the same or different BDD type.

Description

See Biddy_Managed_Copy.

Side effects

If source and target manager are the same then function does nothing. The variable ordering of created BDD is adapted to the target manager. The created formula is refreshed but not preserved.

More info

Macro Biddy_CopyFormula(MNG2,x) is defined for use with anonymous manager.
 
EXTERN Biddy_Edge Biddy_Managed_ConstructBDD (Biddy_Manager MNG, int numV, Biddy_String varlist, int numN, Biddy_String nodelist)
 
EXTERN Biddy_Edge Biddy_Managed_Not (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_Not calculates Boolean function NOT. More...
 
EXTERN 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...
 
EXTERN Biddy_Edge Biddy_Managed_And (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_And calculates Boolean function AND (conjunction). More...
 
EXTERN Biddy_Edge Biddy_Managed_Or (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Or calculates Boolean function OR (disjunction). More...
 
EXTERN Biddy_Edge Biddy_Managed_Nand (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Nand calculates Boolean function NAND (Sheffer). More...
 
EXTERN Biddy_Edge Biddy_Managed_Nor (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Nor calculates Boolean function NOR (Peirce). More...
 
EXTERN Biddy_Edge Biddy_Managed_Xor (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Xor calculates Boolean function XOR. More...
 
EXTERN Biddy_Edge Biddy_Managed_Xnor (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Xnor calculates Boolean function XNOR. More...
 
EXTERN Biddy_Edge Biddy_Managed_Leq (Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
 Function Biddy_Managed_Leq calculates Boolean implication. More...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN 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...
 
EXTERN Biddy_Edge Biddy_Managed_CreateMinterm (Biddy_Manager MNG, Biddy_Edge support, long long unsigned int x)
 Function Biddy_Managed_CreateMinterm generates one minterm. More...
 
EXTERN 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...
 
EXTERN Biddy_Edge Biddy_Managed_RandomFunction (Biddy_Manager MNG, Biddy_Edge support, double r)
 Function Biddy_Managed_RandomFunction generates a random BDD. More...
 
EXTERN Biddy_Edge Biddy_Managed_RandomSet (Biddy_Manager MNG, Biddy_Edge unit, double r)
 Function Biddy_Managed_RandomSet generates a random BDD. More...
 
EXTERN unsigned int Biddy_Managed_CountNodes (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_CountNodes. More...
 
EXTERN unsigned int Biddy_MaxLevel (Biddy_Edge f)
 Function Biddy_MaxLevel. More...
 
EXTERN float Biddy_AvgLevel (Biddy_Edge f)
 Function Biddy_AvgLevel. More...
 
EXTERN Biddy_Variable Biddy_Managed_VariableTableNum (Biddy_Manager MNG)
 Function Biddy_Managed_VariableTableNum returns number of used variables. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableSize (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableSize returns the size of node table. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableBlockNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableBlockNumber. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableGenerated (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableGenerated. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableMax (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableMax returns maximal (peek) number of nodes in node table. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableNum (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableNum returns number of all nodes currently in node table. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableNumVar (Biddy_Manager MNG, Biddy_Variable v)
 Function Biddy_Managed_NodeTableNumVar returns number of nodes with a given variable currently in node table. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableResizeNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableResizeNumber. More...
 
EXTERN unsigned long long int Biddy_Managed_NodeTableFoaNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableFoaNumber. More...
 
EXTERN unsigned long long int Biddy_Managed_NodeTableFindNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableFindNumber. More...
 
EXTERN unsigned long long int Biddy_Managed_NodeTableCompareNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableCompareNumber. More...
 
EXTERN unsigned long long int Biddy_Managed_NodeTableAddNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableAddNumber. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableGCNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableGCNumber. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableGCTime (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableGCTime. More...
 
EXTERN unsigned long long int Biddy_Managed_NodeTableGCObsoleteNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableGCObsoleteNumber. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableSwapNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableSwapNumber. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableSiftingNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableSiftingNumber. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableDRTime (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableDRTime. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableITENumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableITENumber. More...
 
EXTERN unsigned long long int Biddy_Managed_NodeTableITERecursiveNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableITERecursiveNumber. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableANDORNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableANDORNumber. More...
 
EXTERN unsigned long long int Biddy_Managed_NodeTableANDORRecursiveNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableANDORRecursiveNumber. More...
 
EXTERN unsigned int Biddy_Managed_NodeTableXORNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableXORNumber. More...
 
EXTERN unsigned long long int Biddy_Managed_NodeTableXORRecursiveNumber (Biddy_Manager MNG)
 Function Biddy_Managed_NodeTableXORRecursiveNumber. More...
 
EXTERN unsigned int Biddy_Managed_FormulaTableNum (Biddy_Manager MNG)
 Function Biddy_Managed_FormulaTableNum returns number of known formulae. More...
 
EXTERN unsigned int Biddy_Managed_ListUsed (Biddy_Manager MNG)
 Function Biddy_Managed_ListUsed. More...
 
EXTERN unsigned int Biddy_Managed_ListMaxLength (Biddy_Manager MNG)
 Function Biddy_Managed_ListMaxLength. More...
 
EXTERN float Biddy_Managed_ListAvgLength (Biddy_Manager MNG)
 Function Biddy_Managed_ListAvgLength. More...
 
EXTERN unsigned long long int Biddy_Managed_OPCacheSearch (Biddy_Manager MNG)
 Function Biddy_Managed_OPCacheSearch. More...
 
EXTERN unsigned long long int Biddy_Managed_OPCacheFind (Biddy_Manager MNG)
 Function Biddy_Managed_OPCacheFind. More...
 
EXTERN unsigned long long int Biddy_Managed_OPCacheInsert (Biddy_Manager MNG)
 Function Biddy_Managed_OPCacheInsert. More...
 
EXTERN unsigned long long int Biddy_Managed_OPCacheOverwrite (Biddy_Manager MNG)
 Function Biddy_Managed_OPCacheOverwrite. More...
 
EXTERN unsigned int Biddy_Managed_CountNodesPlain (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_CountNodesPlain. More...
 
EXTERN unsigned int Biddy_Managed_DependentVariableNumber (Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean select)
 Function Biddy_Managed_DependentVariableNumber. More...
 
EXTERN unsigned int Biddy_Managed_CountComplementedEdges (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_CountComplementedEdges count the number of complemented edges. More...
 
EXTERN unsigned long long int Biddy_Managed_CountPaths (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_CountPaths count the number of 1-paths. More...
 
EXTERN double Biddy_Managed_CountMinterms (Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
 Function Biddy_Managed_CountMinterms. More...
 
EXTERN double Biddy_Managed_DensityOfFunction (Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
 Function Biddy_Managed_DensityOfFunction calculates the ratio of the number of on-set minterms to the number of all minterms. More...
 
EXTERN double Biddy_Managed_DensityOfBDD (Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
 Function Biddy_Managed_DensityOfBDD calculates the ratio of the number of on-set minterms to the number of nodes. More...
 
EXTERN unsigned int Biddy_Managed_MinNodes (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_MinNodes reports number of nodes in the optimal ordering. More...
 
EXTERN unsigned int Biddy_Managed_MaxNodes (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_MaxNodes reports number of nodes in the worst ordering. More...
 
EXTERN unsigned long long int Biddy_Managed_ReadMemoryInUse (Biddy_Manager MNG)
 Function Biddy_Managed_ReadMemoryInUse reports memory consumption of main data strucutures in bytes (nodes, node table, variable table, ordering table, formula table, ITE cache, EA cache, RC cache, REPLACEcache). More...
 
EXTERN void Biddy_Managed_PrintInfo (Biddy_Manager MNG, FILE *f)
 Function Biddy_Managed_PrintInfo prepares a file with stats. More...
 
EXTERN Biddy_String Biddy_Managed_Eval0 (Biddy_Manager MNG, Biddy_String s)
 Function Biddy_Managed_Eval0 evaluates raw format. More...
 
EXTERN Biddy_Edge Biddy_Managed_Eval1x (Biddy_Manager MNG, Biddy_String s, Biddy_LookupFunction lf)
 Function Biddy_Managed_Eval1x evaluates prefix AND-OR-EXOR-NOT format. More...
 
EXTERN Biddy_Edge Biddy_Managed_Eval2 (Biddy_Manager MNG, Biddy_String boolFunc)
 Function Biddy_Managed_Eval2 evaluates infix format. More...
 
EXTERN Biddy_String Biddy_Managed_ReadBddview (Biddy_Manager MNG, const char filename[], Biddy_String name)
 Function Biddy_Managed_ReadBddview reads bddview file and creates a Boolean function. More...
 
EXTERN void Biddy_Managed_ReadVerilogFile (Biddy_Manager MNG, const char filename[], Biddy_String prefix)
 Function Biddy_Managed_ReadVerilogFile reads Verilog file and creates variables for all primary inputs and Boolean functions for all primary outputs. More...
 
EXTERN void Biddy_Managed_PrintfBDD (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_PrintfBDD writes raw format using printf. More...
 
EXTERN void Biddy_Managed_WriteBDD (Biddy_Manager MNG, const char filename[], Biddy_Edge f, Biddy_String label)
 Function Biddy_Managed_WriteBDD writes raw format using fprintf. More...
 
EXTERN void Biddy_Managed_PrintfTable (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_PrintfTable writes truth table using printf. More...
 
EXTERN void Biddy_Managed_WriteTable (Biddy_Manager MNG, const char filename[], Biddy_Edge f)
 Function Biddy_Managed_WriteTable writes truth table using fprintf. More...
 
EXTERN void Biddy_Managed_PrintfSOP (Biddy_Manager MNG, Biddy_Edge f)
 Function Biddy_Managed_PrintfSOP writes SOP using printf. More...
 
EXTERN void Biddy_Managed_WriteSOP (Biddy_Manager MNG, const char filename[], Biddy_Edge f)
 Function Biddy_Managed_WriteSOP writes SOP using fprintf. More...
 
EXTERN unsigned int Biddy_Managed_WriteDot (Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], int id, Biddy_Boolean cudd)
 Function Biddy_Managed_WriteDot writes dot/graphviz format using fprintf. More...
 
EXTERN unsigned int Biddy_Managed_WriteBddview (Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], void *xytable)
 Function Biddy_Managed_WriteBDDView writes bddview format using fprintf. 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    [biddy.h]
Revision    [$Revision: 455 $]
Date        [$Date: 2018-07-14 12:11:54 +0200 (sob, 14 jul 2018) $]
Authors     [Robert Meolic (robert.meolic@um.si),
             Ales Casar (ales@homemade.net)]

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: biddyInt.h

Definition in file biddy.h.

Macro Definition Documentation

◆ Biddy_A

#define Biddy_A (   f,
 
)    Biddy_Managed_A(NULL,f,v)

Macro Biddy_A is defined for use with anonymous manager.

Definition at line 796 of file biddy.h.

◆ Biddy_AddCache

#define Biddy_AddCache (   gc)    Biddy_Managed_AddCache(NULL,gc)

Macro Biddy_AddCache is defined for use with anonymous manager.

Definition at line 608 of file biddy.h.

◆ Biddy_AddElementByName

#define Biddy_AddElementByName (   x)    Biddy_Managed_AddElementByName(NULL,x)

Macro Biddy_AddElementByName is defined for use with anonymous manager.

Definition at line 538 of file biddy.h.

◆ Biddy_AddFormula

#define Biddy_AddFormula (   x,
  f,
 
)    Biddy_Managed_AddFormula(NULL,x,f,c)

Macro Biddy_AddFormula is defined for use with anonymous manager.

Macros Biddy_Managed_AddTmpFormula, Biddy_AddTmpFormula,

Biddy_Managed_AddPersistentFormula, Biddy_AddPersistentFormula,

Biddy_Managed_KeepFormula, Biddy_KeepFormula,

Biddy_Managed_KeepFormulaProlonged, Biddy_KeepFormulaProlonged,

Biddy_Managed_KeepFormulaUntilPurge, and Biddy_KeepFormulaUntilPurge

are defined to simplify formulae management.

Definition at line 619 of file biddy.h.

◆ Biddy_AddVariableAbove

#define Biddy_AddVariableAbove (   v)    Biddy_Managed_AddVariableAbove(NULL,v)

Macro Biddy_AddVariableAbove is defined for use with anonymous manager.

Definition at line 550 of file biddy.h.

◆ Biddy_AddVariableBelow

#define Biddy_AddVariableBelow (   v)    Biddy_Managed_AddVariableBelow(NULL,v)

Macro Biddy_AddVariableBelow is defined for use with anonymous manager.

Definition at line 545 of file biddy.h.

◆ Biddy_AddVariableByName

#define Biddy_AddVariableByName (   x)    Biddy_Managed_AddVariableByName(NULL,x)

Macro Biddy_AddVariableByName is defined for use with anonymous manager.

Macros Biddy_Managed_AddVariable(MNG) and Biddy_AddVariable() are defined for creating numbered variables.

Macros Biddy_Managed_AddVariableEdge(MNG) and Biddy_AddVariableEdge() also create numbered variables but return the variable edge.

Definition at line 529 of file biddy.h.

◆ Biddy_And

#define Biddy_And (   f,
 
)    Biddy_Managed_And(NULL,f,g)

Macro Biddy_And is defined for use with anonymous manager.

Macros Biddy_Managed_Intersect and Biddy_Intersect are defined for set manipulation.

Definition at line 728 of file biddy.h.

◆ Biddy_AndAbstract

#define Biddy_AndAbstract (   f,
  g,
  cube 
)    Biddy_Managed_AndAbstract(NULL,f,g,cube)

Macro Biddy_AndAbstract is defined for use with anonymous manager.

Definition at line 816 of file biddy.h.

◆ Biddy_Change

#define Biddy_Change (   f,
 
)    Biddy_Managed_Change(NULL,f,v)

Macro Biddy_Change is defined for use with anonymous manager.

Definition at line 846 of file biddy.h.

◆ Biddy_ChangeVariableName

#define Biddy_ChangeVariableName (   v,
 
)    Biddy_Managed_ChangeVariableName(NULL,v,x)

Macro Biddy_ChangeVariableName is defined for use with anonymous manager.

Definition at line 522 of file biddy.h.

◆ Biddy_Clean

#define Biddy_Clean ( )    Biddy_Managed_Clean(NULL)

Macro Biddy_Clean is defined for use with anonymous manager.

Definition at line 588 of file biddy.h.

◆ Biddy_ClearMark

#define Biddy_ClearMark (   f)    (f = (Biddy_Edge) ((uintptr_t) f & ~((uintptr_t) 1)))

Biddy_ClearMark makes given edge not-complemented.

Definition at line 174 of file biddy.h.

◆ Biddy_ClearTag

#define Biddy_ClearTag (   f)    0

Biddy_ClearTag removes tag from the given edge, since Biddy v1.7.

Definition at line 216 of file biddy.h.

◆ Biddy_ClearVariablesData

#define Biddy_ClearVariablesData ( )    Biddy_Managed_ClearVariablesData(NULL)

Macro Biddy_ClearVariablesData is defined for use with anonymous manager.

Definition at line 477 of file biddy.h.

◆ Biddy_Complement

#define Biddy_Complement (   f)    ((Biddy_Edge) ((uintptr_t) f | (uintptr_t) 1))

Biddy_Complement returns complemented version of edge, since Biddy v1.4.

Definition at line 190 of file biddy.h.

◆ Biddy_Compose

#define Biddy_Compose (   f,
  g,
 
)    Biddy_Managed_Compose(NULL,f,g,v)

Macro Biddy_Compose is defined for use with anonymous manager.

Definition at line 786 of file biddy.h.

◆ Biddy_Constrain

#define Biddy_Constrain (   f,
 
)    Biddy_Managed_Constrain(NULL,f,c)

Macro Biddy_Constrain is defined for use with anonymous manager.

Definition at line 821 of file biddy.h.

◆ Biddy_ConstructBDD

#define Biddy_ConstructBDD (   numV,
  varlist,
  numN,
  nodelist 
)    Biddy_Managed_ConstructBDD(NULL,numV,varlist,numV,nodelist)

Macro Biddy_ConstructBDD is defined for use with anonymous manager.

Definition at line 699 of file biddy.h.

◆ Biddy_Copy

#define Biddy_Copy (   MNG2,
 
)    Biddy_Managed_Copy(NULL,MNG2,f)

Macro Biddy_Copy is defined for use with anonymous manager.

Definition at line 689 of file biddy.h.

◆ Biddy_CopyFormula

#define Biddy_CopyFormula (   MNG2,
 
)    Biddy_Managed_CopyFormula(NULL,MNG2,x)

Macro Biddy_CopyFormula is defined for use with anonymous manager.

Definition at line 694 of file biddy.h.

◆ Biddy_CountComplementedEdges

#define Biddy_CountComplementedEdges (   f)    Biddy_Managed_CountComplementedEdges(NULL,f)

Macro Biddy_CountComplementedEdges is defined for use with anonymous manager.

Definition at line 1082 of file biddy.h.

◆ Biddy_CountMinterms

#define Biddy_CountMinterms (   f,
  nvars 
)    Biddy_Managed_CountMinterms(NULL,f,nvars)

Macro Biddy_CountMinterms is defined for use with anonymous manager.

Definition at line 1092 of file biddy.h.

◆ Biddy_CountNodes

#define Biddy_CountNodes (   f)    Biddy_Managed_CountNodes(NULL,f)

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

Definition at line 897 of file biddy.h.

◆ Biddy_CountNodesPlain

#define Biddy_CountNodesPlain (   f)    Biddy_Managed_CountNodesPlain(NULL,f)

Macro Biddy_CountNodesPlain is defined for use with anonymous manager.

Definition at line 1072 of file biddy.h.

◆ Biddy_CountPaths

#define Biddy_CountPaths (   f)    Biddy_Managed_CountPaths(NULL,f)

Macro Biddy_CountPaths is defined for use with anonymous manager.

Definition at line 1087 of file biddy.h.

◆ Biddy_CreateFunction

#define Biddy_CreateFunction (   support,
 
)    Biddy_Managed_CreateFunction(NULL,support,x)

Macro Biddy_CreateFunction is defined for use with anonymous manager.

Definition at line 866 of file biddy.h.

◆ Biddy_CreateMinterm

#define Biddy_CreateMinterm (   support,
 
)    Biddy_Managed_CreateMinterm(NULL,support,x)

Macro Biddy_CreateMinterm is defined for use with anonymous manager.

Definition at line 861 of file biddy.h.

◆ Biddy_DeleteFormula

#define Biddy_DeleteFormula (   x)    Biddy_Managed_DeleteFormula(NULL,x)

Macro Biddy_DeleteFormula is defined for use with anonymous manager.

Definition at line 639 of file biddy.h.

◆ Biddy_DeleteIthFormula

#define Biddy_DeleteIthFormula (   x)    Biddy_Managed_DeleteIthFormula(NULL,x)

Macro Biddy_DeleteIthFormula is defined for use with anonymous manager.

Definition at line 644 of file biddy.h.

◆ Biddy_DensityOfBDD

#define Biddy_DensityOfBDD (   f,
  nvars 
)    Biddy_Managed_DensityOfBDD(NULL,f,nvars)

Macro Biddy_DensityOfBDD is defined for use with anonymous manager.

Definition at line 1104 of file biddy.h.

◆ Biddy_DensityOfFunction

#define Biddy_DensityOfFunction (   f,
  nvars 
)    Biddy_Managed_DensityOfFunction(NULL,f,nvars)

Macro Biddy_DensityOfFunction is defined for use with anonymous manager.

Definition at line 1099 of file biddy.h.

◆ Biddy_DependentVariableNumber

#define Biddy_DependentVariableNumber (   f,
  select 
)    Biddy_Managed_DependentVariableNumber(NULL,f,select)

Macro Biddy_DependentVariableNumber is defined for use with anonymous manager.

Definition at line 1077 of file biddy.h.

◆ Biddy_DeselectAll

#define Biddy_DeselectAll ( )    Biddy_Managed_DeselectAll(NULL)

Macro Biddy_DeselectAll is defined for use with anonymous manager.

Definition at line 378 of file biddy.h.

◆ Biddy_DeselectNode

#define Biddy_DeselectNode (   f)    Biddy_Managed_DeselectNode(NULL,f)

Macro Biddy_DeselectNode is defined for use with anonymous manager.

Definition at line 363 of file biddy.h.

◆ Biddy_E

#define Biddy_E (   f,
 
)    Biddy_Managed_E(NULL,f,v)

Macro Biddy_E is defined for use with anonymous manager.

Definition at line 791 of file biddy.h.

◆ Biddy_Eval

#define Biddy_Eval (   f)    Biddy_Managed_Eval(NULL,f)

Macro Biddy_Eval is defined for use with anonymous manager.

Definition at line 492 of file biddy.h.

◆ Biddy_Eval0

#define Biddy_Eval0 (   s)    Biddy_Managed_Eval0(NULL,s)

Macro Biddy_Eval0 is defined for use with anonymous manager.

Definition at line 1141 of file biddy.h.

◆ Biddy_Eval1x

#define Biddy_Eval1x (   s,
  lf 
)    Biddy_Managed_Eval1x(NULL,s,lf)

Macro Biddy_Eval1x is defined for use with anonymous manager.

Definition at line 1146 of file biddy.h.

◆ Biddy_Eval2

#define Biddy_Eval2 (   boolFunc)    Biddy_Managed_Eval2(NULL,boolFunc)

Macro Biddy_Eval2 is defined for use with anonymous manager.

Definition at line 1153 of file biddy.h.

◆ Biddy_EvalProbability

#define Biddy_EvalProbability (   f)    Biddy_Managed_EvalProbability(NULL,f)

Macro Biddy_EvalProbability is defined for use with anonymous manager.

Definition at line 497 of file biddy.h.

◆ Biddy_ExistAbstract

#define Biddy_ExistAbstract (   f,
  cube 
)    Biddy_Managed_ExistAbstract(NULL,f,cube)

Macro Biddy_ExistAbstract is defined for use with anonymous manager.

Definition at line 806 of file biddy.h.

◆ Biddy_Exit

#define Biddy_Exit ( )    Biddy_ExitMNG(NULL)

Macro Biddy_Exit will delete anonymous manager.

Definition at line 315 of file biddy.h.

◆ Biddy_FindFormula

#define Biddy_FindFormula (   x,
  idx,
 
)    Biddy_Managed_FindFormula(NULL,x,idx,f)

Macro Biddy_FindFormula is defined for use with anonymous manager.

Definition at line 634 of file biddy.h.

◆ Biddy_FoaVariable

#define Biddy_FoaVariable (   x,
  varelem 
)    Biddy_Managed_FoaVariable(NULL,x,varelem)

Macro Biddy_FoaVariable is defined for use with anonymous manager.

Definition at line 517 of file biddy.h.

◆ Biddy_FormulaTableNum

#define Biddy_FormulaTableNum ( )    Biddy_Managed_FormulaTableNum(NULL)

Macro Biddy_FormulaTableNum is defined for use with anonymous manager.

Definition at line 1032 of file biddy.h.

◆ Biddy_GC

#define Biddy_GC (   targetLT,
  targetGEQ,
  purge,
  total 
)    Biddy_Managed_GC(NULL,targetLT,targetGEQ,purge,total)

Macro Biddy_GC is defined for use with anonymous manager.

Macros Biddy_Managed_AutoGC, Biddy_AutoGC, Biddy_Managed_ForceGC, and Biddy_ForceGC are useful variants.

Definition at line 579 of file biddy.h.

◆ Biddy_GetBaseSet

#define Biddy_GetBaseSet ( )    Biddy_Managed_GetBaseSet(NULL)

Macro Biddy_GetBaseSet is defined for use with anonymous manager.

Definition at line 402 of file biddy.h.

◆ Biddy_GetConstantOne

#define Biddy_GetConstantOne ( )    Biddy_Managed_GetConstantOne(NULL)

Macro Biddy_GetConstantOne is defined for use with anonymous manager.

Definition at line 395 of file biddy.h.

◆ Biddy_GetConstantZero

#define Biddy_GetConstantZero ( )    Biddy_Managed_GetConstantZero(NULL)

Macro Biddy_GetConstantZero is defined for use with anonymous manager.

Definition at line 388 of file biddy.h.

◆ Biddy_GetElementEdge

#define Biddy_GetElementEdge (   v)    Biddy_Managed_GetElementEdge(NULL,v)

Macro Biddy_GetElementEdge is defined for use with anonymous manager.

Definition at line 437 of file biddy.h.

◆ Biddy_GetIthFormula

#define Biddy_GetIthFormula (   i)    Biddy_Managed_GetIthFormula(NULL,i)

Macro Biddy_GetIthFormula is defined for use with anonymous manager.

Definition at line 649 of file biddy.h.

◆ Biddy_GetIthFormulaName

#define Biddy_GetIthFormulaName (   i)    Biddy_Managed_GetIthFormulaName(NULL,i)

Macro Biddy_GetIthFormulaName is defined for use with anonymous manager.

Definition at line 654 of file biddy.h.

◆ Biddy_GetIthVariable

#define Biddy_GetIthVariable (   i)    Biddy_Managed_GetIthVariable(NULL,i)

Macro Biddy_GetIthVariable is defined for use with anonymous manager.

Definition at line 417 of file biddy.h.

◆ Biddy_GetLowestVariable

#define Biddy_GetLowestVariable ( )    Biddy_Managed_GetLowestVariable(NULL)

Macro Biddy_GetLowestVariable is defined for use with anonymous manager.

Definition at line 412 of file biddy.h.

◆ Biddy_GetManagerName

#define Biddy_GetManagerName ( )    Biddy_Managed_GetManagerName(NULL)

Macro Biddy_GetManagerName is defined for use with anonymous manager.

Definition at line 328 of file biddy.h.

◆ Biddy_GetManagerType

#define Biddy_GetManagerType ( )    Biddy_Managed_GetManagerType(NULL)

Macro Biddy_GetManagerType is defined for use with anonymous manager.

Definition at line 323 of file biddy.h.

◆ Biddy_GetMark

#define Biddy_GetMark (   f)    (((uintptr_t) f & (uintptr_t) 1) != 0)

Biddy_GetMark returns TRUE iff given edge is complemented.

Definition at line 168 of file biddy.h.

◆ Biddy_GetNextVariable

#define Biddy_GetNextVariable (   v)    Biddy_Managed_GetNextVariable(NULL,v)

Macro Biddy_GetNextVariable is defined for use with anonymous manager.

Definition at line 427 of file biddy.h.

◆ Biddy_GetPrevVariable

#define Biddy_GetPrevVariable (   v)    Biddy_Managed_GetPrevVariable(NULL,v)

Macro Biddy_GetPrevVariable is defined for use with anonymous manager.

Definition at line 422 of file biddy.h.

◆ Biddy_GetTag

#define Biddy_GetTag (   f)    0

Biddy_GetTag returns tag used for the given edge, since Biddy v1.7.

Definition at line 199 of file biddy.h.

◆ Biddy_GetTerminal

#define Biddy_GetTerminal ( )    Biddy_Managed_GetTerminal(NULL)

Macro Biddy_GetTerminal is defined for use with anonymous manager.

Definition at line 383 of file biddy.h.

◆ Biddy_GetTopVariableChar

#define Biddy_GetTopVariableChar (   f)    Biddy_Managed_GetTopVariableChar(NULL,f)

Macro Biddy_GetTopVariableChar is defined for use with anonymous manager.

Definition at line 457 of file biddy.h.

◆ Biddy_GetTopVariableEdge

#define Biddy_GetTopVariableEdge (   f)    Biddy_Managed_GetTopVariableEdge(NULL,f)

Macro Biddy_GetTopVariableEdge is defined for use with anonymous manager.

Definition at line 447 of file biddy.h.

◆ Biddy_GetTopVariableName

#define Biddy_GetTopVariableName (   f)    Biddy_Managed_GetTopVariableName(NULL,f)

Macro Biddy_GetTopVariableName is defined for use with anonymous manager.

Definition at line 452 of file biddy.h.

◆ Biddy_GetVariable

#define Biddy_GetVariable (   x)    Biddy_Managed_GetVariable(NULL,x)

Macro Biddy_GetVariable is defined for use with anonymous manager.

Definition at line 407 of file biddy.h.

◆ Biddy_GetVariableData

#define Biddy_GetVariableData (   v)    Biddy_Managed_GetVariableData(NULL,v)

Macro Biddy_GetVariableData is defined for use with anonymous manager.

Definition at line 487 of file biddy.h.

◆ Biddy_GetVariableEdge

#define Biddy_GetVariableEdge (   v)    Biddy_Managed_GetVariableEdge(NULL,v)

Macro Biddy_GetVariableEdge is defined for use with anonymous manager.

Definition at line 432 of file biddy.h.

◆ Biddy_GetVariableName

#define Biddy_GetVariableName (   v)    Biddy_Managed_GetVariableName(NULL,v)

Macro Biddy_GetVariableName is defined for use with anonymous manager.

Definition at line 442 of file biddy.h.

◆ Biddy_GetVariableValue

#define Biddy_GetVariableValue (   v)    Biddy_Managed_GetVariableValue(NULL,v)

Macro Biddy_GetVariableValue is defined for use with anonymous manager.

Definition at line 472 of file biddy.h.

◆ Biddy_Gt

#define Biddy_Gt (   f,
 
)    Biddy_Managed_Gt(NULL,f,g)

Macro Biddy_Gt is defined for use with anonymous manager.

Definition at line 768 of file biddy.h.

◆ Biddy_IncTag

#define Biddy_IncTag (   f)    Biddy_Managed_IncTag(NULL,f)

Macro Biddy_IncTag is defined for use with anonymous manager.

Definition at line 561 of file biddy.h.

◆ Biddy_Init

#define Biddy_Init ( )    Biddy_InitMNG(NULL,BIDDYTYPEOBDDC)

Macros Biddy_Init and Biddy_InitAnonymous will initialize anonymous manager.

Definition at line 309 of file biddy.h.

◆ Biddy_Inv

#define Biddy_Inv (   f)    ((Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1))

Biddy_Inv returns edge with changed complement bit.

Definition at line 181 of file biddy.h.

◆ Biddy_InvCond

#define Biddy_InvCond (   f,
 
)    (c ? ((Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1)) : f)

Biddy_InvCond returns edge with conditinonaly changed complement bit.

Definition at line 184 of file biddy.h.

◆ Biddy_InvertMark

#define Biddy_InvertMark (   f)    (f = (Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1))

Biddy_InvertMark changes complement bit of the given edge.

Definition at line 177 of file biddy.h.

◆ Biddy_IsEqv

#define Biddy_IsEqv (   f1,
  MNG2,
  f2 
)    Biddy_Managed_IsEqv(NULL,f1,MNG2,f2)

Macro Biddy_IsEqv is defined for use with anonymous manager.

Definition at line 353 of file biddy.h.

◆ Biddy_IsEqvPointer

#define Biddy_IsEqvPointer (   f,
 
)    (((uintptr_t) f & ~((uintptr_t) 1)) == ((uintptr_t) g & ~((uintptr_t) 1)))

Biddy_IsEqvPointer returns TRUE iff given edges points to the same node.

Definition at line 165 of file biddy.h.

◆ Biddy_IsHighest

#define Biddy_IsHighest (   v)    Biddy_Managed_IsHighest(NULL,v)

Macro Biddy_IsHighest is defined for use with anonymous manager.

Definition at line 512 of file biddy.h.

◆ Biddy_IsLeq

#define Biddy_IsLeq (   f,
 
)    Biddy_Managed_IsLeq(NULL,f,g)

Macro Biddy_IsLeq is defined for use with anonymous manager.

Definition at line 775 of file biddy.h.

◆ Biddy_IsLowest

#define Biddy_IsLowest (   v)    Biddy_Managed_IsLowest(NULL,v)

Macro Biddy_IsLowest is defined for use with anonymous manager.

Definition at line 507 of file biddy.h.

◆ Biddy_IsNull

#define Biddy_IsNull (   f)    (f == NULL)

Biddy_IsNull returns TRUE iff given BDD is a null edge.

Definition at line 150 of file biddy.h.

◆ Biddy_IsOK

#define Biddy_IsOK (   f)    Biddy_Managed_IsOK(NULL,f)

Macro Biddy_IsOK is defined for use with anonymous manager.

Definition at line 573 of file biddy.h.

◆ Biddy_IsSelected

#define Biddy_IsSelected (   f)    Biddy_Managed_IsSelected(NULL,f)

Macro Biddy_IsSelected is defined for use with anonymous manager.

Definition at line 368 of file biddy.h.

◆ Biddy_IsSmaller

#define Biddy_IsSmaller (   fv,
  gv 
)    Biddy_Managed_IsSmaller(NULL,fv,gv)

Macro Biddy_IsSmaller is defined for use with anonymous manager.

Definition at line 502 of file biddy.h.

◆ Biddy_IsTerminal

#define Biddy_IsTerminal (   f)    ((((void**)((uintptr_t) f & ~((uintptr_t) 1)))[2] == NULL) && (((void**)((uintptr_t) f & ~((uintptr_t) 1)))[3] == NULL))

Biddy_IsTerminal returns TRUE iff given edge points to the terminal node.

Definition at line 160 of file biddy.h.

◆ Biddy_IsVariableDependent

#define Biddy_IsVariableDependent (   f,
 
)    Biddy_Managed_IsVariableDependent(NULL,f,v)

Macro Biddy_IsVariableDependent is defined for use with anonymous manager.

Definition at line 801 of file biddy.h.

◆ Biddy_ITE

#define Biddy_ITE (   f,
  g,
 
)    Biddy_Managed_ITE(NULL,f,g,h)

Macro Biddy_ITE is defined for use with anonymous manager.

Definition at line 722 of file biddy.h.

◆ Biddy_Leq

#define Biddy_Leq (   f,
 
)    Biddy_Managed_Leq(NULL,f,g)

Macro Biddy_Leq is defined for use with anonymous manager.

Definition at line 763 of file biddy.h.

◆ Biddy_ListAvgLength

#define Biddy_ListAvgLength ( )    Biddy_Managed_ListAvgLength(NULL)

Macro Biddy_ListAvgLength is defined for use with anonymous manager.

Definition at line 1047 of file biddy.h.

◆ Biddy_ListMaxLength

#define Biddy_ListMaxLength ( )    Biddy_Managed_ListMaxLength(NULL)

Macro Biddy_ListMaxLength is defined for use with anonymous manager.

Definition at line 1042 of file biddy.h.

◆ Biddy_ListUsed

#define Biddy_ListUsed ( )    Biddy_Managed_ListUsed(NULL)

Macro Biddy_ListUsed is defined for use with anonymous manager.

Definition at line 1037 of file biddy.h.

◆ Biddy_Managed_AvgLevel

#define Biddy_Managed_AvgLevel (   MNG,
 
)    Biddy_AvgLevel(f)

Macro Biddy_Managed_AvgLevel(MNG,f) is defined for your convenience.

Definition at line 907 of file biddy.h.

◆ Biddy_Managed_GetElse

#define Biddy_Managed_GetElse (   MNG,
 
)    Biddy_GetElse(f)

Macro Biddy_Managed_GetElse is defined for your convenience.

Definition at line 343 of file biddy.h.

◆ Biddy_Managed_GetThen

#define Biddy_Managed_GetThen (   MNG,
 
)    Biddy_GetThen(f)

Macro Biddy_Managed_GetThen is defined for your convenience.

Definition at line 338 of file biddy.h.

◆ Biddy_Managed_GetTopVariable

#define Biddy_Managed_GetTopVariable (   MNG,
 
)    Biddy_GetTopVariable(f)

Macro Biddy_Managed_GetTopVariable is defined for your convenience.

Definition at line 348 of file biddy.h.

◆ Biddy_Managed_MaxLevel

#define Biddy_Managed_MaxLevel (   MNG,
 
)    Biddy_MaxLevel(f)

Macro Biddy_Managed_MaxLevel(MNG,f) is defined for your convenience.

Definition at line 902 of file biddy.h.

◆ Biddy_MaximizeBDD

#define Biddy_MaximizeBDD (   f)    Biddy_Managed_MaximizeBDD(NULL,f)

Macro Biddy_MaximizeBDD is defined for use with anonymous manager.

Definition at line 684 of file biddy.h.

◆ Biddy_MaxNodes

#define Biddy_MaxNodes (   f)    Biddy_Managed_MaxNodes(NULL,f)

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

Definition at line 1114 of file biddy.h.

◆ Biddy_MinimizeBDD

#define Biddy_MinimizeBDD (   f)    Biddy_Managed_MinimizeBDD(NULL,f)

Macro Biddy_MinimizeBDD is defined for use with anonymous manager.

Definition at line 679 of file biddy.h.

◆ Biddy_MinNodes

#define Biddy_MinNodes (   f)    Biddy_Managed_MinNodes(NULL,f)

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

Definition at line 1109 of file biddy.h.

◆ Biddy_Nand

#define Biddy_Nand (   f,
 
)    Biddy_Managed_Nand(NULL,f,g)

Macro Biddy_Nand is defined for use with anonymous manager.

Definition at line 743 of file biddy.h.

◆ Biddy_NodeTableAddNumber

#define Biddy_NodeTableAddNumber ( )    Biddy_Managed_NodeTableAddNumber(NULL)

Macro Biddy_NodeTableAddNumber is defined for use with anonymous manager.

Definition at line 967 of file biddy.h.

◆ Biddy_NodeTableANDORNumber

#define Biddy_NodeTableANDORNumber ( )    Biddy_Managed_NodeTableANDORNumber(NULL)

Macro Biddy_NodeTableANDORNumber is defined for use with anonymous manager.

Definition at line 1012 of file biddy.h.

◆ Biddy_NodeTableANDORRecursiveNumber

#define Biddy_NodeTableANDORRecursiveNumber ( )    Biddy_Managed_NodeTableANDORRecursiveNumber(NULL)

Macro Biddy_NodeTableANDORRecursiveNumber is defined for use with anonymous manager.

Definition at line 1017 of file biddy.h.

◆ Biddy_NodeTableBlockNumber

#define Biddy_NodeTableBlockNumber ( )    Biddy_Managed_NodeTableBlockNumber(NULL)

Macro Biddy_NodeTableBlockNumber is defined for use with anonymous manager.

Definition at line 922 of file biddy.h.

◆ Biddy_NodeTableCompareNumber

#define Biddy_NodeTableCompareNumber ( )    Biddy_Managed_NodeTableCompareNumber(NULL)

Macro Biddy_NodeTableCompareNumber is defined for use with anonymous manager.

Definition at line 962 of file biddy.h.

◆ Biddy_NodeTableDRTime

#define Biddy_NodeTableDRTime ( )    Biddy_Managed_NodeTableDRTime(NULL)

Macro Biddy_NodeTableDRTime is defined for use with anonymous manager.

Definition at line 997 of file biddy.h.

◆ Biddy_NodeTableFindNumber

#define Biddy_NodeTableFindNumber ( )    Biddy_Managed_NodeTableFindNumber(NULL)

Macro Biddy_NodeTableFindNumber is defined for use with anonymous manager.

Definition at line 957 of file biddy.h.

◆ Biddy_NodeTableFoaNumber

#define Biddy_NodeTableFoaNumber ( )    Biddy_Managed_NodeTableFoaNumber(NULL)

Macro Biddy_NodeTableFoaNumber is defined for use with anonymous manager.

Definition at line 952 of file biddy.h.

◆ Biddy_NodeTableGCNumber

#define Biddy_NodeTableGCNumber ( )    Biddy_Managed_NodeTableGCNumber(NULL)

Macro Biddy_NodeTableGCNumber is defined for use with anonymous manager.

Definition at line 972 of file biddy.h.

◆ Biddy_NodeTableGCObsoleteNumber

#define Biddy_NodeTableGCObsoleteNumber ( )    Biddy_Managed_NodeTableGCObsoleteNumber(NULL)

Macro Biddy_NodeTableGCObsoleteNumber is defined for use with anonymous manager.

Definition at line 982 of file biddy.h.

◆ Biddy_NodeTableGCTime

#define Biddy_NodeTableGCTime ( )    Biddy_Managed_NodeTableGCTime(NULL)

Macro Biddy_NodeTableGCTime is defined for use with anonymous manager.

Definition at line 977 of file biddy.h.

◆ Biddy_NodeTableGenerated

#define Biddy_NodeTableGenerated ( )    Biddy_Managed_NodeTableGenerated(NULL)

Macro Biddy_NodeTableGenerated is defined for use with anonymous manager.

Definition at line 927 of file biddy.h.

◆ Biddy_NodeTableITENumber

#define Biddy_NodeTableITENumber ( )    Biddy_Managed_NodeTableITENumber(NULL)

Macro Biddy_NodeTableITENumber is defined for use with anonymous manager.

Definition at line 1002 of file biddy.h.

◆ Biddy_NodeTableITERecursiveNumber

#define Biddy_NodeTableITERecursiveNumber ( )    Biddy_Managed_NodeTableITERecursiveNumber(NULL)

Macro Biddy_NodeTableITERecursiveNumber is defined for use with anonymous manager.

Definition at line 1007 of file biddy.h.

◆ Biddy_NodeTableMax

#define Biddy_NodeTableMax ( )    Biddy_Managed_NodeTableMax(NULL)

Macro Biddy_NodeTableMax is defined for use with anonymous manager.

Definition at line 932 of file biddy.h.

◆ Biddy_NodeTableNum

#define Biddy_NodeTableNum ( )    Biddy_Managed_NodeTableNum(NULL)

Macro Biddy_NodeTableNum is defined for use with anonymous manager.

Definition at line 937 of file biddy.h.

◆ Biddy_NodeTableNumVar

#define Biddy_NodeTableNumVar (   v)    Biddy_Managed_NodeTableNumVar(NULL,v)

Macro Biddy_NodeTableNumVar is defined for use with anonymous manager.

Definition at line 942 of file biddy.h.

◆ Biddy_NodeTableResizeNumber

#define Biddy_NodeTableResizeNumber ( )    Biddy_Managed_NodeTableResizeNumber(NULL)

Macro Biddy_NodeTableResizeNumber is defined for use with anonymous manager.

Definition at line 947 of file biddy.h.

◆ Biddy_NodeTableSiftingNumber

#define Biddy_NodeTableSiftingNumber ( )    Biddy_Managed_NodeTableSiftingNumber(NULL)

Macro Biddy_NodeTableSiftingNumber is defined for use with anonymous manager.

Definition at line 992 of file biddy.h.

◆ Biddy_NodeTableSize

#define Biddy_NodeTableSize ( )    Biddy_Managed_NodeTableSize(NULL)

Macro Biddy_NodeTableSize is defined for use with anonymous manager.

Definition at line 917 of file biddy.h.

◆ Biddy_NodeTableSwapNumber

#define Biddy_NodeTableSwapNumber ( )    Biddy_Managed_NodeTableSwapNumber(NULL)

Macro Biddy_NodeTableSwapNumber is defined for use with anonymous manager.

Definition at line 987 of file biddy.h.

◆ Biddy_NodeTableXORNumber

#define Biddy_NodeTableXORNumber ( )    Biddy_Managed_NodeTableXORNumber(NULL)

Macro Biddy_NodeTableXORNumber is defined for use with anonymous manager.

Definition at line 1022 of file biddy.h.

◆ Biddy_NodeTableXORRecursiveNumber

#define Biddy_NodeTableXORRecursiveNumber ( )    Biddy_Managed_NodeTableXORRecursiveNumber(NULL)

Macro Biddy_NodeTableXORRecursiveNumber is defined for use with anonymous manager.

Definition at line 1027 of file biddy.h.

◆ Biddy_Nor

#define Biddy_Nor (   f,
 
)    Biddy_Managed_Nor(NULL,f,g)

Macro Biddy_Nor is defined for use with anonymous manager.

Definition at line 748 of file biddy.h.

◆ Biddy_Not

#define Biddy_Not (   f)    Biddy_Managed_Not(NULL,f)

Macro Biddy_Not is defined for use with anonymous manager.

For OBDD and OFDD, use macro Biddy_Inv.

Definition at line 717 of file biddy.h.

◆ Biddy_OPCacheFind

#define Biddy_OPCacheFind ( )    Biddy_Managed_OPCacheFind(NULL)

Macro Biddy_OPCacheFind is defined for use with anonymous manager.

Definition at line 1057 of file biddy.h.

◆ Biddy_OPCacheInsert

#define Biddy_OPCacheInsert ( )    Biddy_Managed_OPCacheInsert(NULL)

Macro Biddy_OPCacheInsert is defined for use with anonymous manager.

Definition at line 1062 of file biddy.h.

◆ Biddy_OPCacheOverwrite

#define Biddy_OPCacheOverwrite ( )    Biddy_Managed_OPCacheOverwrite(NULL)

Macro Biddy_OPCacheOverwrite is defined for use with anonymous manager.

Definition at line 1067 of file biddy.h.

◆ Biddy_OPCacheSearch

#define Biddy_OPCacheSearch ( )    Biddy_Managed_OPCacheSearch(NULL)

Macro Biddy_OPCacheSearch is defined for use with anonymous manager.

Definition at line 1052 of file biddy.h.

◆ Biddy_Or

#define Biddy_Or (   f,
 
)    Biddy_Managed_Or(NULL,f,g)

Macro Biddy_Or is defined for use with anonymous manager.

Macros Biddy_Managed_Union and Biddy_Union are defined for set manipulation.

Definition at line 736 of file biddy.h.

◆ Biddy_PrintfBDD

#define Biddy_PrintfBDD (   f)    Biddy_Managed_PrintfBDD(NULL,f)

Macro Biddy_PrintfBDD is defined for use with anonymous manager.

Definition at line 1168 of file biddy.h.

◆ Biddy_PrintfSOP

#define Biddy_PrintfSOP (   f)    Biddy_Managed_PrintfSOP(NULL,f)

Macro Biddy_PrintfSOP is defined for use with anonymous manager.

Definition at line 1188 of file biddy.h.

◆ Biddy_PrintfTable

#define Biddy_PrintfTable (   f)    Biddy_Managed_PrintfTable(NULL,f)

Macro Biddy_PrintfTable is defined for use with anonymous manager.

Definition at line 1178 of file biddy.h.

◆ Biddy_PrintInfo

#define Biddy_PrintInfo (   f)    Biddy_Managed_PrintInfo(NULL,f)

Macro Biddy_PrintInfo is defined for use with anonymous manager.

Definition at line 1124 of file biddy.h.

◆ Biddy_Purge

#define Biddy_Purge ( )    Biddy_Managed_Purge(NULL)

Macro Biddy_Purge is defined for use with anonymous manager.

Definition at line 593 of file biddy.h.

◆ Biddy_PurgeAndReorder

#define Biddy_PurgeAndReorder (   f,
 
)    Biddy_Managed_PurgeAndReorder(NULL,f,c)

Macro Biddy_PurgeAndReorder is defined for use with anonymous manager.

Definition at line 598 of file biddy.h.

◆ Biddy_RandomFunction

#define Biddy_RandomFunction (   support,
 
)    Biddy_Managed_RandomFunction(NULL,support,r)

Macro Biddy_RandomFunction is defined for use with anonymous manager.

Definition at line 871 of file biddy.h.

◆ Biddy_RandomSet

#define Biddy_RandomSet (   unit,
 
)    Biddy_Managed_RandomSet(NULL,unit,r)

Macro Biddy_RandomSet is defined for use with anonymous manager.

Definition at line 876 of file biddy.h.

◆ Biddy_ReadBddview

#define Biddy_ReadBddview (   filename,
  name 
)    Biddy_Managed_ReadBddview(NULL,filename,name)

Macro Biddy_ReadBddview is defined for use with anonymous manager.

Definition at line 1158 of file biddy.h.

◆ Biddy_ReadMemoryInUse

#define Biddy_ReadMemoryInUse ( )    Biddy_Managed_ReadMemoryInUse(NULL)

Macro Biddy_ReadMemoryInUse is defined for use with anonymous manager.

Definition at line 1119 of file biddy.h.

◆ Biddy_ReadVerilogFile

#define Biddy_ReadVerilogFile (   filename,
  prefix 
)    Biddy_Managed_ReadVerilogFile(NULL,filename,prefix)

Macro Biddy_ReadVerilogFile is defined for use with anonymous manager.

Definition at line 1163 of file biddy.h.

◆ Biddy_Refresh

#define Biddy_Refresh (   f)    Biddy_Managed_Refresh(NULL,f)

Macro Biddy_Refresh is defined for use with anonymous manager.

Definition at line 603 of file biddy.h.

◆ Biddy_Regular

#define Biddy_Regular (   f)    ((Biddy_Edge) ((uintptr_t) f & ~((uintptr_t) 1)))

Biddy_Regular returns not-complemented version of edge, since Biddy v1.4.

Definition at line 187 of file biddy.h.

◆ Biddy_ReplaceByKeyword

#define Biddy_ReplaceByKeyword (   f,
  keyword 
)    Biddy_Managed_ReplaceByKeyword(NULL,f,keyword)

Macro Biddy_ReplaceByKeyword is defined for use with anonymous manager.

Macros Biddy_Managed_Replace and Biddy_Replace are variants

with less effective cache table

Definition at line 839 of file biddy.h.

◆ Biddy_ResetVariablesValue

#define Biddy_ResetVariablesValue ( )    Biddy_Managed_ResetVariablesValue(NULL)

Macro Biddy_ResetVariablesValue is defined for use with anonymous manager.

Definition at line 462 of file biddy.h.

◆ Biddy_Restrict

#define Biddy_Restrict (   f,
  v,
  value 
)    Biddy_Managed_Restrict(NULL,f,v,value)

Macro Biddy_Restrict is defined for use with anonymous manager.

Definition at line 781 of file biddy.h.

◆ Biddy_SelectFunction

#define Biddy_SelectFunction (   f)    Biddy_Managed_SelectFunction(NULL,f)

Macro Biddy_SelectFunction is defined for use with anonymous manager.

Definition at line 373 of file biddy.h.

◆ Biddy_SelectNode

#define Biddy_SelectNode (   f)    Biddy_Managed_SelectNode(NULL,f)

Macro Biddy_SelectNode is defined for use with anonymous manager.

Definition at line 358 of file biddy.h.

◆ Biddy_SetAlphabeticOrdering

#define Biddy_SetAlphabeticOrdering ( )    Biddy_Managed_SetAlphabeticOrdering(NULL)

Macro Biddy_SetAlphabeticOrdering is defined for use with anonymous manager.

Definition at line 659 of file biddy.h.

◆ Biddy_SetManagerParameters

#define Biddy_SetManagerParameters (   gcr,
  gcrF,
  gcrX,
  rr,
  rrF,
  rrX,
  st,
  cst 
)    Biddy_Managed_SetManagerParameters(NULL,gcr,gcrF,gcrX,rr,rrF,rrX,st,cst)

Macro Biddy_SetManagerParameters is defined for use with anonymous manager.

Definition at line 333 of file biddy.h.

◆ Biddy_SetMark

#define Biddy_SetMark (   f)    (f = (Biddy_Edge) ((uintptr_t) f | (uintptr_t) 1))

Biddy_SetMark makes given edge complemented.

Definition at line 171 of file biddy.h.

◆ Biddy_SetTag

#define Biddy_SetTag (   f,
 
)    0

Biddy_SetTag adds tag to the given edge, since Biddy v1.7.

Definition at line 208 of file biddy.h.

◆ Biddy_SetVariableData

#define Biddy_SetVariableData (   v,
 
)    Biddy_Managed_SetVariableData(NULL,v,x)

Macro Biddy_SetVariableData is defined for use with anonymous manager.

Definition at line 482 of file biddy.h.

◆ Biddy_SetVariableValue

#define Biddy_SetVariableValue (   v,
 
)    Biddy_Managed_SetVariableValue(NULL,v,f)

Macro Biddy_SetVariableValue is defined for use with anonymous manager.

Definition at line 467 of file biddy.h.

◆ Biddy_Sifting

#define Biddy_Sifting (   f,
 
)    Biddy_Managed_Sifting(NULL,f,c)

Macro Biddy_Sifting is defined for use with anonymous manager.

Definition at line 674 of file biddy.h.

◆ Biddy_Simplify

#define Biddy_Simplify (   f,
 
)    Biddy_Managed_Simplify(NULL,f,c)

Macro Biddy_Simplify is defined for use with anonymous manager.

Definition at line 827 of file biddy.h.

◆ Biddy_Subset

#define Biddy_Subset (   f,
  v,
  value 
)    Biddy_Managed_Subset(NULL,f,v,value)

Macro Biddy_Subset is defined for use with anonymous manager.

Definition at line 852 of file biddy.h.

◆ Biddy_Support

#define Biddy_Support (   f)    Biddy_Managed_Support(NULL,f)

Macro Biddy_Support is defined for use with anonymous manager.

Definition at line 832 of file biddy.h.

◆ Biddy_SwapWithHigher

#define Biddy_SwapWithHigher (   v)    Biddy_Managed_SwapWithHigher(NULL,v)

Macro Biddy_SwapWithHigher is defined for use with anonymous manager.

Definition at line 664 of file biddy.h.

◆ Biddy_SwapWithLower

#define Biddy_SwapWithLower (   v)    Biddy_Managed_SwapWithLower(NULL,v)

Macro Biddy_SwapWithLower is defined for use with anonymous manager.

Definition at line 669 of file biddy.h.

◆ Biddy_TaggedFoaNode

#define Biddy_TaggedFoaNode (   v,
  pf,
  pt,
  ptag,
  garbageAllowed 
)    Biddy_Managed_TaggedFoaNode(NULL,v,pf,pt,ptag,garbageAllowed)

Macro Biddy_TaggedFoaNode is defined for use with anonymous manager.

Definition at line 566 of file biddy.h.

◆ Biddy_TransferMark

#define Biddy_TransferMark (   f,
  mark,
  leftright 
)    Biddy_Managed_TransferMark(NULL,f,mark,leftright)

Macro Biddy_TransferMark is defined for use with anonymous manager.

For OBDD, use macro Biddy_InvCond.

Definition at line 556 of file biddy.h.

◆ Biddy_UnivAbstract

#define Biddy_UnivAbstract (   f,
  cube 
)    Biddy_Managed_UnivAbstract(NULL,f,cube)

Macro Biddy_UnivAbstract is defined for use with anonymous manager.

Definition at line 811 of file biddy.h.

◆ Biddy_Untagged

#define Biddy_Untagged (   f)    0

Biddy_Untagged returns untagged version of edge, since Biddy v1.7.

Definition at line 224 of file biddy.h.

◆ Biddy_VariableTableNum

#define Biddy_VariableTableNum ( )    Biddy_Managed_VariableTableNum(NULL)

Macro Biddy_VariableTableNum is defined for use with anonymous manager.

Definition at line 912 of file biddy.h.

◆ Biddy_WriteBDD

#define Biddy_WriteBDD (   filename,
  f,
  label 
)    Biddy_Managed_WriteBDD(NULL,filename,f,label)

Macro Biddy_WriteBDD is defined for use with anonymous manager.

Definition at line 1173 of file biddy.h.

◆ Biddy_WriteBddview

#define Biddy_WriteBddview (   filename,
  f,
  label,
  table 
)    Biddy_Managed_WriteBddview(NULL,filename,f,label,table);

Macro Biddy_WriteBddview is defined for use with anonymous manager.

Definition at line 1203 of file biddy.h.

◆ Biddy_WriteDot

#define Biddy_WriteDot (   filename,
  f,
  label,
  id,
  cudd 
)    Biddy_Managed_WriteDot(NULL,filename,f,label,id,cudd);

Macro Biddy_WriteDot is defined for use with anonymous manager.

Definition at line 1198 of file biddy.h.

◆ Biddy_WriteSOP

#define Biddy_WriteSOP (   filename,
 
)    Biddy_Managed_WriteSOP(NULL,filename,f)

Macro Biddy_WriteSOP is defined for use with anonymous manager.

Definition at line 1193 of file biddy.h.

◆ Biddy_WriteTable

#define Biddy_WriteTable (   filename,
 
)    Biddy_Managed_WriteTable(NULL,filename,f)

Macro Biddy_WriteTable is defined for use with anonymous manager.

Definition at line 1183 of file biddy.h.

◆ Biddy_Xnor

#define Biddy_Xnor (   f,
 
)    Biddy_Managed_Xnor(NULL,f,g)

Macro Biddy_Xnor is defined for use with anonymous manager.

Definition at line 758 of file biddy.h.

◆ Biddy_Xor

#define Biddy_Xor (   f,
 
)    Biddy_Managed_Xor(NULL,f,g)

Macro Biddy_Xor is defined for use with anonymous manager.

Definition at line 753 of file biddy.h.

Function Documentation

◆ Biddy_About()

EXTERN Biddy_String Biddy_About ( )

Description

Side effects

More info

Definition at line 1106 of file biddyMain.c.

◆ Biddy_AvgLevel()

EXTERN float Biddy_AvgLevel ( Biddy_Edge  f)

Description

Side effects

The result may not be compatible with your definition of Average Level for DAG. The result is especially problematic if there exists a node with two equal descendants (e.g for ZBDDs and TZBDDs).

More info

Macro Biddy_Managed_AvgLevel(f) is defined for user convenience.

Definition at line 196 of file biddyStat.c.

◆ Biddy_ExitMNG()

EXTERN void Biddy_ExitMNG ( Biddy_Manager mng)

Description

Deallocates all memory allocated by Biddy_InitMNG, Biddy_FoaVariable, Biddy_FoaNode etc.

Side effects

More info

Macro Biddy_Exit() will delete anonymous manager.

Definition at line 883 of file biddyMain.c.

◆ Biddy_GetElse()

EXTERN Biddy_Edge Biddy_GetElse ( Biddy_Edge  fun)

Description

Input mark is not transfered! External use, only.

Side effects

For terminal nodes, function returns the same node.

More info

Macro BiddyE(fun) is defined for internal use.

Definition at line 1282 of file biddyMain.c.

◆ Biddy_GetThen()

EXTERN Biddy_Edge Biddy_GetThen ( Biddy_Edge  fun)

Description

Input mark is not transfered! External use, only.

Side effects

For terminal nodes, function returns the same node.

More info

Macro BiddyT(fun) is defined for internal use.

Definition at line 1243 of file biddyMain.c.

◆ Biddy_GetTopVariable()

EXTERN Biddy_Variable Biddy_GetTopVariable ( Biddy_Edge  fun)

Description

External use, only.

Side effects

More info

Macro BiddyV(fun) is defined for internal use.

Definition at line 1320 of file biddyMain.c.

◆ Biddy_InitMNG()

EXTERN void Biddy_InitMNG ( Biddy_Manager mng,
int  bddtype 
)

Description

Biddy_InitMNG creates and initializes a manager. Initialization consists of creating manager structure (MNG), node table (biddyNodeTable), variable table (biddyVariableTable), formula table (biddyFormulaTable), four basic caches (biddyOPCache, biddyEACache, biddyRCCache, and biddyReplaceCache), and cache list (biddyCacheList). Biddy_InitMNG also initializes constant edges (biddyOne, biddyZero), memory management and automatic garbage collection.

Side effects

Allocates a lot of memory.

More info

Macro Biddy_InitAnonymous() will initialize anonymous manager. Macro Biddy_Init() will initialize anonymous manager for ROBDDs.

Definition at line 177 of file biddyMain.c.

◆ Biddy_Managed_A()

EXTERN 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_AddCache()

EXTERN void Biddy_Managed_AddCache ( Biddy_Manager  MNG,
Biddy_GCFunction  gc 
)

Description

If Cache list does not exist, function creates it.

Side effects

More info

Macro Biddy_AddCache(gc) is defined for use with anonymous manager.

Definition at line 4406 of file biddyMain.c.

◆ Biddy_Managed_AddElementByName()

EXTERN Biddy_Variable Biddy_Managed_AddElementByName ( Biddy_Manager  MNG,
Biddy_String  x 
)

Description

Biddy_Managed_AddElementByName uses Biddy_Managed_FoaVariable to find or add element. Function returns element edge. If element already exists, function returns the existing element edge. For more details see Biddy_Managed_FoaVariable.

Side effects

See Biddy_Managed_FoaVariable.

More info

Macro Biddy_AddElementByName(x) is defined for use with anonymous manager. Macros Biddy_Managed_AddElement(MNG) and Biddy_AddElement() are defined for creating numbered elements.

Definition at line 2903 of file biddyMain.c.

◆ Biddy_Managed_AddFormula()

EXTERN unsigned int Biddy_Managed_AddFormula ( Biddy_Manager  MNG,
Biddy_String  x,
Biddy_Edge  f,
int  c 
)

Description

Given BDD becomes a formula. If (x != NULL) then formula is accessible by its name. If (x != NULL) then index of the formula in the Formulae Table is returned, otherwise function returns 0. Nodes of the given BDD will be preserved for the given number of clearings. If (c == -1) then formula is refreshed but not preserved. If (c == 0) then formula is persistently preserved. You have to use Biddy_DeleteFormula and Biddy_Purge to remove nodes of persistently preserved formulae. There are five macros defined to simplify formulae management: Biddy_Managed_AddTmpFormula(mng,name,bdd) := Biddy_Managed_AddFormula(mng,name,bdd,-1) Biddy_Managed_AddPersistentFormula(mng,name,bdd) := Biddy_Managed_AddFormula(mng,name,bdd,0) Biddy_Managed_KeepFormula(mng,bdd) := Biddy_Managed_AddFormula(mng,NULL,bdd,1) Biddy_Managed_KeepFormulaProlonged(mng,bdd,c) := Biddy_Managed_AddFormula(mng,NULL,bdd,c) Biddy_Managed_KeepFormulaUntilPurge(mng,bdd) := Biddy_Managed_AddFormula(mng,NULL,bdd,0)

Side effects

Function is prolonged or fortified. Formulae with name are ordered by name. If formula with the same name already exists, it will be overwritten - preserved (i.e. not obsolete and not fresh) and persistently preserved formulae will be deleted at the original index and recreated at new index!

More info

Macros Biddy_AddFormula(x,f,c), Biddy_AddTmpFormula(x,f), Biddy_AddPersistentFormula(x,f), Biddy_KeepFormula(f), Biddy_KeepFormulaProlonged(f,c), and Biddy_KeepFormulaUntilPurge(f) are defined for use with anonymous manager.

Definition at line 4480 of file biddyMain.c.

◆ Biddy_Managed_AddVariableAbove()

EXTERN Biddy_Edge Biddy_Managed_AddVariableAbove ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Biddy_Managed_AddVariableAbove uses Biddy_Managed_AddVariableByName to add new variable. Then, the order of the new variable is changed to become immediately above the given variable (above = previous = topmore in BDD) Function returns variable edge.

Side effects

More info

Macro Biddy_AddVariableAbove(v) is defined for use with anonymous manager.

Definition at line 3015 of file biddyMain.c.

◆ Biddy_Managed_AddVariableBelow()

EXTERN Biddy_Edge Biddy_Managed_AddVariableBelow ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Biddy_Managed_AddVariableBelow uses Biddy_Managed_AddVariableByName to add new variable. Then, the order of the new variable is changed to become immediately below the given variable (below = next = bottommore in BDD) Function returns variable edge.

Side effects

More info

Macro Biddy_AddVariableBelow(v) is defined for use with anonymous manager.

Definition at line 2932 of file biddyMain.c.

◆ Biddy_Managed_AddVariableByName()

EXTERN Biddy_Variable Biddy_Managed_AddVariableByName ( Biddy_Manager  MNG,
Biddy_String  x 
)

Description

Biddy_Managed_AddVariableByName uses Biddy_Managed_FoaVariable to find or add variable. Function returns variable edge. If variable already exists, function returns the existing variable edge. For more details see Biddy_Managed_FoaVariable.

Side effects

See Biddy_Managed_FoaVariable.

More info

Macro Biddy_AddVariableByName(x) is defined for use with anonymous manager. Macros Biddy_Managed_AddVariable(MNG) and Biddy_AddVariable() are defined for creating numbered variables.

Definition at line 2871 of file biddyMain.c.

◆ Biddy_Managed_And()

EXTERN 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()

EXTERN 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()

EXTERN 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_ChangeVariableName()

EXTERN void Biddy_Managed_ChangeVariableName ( Biddy_Manager  MNG,
Biddy_Variable  v,
Biddy_String  x 
)

Description

Side effects

It is not checked that the same variable/element does not already exist. The ordering of the variable is not changed.

More info

Macro Biddy_ChangeVariableName(v,x) is defined for use with anonymous manager.

Definition at line 2835 of file biddyMain.c.

◆ Biddy_Managed_Clean()

EXTERN void Biddy_Managed_Clean ( Biddy_Manager  MNG)

Description

Discard all nodes which are not preserved or which are not preserved anymore. Obsolete nodes are not immediately removed, they will be removed during the first garbage collection.

Side effects

Field deleted is not considered and thus no fortified node and no prolonged node is discarded.

More info

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

Definition at line 4252 of file biddyMain.c.

◆ Biddy_Managed_ClearVariablesData()

EXTERN void Biddy_Managed_ClearVariablesData ( Biddy_Manager  MNG)

Description

Side effects

Only active (used) variables are considered.

More info

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

Definition at line 2147 of file biddyMain.c.

◆ Biddy_Managed_Compose()

EXTERN 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()

EXTERN 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_ConstructBDD()

EXTERN Biddy_Edge Biddy_Managed_ConstructBDD ( Biddy_Manager  MNG,
int  numV,
Biddy_String  varlist,
int  numN,
Biddy_String  nodelist 
)

Function**************************************************************** Synopsis [Function Biddy_Managed_ConstructBDD.] Description [Biddy_Managed_ConstructBDD constructs BDD from lists of nodes and edges. In both lists, elements are separated with spaces. Elements of node list has the following format: terminal node zero = (type=0,l=-1,r=-1), terminal node one = (type=1,l=-1,r=-1), regular label = (type=2,r=-1), complemented label = (type=3,r=-1), regular node = (type=4), node with complemented successor(s) = (type=5) The first element in nodelist is ignored. An example node list is: 'Biddy 0 Biddy 2 1 -1 1 B 4 2 3 2 0 0 -1 -1 3 i 4 4 9 4 d 4 5 6 5 0 0 -1 -1 6 y 4 7 8 7 0 0 -1 -1 8 1 1 -1 -1 9 d 4 6 10 10 1 1 -1 -1' which is constructed as: '{Biddy} {0 Biddy 2 1 -1} {1 B 4 2 3} {2 0 0 -1 -1} {3 i 4 4 9} {4 d 4 5 6} {5 0 0 -1 -1} {6 y 4 7 8} {7 0 0 -1 -1} {8 1 1 -1 -1} {9 d 4 6 10} {10 1 1 -1 -1}'. ] SideEffects [If variable ordering in the file is not compatible with the active ordering then the result will be wrong.] SeeAlso []

Definition at line 6044 of file biddyMain.c.

◆ Biddy_Managed_CountComplementedEdges()

EXTERN unsigned int Biddy_Managed_CountComplementedEdges ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Count number of complemented edges in a given BDD.

Side effects

Terminal 0 is represented by complemented edge to terminal 1 with all BDD types but this edge is counted as a complemented one only if complemented edges are explicitly used.

More info

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

Definition at line 1401 of file biddyStat.c.

◆ Biddy_Managed_CountMinterms()

EXTERN double Biddy_Managed_CountMinterms ( Biddy_Manager  MNG,
Biddy_Edge  f,
unsigned int  nvars 
)

Description

Parameter nvars is a user-defined number of dependent variables. If nvars == 0 then number of variables existing in the graph is used. For combination sets, this function coincides with combination counting.

Side effects

We are using GNU Multiple Precision Arithmetic Library (GMP). For ZBDDs, this function coincides with the 1-path count.

More info

Macro Biddy_CountMinterms(f,nvars) is defined for use with anonymous manager. Macros Biddy_Managed_CountCombination(MNG,f,nvars) and Biddy_CountCombinations(f,nvars) are defined for use with combination sets.

Definition at line 1526 of file biddyStat.c.

◆ Biddy_Managed_CountNodes()

EXTERN unsigned int Biddy_Managed_CountNodes ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Count number of nodes in a BDD.

Side effects

This function must be managed because node selection is used.

More info

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

Definition at line 85 of file biddyStat.c.

◆ Biddy_Managed_CountNodesPlain()

EXTERN unsigned int Biddy_Managed_CountNodesPlain ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Count number of nodes in a corresponding BDD without complement edges.

Side effects

More info

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

Definition at line 1191 of file biddyStat.c.

◆ Biddy_Managed_CountPaths()

EXTERN unsigned long long int Biddy_Managed_CountPaths ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

Implemented for OBDD, OBDDC, ZBDD, ZBDDC, and TZBDD. TO DO: implement this using GNU Multiple Precision Arithmetic Library (GMP).

More info

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

Definition at line 1457 of file biddyStat.c.

◆ Biddy_Managed_CreateFunction()

EXTERN 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()

EXTERN 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_DeleteFormula()

EXTERN Biddy_Boolean Biddy_Managed_DeleteFormula ( Biddy_Manager  MNG,
Biddy_String  x 
)

Description

Formula is labelled but not immediately removed. Nodes of the given formula are not immediately removed.

Side effects

Formula is not accessible by its name anymore. Formulae representing constants and variables will not be deleted.

More info

Macro Biddy_DeleteFormula(x) is defined for use with anonymous manager.

Definition at line 4933 of file biddyMain.c.

◆ Biddy_Managed_DeleteIthFormula()

EXTERN Biddy_Boolean Biddy_Managed_DeleteIthFormula ( Biddy_Manager  MNG,
unsigned int  i 
)

Description

Formula is labelled but not immediately removed. Nodes of the given formula are not immediately removed.

Side effects

Formula is not accessible by its name anymore. The first two formulae ("0" and "1") will not be deleted. Formulae representing variables will not be deleted.

More info

Macro Biddy_DeleteIthFormula(x) is defined for use with anonymous manager.

Definition at line 4997 of file biddyMain.c.

◆ Biddy_Managed_DensityOfBDD()

EXTERN double Biddy_Managed_DensityOfBDD ( Biddy_Manager  MNG,
Biddy_Edge  f,
unsigned int  nvars 
)

Description

If nvars == 0 then number of dependent variables is used.

Side effects

More info

Macro Biddy_DensityOfBDD(f,nvars) is defined for use with anonymous manager.

Definition at line 1743 of file biddyStat.c.

◆ Biddy_Managed_DensityOfFunction()

EXTERN double Biddy_Managed_DensityOfFunction ( Biddy_Manager  MNG,
Biddy_Edge  f,
unsigned int  nvars 
)

Description

If nvars == 0 then number of dependent variables is used.

Side effects

More info

Macro Biddy_DensityOfFunction(f,nvars) is defined for use with anonymous manager.

Definition at line 1670 of file biddyStat.c.

◆ Biddy_Managed_DependentVariableNumber()

EXTERN unsigned int Biddy_Managed_DependentVariableNumber ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Boolean  select 
)

Description

Count number of dependent variables. For OBDDs, the number of dependent variables is the same as the number of variables in the graph. For ZBDDs and TZBDDs, this is not true. If (select == TRUE) then dependent variables remain selected otherwise the function will unselect them.

Side effects

For ZBDDs, variables above the top variable (which are always all dependent) are not counted and not selected!

More info

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

Definition at line 1279 of file biddyStat.c.

◆ Biddy_Managed_DeselectAll()

EXTERN void Biddy_Managed_DeselectAll ( Biddy_Manager  MNG)

Description

Deselect all nodes.

Side effects

More info

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

Definition at line 1515 of file biddyMain.c.

◆ Biddy_Managed_DeselectNode()

EXTERN void Biddy_Managed_DeselectNode ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

More info

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

Definition at line 1405 of file biddyMain.c.

◆ Biddy_Managed_E()

EXTERN 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_Eval0()

EXTERN Biddy_String Biddy_Managed_Eval0 ( Biddy_Manager  MNG,
Biddy_String  s 
)

Description

First word is a name. It is followed by raw format. Function return name of the formula.

Side effects

All variables should already exists in the correct ordering! Not reentrant.

More info

Macro Biddy_Eval0(s) is defined for use with anonymous manager.

Definition at line 172 of file biddyInOut.c.

◆ Biddy_Managed_Eval1x()

EXTERN Biddy_Edge Biddy_Managed_Eval1x ( Biddy_Manager  MNG,
Biddy_String  s,
Biddy_LookupFunction  lf 
)

Description

Parameter lf is a lookup function in the user-defined cache table.

Side effects

Not reentrant.

More info

Macro Biddy_Eval1x(s,lf) is defined for use with anonymous manager. Macros Biddy_Managed_Eval1(s) and Biddy_Eval1(s) are defined for use without searching in the user-defined cache.

Definition at line 249 of file biddyInOut.c.

◆ Biddy_Managed_Eval2()

EXTERN Biddy_Edge Biddy_Managed_Eval2 ( Biddy_Manager  MNG,
Biddy_String  boolFunc 
)

Description

Parenthesis are implemented. Operators' priority is implemented. Formula Tree is suported (global table, only). Boolean constants are '0' and '1'. Boolean operators are NOT (~!), AND (&*), OR (|+), XOR (^%), XNOR (-), IMPLIES (><), NAND (@), NOR (#), BUTNOT (), NOTBUT (/).

Side effects

More info

Original author: Volodymyr Mihav (mihaw.nosp@m..wol.nosp@m.odymy.nosp@m.r@gm.nosp@m.ail.c.nosp@m.om) Original implementation of this function is on https://github.com/sungmaster/liBDD. Macro Biddy_Eval2(boolFunc) is defined for use with anonymous manager.

Definition at line 348 of file biddyInOut.c.

◆ Biddy_Managed_EvalProbability()

EXTERN double Biddy_Managed_EvalProbability ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Each variable should be associated with a probability q (0-1) via data element in BiddyVariable. For each 1-path a product of variable's probability is calculated (q for 'then' successor and (1-q) for 'else' successor). The result of the function is the sum of all such products.

Side effects

Implemented for OBDD, ZBDD, and TZBDD.

More info

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

Definition at line 2366 of file biddyMain.c.

◆ Biddy_Managed_ExistAbstract()

EXTERN 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_FindFormula()

EXTERN Biddy_Boolean Biddy_Managed_FindFormula ( Biddy_Manager  MNG,
Biddy_String  x,
unsigned int *  idx,
Biddy_Edge f 
)

Description

Return TRUE/FALSE, index, and the formula. If formula is constant or variable then idx = 0 and f != biddyNull. If formula is not found then idx is a position where the formulae should exist and f == biddyNull.

Side effects

More info

Macro Biddy_FindFormula(x,f) is defined for use with anonymous manager.

Definition at line 4759 of file biddyMain.c.

◆ Biddy_Managed_FoaVariable()

EXTERN Biddy_Variable Biddy_Managed_FoaVariable ( Biddy_Manager  MNG,
Biddy_String  x,
Biddy_Boolean  varelem 
)

Description

If variable/element already exists, function returns the existing one. If x == NULL then numbered variable/element is added. Numbered variables/elements have only digits in its name. The current number of numbered variables/elements is stored in numnum. If numbered variable/element is requested then function increments numnum and creates a new (non-existing) variable/element. Parameter varelem is used to determine how to adapt the existing BDD base to keep the current formula valid (use varelem = TRUE if formulae represent Boolean functions and varelem = FALSE if they represent combination sets). The ordering of the new variable/element is determined in Biddy_InitMNG. Function always returns variable.

Side effects

Adding new variable/element may change the meaning of the existing BDDs. Variables and elements are always repaired. Formulae are repaired with regards to the parameter varelem. BDDs without external references are not repaired. For OBDDs, OFDDs, TZBDDS, and TZFDDs, it is safe to add new variables/elements if BDDs are used to represent Boolean functions. For ZBDDs and ZFDDs, it is safe to add new variables/elements if BDDs are used to represent combination sets. User should not add numbered variables/elements with some other function. TO DO: Formulae in user's formula tables are not repaired, yet! TO DO: Variables cannot be deleted, yet!

More info

Macro Biddy_FoaVariable(x) is defined for use with anonymous manager.

Definition at line 2551 of file biddyMain.c.

◆ Biddy_Managed_FormulaTableNum()

EXTERN unsigned int Biddy_Managed_FormulaTableNum ( Biddy_Manager  MNG)

Description

Side effects

Formulae '0' and '1' are included.

More info

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

Definition at line 913 of file biddyStat.c.

◆ Biddy_Managed_GC()

EXTERN void Biddy_Managed_GC ( Biddy_Manager  MNG,
Biddy_Variable  targetLT,
Biddy_Variable  targetGEQ,
Biddy_Boolean  purge,
Biddy_Boolean  total 
)

Description

All obsolete nodes are deleted. Iff parameter purge is true then all formulae without name are deleted. Iff parameter purge is true then all nodes which are not part of non-obsolete non-deleted formulae are removed even if they are fresh or fortified (this should not be used during automatic garbage collection!). If parameter total is true than all unnecessary nodes are immediately deleted, otherwise they are deleted only when there are enough of them. If (targetLT != 0) then node table resizing is disabled. If (targetLT != 0) then there should not exist obsolete formulae. If (targetLT != 0) then there should not exist obsolete nodes which are not part of any non-obsolete non-deleted formulae. If (targetLT != 0) then there should not exist obsolete nodes with variable equal or higher (bottom-more) than target and smaller (top-more) than targetGEQ.

Side effects

The first element of each chain in a node table should have a special value for its 'prev' element to allow tricky but efficient deleting. Moreover, 'prev' and 'next' should be the first and the second element in the structure BiddyNode, respectively. Garbage collecion is reported by biddyNodeTable.garbage only if some bad nodes are purged! Parameters targetLT and targetGEQ are used during sifting, only, in all other cases 0 is used.

More info

Macro Biddy_GC(targetLT,targetGEQ,purge,total) is defined for use with anonymous manager. Macros Biddy_Managed_AutoGC(MNG) and Biddy_AutoGC() are useful variants with targetLT = targetGEQ = 0, purge = FALSE, and total = FALSE. Macros Biddy_Managed_ForceGC(MNG) and Biddy_ForceGC() are useful variants with targetLT = targetGEQ = 0, purge = FALSE, and total = TRUE.

Definition at line 3762 of file biddyMain.c.

◆ Biddy_Managed_GetBaseSet()

EXTERN Biddy_Edge Biddy_Managed_GetBaseSet ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 1647 of file biddyMain.c.

◆ Biddy_Managed_GetConstantOne()

EXTERN Biddy_Edge Biddy_Managed_GetConstantOne ( Biddy_Manager  MNG)

Description

Constants 0 and 1 depend on a manager. For combination sets, constant 1 coincides with universal set.

Side effects

For ZBDDs and ZFDDs, you should always obtain constant 1 through the call of this function!

More info

Internally, use macro biddyOne (also for ZBDDs and ZFDDs!). Macro Biddy_GetConstantOne() is defined for use with anonymous manager. Macros Biddy_Managed_GetUniversalSet(MNG) and Biddy_GetUniversalSet() are defined for manipulation of combination sets.

Definition at line 1621 of file biddyMain.c.

◆ Biddy_Managed_GetConstantZero()

EXTERN Biddy_Edge Biddy_Managed_GetConstantZero ( Biddy_Manager  MNG)

Description

Constants 0 and 1 depend on a manager. For combination sets, constant 0 coincides with empty set.

Side effects

More info

Internally, use macro biddyZero. Macro Biddy_GetConstantZero() is defined for use with anonymous manager. Macros Biddy_Managed_GetEmptySet(MNG) and Biddy_GetEmptySet() are defined for manipulation of combination sets.

Definition at line 1589 of file biddyMain.c.

◆ Biddy_Managed_GetElementEdge()

EXTERN Biddy_Edge Biddy_Managed_GetElementEdge ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

Macro Biddy_GetElementEdge(v) is defined for use with anonymous manager.

Definition at line 1926 of file biddyMain.c.

◆ Biddy_Managed_GetIthFormula()

EXTERN Biddy_Edge Biddy_Managed_GetIthFormula ( Biddy_Manager  MNG,
unsigned int  i 
)

Description

Return biddyNull if ith formulae does not exist.

Side effects

After addding new formula the index of others may change!

More info

Macro Biddy_GetIthFormula(i) is defined for use with anonymous manager.

Definition at line 5057 of file biddyMain.c.

◆ Biddy_Managed_GetIthFormulaName()

EXTERN Biddy_String Biddy_Managed_GetIthFormulaName ( Biddy_Manager  MNG,
unsigned int  i 
)

Description

Return NULL if ith formulae does not exist.

Side effects

After addding new formula the index of others may change!

More info

Macro Biddy_GetIthFormulaName(i) is defined for use with anonymous manager.

Definition at line 5088 of file biddyMain.c.

◆ Biddy_Managed_GetIthVariable()

EXTERN Biddy_Variable Biddy_Managed_GetIthVariable ( Biddy_Manager  MNG,
Biddy_Variable  i 
)

Description

The lowest (topmost) variable has global ordering 1. The highest (bottommost) variable is '1' and has global ordering equal to numUsedVariables.

Side effects

If argument is 0, function returns 0. If argument is larger than the number of variables, function returns 0.

More info

Macro Biddy_GetIthVariable(x) is defined for use with anonymous manager.

Definition at line 1804 of file biddyMain.c.

◆ Biddy_Managed_GetLowestVariable()

EXTERN Biddy_Variable Biddy_Managed_GetLowestVariable ( Biddy_Manager  MNG)

Description

The lowest variable is the tompost variable.

Side effects

More info

Macro Biddy_GetLowestVariable(x) is defined for use with anonymous manager.

Definition at line 1766 of file biddyMain.c.

◆ Biddy_Managed_GetManagerName()

EXTERN Biddy_String Biddy_Managed_GetManagerName ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 1155 of file biddyMain.c.

◆ Biddy_Managed_GetManagerType()

EXTERN int Biddy_Managed_GetManagerType ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 1129 of file biddyMain.c.

◆ Biddy_Managed_GetNextVariable()

EXTERN Biddy_Variable Biddy_Managed_GetNextVariable ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

Macro Biddy_GetNextVariable(v) is defined for use with anonymous manager.

Definition at line 1872 of file biddyMain.c.

◆ Biddy_Managed_GetPrevVariable()

EXTERN Biddy_Variable Biddy_Managed_GetPrevVariable ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

Macro Biddy_GetPrevVariable(v) is defined for use with anonymous manager.

Definition at line 1842 of file biddyMain.c.

◆ Biddy_Managed_GetTerminal()

EXTERN Biddy_Edge Biddy_Managed_GetTerminal ( Biddy_Manager  MNG)

Description

Terminal node depends on a manager.

Side effects

More info

Internally, use macro biddyTerminal. Macro Biddy_GetTerminal() is defined for use with anonymous manager.

Definition at line 1559 of file biddyMain.c.

◆ Biddy_Managed_GetTopVariableChar()

EXTERN char Biddy_Managed_GetTopVariableChar ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

More info

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

Definition at line 2035 of file biddyMain.c.

◆ Biddy_Managed_GetTopVariableEdge()

EXTERN Biddy_Edge Biddy_Managed_GetTopVariableEdge ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

TO DO: For ZBDDs, element edge is sometimes preffered over variable edge.

More info

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

Definition at line 1979 of file biddyMain.c.

◆ Biddy_Managed_GetTopVariableName()

EXTERN Biddy_String Biddy_Managed_GetTopVariableName ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

More info

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

Definition at line 2007 of file biddyMain.c.

◆ Biddy_Managed_GetVariable()

EXTERN Biddy_Variable Biddy_Managed_GetVariable ( Biddy_Manager  MNG,
Biddy_String  x 
)

Description

Side effects

If variable is not found function returns 0!

More info

Macro Biddy_GetVariable(x) is defined for use with anonymous manager.

Definition at line 1712 of file biddyMain.c.

◆ Biddy_Managed_GetVariableData()

EXTERN void* Biddy_Managed_GetVariableData ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

It is not checked that the given variable is valid.

More info

Macro Biddy_GetVariableData(v) is defined for use with anonymous manager.

Definition at line 2206 of file biddyMain.c.

◆ Biddy_Managed_GetVariableEdge()

EXTERN Biddy_Edge Biddy_Managed_GetVariableEdge ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

Macro Biddy_GetVariableEdge(v) is defined for use with anonymous manager.

Definition at line 1901 of file biddyMain.c.

◆ Biddy_Managed_GetVariableName()

EXTERN Biddy_String Biddy_Managed_GetVariableName ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

Macro Biddy_GetVariableName(v) is defined for use with anonymous manager.

Definition at line 1951 of file biddyMain.c.

◆ Biddy_Managed_GetVariableValue()

EXTERN Biddy_Edge Biddy_Managed_GetVariableValue ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

It is not checked that the given variable is valid.

More info

Macro Biddy_GetVariableValue(v) is defined for use with anonymous manager.

Definition at line 2120 of file biddyMain.c.

◆ Biddy_Managed_Gt()

EXTERN 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_IncTag()

EXTERN Biddy_Edge Biddy_Managed_IncTag ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Used for TZBDDs and TZFDDs, only.

Side effects

It is not checked, that the resulting tag is not greater than top variable. Function may return non-fresh node even if f is fresh.

More info

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

Definition at line 3162 of file biddyMain.c.

◆ Biddy_Managed_IsEqv()

EXTERN Biddy_Boolean Biddy_Managed_IsEqv ( Biddy_Manager  MNG1,
Biddy_Edge  f1,
Biddy_Manager  MNG2,
Biddy_Edge  f2 
)

Description

It is assumed that f1 and f2 have the same ordering.

Side effects

More info

Macro Biddy_IsEqv(f1,MNG2,f2) is defined for use with anonymous manager.

Definition at line 1344 of file biddyMain.c.

◆ Biddy_Managed_IsHighest()

EXTERN Biddy_Boolean Biddy_Managed_IsHighest ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

Macro BiddyIsHighest(v) is defined for internal use. Macro Biddy_IsHighest(v) is defined for use with anonymous manager.

Definition at line 2493 of file biddyMain.c.

◆ Biddy_Managed_IsLeq()

EXTERN 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_IsLowest()

EXTERN Biddy_Boolean Biddy_Managed_IsLowest ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

Macro BiddyIsLowest(v) is defined for internal use. Macro Biddy_IsLowest(v) is defined for use with anonymous manager.

Definition at line 2456 of file biddyMain.c.

◆ Biddy_Managed_IsOK()

EXTERN Biddy_Boolean Biddy_Managed_IsOK ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

This is needed for implementation of user caches.

Side effects

More info

Macro BiddyIsOK(f) is defined for debugging. It will check more properties and not only the expiry value. Macro Biddy_IsOK(f) is defined for use with anonymous manager.

Definition at line 3711 of file biddyMain.c.

◆ Biddy_Managed_IsSelected()

EXTERN Biddy_Boolean Biddy_Managed_IsSelected ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

More info

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

Definition at line 1431 of file biddyMain.c.

◆ Biddy_Managed_IsSmaller()

EXTERN Biddy_Boolean Biddy_Managed_IsSmaller ( Biddy_Manager  MNG,
Biddy_Variable  fv,
Biddy_Variable  gv 
)

Description

Side effects

More info

Macro BiddyIsSmaller(fv,gv) is defined for internal use. Macro Biddy_IsSmaller(fv,gv) is defined for use with anonymous manager.

Definition at line 2429 of file biddyMain.c.

◆ Biddy_Managed_IsVariableDependent()

EXTERN 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()

EXTERN 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()

EXTERN 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_ListAvgLength()

EXTERN float Biddy_Managed_ListAvgLength ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 1035 of file biddyStat.c.

◆ Biddy_Managed_ListMaxLength()

EXTERN unsigned int Biddy_Managed_ListMaxLength ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 971 of file biddyStat.c.

◆ Biddy_Managed_ListUsed()

EXTERN unsigned int Biddy_Managed_ListUsed ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 938 of file biddyStat.c.

◆ Biddy_Managed_MaximizeBDD()

EXTERN void Biddy_Managed_MaximizeBDD ( Biddy_Manager  MNG,
Biddy_String  name 
)

Description

Steinhaus–Johnson–Trotter algorithm is used to generate all possible permutations. An optimized version of Bubble Sort is used to setup the final ordering. Variables are reordered globally. All obsolete nodes will be removed.

Side effects

Indeed, this function may take a lot of time! For TZBDD, all unreferenced nodes (not part of registered formulae) will be removed. For TZBDD, this function may change top edge or even a top node of any function/formula - this is a problem, because functions referenced by local variables only may become wrong. Consequently, for TZBDDs, sifting is not safe to start automatically!

More info

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

Definition at line 5576 of file biddyMain.c.

◆ Biddy_Managed_MaxNodes()

EXTERN unsigned int Biddy_Managed_MaxNodes ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

BDD is copyed into new empty manager and then Steinhaus–Johnson–Trotter algorithm is used to check the node number for all possible orderings.

Side effects

Function will finish in a good time only for small number of variables.

More info

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

Definition at line 1982 of file biddyStat.c.

◆ Biddy_Managed_MinimizeBDD()

EXTERN void Biddy_Managed_MinimizeBDD ( Biddy_Manager  MNG,
Biddy_String  name 
)

Description

Steinhaus–Johnson–Trotter algorithm is used to generate all possible permutations. An optimized version of Bubble Sort is used to setup the final ordering. Variables are reordered globally. All obsolete nodes will be removed.

Side effects

Indeed, this function may take a lot of time! For TZBDD, all unreferenced nodes (not part of registered formulae) will be removed. For TZBDD, this function may change top edge or even a top node of any function/formula - this is a problem, because functions referenced by local variables only may become wrong. Consequently, for TZBDDs, sifting is not safe to start automatically!

More info

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

Definition at line 5481 of file biddyMain.c.

◆ Biddy_Managed_MinNodes()

EXTERN unsigned int Biddy_Managed_MinNodes ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

BDD is copyed into new empty manager and then Steinhaus–Johnson–Trotter algorithm is used to check the node number for all possible orderings.

Side effects

Function will finish in a good time only for small number of variables.

More info

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

Definition at line 1839 of file biddyStat.c.

◆ Biddy_Managed_Nand()

EXTERN 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_NodeTableAddNumber()

EXTERN unsigned long long int Biddy_Managed_NodeTableAddNumber ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 534 of file biddyStat.c.

◆ Biddy_Managed_NodeTableANDORNumber()

EXTERN unsigned int Biddy_Managed_NodeTableANDORNumber ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 794 of file biddyStat.c.

◆ Biddy_Managed_NodeTableANDORRecursiveNumber()

EXTERN unsigned long long int Biddy_Managed_NodeTableANDORRecursiveNumber ( Biddy_Manager  MNG)

Description

Side effects

Recursive AND/OR calls are counted only if Biddy is compiled using directive BIDDYEXTENDEDSTATS_YES.

More info

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

Definition at line 822 of file biddyStat.c.

◆ Biddy_Managed_NodeTableBlockNumber()

EXTERN unsigned int Biddy_Managed_NodeTableBlockNumber ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 283 of file biddyStat.c.

◆ Biddy_Managed_NodeTableCompareNumber()

EXTERN unsigned long long int Biddy_Managed_NodeTableCompareNumber ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 502 of file biddyStat.c.

◆ Biddy_Managed_NodeTableDRTime()

EXTERN unsigned int Biddy_Managed_NodeTableDRTime ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 709 of file biddyStat.c.

◆ Biddy_Managed_NodeTableFindNumber()

EXTERN unsigned long long int Biddy_Managed_NodeTableFindNumber ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 470 of file biddyStat.c.

◆ Biddy_Managed_NodeTableFoaNumber()

EXTERN unsigned long long int Biddy_Managed_NodeTableFoaNumber ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 438 of file biddyStat.c.

◆ Biddy_Managed_NodeTableGCNumber()

EXTERN unsigned int Biddy_Managed_NodeTableGCNumber ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 565 of file biddyStat.c.

◆ Biddy_Managed_NodeTableGCObsoleteNumber()

EXTERN unsigned long long int Biddy_Managed_NodeTableGCObsoleteNumber ( Biddy_Manager  MNG)

Description

Return the number of nodes deleted by GC.

Side effects

Obsolete nodes deleted by GC are counted only if Biddy is compiled using directive BIDDYEXTENDEDSTATS_YES.

More info

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

Definition at line 619 of file biddyStat.c.

◆ Biddy_Managed_NodeTableGCTime()

EXTERN unsigned int Biddy_Managed_NodeTableGCTime ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 590 of file biddyStat.c.

◆ Biddy_Managed_NodeTableGenerated()

EXTERN unsigned int Biddy_Managed_NodeTableGenerated ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 308 of file biddyStat.c.

◆ Biddy_Managed_NodeTableITENumber()

EXTERN unsigned int Biddy_Managed_NodeTableITENumber ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 734 of file biddyStat.c.

◆ Biddy_Managed_NodeTableITERecursiveNumber()

EXTERN unsigned long long int Biddy_Managed_NodeTableITERecursiveNumber ( Biddy_Manager  MNG)

Description

Side effects

Recursive ITE calls are counted only if Biddy is compiled using directive BIDDYEXTENDEDSTATS_YES.

More info

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

Definition at line 762 of file biddyStat.c.

◆ Biddy_Managed_NodeTableMax()

EXTERN unsigned int Biddy_Managed_NodeTableMax ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 334 of file biddyStat.c.

◆ Biddy_Managed_NodeTableNum()

EXTERN unsigned int Biddy_Managed_NodeTableNum ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 360 of file biddyStat.c.

◆ Biddy_Managed_NodeTableNumVar()

EXTERN unsigned int Biddy_Managed_NodeTableNumVar ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Side effects

More info

Macro Biddy_NodeTableNumVar(v) is defined for use with anonymous manager.

Definition at line 386 of file biddyStat.c.

◆ Biddy_Managed_NodeTableResizeNumber()

EXTERN unsigned int Biddy_Managed_NodeTableResizeNumber ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 412 of file biddyStat.c.

◆ Biddy_Managed_NodeTableSiftingNumber()

EXTERN unsigned int Biddy_Managed_NodeTableSiftingNumber ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 684 of file biddyStat.c.

◆ Biddy_Managed_NodeTableSize()

EXTERN unsigned int Biddy_Managed_NodeTableSize ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 253 of file biddyStat.c.

◆ Biddy_Managed_NodeTableSwapNumber()

EXTERN unsigned int Biddy_Managed_NodeTableSwapNumber ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 658 of file biddyStat.c.

◆ Biddy_Managed_NodeTableXORNumber()

EXTERN unsigned int Biddy_Managed_NodeTableXORNumber ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 853 of file biddyStat.c.

◆ Biddy_Managed_NodeTableXORRecursiveNumber()

EXTERN unsigned long long int Biddy_Managed_NodeTableXORRecursiveNumber ( Biddy_Manager  MNG)

Description

Side effects

Recursive XOR calls are counted only if Biddy is compiled using directive BIDDYEXTENDEDSTATS_YES.

More info

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

Definition at line 881 of file biddyStat.c.

◆ Biddy_Managed_Nor()

EXTERN 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()

EXTERN 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_OPCacheFind()

EXTERN unsigned long long int Biddy_Managed_OPCacheFind ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 1102 of file biddyStat.c.

◆ Biddy_Managed_OPCacheInsert()

EXTERN unsigned long long int Biddy_Managed_OPCacheInsert ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 1127 of file biddyStat.c.

◆ Biddy_Managed_OPCacheOverwrite()

EXTERN unsigned long long int Biddy_Managed_OPCacheOverwrite ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 1158 of file biddyStat.c.

◆ Biddy_Managed_OPCacheSearch()

EXTERN unsigned long long int Biddy_Managed_OPCacheSearch ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 1077 of file biddyStat.c.

◆ Biddy_Managed_Or()

EXTERN 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_PrintfBDD()

EXTERN void Biddy_Managed_PrintfBDD ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

This function is intended for writing to an output channel via macro which overrides the meaning of standard printf calls. For writing raw format into the file, use Biddy_Managed_WriteBDD.

Side effects

More info

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

Definition at line 1080 of file biddyInOut.c.

◆ Biddy_Managed_PrintfSOP()

EXTERN void Biddy_Managed_PrintfSOP ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

More info

Definition at line 1376 of file biddyInOut.c.

◆ Biddy_Managed_PrintfTable()

EXTERN void Biddy_Managed_PrintfTable ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

This function is intended for writing to an output channel via macro which overrides the meaning of standard printf calls. For writing truth table into the file, use Biddy_Managed_WriteTable.

Side effects

More info

Thanks to Jan Kraner (jankr.nosp@m.isti.nosp@m.an.kr.nosp@m.aner.nosp@m.@stud.nosp@m.ent..nosp@m.um.si) and Ziga Kobale (ziga..nosp@m.koba.nosp@m.le@st.nosp@m.uden.nosp@m.t.um..nosp@m.si). Macro Biddy_PrintfTable(f) is defined for use with anonymous manager.

Definition at line 1157 of file biddyInOut.c.

◆ Biddy_Managed_PrintInfo()

EXTERN void Biddy_Managed_PrintInfo ( Biddy_Manager  MNG,
FILE *  f 
)

Description

Side effects

More info

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

Definition at line 2221 of file biddyStat.c.

◆ Biddy_Managed_Purge()

EXTERN void Biddy_Managed_Purge ( Biddy_Manager  MNG)

Description

All formulae without name are deleted. All deleted formulae (including prolonged/fortified formulae) are removed. All fresh and obsolete nodes are immediatelly removed. Moreover, all prolonged and fortified nodes are removed if they are not needed by some of the remaining formula. Call to Biddy_Purge does not count as clearing and thus all preserved formulae remains preserved for the same number of clearings.

Side effects

Removes all fresh nodes!

More info

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

Definition at line 4303 of file biddyMain.c.

◆ Biddy_Managed_PurgeAndReorder()

EXTERN void Biddy_Managed_PurgeAndReorder ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Boolean  converge 
)

Description

All obsolete nodes are immediatelly removed. Moreover, nodes from deleted prolonged formulae and nodes from deleted fortified formulae are removed if they are not needed by other formulae. If BDD is given (f != NULL), reordering on function is used. Otherwise (f == NULL) global reordering is used. Call to Biddy_PurgeAndReorder does not count as clearing and thus all preserved formulae remains preserved for the same number of clearings.

Side effects

Removes all fresh nodes.

More info

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

Definition at line 4351 of file biddyMain.c.

◆ Biddy_Managed_RandomFunction()

EXTERN 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()

EXTERN 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_ReadBddview()

EXTERN Biddy_String Biddy_Managed_ReadBddview ( Biddy_Manager  MNG,
const char  filename[],
Biddy_String  name 
)

Description

If (name != NULL) then name will be used for the resulting BDD. If (name == NULL) then the resulting BDD will have name given in the file. Resulting BDD will not be preserved. See Biddy_Managed_ConstructBDD for the format of its arguments.

Side effects

To improve efficiency, only the first lines with "type", "var", and "label" are used.

More info

Macro Biddy_ReadBddview(filename) is defined for use with anonymous manager.

Definition at line 543 of file biddyInOut.c.

◆ Biddy_Managed_ReadMemoryInUse()

EXTERN unsigned long long int Biddy_Managed_ReadMemoryInUse ( Biddy_Manager  MNG)

Description

Side effects

More info

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

Definition at line 2124 of file biddyStat.c.

◆ Biddy_Managed_ReadVerilogFile()

EXTERN void Biddy_Managed_ReadVerilogFile ( Biddy_Manager  MNG,
const char  filename[],
Biddy_String  prefix 
)

Description

If (prefix != NULL) then the created BDD variables and formulae will get it.

Side effects

More info

Original author: David Kebo Houngninou, Southern Methodist University Original implementation of this function is on https://github.com/davidkebo/verilog-parser Macro Biddy_ReadVerilogFile(filename,prefix) is defined for use with anonymous manager.

Definition at line 979 of file biddyInOut.c.

◆ Biddy_Managed_Refresh()

EXTERN void Biddy_Managed_Refresh ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

This is an external variant of internal macro BiddyRefresh This is needed for implementing user caches.

Side effects

More info

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

Definition at line 4380 of file biddyMain.c.

◆ Biddy_Managed_ReplaceByKeyword()

EXTERN 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_ResetVariablesValue()

EXTERN void Biddy_Managed_ResetVariablesValue ( Biddy_Manager  MNG)

Description

Side effects

Only active (used) variables are reinitialized.

More info

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

Definition at line 2064 of file biddyMain.c.

◆ Biddy_Managed_Restrict()

EXTERN 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_SelectFunction()

EXTERN void Biddy_Managed_SelectFunction ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

Terminal node must be selected before starting this function!

More info

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

Definition at line 1458 of file biddyMain.c.

◆ Biddy_Managed_SelectNode()

EXTERN void Biddy_Managed_SelectNode ( Biddy_Manager  MNG,
Biddy_Edge  f 
)

Description

Side effects

More info

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

Definition at line 1379 of file biddyMain.c.

◆ Biddy_Managed_SetAlphabeticOrdering()

EXTERN void Biddy_Managed_SetAlphabeticOrdering ( Biddy_Manager  MNG)

Description

Named variables are ordered according to their names. Numbered variables are ordered according to their numbers and are always smaller (topmore) as any named variable.

Side effects

More info

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

Definition at line 5129 of file biddyMain.c.

◆ Biddy_Managed_SetManagerParameters()

EXTERN void Biddy_Managed_SetManagerParameters ( Biddy_Manager  MNG,
float  gcr,
float  gcrF,
float  gcrX,
float  rr,
float  rrF,
float  rrX,
float  st,
float  cst 
)

Description

Function expect 6 float values. If the value is < 0 then the parameter is not modified. The parameters are: biddyNodeTable.gcratio (do not delete nodes if the effect is to small), biddyNodeTable.gcratioF (do not delete nodes if the effect is to small), biddyNodeTable.gcratioX (do not delete nodes if the effect is to small), biddyNodeTable.resizeratio (resize Node table if there are to many nodes), biddyNodeTable.resizeratioF (resize Node table if there are to many nodes), biddyNodeTable.resizeratioX (resize Node table if there are to many nodes), biddyNodeTable.siftingtreshold (stop sifting if the size of the system grows to much), biddyNodeTable.fsiftingtreshold (stop sifting if the size of the function grows to much), biddyNodeTable.convergesiftingtreshold (stop one step of converging sifting if the size of the system grows to much), biddyNodeTable.fconvergesiftingtreshold (stop one step of converging sifting if the size of the function grows to much).

Side effects

Initial values are given in Biddy_InitMNG.

More info

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

Definition at line 1198 of file biddyMain.c.

◆ Biddy_Managed_SetVariableData()

EXTERN void Biddy_Managed_SetVariableData ( Biddy_Manager  MNG,
Biddy_Variable  v,
void *  x 
)

Description

Side effects

It is not checked that the given variable is valid.

More info

Macro Biddy_SetVariableData(v,x) is defined for use with anonymous manager.

Definition at line 2180 of file biddyMain.c.

◆ Biddy_Managed_SetVariableValue()

EXTERN void Biddy_Managed_SetVariableValue ( Biddy_Manager  MNG,
Biddy_Variable  v,
Biddy_Edge  f 
)

Description

Side effects

It is not checked that the given variable is valid.

More info

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

Definition at line 2094 of file biddyMain.c.

◆ Biddy_Managed_Sifting()

EXTERN Biddy_Boolean Biddy_Managed_Sifting ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Boolean  converge 
)

Description

Variables are reordered globally. All obsolete nodes will be removed.

Side effects

For TZBDD, all unreferenced nodes (not part of registered formulae) will be removed. For TZBDD, sifting may change top edge or even a top node of any function/formula - this is a problem, because functions referenced by local variables only may become wrong. Consequently, for TZBDDs, sifting is not safe to start automatically!

More info

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

Definition at line 5298 of file biddyMain.c.

◆ Biddy_Managed_Simplify()

EXTERN 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()

EXTERN 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()

EXTERN 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_SwapWithHigher()

EXTERN Biddy_Variable Biddy_Managed_SwapWithHigher ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Higher (greater) variable is the bottommore one! The highest variable is constant variable "1". Global ordering is number of zeros in corresponding line of orderingTable. Constant variable '1' has global ordering greater than all others.

Side effects

All obsolete nodes will be removed.

More info

Macro Biddy_SwapWithHigher(v) is defined for use with anonymous manager.

Definition at line 5162 of file biddyMain.c.

◆ Biddy_Managed_SwapWithLower()

EXTERN Biddy_Variable Biddy_Managed_SwapWithLower ( Biddy_Manager  MNG,
Biddy_Variable  v 
)

Description

Lower (smaller) variable is the topmore one! The lowest (topmost) element is not fixed. Topmost variable has global ordering 1 (smaller than all except itself). Global ordering is the number of zeros in corresponding line of orderingTable.

Side effects

All obsolete nodes will be removed.

More info

Macro Biddy_SwapWithLower(v) is defined for use with anonymous manager.

Definition at line 5228 of file biddyMain.c.

◆ Biddy_Managed_TaggedFoaNode()

EXTERN Biddy_Edge Biddy_Managed_TaggedFoaNode ( Biddy_Manager  MNG,
Biddy_Variable  v,
Biddy_Edge  pf,
Biddy_Edge  pt,
Biddy_Variable  ptag,
Biddy_Boolean  garbageAllowed 
)

Description

If such node already exists, function returns it and does not create the new one. For OBDDs, ZBDDs, OFDDs, and ZFDDs, the returned edge is not tagged (i.e. tag == 0). For TZBDDs and TZFDDs, the returned edge is tagged with the given ptag. There are two special cases:

  1. If (pf == pt == NULL) then new variable (for OBDDs, OFDDs, TZBDDs, and TZFDDs) or new element (for ZBDDs and ZFDDs) is created.
  2. (If ptag == 0) then the reduction rule and the normalization of complemented edges is not used and the node is added exactly as specified (be careful, this may create a wrong node!).

    Side effects

This function should not be called directly to add new variables and elements, you must use Biddy_Managed_FoaVariable, Biddy_Managed_AddVariableByName, or Biddy_Managed_AddElementByName. Using Biddy_Managed_TaggedFoaNode you can create node with an arbitrary ordering. It is much more safe to use Boolean operators, e.g. Biddy_Managed_ITE.

More info

Macro Biddy_Managed_FoaNode(MNG,v,pf,pt,garbageAllowed) is defined for use without tags. Macros Biddy_TaggedFoaNode(v,pf,pt,tag,garbageAllowed) and Biddy_FoaNode(v,pf,pt,garbageAllowed) are defined for use with anonymous manager.

Definition at line 3244 of file biddyMain.c.

◆ Biddy_Managed_TransferMark()

EXTERN Biddy_Edge Biddy_Managed_TransferMark ( Biddy_Manager  MNG,
Biddy_Edge  f,
Biddy_Boolean  mark,
Biddy_Boolean  leftright 
)

Description

Parameter leftright should be TRUE for left and FALSE for right. For OBDDC, it is better to use macro Biddy_InvCond. For OBDDC, parameter leftright is ignored.

Side effects

TO DO: swap the meaning of parameter leftright (left should be FALSE)

More info

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

Definition at line 3096 of file biddyMain.c.

◆ Biddy_Managed_UnivAbstract()

EXTERN 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_VariableTableNum()

EXTERN Biddy_Variable Biddy_Managed_VariableTableNum ( Biddy_Manager  MNG)

Description

Side effects

Variable '1' is included.

More info

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

Definition at line 228 of file biddyStat.c.

◆ Biddy_Managed_WriteBDD()

EXTERN void Biddy_Managed_WriteBDD ( Biddy_Manager  MNG,
const char  filename[],
Biddy_Edge  f,
Biddy_String  label 
)

Description

Side effects

More info

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

Definition at line 1110 of file biddyInOut.c.

◆ Biddy_Managed_WriteBddview()

EXTERN unsigned int Biddy_Managed_WriteBddview ( Biddy_Manager  MNG,
const char  filename[],
Biddy_Edge  f,
const char  label[],
void *  xytable 
)

Description

Output bddview format. Parameter table is optional, if not NULL then it must contain node names and coordinates. If (filename == NULL) then output is to stdout.

Side effects

A conservative approach to list all the existing variables in the manager (and not only the dependent ones) is used. Variable names containing # are adpated. To support EST, also variable names containing <> are adapted. The optional table is type-casted to BiddyXYTable.

More info

Macro Biddy_WriteBddview(filename,f,label) is defined for use with anonymous manager.

Definition at line 1804 of file biddyInOut.c.

◆ Biddy_Managed_WriteDot()

EXTERN unsigned int Biddy_Managed_WriteDot ( Biddy_Manager  MNG,
const char  filename[],
Biddy_Edge  f,
const char  label[],
int  id,
Biddy_Boolean  cudd 
)

Description

Output dot format. Two approaches are implemented. The CUDD-like implementation is copyied from CUDD 3.0.

Side effects

If (id != -1) then id is used instead of <...> for variable names. If (filename == NULL) then output is to stdout. Function resets all variables value. Variable names containing # are adpated.

More info

Macro Biddy_WriteDot(filename,f,label,id,cudd) is defined for use with anonymous manager.

Definition at line 1581 of file biddyInOut.c.

◆ Biddy_Managed_WriteSOP()

EXTERN void Biddy_Managed_WriteSOP ( Biddy_Manager  MNG,
const char  filename[],
Biddy_Edge  f 
)

Description

Side effects

More info

Definition at line 1460 of file biddyInOut.c.

◆ Biddy_Managed_WriteTable()

EXTERN void Biddy_Managed_WriteTable ( Biddy_Manager  MNG,
const char  filename[],
Biddy_Edge  f 
)

Description

Side effects

More info

Thanks to Jan Kraner (jankr.nosp@m.isti.nosp@m.an.kr.nosp@m.aner.nosp@m.@stud.nosp@m.ent..nosp@m.um.si) and Ziga Kobale (ziga..nosp@m.koba.nosp@m.le@st.nosp@m.uden.nosp@m.t.um..nosp@m.si). Macro Biddy_WriteTable(f) is defined for use with anonymous manager.

Definition at line 1266 of file biddyInOut.c.

◆ Biddy_Managed_Xnor()

EXTERN 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()

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

◆ Biddy_MaxLevel()

EXTERN unsigned int Biddy_MaxLevel ( Biddy_Edge  f)

Description

Side effects

More info

Macro Biddy_Managed_MaxLevel(f) is defined for user convenience.

Definition at line 164 of file biddyStat.c.