cudd  3.0.0
The University of Colorado Decision Diagram Package
cuddObj.hh
Go to the documentation of this file.
1 
47 #ifndef CUDD_OBJ_H_
48 #define CUDD_OBJ_H_
49 
50 /*---------------------------------------------------------------------------*/
51 /* Nested includes */
52 /*---------------------------------------------------------------------------*/
53 
54 #include <cstdio>
55 #include <string>
56 #include <vector>
57 #include "cudd.h"
58 
59 /*---------------------------------------------------------------------------*/
60 /* Type definitions */
61 /*---------------------------------------------------------------------------*/
62 class BDD;
63 class ADD;
64 class ZDD;
65 class Cudd;
66 
67 typedef void (*PFC)(std::string); // handler function type
68 
69 /*---------------------------------------------------------------------------*/
70 /* Class definitions */
71 /*---------------------------------------------------------------------------*/
72 
73 class Capsule;
74 
75 
82 class DD {
83 protected:
84  Capsule *p;
85  DdNode *node;
86  inline DdManager * checkSameManager(const DD &other) const;
87  inline void checkReturnValue(const void *result) const;
88  inline void checkReturnValue(int result, int expected = 1)
89  const;
90  DD();
91  DD(Capsule *cap, DdNode *ddNode);
92  DD(Cudd const & manager, DdNode *ddNode);
93  DD(const DD &from);
94  ~DD();
95 public:
96  // This operator should be declared explicit, but there are still too many
97  // compilers out there that do not support this C++11 feature.
98  operator bool() const { return node; }
99  DdManager * manager() const;
100  DdNode * getNode() const;
101  DdNode * getRegularNode() const;
102  int nodeCount() const;
103  unsigned int NodeReadIndex() const;
104 
105 }; // DD
106 
107 
114 class ABDD : public DD {
115  friend class Cudd;
116 protected:
117  ABDD();
118  ABDD(Capsule *cap, DdNode *bddNode);
119  ABDD(Cudd const & manager, DdNode *ddNode);
120  ABDD(const ABDD &from);
121  ~ABDD();
122 public:
123  bool operator==(const ABDD &other) const;
124  bool operator!=(const ABDD &other) const;
125  void print(int nvars, int verbosity = 1) const;
126  void summary(int nvars, int mode = 0) const;
127  DdApaNumber ApaCountMinterm(int nvars, int * digits) const;
128  void ApaPrintMinterm(int nvars, FILE * fp = stdout) const;
129  void ApaPrintMintermExp(int nvars, int precision = 6, FILE * fp = stdout) const;
130  void EpdPrintMinterm(int nvars, FILE * fp = stdout) const;
131  long double LdblCountMinterm(int nvars) const;
132  bool IsOne() const;
133  bool IsCube() const;
134  BDD FindEssential() const;
135  void PrintTwoLiteralClauses(char ** names = 0, FILE * fp = stdout) const;
136  BDD ShortestPath(int * weight, int * support, int * length) const;
137  BDD LargestCube(int * length = 0) const;
138  int ShortestLength(int * weight = 0) const;
139  bool EquivDC(const ABDD& G, const ABDD& D) const;
140  double * CofMinterm() const;
141  void PrintMinterm() const;
142  double CountMinterm(int nvars) const;
143  double CountPath() const;
144  BDD Support() const;
145  int SupportSize() const;
146  std::vector<unsigned int> SupportIndices() const;
147  void ClassifySupport(const ABDD& g, BDD* common, BDD* onlyF, BDD* onlyG)
148  const;
149  int CountLeaves() const;
150  double Density(int nvars) const;
151 
152 }; // ABDD
153 
154 
161 class BDD : public ABDD {
162  friend class Cudd;
163 public:
164  BDD();
165  BDD(Capsule *cap, DdNode *bddNode);
166  BDD(Cudd const & manager, DdNode *ddNode);
167  BDD(const BDD &from);
168  BDD operator=(const BDD& right);
169  bool operator<=(const BDD& other) const;
170  bool operator>=(const BDD& other) const;
171  bool operator<(const BDD& other) const;
172  bool operator>(const BDD& other) const;
173  BDD operator!() const;
174  BDD operator~() const;
175  BDD operator*(const BDD& other) const;
176  BDD operator*=(const BDD& other);
177  BDD operator&(const BDD& other) const;
178  BDD operator&=(const BDD& other);
179  BDD operator+(const BDD& other) const;
180  BDD operator+=(const BDD& other);
181  BDD operator|(const BDD& other) const;
182  BDD operator|=(const BDD& other);
183  BDD operator^(const BDD& other) const;
184  BDD operator^=(const BDD& other);
185  BDD operator-(const BDD& other) const;
186  BDD operator-=(const BDD& other);
187  friend std::ostream & operator<<(std::ostream & os, BDD const & f);
188  bool IsZero() const;
189  bool IsVar() const;
190  BDD AndAbstract(const BDD& g, const BDD& cube, unsigned int limit = 0)
191  const;
192  BDD UnderApprox(
193  int numVars,
194  int threshold = 0,
195  bool safe = false,
196  double quality = 1.0) const;
197  BDD OverApprox(
198  int numVars,
199  int threshold = 0,
200  bool safe = false,
201  double quality = 1.0) const;
202  BDD RemapUnderApprox(int numVars, int threshold = 0, double quality = 1.0)
203  const;
204  BDD RemapOverApprox(int numVars, int threshold = 0, double quality = 1.0)
205  const;
206  BDD BiasedUnderApprox(const BDD& bias, int numVars, int threshold = 0,
207  double quality1 = 1.0, double quality0 = 1.0) const;
208  BDD BiasedOverApprox(const BDD& bias, int numVars, int threshold = 0,
209  double quality1 = 1.0, double quality0 = 1.0) const;
210  BDD ExistAbstract(const BDD& cube, unsigned int limit = 0) const;
211  BDD XorExistAbstract(const BDD& g, const BDD& cube) const;
212  BDD UnivAbstract(const BDD& cube) const;
213  BDD BooleanDiff(int x) const;
214  bool VarIsDependent(const BDD& var) const;
215  double Correlation(const BDD& g) const;
216  double CorrelationWeights(const BDD& g, double * prob) const;
217  BDD Ite(const BDD& g, const BDD& h, unsigned int limit = 0) const;
218  BDD IteConstant(const BDD& g, const BDD& h) const;
219  BDD Intersect(const BDD& g) const;
220  BDD And(const BDD& g, unsigned int limit = 0) const;
221  BDD Or(const BDD& g, unsigned int limit = 0) const;
222  BDD Nand(const BDD& g) const;
223  BDD Nor(const BDD& g) const;
224  BDD Xor(const BDD& g) const;
225  BDD Xnor(const BDD& g, unsigned int limit = 0) const;
226  bool Leq(const BDD& g) const;
227  ADD Add() const;
228  BDD Transfer(Cudd& destination) const;
229  BDD ClippingAnd(const BDD& g, int maxDepth, int direction = 0) const;
230  BDD ClippingAndAbstract(const BDD& g, const BDD& cube, int maxDepth,
231  int direction = 0) const;
232  BDD Cofactor(const BDD& g) const;
233  bool VarAreSymmetric(int index1, int index2) const;
234  BDD Compose(const BDD& g, int v) const;
235  BDD Permute(int * permut) const;
236  BDD SwapVariables(std::vector<BDD> x, std::vector<BDD> y) const;
237  BDD AdjPermuteX(std::vector<BDD> x) const;
238  BDD VectorCompose(std::vector<BDD> vector) const;
239  void ApproxConjDecomp(BDD* g, BDD* h) const;
240  void ApproxDisjDecomp(BDD* g, BDD* h) const;
241  void IterConjDecomp(BDD* g, BDD* h) const;
242  void IterDisjDecomp(BDD* g, BDD* h) const;
243  void GenConjDecomp(BDD* g, BDD* h) const;
244  void GenDisjDecomp(BDD* g, BDD* h) const;
245  void VarConjDecomp(BDD* g, BDD* h) const;
246  void VarDisjDecomp(BDD* g, BDD* h) const;
247  bool IsVarEssential(int id, int phase) const;
248  BDD Constrain(const BDD& c) const;
249  BDD Restrict(const BDD& c) const;
250  BDD NPAnd(const BDD& g) const;
251  std::vector<BDD> ConstrainDecomp() const;
252  std::vector<BDD> CharToVect() const;
253  BDD LICompaction(const BDD& c) const;
254  BDD Squeeze(const BDD& u) const;
255  BDD Interpolate(const BDD& u) const;
256  BDD Minimize(const BDD& c) const;
257  BDD SubsetCompress(int nvars, int threshold) const;
258  BDD SupersetCompress(int nvars, int threshold) const;
259  BDD LiteralSetIntersection(const BDD& g) const;
260  BDD PrioritySelect(std::vector<BDD> x, std::vector<BDD> y,
261  std::vector<BDD> z, const BDD& Pi, DD_PRFP Pifunc) const;
262  BDD CProjection(const BDD& Y) const;
263  int MinHammingDist(int *minterm, int upperBound) const;
264  BDD Eval(int * inputs) const;
265  BDD Decreasing(int i) const;
266  BDD Increasing(int i) const;
267  bool LeqUnless(const BDD& G, const BDD& D) const;
268  BDD MakePrime(const BDD& F) const;
269  BDD MaximallyExpand(const BDD& ub, const BDD& f);
270  BDD LargestPrimeUnate(const BDD& phases);
271  BDD SolveEqn(const BDD& Y, std::vector<BDD> & G, int ** yIndex, int n) const;
272  BDD VerifySol(std::vector<BDD> const & G, int * yIndex) const;
273  BDD SplitSet(std::vector<BDD> xVars, double m) const;
274  BDD SubsetHeavyBranch(int numVars, int threshold) const;
275  BDD SupersetHeavyBranch(int numVars, int threshold) const;
276  BDD SubsetShortPaths(int numVars, int threshold, bool hardlimit = false) const;
277  BDD SupersetShortPaths(int numVars, int threshold, bool hardlimit = false) const;
278  void PrintCover() const;
279  void PrintCover(const BDD& u) const;
280  int EstimateCofactor(int i, int phase) const;
281  int EstimateCofactorSimple(int i) const;
282  void PickOneCube(char * string) const;
283  BDD PickOneMinterm(std::vector<BDD> vars) const;
284  BDD zddIsop(const BDD& U, ZDD* zdd_I) const;
285  BDD Isop(const BDD& U) const;
286  ZDD PortToZdd() const;
287  void PrintFactoredForm(char const * const * inames = 0, FILE * fp = stdout) const;
288  std::string FactoredFormString(char const * const * inames = 0) const;
289 
290 }; // BDD
291 
292 
299 class ADD : public ABDD {
300  friend class Cudd;
301 public:
302  ADD();
303  ADD(Capsule *cap, DdNode *bddNode);
304  ADD(Cudd const & manager, DdNode *ddNode);
305  ADD(const ADD &from);
306  ADD operator=(const ADD& right);
307  // Relational operators
308  bool operator<=(const ADD& other) const;
309  bool operator>=(const ADD& other) const;
310  bool operator<(const ADD& other) const;
311  bool operator>(const ADD& other) const;
312  // Arithmetic operators
313  ADD operator-() const;
314  ADD operator*(const ADD& other) const;
315  ADD operator*=(const ADD& other);
316  ADD operator+(const ADD& other) const;
317  ADD operator+=(const ADD& other);
318  ADD operator-(const ADD& other) const;
319  ADD operator-=(const ADD& other);
320  // Logical operators
321  ADD operator~() const;
322  ADD operator&(const ADD& other) const;
323  ADD operator&=(const ADD& other);
324  ADD operator|(const ADD& other) const;
325  ADD operator|=(const ADD& other);
326  bool IsZero() const;
327  ADD ExistAbstract(const ADD& cube) const;
328  ADD UnivAbstract(const ADD& cube) const;
329  ADD OrAbstract(const ADD& cube) const;
330  ADD Plus(const ADD& g) const;
331  ADD Times(const ADD& g) const;
332  ADD Threshold(const ADD& g) const;
333  ADD SetNZ(const ADD& g) const;
334  ADD Divide(const ADD& g) const;
335  ADD Minus(const ADD& g) const;
336  ADD Minimum(const ADD& g) const;
337  ADD Maximum(const ADD& g) const;
338  ADD OneZeroMaximum(const ADD& g) const;
339  ADD Diff(const ADD& g) const;
340  ADD Agreement(const ADD& g) const;
341  ADD Or(const ADD& g) const;
342  ADD Nand(const ADD& g) const;
343  ADD Nor(const ADD& g) const;
344  ADD Xor(const ADD& g) const;
345  ADD Xnor(const ADD& g) const;
346  ADD Log() const;
347  ADD FindMax() const;
348  ADD FindMin() const;
349  ADD IthBit(int bit) const;
350  ADD ScalarInverse(const ADD& epsilon) const;
351  ADD Ite(const ADD& g, const ADD& h) const;
352  ADD IteConstant(const ADD& g, const ADD& h) const;
353  ADD EvalConst(const ADD& g) const;
354  bool Leq(const ADD& g) const;
355  ADD Cmpl() const;
356  ADD Negate() const;
357  ADD RoundOff(int N) const;
358  BDD BddThreshold(CUDD_VALUE_TYPE value) const;
359  BDD BddStrictThreshold(CUDD_VALUE_TYPE value) const;
360  BDD BddInterval(CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper) const;
361  BDD BddIthBit(int bit) const;
362  BDD BddPattern() const;
363  ADD Cofactor(const ADD& g) const;
364  ADD Compose(const ADD& g, int v) const;
365  ADD Permute(int * permut) const;
366  ADD SwapVariables(std::vector<ADD> x, std::vector<ADD> y) const;
367  ADD VectorCompose(std::vector<ADD> vector) const;
368  ADD NonSimCompose(std::vector<ADD> vector) const;
369  ADD Constrain(const ADD& c) const;
370  ADD Restrict(const ADD& c) const;
371  ADD MatrixMultiply(const ADD& B, std::vector<ADD> z) const;
372  ADD TimesPlus(const ADD& B, std::vector<ADD> z) const;
373  ADD Triangle(const ADD& g, std::vector<ADD> z) const;
374  ADD Eval(int * inputs) const;
375  bool EqualSupNorm(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr) const;
376 
377 }; // ADD
378 
379 
386 class ZDD : public DD {
387  friend class Cudd;
388 public:
389  ZDD(Capsule *cap, DdNode *bddNode);
390  ZDD();
391  ZDD(const ZDD &from);
392  ~ZDD();
393  ZDD operator=(const ZDD& right);
394  bool operator==(const ZDD& other) const;
395  bool operator!=(const ZDD& other) const;
396  bool operator<=(const ZDD& other) const;
397  bool operator>=(const ZDD& other) const;
398  bool operator<(const ZDD& other) const;
399  bool operator>(const ZDD& other) const;
400  void print(int nvars, int verbosity = 1) const;
401  ZDD operator*(const ZDD& other) const;
402  ZDD operator*=(const ZDD& other);
403  ZDD operator&(const ZDD& other) const;
404  ZDD operator&=(const ZDD& other);
405  ZDD operator+(const ZDD& other) const;
406  ZDD operator+=(const ZDD& other);
407  ZDD operator|(const ZDD& other) const;
408  ZDD operator|=(const ZDD& other);
409  ZDD operator-(const ZDD& other) const;
410  ZDD operator-=(const ZDD& other);
411  int Count() const;
412  double CountDouble() const;
413  ZDD Product(const ZDD& g) const;
414  ZDD UnateProduct(const ZDD& g) const;
415  ZDD WeakDiv(const ZDD& g) const;
416  ZDD Divide(const ZDD& g) const;
417  ZDD WeakDivF(const ZDD& g) const;
418  ZDD DivideF(const ZDD& g) const;
419  double CountMinterm(int path) const;
420  BDD PortToBdd() const;
421  ZDD Ite(const ZDD& g, const ZDD& h) const;
422  ZDD Union(const ZDD& Q) const;
423  ZDD Intersect(const ZDD& Q) const;
424  ZDD Diff(const ZDD& Q) const;
425  ZDD DiffConst(const ZDD& Q) const;
426  ZDD Subset1(int var) const;
427  ZDD Subset0(int var) const;
428  ZDD Change(int var) const;
429  void PrintMinterm() const;
430  void PrintCover() const;
431  BDD Support() const;
432 
433 }; // ZDD
434 
435 
439 extern void defaultError(std::string message);
440 
441 
448 class Cudd {
449  friend class DD;
450  friend class ABDD;
451  friend class BDD;
452  friend class ADD;
453  friend class ZDD;
454  friend std::ostream & operator<<(std::ostream & os, BDD const & f);
455 private:
456  Capsule *p;
457 public:
458  Cudd(
459  unsigned int numVars = 0,
460  unsigned int numVarsZ = 0,
461  unsigned int numSlots = CUDD_UNIQUE_SLOTS,
462  unsigned int cacheSize = CUDD_CACHE_SLOTS,
463  unsigned long maxMemory = 0,
464  PFC defaultHandler = defaultError);
465  Cudd(const Cudd& x);
466  ~Cudd(void);
467  PFC setHandler(PFC newHandler) const;
468  PFC getHandler(void) const;
469  PFC setTimeoutHandler(PFC newHandler) const;
470  PFC getTimeoutHandler(void) const;
471  PFC setTerminationHandler(PFC newHandler) const;
472  PFC getTerminationHandler(void) const;
473  void pushVariableName(std::string s) const;
474  void clearVariableNames(void) const;
475  std::string getVariableName(size_t i) const;
476  DdManager *getManager(void) const;
477  void makeVerbose(void) const;
478  void makeTerse(void) const;
479  bool isVerbose(void) const;
480  void checkReturnValue(const void *result) const;
481  void checkReturnValue(const int result) const;
482  Cudd& operator=(const Cudd& right);
483  void info(void) const;
484  BDD bddVar(void) const;
485  BDD bddVar(int index) const;
486  BDD bddOne(void) const;
487  BDD bddZero(void) const;
488  ADD addVar(void) const;
489  ADD addVar(int index) const;
490  ADD addOne(void) const;
491  ADD addZero(void) const;
492  ADD constant(CUDD_VALUE_TYPE c) const;
493  ADD plusInfinity(void) const;
494  ADD minusInfinity(void) const;
495  ZDD zddVar(int index) const;
496  ZDD zddOne(int i) const;
497  ZDD zddZero(void) const;
498  ADD addNewVarAtLevel(int level) const;
499  BDD bddNewVarAtLevel(int level) const;
500  void zddVarsFromBddVars(int multiplicity) const;
501  unsigned long ReadStartTime(void) const;
502  unsigned long ReadElapsedTime(void) const;
503  void SetStartTime(unsigned long st) const;
504  void ResetStartTime(void) const;
505  unsigned long ReadTimeLimit(void) const;
506  unsigned long SetTimeLimit(unsigned long tl) const;
507  void UpdateTimeLimit(void) const;
508  void IncreaseTimeLimit(unsigned long increase) const;
509  void UnsetTimeLimit(void) const;
510  bool TimeLimited(void) const;
511  void RegisterTerminationCallback(DD_THFP callback,
512  void * callback_arg) const;
513  void UnregisterTerminationCallback(void) const;
514  DD_OOMFP RegisterOutOfMemoryCallback(DD_OOMFP callback) const;
515  void UnregisterOutOfMemoryCallback(void) const;
516  void AutodynEnable(Cudd_ReorderingType method = CUDD_REORDER_SIFT) const;
517  void AutodynDisable(void) const;
518  bool ReorderingStatus(Cudd_ReorderingType * method) const;
519  void AutodynEnableZdd(Cudd_ReorderingType method = CUDD_REORDER_SIFT) const;
520  void AutodynDisableZdd(void) const;
521  bool ReorderingStatusZdd(Cudd_ReorderingType * method) const;
522  bool zddRealignmentEnabled(void) const;
523  void zddRealignEnable(void) const;
524  void zddRealignDisable(void) const;
525  bool bddRealignmentEnabled(void) const;
526  void bddRealignEnable(void) const;
527  void bddRealignDisable(void) const;
528  ADD background(void) const;
529  void SetBackground(ADD bg) const;
530  unsigned int ReadCacheSlots(void) const;
531  double ReadCacheUsedSlots(void) const;
532  double ReadCacheLookUps(void) const;
533  double ReadCacheHits(void) const;
534  unsigned int ReadMinHit(void) const;
535  void SetMinHit(unsigned int hr) const;
536  unsigned int ReadLooseUpTo(void) const;
537  void SetLooseUpTo(unsigned int lut) const;
538  unsigned int ReadMaxCache(void) const;
539  unsigned int ReadMaxCacheHard(void) const;
540  void SetMaxCacheHard(unsigned int mc) const;
541  int ReadSize(void) const;
542  int ReadZddSize(void) const;
543  unsigned int ReadSlots(void) const;
544  unsigned int ReadKeys(void) const;
545  unsigned int ReadDead(void) const;
546  unsigned int ReadMinDead(void) const;
547  unsigned int ReadReorderings(void) const;
548  unsigned int ReadMaxReorderings(void) const;
549  void SetMaxReorderings(unsigned int mr) const;
550  long ReadReorderingTime(void) const;
551  int ReadGarbageCollections(void) const;
552  long ReadGarbageCollectionTime(void) const;
553  int ReadSiftMaxVar(void) const;
554  void SetSiftMaxVar(int smv) const;
555  int ReadSiftMaxSwap(void) const;
556  void SetSiftMaxSwap(int sms) const;
557  double ReadMaxGrowth(void) const;
558  void SetMaxGrowth(double mg) const;
559 #ifdef MTR_H_
560  MtrNode * ReadTree(void) const;
561  void SetTree(MtrNode * tree) const;
562  void FreeTree(void) const;
563  MtrNode * ReadZddTree(void) const;
564  void SetZddTree(MtrNode * tree) const;
565  void FreeZddTree(void) const;
566  MtrNode * MakeTreeNode(unsigned int low, unsigned int size,
567  unsigned int type) const;
568  MtrNode * MakeZddTreeNode(unsigned int low, unsigned int size,
569  unsigned int type) const;
570 #endif
571  int ReadPerm(int i) const;
572  int ReadPermZdd(int i) const;
573  int ReadInvPerm(int i) const;
574  int ReadInvPermZdd(int i) const;
575  BDD ReadVars(int i) const;
576  CUDD_VALUE_TYPE ReadEpsilon(void) const;
577  void SetEpsilon(CUDD_VALUE_TYPE ep) const;
578  Cudd_AggregationType ReadGroupcheck(void) const;
579  void SetGroupcheck(Cudd_AggregationType gc) const;
580  bool GarbageCollectionEnabled(void) const;
581  void EnableGarbageCollection(void) const;
582  void DisableGarbageCollection(void) const;
583  bool DeadAreCounted(void) const;
584  void TurnOnCountDead(void) const;
585  void TurnOffCountDead(void) const;
586  int ReadRecomb(void) const;
587  void SetRecomb(int recomb) const;
588  int ReadSymmviolation(void) const;
589  void SetSymmviolation(int symmviolation) const;
590  int ReadArcviolation(void) const;
591  void SetArcviolation(int arcviolation) const;
592  int ReadPopulationSize(void) const;
593  void SetPopulationSize(int populationSize) const;
594  int ReadNumberXovers(void) const;
595  void SetNumberXovers(int numberXovers) const;
596  unsigned int ReadOrderRandomization(void) const;
597  void SetOrderRandomization(unsigned int factor) const;
598  unsigned long ReadMemoryInUse(void) const;
599  long ReadPeakNodeCount(void) const;
600  long ReadNodeCount(void) const;
601  long zddReadNodeCount(void) const;
602  void AddHook(DD_HFP f, Cudd_HookType where) const;
603  void RemoveHook(DD_HFP f, Cudd_HookType where) const;
604  bool IsInHook(DD_HFP f, Cudd_HookType where) const;
605  void EnableReorderingReporting(void) const;
606  void DisableReorderingReporting(void) const;
607  bool ReorderingReporting(void) const;
608  int ReadErrorCode(void) const;
609  DD_OOMFP InstallOutOfMemoryHandler(DD_OOMFP newHandler) const;
610  void ClearErrorCode(void) const;
611  FILE *ReadStdout(void) const;
612  void SetStdout(FILE * fp) const;
613  FILE *ReadStderr(void) const;
614  void SetStderr(FILE * fp) const;
615  unsigned int ReadNextReordering(void) const;
616  void SetNextReordering(unsigned int) const;
617  double ReadSwapSteps(void) const;
618  unsigned int ReadMaxLive(void) const;
619  void SetMaxLive(unsigned int) const;
620  size_t ReadMaxMemory(void) const;
621  size_t SetMaxMemory(size_t) const;
622  int bddBindVar(int) const;
623  int bddUnbindVar(int) const;
624  bool bddVarIsBound(int) const;
625  ADD Walsh(std::vector<ADD> x, std::vector<ADD> y) const;
626  ADD addResidue(int n, int m, int options, int top) const;
627  int ApaNumberOfDigits(int binaryDigits) const;
628  DdApaNumber NewApaNumber(int digits) const;
629  void ApaCopy(int digits, DdApaNumber source, DdApaNumber dest) const;
630  DdApaDigit ApaAdd(int digits, DdApaNumber a, DdApaNumber b, DdApaNumber
631  sum) const;
632  DdApaDigit ApaSubtract(int digits, DdApaNumber a, DdApaNumber b,
633  DdApaNumber diff) const;
634  DdApaDigit ApaShortDivision(int digits, DdApaNumber dividend, DdApaDigit
635  divisor, DdApaNumber quotient) const;
636  void ApaShiftRight(int digits, DdApaDigit in, DdApaNumber a, DdApaNumber
637  b) const;
638  void ApaSetToLiteral(int digits, DdApaNumber number, DdApaDigit literal)
639  const;
640  void ApaPowerOfTwo(int digits, DdApaNumber number, int power) const;
641  void ApaPrintHex(int digits, DdApaNumber number, FILE * fp = stdout) const;
642  void ApaPrintDecimal(int digits, DdApaNumber number, FILE * fp = stdout) const;
643  std::string ApaStringDecimal(int digits, DdApaNumber number) const;
644  void ApaPrintExponential(int digits, DdApaNumber number,
645  int precision = 6, FILE * fp = stdout) const;
646  void DebugCheck(void) const;
647  void CheckKeys(void) const;
648  ADD Harwell(FILE * fp, std::vector<ADD>& x, std::vector<ADD>& y,
649  std::vector<ADD>& xn, std::vector<ADD>& yn_,
650  int * m, int * n, int bx = 0, int sx = 2, int by = 1,
651  int sy = 2, int pr = 0) const;
652  void PrintLinear(void) const;
653  int ReadLinear(int x, int y) const;
654  BDD Xgty(std::vector<BDD> z, std::vector<BDD> x, std::vector<BDD> y) const;
655  BDD Xeqy(std::vector<BDD> x, std::vector<BDD> y) const;
656  ADD Xeqy(std::vector<ADD> x, std::vector<ADD> y) const;
657  BDD Dxygtdxz(std::vector<BDD> x, std::vector<BDD> y,
658  std::vector<BDD> z) const;
659  BDD Dxygtdyz(std::vector<BDD> x, std::vector<BDD> y,
660  std::vector<BDD> z) const;
661  BDD Inequality(int c, std::vector<BDD> x, std::vector<BDD> y) const;
662  BDD Disequality(int c, std::vector<BDD> x, std::vector<BDD> y) const;
663  BDD Interval(std::vector<BDD> x, unsigned int lowerB,
664  unsigned int upperB) const;
665  ADD Hamming(std::vector<ADD> xVars, std::vector<ADD> yVars) const;
666  ADD Read(FILE * fp, std::vector<ADD>& x, std::vector<ADD>& y, std::vector<ADD>& xn,
667  std::vector<ADD>& yn_, int * m, int * n, int bx = 0, int sx = 2,
668  int by = 1, int sy = 2) const;
669  BDD Read(FILE * fp, std::vector<BDD>& x, std::vector<BDD>& y,
670  int * m, int * n, int bx = 0, int sx = 2, int by = 1,
671  int sy = 2) const;
672  void ReduceHeap(Cudd_ReorderingType heuristic = CUDD_REORDER_SIFT,
673  int minsize = 0) const;
674  void ShuffleHeap(int * permutation) const;
675  void SymmProfile(int lower, int upper) const;
676  unsigned int Prime(unsigned int pr) const;
677  void Reserve(int amount) const;
678  int SharingSize(DD* nodes, int n) const;
679  int SharingSize(const std::vector<BDD>& v) const;
680  BDD bddComputeCube(BDD * vars, int * phase, int n) const;
681  BDD computeCube(std::vector<BDD> const & vars) const;
682  ADD addComputeCube(ADD * vars, int * phase, int n) const;
683  ADD computeCube(std::vector<ADD> const & vars) const;
684  BDD IndicesToCube(int * array, int n) const;
685  void PrintVersion(FILE * fp) const;
686  double AverageDistance(void) const;
687  int32_t Random(void) const;
688  void Srandom(int32_t seed) const;
689  void zddPrintSubtable() const;
690  void zddReduceHeap(Cudd_ReorderingType heuristic = CUDD_REORDER_SIFT,
691  int minsize = 0) const;
692  void zddShuffleHeap(int * permutation) const;
693  void zddSymmProfile(int lower, int upper) const;
694  void DumpDot(
695  const std::vector<BDD>& nodes,
696  char const * const * inames = 0,
697  char const * const * onames = 0,
698  FILE * fp = stdout) const;
699  void DumpDaVinci(
700  const std::vector<BDD>& nodes,
701  char const * const * inames = 0,
702  char const * const * onames = 0,
703  FILE * fp = stdout) const;
704  void DumpBlif(
705  const std::vector<BDD>& nodes,
706  char const * const * inames = 0,
707  char const * const * onames = 0,
708  char * mname = 0,
709  FILE * fp = stdout,
710  int mv = 0) const;
711  void DumpDDcal(
712  const std::vector<BDD>& nodes,
713  char const * const * inames = 0,
714  char const * const * onames = 0,
715  FILE * fp = stdout) const;
716  void DumpFactoredForm(
717  const std::vector<BDD>& nodes,
718  char const * const * inames = 0,
719  char const * const * onames = 0,
720  FILE * fp = stdout) const;
721  BDD VectorSupport(const std::vector<BDD>& roots) const;
722  std::vector<unsigned int>
723  SupportIndices(const std::vector<BDD>& roots) const;
724  std::vector<unsigned int>
725  SupportIndices(const std::vector<ADD>& roots) const;
726  int nodeCount(const std::vector<BDD>& roots) const;
727  int VectorSupportSize(const std::vector<BDD>& roots) const;
728  void DumpDot(
729  const std::vector<ADD>& nodes,
730  char const * const * inames = 0,
731  char const * const * onames = 0,
732  FILE * fp = stdout) const;
733  void DumpDaVinci(
734  const std::vector<ADD>& nodes,
735  char const * const * inames = 0,
736  char const * const * onames = 0,
737  FILE * fp = stdout) const;
738  BDD VectorSupport(const std::vector<ADD>& roots) const;
739  int VectorSupportSize(const std::vector<ADD>& roots) const;
740  void DumpDot(
741  const std::vector<ZDD>& nodes,
742  char const * const * inames = 0,
743  char const * const * onames = 0,
744  FILE * fp = stdout) const;
745  std::string OrderString(void) const;
746 
747 }; // Cudd
748 
749 
750 #endif
ADD
Class for ADDs.
Definition: cuddObj.hh:299
BDD
Class for BDDs.
Definition: cuddObj.hh:161
CUDD_UNIQUE_SLOTS
#define CUDD_UNIQUE_SLOTS
Definition: cudd.h:74
Cudd_AggregationType
Cudd_AggregationType
Type of aggregation methods.
Definition: cudd.h:123
DdNode
Decision diagram node.
Definition: cuddInt.h:261
MtrNode_
multi-way tree node.
Definition: mtrInt.h:109
defaultError
void defaultError(std::string message)
Default error handler.
CUDD_CACHE_SLOTS
#define CUDD_CACHE_SLOTS
Definition: cudd.h:75
DdManager
Specialized DD symbol table.
Definition: cuddInt.h:399
DD_OOMFP
void(* DD_OOMFP)(size_t)
Type of memory-out function.
Definition: cudd.h:258
cudd.h
The University of Colorado decision diagram package.
Cudd_HookType
Cudd_HookType
Type of hooks.
Definition: cudd.h:140
DD_HFP
int(* DD_HFP)(DdManager *, const char *, void *)
Type of hook function.
Definition: cudd.h:234
DD
Base class for all decision diagrams in CUDD.
Definition: cuddObj.hh:82
Capsule
Class for reference counting of CUDD managers.
Definition: cuddObj.cc:80
Cudd
Class for CUDD managers.
Definition: cuddObj.hh:448
DdApaNumber
DdApaDigit * DdApaNumber
Type of an arbitrary precision intger, which is an array of digits.
Definition: cudd.h:219
DD_THFP
int(* DD_THFP)(const void *)
Type of termination handler.
Definition: cudd.h:266
DdApaDigit
uint32_t DdApaDigit
Type of an arbitrary precision integer "digit.".
Definition: cudd.h:214
ZDD
Class for ZDDs.
Definition: cuddObj.hh:386
DD_PRFP
DdNode *(* DD_PRFP)(DdManager *, int, DdNode **, DdNode **, DdNode **)
Type of priority function.
Definition: cudd.h:238
ABDD
Class for ADDs and BDDs.
Definition: cuddObj.hh:114
onames
static char const * onames[]
Definition: ntr.c:67
Cudd_ReorderingType
Cudd_ReorderingType
Type of reordering algorithm.
Definition: cudd.h:94
CUDD_VALUE_TYPE
double CUDD_VALUE_TYPE
Type of the value of a terminal node.
Definition: cudd.h:189
Generated on Thu Jun 21 2018 10:18:16 for cudd by   doxygen 1.8.14