distr/obj/cuddObj.hh

   1 /**CHeaderFile***************************************************************
   2
   3   FileName    [cuddObj.hh]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Class definitions for C++ object-oriented encapsulation of
   8   CUDD.]
   9
  10   Description [Class definitions for C++ object-oriented encapsulation of
  11   CUDD.]
  12
  13   SeeAlso     []
  14
  15   Author      [Fabio Somenzi]
  16
  17   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  18
  19   All rights reserved.
  20
  21   Redistribution and use in source and binary forms, with or without
  22   modification, are permitted provided that the following conditions
  23   are met:
  24
  25   Redistributions of source code must retain the above copyright
  26   notice, this list of conditions and the following disclaimer.
  27
  28   Redistributions in binary form must reproduce the above copyright
  29   notice, this list of conditions and the following disclaimer in the
  30   documentation and/or other materials provided with the distribution.
  31
  32   Neither the name of the University of Colorado nor the names of its
  33   contributors may be used to endorse or promote products derived from
  34   this software without specific prior written permission.
  35
  36   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  37   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  38   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  39   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  40   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  41   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  42   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  43   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  44   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  45   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  46   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  47   POSSIBILITY OF SUCH DAMAGE.]
  48
  49   Revision    [$Id: cuddObj.hh,v 1.11 2009/02/21 19:41:38 fabio Exp fabio $]
  50
  51 ******************************************************************************/
  52
  53 #ifndef _CPPCUDD
  54 #define _CPPCUDD
  55
  56 /*---------------------------------------------------------------------------*/
  57 /* Nested includes                                                           */
  58 /*---------------------------------------------------------------------------*/
  59
  60 #include <string>
  61 #include <iostream>
  62 #include "util.h"
  63 #include "cudd.h"
  64
  65 using std::cout;
  66 using std::cerr;
  67 using std::endl;
  68 using std::hex;
  69 using std::string;
  70
  71 /*---------------------------------------------------------------------------*/
  72 /* Type definitions                                                          */
  73 /*---------------------------------------------------------------------------*/
  74
  75 class ADD;
  76 class BDD;
  77 class ZDD;
  78 class Cudd;
  79 class BDDvector;
  80 class ADDvector;
  81 class ZDDvector;
  82
  83 typedef void (*PFC)(string);    // error function type
  84
  85 /*---------------------------------------------------------------------------*/
  86 /* Class definitions                                                         */
  87 /*---------------------------------------------------------------------------*/
  88
  89
  90 /**Class***********************************************************************
  91
  92   Synopsis     [Base class for all decision diagrams in CUDD.]
  93
  94   Description  []
  95
  96   SeeAlso      [Cudd ABDD ADD BDD ZDD]
  97
  98 ******************************************************************************/
  99 class DD {
 100     friend class ABDD;
 101     friend class ADD;
 102     friend class BDD;
 103     friend class ZDD;
 104     Cudd *ddMgr;
 105     DdNode *node;
 106     inline DdManager * checkSameManager(const DD &other) const;
 107     inline void checkReturnValue(const DdNode *result) const;
 108     inline void checkReturnValue(const int result, const int expected = 1)
 109         const;
 110 public:
 111     DD(Cudd *ddManager, DdNode *ddNode);
 112     DD();
 113     DD(const DD &from);
 114     virtual ~DD();
 115     Cudd *manager() const;
 116     inline DdNode * getNode() const;
 117     int nodeCount() const;
 118     unsigned int NodeReadIndex() const;
 119
 120 }; // DD
 121
 122
 123 /**Class***********************************************************************
 124
 125   Synopsis     [Class for ADDs and BDDs.]
 126
 127   Description  []
 128
 129   SeeAlso      [Cudd ADD BDD]
 130
 131 ******************************************************************************/
 132 class ABDD : public DD {
 133     friend class BDD;
 134     friend class ADD;
 135     friend class Cudd;
 136 public:
 137     ABDD(Cudd *bddManager, DdNode *bddNode);
 138     ABDD();
 139     ABDD(const ABDD &from);
 140     virtual ~ABDD();
 141     int operator==(const ABDD &other) const;
 142     int operator!=(const ABDD &other) const;
 143     void print(int nvars, int verbosity = 1) const;
 144     DdApaNumber ApaCountMinterm(int nvars, int * digits) const;
 145     void ApaPrintMinterm(int nvars, FILE * fp = stdout) const;
 146     void EpdPrintMinterm(int nvars, FILE * fp = stdout) const;
 147     BDD FindEssential() const;
 148     void PrintTwoLiteralClauses(char ** names, FILE * fp = stdout) const;
 149     BDD ShortestPath(int * weight, int * support, int * length) const;
 150     BDD LargestCube(int * length) const;
 151     int ShortestLength(int * weight) const;
 152     int EquivDC(const ABDD& G, const ABDD& D) const;
 153     double * CofMinterm() const;
 154     void PrintMinterm() const;
 155     double CountMinterm(int nvars) const;
 156     double CountPath() const;
 157     BDD Support() const;
 158     int SupportSize() const;
 159     void ClassifySupport(const ABDD& g, BDD* common, BDD* onlyF, BDD* onlyG)
 160         const;
 161     int CountLeaves() const;
 162     DdGen * FirstCube(int ** cube, CUDD_VALUE_TYPE * value) const;
 163     double Density(int nvars) const;
 164
 165 }; // ABDD
 166
 167
 168 /**Class***********************************************************************
 169
 170   Synopsis     [Class for BDDs.]
 171
 172   Description  []
 173
 174   SeeAlso      [Cudd]
 175
 176 ******************************************************************************/
 177 class BDD : public ABDD {
 178     friend class Cudd;
 179 public:
 180     BDD(Cudd *bddManager, DdNode *bddNode);
 181     BDD();
 182     BDD(const BDD &from);
 183     int operator==(const BDD& other) const;
 184     int operator!=(const BDD& other) const;
 185     BDD operator=(const BDD& right);
 186     int operator<=(const BDD& other) const;
 187     int operator>=(const BDD& other) const;
 188     int operator<(const BDD& other) const;
 189     int operator>(const BDD& other) const;
 190     BDD operator!() const;
 191     BDD operator~() const;
 192     BDD operator*(const BDD& other) const;
 193     BDD operator*=(const BDD& other);
 194     BDD operator&(const BDD& other) const;
 195     BDD operator&=(const BDD& other);
 196     BDD operator+(const BDD& other) const;
 197     BDD operator+=(const BDD& other);
 198     BDD operator|(const BDD& other) const;
 199     BDD operator|=(const BDD& other);
 200     BDD operator^(const BDD& other) const;
 201     BDD operator^=(const BDD& other);
 202     BDD operator-(const BDD& other) const;
 203     BDD operator-=(const BDD& other);
 204     BDD AndAbstract(const BDD& g, const BDD& cube) const;
 205     BDD AndAbstractLimit(const BDD& g, const BDD& cube, unsigned int limit)
 206         const;
 207     BDD UnderApprox(
 208       int numVars,
 209       int threshold = 0,
 210       int safe = 0,
 211       double quality = 1.0) const;
 212     BDD OverApprox(
 213       int numVars,
 214       int threshold = 0,
 215       int safe = 0,
 216       double quality = 1.0) const;
 217     BDD RemapUnderApprox(int numVars, int threshold = 0, double quality = 1.0)
 218         const;
 219     BDD RemapOverApprox(int numVars, int threshold = 0, double quality = 1.0)
 220         const;
 221     BDD ExistAbstract(const BDD& cube) const;
 222     BDD XorExistAbstract(const BDD& g, const BDD& cube) const;
 223     BDD UnivAbstract(const BDD& cube) const;
 224     BDD BooleanDiff(int x) const;
 225     int VarIsDependent(const BDD& var) const;
 226     double Correlation(const BDD& g) const;
 227     double CorrelationWeights(const BDD& g, double * prob) const;
 228     BDD Ite(const BDD& g, const BDD& h) const;
 229     BDD IteConstant(const BDD& g, const BDD& h) const;
 230     BDD Intersect(const BDD& g) const;
 231     BDD And(const BDD& g) const;
 232     BDD AndLimit(const BDD& g, unsigned int limit) const;
 233     BDD Or(const BDD& g) const;
 234     BDD Nand(const BDD& g) const;
 235     BDD Nor(const BDD& g) const;
 236     BDD Xor(const BDD& g) const;
 237     BDD Xnor(const BDD& g) const;
 238     int Leq(const BDD& g) const;
 239     ADD Add() const;
 240     BDD Transfer(Cudd& destination) const;
 241     BDD ClippingAnd(const BDD& g, int maxDepth, int direction) const;
 242     BDD ClippingAndAbstract(const BDD& g, const BDD& cube, int maxDepth,
 243                             int direction) const;
 244     BDD Cofactor(const BDD& g) const;
 245     BDD Compose(const BDD& g, int v) const;
 246     BDD Permute(int * permut) const;
 247     BDD SwapVariables(BDDvector x, BDDvector y) const;
 248     BDD AdjPermuteX(BDDvector x) const;
 249     BDD VectorCompose(BDDvector vector) const;
 250     void ApproxConjDecomp(BDD* g, BDD* h) const;
 251     void ApproxDisjDecomp(BDD* g, BDD* h) const;
 252     void IterConjDecomp(BDD* g, BDD* h) const;
 253     void IterDisjDecomp(BDD* g, BDD* h) const;
 254     void GenConjDecomp(BDD* g, BDD* h) const;
 255     void GenDisjDecomp(BDD* g, BDD* h) const;
 256     void VarConjDecomp(BDD* g, BDD* h) const;
 257     void VarDisjDecomp(BDD* g, BDD* h) const;
 258     int IsVarEssential(int id, int phase) const;
 259     BDD Constrain(const BDD& c) const;
 260     BDD Restrict(const BDD& c) const;
 261     BDD NPAnd(const BDD& g) const;
 262     BDDvector ConstrainDecomp() const;
 263     BDDvector CharToVect() const;
 264     BDD LICompaction(const BDD& c) const;
 265     BDD Squeeze(const BDD& u) const;
 266     BDD Minimize(const BDD& c) const;
 267     BDD SubsetCompress(int nvars, int threshold) const;
 268     BDD SupersetCompress(int nvars, int threshold) const;
 269     BDD LiteralSetIntersection(const BDD& g) const;
 270     BDD PrioritySelect(BDDvector x, BDDvector y, BDDvector z, const BDD& Pi,
 271                        DD_PRFP Pifunc) const;
 272     BDD CProjection(const BDD& Y) const;
 273     int MinHammingDist(int *minterm, int upperBound) const;
 274     BDD Eval(int * inputs) const;
 275     BDD Decreasing(int i) const;
 276     BDD Increasing(int i) const;
 277     BDD SolveEqn(const BDD& Y, BDD* G, int ** yIndex, int n) const;
 278     BDD VerifySol(BDD* G, int * yIndex, int n) const;
 279     BDD SplitSet(BDDvector xVars, double m) const;
 280     BDD SubsetHeavyBranch(int numVars, int threshold) const;
 281     BDD SupersetHeavyBranch(int numVars, int threshold) const;
 282     BDD SubsetShortPaths(int numVars, int threshold, int hardlimit) const;
 283     BDD SupersetShortPaths(int numVars, int threshold, int hardlimit) const;
 284     void PrintCover() const;
 285     void PrintCover(const BDD& u) const;
 286     int EstimateCofactor(int i, int phase) const;
 287     int EstimateCofactorSimple(int i) const;
 288     void PickOneCube(char * string) const;
 289     BDD PickOneMinterm(BDDvector vars) const;
 290     DdGen * FirstNode(BDD* fnode) const;
 291     BDD zddIsop(const BDD& U, ZDD* zdd_I) const;
 292     BDD Isop(const BDD& U) const;
 293     ZDD PortToZdd() const;
 294
 295 }; // BDD
 296
 297
 298 /**Class***********************************************************************
 299
 300   Synopsis     [Class for ADDs.]
 301
 302   Description  []
 303
 304   SeeAlso      [Cudd]
 305
 306 ******************************************************************************/
 307 class ADD : public ABDD {
 308     friend class Cudd;
 309 public:
 310     ADD(Cudd *bddManager, DdNode *bddNode);
 311     ADD();
 312     ADD(const ADD &from);
 313     int operator==(const ADD& other) const;
 314     int operator!=(const ADD& other) const;
 315     ADD operator=(const ADD& right);
 316     // Relational operators
 317     int operator<=(const ADD& other) const;
 318     int operator>=(const ADD& other) const;
 319     int operator<(const ADD& other) const;
 320     int operator>(const ADD& other) const;
 321     // Arithmetic operators
 322     ADD operator-() const;
 323     ADD operator*(const ADD& other) const;
 324     ADD operator*=(const ADD& other);
 325     ADD operator+(const ADD& other) const;
 326     ADD operator+=(const ADD& other);
 327     ADD operator-(const ADD& other) const;
 328     ADD operator-=(const ADD& other);
 329     // Logical operators
 330     ADD operator~() const;
 331     ADD operator&(const ADD& other) const;
 332     ADD operator&=(const ADD& other);
 333     ADD operator|(const ADD& other) const;
 334     ADD operator|=(const ADD& other);
 335     ADD ExistAbstract(const ADD& cube) const;
 336     ADD UnivAbstract(const ADD& cube) const;
 337     ADD OrAbstract(const ADD& cube) const;
 338     ADD Plus(const ADD& g) const;
 339     ADD Times(const ADD& g) const;
 340     ADD Threshold(const ADD& g) const;
 341     ADD SetNZ(const ADD& g) const;
 342     ADD Divide(const ADD& g) const;
 343     ADD Minus(const ADD& g) const;
 344     ADD Minimum(const ADD& g) const;
 345     ADD Maximum(const ADD& g) const;
 346     ADD OneZeroMaximum(const ADD& g) const;
 347     ADD Diff(const ADD& g) const;
 348     ADD Agreement(const ADD& g) const;
 349     ADD Or(const ADD& g) const;
 350     ADD Nand(const ADD& g) const;
 351     ADD Nor(const ADD& g) const;
 352     ADD Xor(const ADD& g) const;
 353     ADD Xnor(const ADD& g) const;
 354     ADD Log() const;
 355     ADD FindMax() const;
 356     ADD FindMin() const;
 357     ADD IthBit(int bit) const;
 358     ADD ScalarInverse(const ADD& epsilon) const;
 359     ADD Ite(const ADD& g, const ADD& h) const;
 360     ADD IteConstant(const ADD& g, const ADD& h) const;
 361     ADD EvalConst(const ADD& g) const;
 362     int Leq(const ADD& g) const;
 363     ADD Cmpl() const;
 364     ADD Negate() const;
 365     ADD RoundOff(int N) const;
 366     BDD BddThreshold(CUDD_VALUE_TYPE value) const;
 367     BDD BddStrictThreshold(CUDD_VALUE_TYPE value) const;
 368     BDD BddInterval(CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper) const;
 369     BDD BddIthBit(int bit) const;
 370     BDD BddPattern() const;
 371     ADD Cofactor(const ADD& g) const;
 372     ADD Compose(const ADD& g, int v) const;
 373     ADD Permute(int * permut) const;
 374     ADD SwapVariables(ADDvector x, ADDvector y) const;
 375     ADD VectorCompose(ADDvector vector) const;
 376     ADD NonSimCompose(ADDvector vector) const;
 377     ADD Constrain(const ADD& c) const;
 378     ADD Restrict(const ADD& c) const;
 379     ADD MatrixMultiply(const ADD& B, ADDvector z) const;
 380     ADD TimesPlus(const ADD& B, ADDvector z) const;
 381     ADD Triangle(const ADD& g, ADDvector z) const;
 382     ADD Eval(int * inputs) const;
 383     int EqualSupNorm(const ADD& g, CUDD_VALUE_TYPE tolerance, int pr) const;
 384
 385 }; // ADD
 386
 387
 388 /**Class***********************************************************************
 389
 390   Synopsis     [Class for ZDDs.]
 391
 392   Description  []
 393
 394   SeeAlso      [Cudd]
 395
 396 ******************************************************************************/
 397 class ZDD : public DD {
 398     friend class Cudd;
 399 public:
 400     ZDD(Cudd *bddManager, DdNode *bddNode);
 401     ZDD();
 402     ZDD(const ZDD &from);
 403     ~ZDD();
 404     ZDD operator=(const ZDD& right);
 405     int operator==(const ZDD& other) const;
 406     int operator!=(const ZDD& other) const;
 407     int operator<=(const ZDD& other) const;
 408     int operator>=(const ZDD& other) const;
 409     int operator<(const ZDD& other) const;
 410     int operator>(const ZDD& other) const;
 411     void print(int nvars, int verbosity = 1) const;
 412     ZDD operator*(const ZDD& other) const;
 413     ZDD operator*=(const ZDD& other);
 414     ZDD operator&(const ZDD& other) const;
 415     ZDD operator&=(const ZDD& other);
 416     ZDD operator+(const ZDD& other) const;
 417     ZDD operator+=(const ZDD& other);
 418     ZDD operator|(const ZDD& other) const;
 419     ZDD operator|=(const ZDD& other);
 420     ZDD operator-(const ZDD& other) const;
 421     ZDD operator-=(const ZDD& other);
 422     int Count() const;
 423     double CountDouble() const;
 424     ZDD Product(const ZDD& g) const;
 425     ZDD UnateProduct(const ZDD& g) const;
 426     ZDD WeakDiv(const ZDD& g) const;
 427     ZDD Divide(const ZDD& g) const;
 428     ZDD WeakDivF(const ZDD& g) const;
 429     ZDD DivideF(const ZDD& g) const;
 430     double CountMinterm(int path) const;
 431     BDD PortToBdd() const;
 432     ZDD Ite(const ZDD& g, const ZDD& h) const;
 433     ZDD Union(const ZDD& Q) const;
 434     ZDD Intersect(const ZDD& Q) const;
 435     ZDD Diff(const ZDD& Q) const;
 436     ZDD DiffConst(const ZDD& Q) const;
 437     ZDD Subset1(int var) const;
 438     ZDD Subset0(int var) const;
 439     ZDD Change(int var) const;
 440     void PrintMinterm() const;
 441     void PrintCover() const;
 442
 443 }; // ZDD
 444
 445
 446 /**Class***********************************************************************
 447
 448   Synopsis     [Class for CUDD managers.]
 449
 450   Description  []
 451
 452   SeeAlso      [DD]
 453
 454 ******************************************************************************/
 455 class Cudd {
 456     friend class DD;
 457     friend class ABDD;
 458     friend class ADD;
 459     friend class BDD;
 460     friend class ZDD;
 461     struct capsule {
 462         DdManager *manager;
 463         PFC errorHandler;
 464         int verbose;
 465         int ref;
 466     };
 467     capsule *p;
 468 public:
 469     Cudd(
 470       unsigned int numVars = 0,
 471       unsigned int numVarsZ = 0,
 472       unsigned int numSlots = CUDD_UNIQUE_SLOTS,
 473       unsigned int cacheSize = CUDD_CACHE_SLOTS,
 474       unsigned long maxMemory = 0);
 475     Cudd(Cudd& x);
 476     ~Cudd();
 477     PFC setHandler(PFC newHandler);
 478     PFC getHandler() const;
 479     DdManager *getManager() const {return p->manager;}
 480     inline void makeVerbose() {p->verbose = 1;}
 481     inline void makeTerse() {p->verbose = 0;}
 482     inline int isVerbose() const {return p->verbose;}
 483     inline void checkReturnValue(const DdNode *result) const;
 484     inline void checkReturnValue(const int result) const;
 485     Cudd& operator=(const Cudd& right);
 486     void info() const;
 487     BDD bddVar();
 488     BDD bddVar(int index);
 489     BDD bddOne();
 490     BDD bddZero();
 491     ADD addVar();
 492     ADD addVar(int index);
 493     ADD addOne();
 494     ADD addZero();
 495     ADD constant(CUDD_VALUE_TYPE c);
 496     ADD plusInfinity();
 497     ADD minusInfinity();
 498     ZDD zddVar(int index);
 499     ZDD zddOne(int i);
 500     ZDD zddZero();
 501     ADD addNewVarAtLevel(int level);
 502     BDD bddNewVarAtLevel(int level);
 503     void zddVarsFromBddVars(int multiplicity);
 504     void AutodynEnable(Cudd_ReorderingType method);
 505     void AutodynDisable();
 506     int ReorderingStatus(Cudd_ReorderingType * method) const;
 507     void AutodynEnableZdd(Cudd_ReorderingType method);
 508     void AutodynDisableZdd();
 509     int ReorderingStatusZdd(Cudd_ReorderingType * method) const;
 510     int zddRealignmentEnabled() const;
 511     void zddRealignEnable();
 512     void zddRealignDisable();
 513     int bddRealignmentEnabled() const;
 514     void bddRealignEnable();
 515     void bddRealignDisable();
 516     ADD background();
 517     void SetBackground(ADD bg);
 518     unsigned int ReadCacheSlots() const;
 519     double ReadCacheUsedSlots() const;
 520     double ReadCacheLookUps() const;
 521     double ReadCacheHits() const;
 522     unsigned int ReadMinHit() const;
 523     void SetMinHit(unsigned int hr);
 524     unsigned int ReadLooseUpTo() const;
 525     void SetLooseUpTo(unsigned int lut);
 526     unsigned int ReadMaxCache() const;
 527     unsigned int ReadMaxCacheHard() const;
 528     void SetMaxCacheHard(unsigned int mc);
 529     int ReadSize() const;
 530     int ReadZddSize() const;
 531     unsigned int ReadSlots() const;
 532     unsigned int ReadKeys() const;
 533     unsigned int ReadDead() const;
 534     unsigned int ReadMinDead() const;
 535     int ReadReorderings() const;
 536     long ReadReorderingTime() const;
 537     int ReadGarbageCollections() const;
 538     long ReadGarbageCollectionTime() const;
 539     int ReadSiftMaxVar() const;
 540     void SetSiftMaxVar(int smv);
 541     int ReadSiftMaxSwap() const;
 542     void SetSiftMaxSwap(int sms);
 543     double ReadMaxGrowth() const;
 544     void SetMaxGrowth(double mg);
 545     MtrNode * ReadTree() const;
 546     void SetTree(MtrNode * tree);
 547     void FreeTree();
 548     MtrNode * ReadZddTree() const;
 549     void SetZddTree(MtrNode * tree);
 550     void FreeZddTree();
 551     int ReadPerm(int i) const;
 552     int ReadPermZdd(int i) const;
 553     int ReadInvPerm(int i) const;
 554     int ReadInvPermZdd(int i) const;
 555     BDD ReadVars(int i);
 556     CUDD_VALUE_TYPE ReadEpsilon() const;
 557     void SetEpsilon(CUDD_VALUE_TYPE ep);
 558     Cudd_AggregationType ReadGroupcheck() const;
 559     void SetGroupcheck(Cudd_AggregationType gc);
 560     int GarbageCollectionEnabled() const;
 561     void EnableGarbageCollection();
 562     void DisableGarbageCollection();
 563     int DeadAreCounted() const;
 564     void TurnOnCountDead();
 565     void TurnOffCountDead();
 566     int ReadRecomb() const;
 567     void SetRecomb(int recomb);
 568     int ReadSymmviolation() const;
 569     void SetSymmviolation(int symmviolation);
 570     int ReadArcviolation() const;
 571     void SetArcviolation(int arcviolation);
 572     int ReadPopulationSize() const;
 573     void SetPopulationSize(int populationSize);
 574     int ReadNumberXovers() const;
 575     void SetNumberXovers(int numberXovers);
 576     unsigned long ReadMemoryInUse() const;
 577     long ReadPeakNodeCount() const;
 578     long ReadNodeCount() const;
 579     long zddReadNodeCount() const;
 580     void AddHook(DD_HFP f, Cudd_HookType where);
 581     void RemoveHook(DD_HFP f, Cudd_HookType where);
 582     int IsInHook(DD_HFP f, Cudd_HookType where) const;
 583     void EnableReorderingReporting();
 584     void DisableReorderingReporting();
 585     int ReorderingReporting();
 586     int ReadErrorCode() const;
 587     void ClearErrorCode();
 588     FILE *ReadStdout() const;
 589     void SetStdout(FILE *);
 590     FILE *ReadStderr() const;
 591     void SetStderr(FILE *);
 592     unsigned int ReadNextReordering() const;
 593     double ReadSwapSteps() const;
 594     unsigned int ReadMaxLive() const;
 595     void SetMaxLive(unsigned int);
 596     unsigned long ReadMaxMemory() const;
 597     void SetMaxMemory(unsigned long);
 598     int bddBindVar(int);
 599     int bddUnbindVar(int);
 600     int bddVarIsBound(int) const;
 601     ADD Walsh(ADDvector x, ADDvector y);
 602     ADD addResidue(int n, int m, int options, int top);
 603     int ApaNumberOfDigits(int binaryDigits) const;
 604     DdApaNumber NewApaNumber(int digits) const;
 605     void ApaCopy(int digits, DdApaNumber source, DdApaNumber dest) const;
 606     DdApaDigit ApaAdd(int digits, DdApaNumber a, DdApaNumber b, DdApaNumber
 607                       sum) const;
 608     DdApaDigit ApaSubtract(int digits, DdApaNumber a, DdApaNumber b,
 609                            DdApaNumber diff) const;
 610     DdApaDigit ApaShortDivision(int digits, DdApaNumber dividend, DdApaDigit
 611                                 divisor, DdApaNumber quotient) const;
 612     void ApaShiftRight(int digits, DdApaDigit in, DdApaNumber a, DdApaNumber
 613                        b) const;
 614     void ApaSetToLiteral(int digits, DdApaNumber number, DdApaDigit literal)
 615       const;
 616     void ApaPowerOfTwo(int digits, DdApaNumber number, int power) const;
 617     void ApaPrintHex(FILE * fp, int digits, DdApaNumber number) const;
 618     void ApaPrintDecimal(FILE * fp, int digits, DdApaNumber number) const;
 619     void DebugCheck();
 620     void CheckKeys();
 621     MtrNode * MakeTreeNode(unsigned int low, unsigned int size, unsigned int type);
 622     // void Harwell(FILE * fp, ADD* E, ADD** x, ADD** y, ADD** xn, ADD** yn_, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy, int pr);
 623     void PrintLinear();
 624     int ReadLinear(int x, int y);
 625     BDD Xgty(BDDvector z, BDDvector x, BDDvector y);
 626     BDD Xeqy(BDDvector x, BDDvector y);
 627     ADD Xeqy(ADDvector x, ADDvector y);
 628     BDD Dxygtdxz(BDDvector x, BDDvector y, BDDvector z);
 629     BDD Dxygtdyz(BDDvector x, BDDvector y, BDDvector z);
 630     BDD Inequality(int c, BDDvector x, BDDvector y);
 631     BDD Disequality(int c, BDDvector x, BDDvector y);
 632     BDD Interval(BDDvector x, unsigned int lowerB, unsigned int upperB);
 633     ADD Hamming(ADDvector xVars, ADDvector yVars);
 634     // void Read(FILE * fp, ADD* E, ADD** x, ADD** y, ADD** xn, ADD** yn_, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy);
 635     // void Read(FILE * fp, BDD* E, BDD** x, BDD** y, int * nx, int * ny, int * m, int * n, int bx, int sx, int by, int sy);
 636     void ReduceHeap(Cudd_ReorderingType heuristic, int minsize);
 637     void ShuffleHeap(int * permutation);
 638     void SymmProfile(int lower, int upper) const;
 639     unsigned int Prime(unsigned int pr) const;
 640     int SharingSize(DD* nodes, int n) const;
 641     BDD bddComputeCube(BDD * vars, int * phase, int n);
 642     ADD addComputeCube(ADD * vars, int * phase, int n);
 643     int NextNode(DdGen * gen, BDD * nnode);
 644     BDD IndicesToCube(int * array, int n);
 645     void PrintVersion(FILE * fp) const;
 646     double AverageDistance() const;
 647     long Random();
 648     void Srandom(long seed);
 649     MtrNode * MakeZddTreeNode(unsigned int low, unsigned int size, unsigned int type);
 650     void zddPrintSubtable() const;
 651     void zddReduceHeap(Cudd_ReorderingType heuristic, int minsize);
 652     void zddShuffleHeap(int * permutation);
 653     void zddSymmProfile(int lower, int upper) const;
 654   //void DumpDot(int n, ZDD* f, char ** inames, char ** onames, FILE * fp);
 655
 656 }; // Cudd
 657
 658
 659 /**Class***********************************************************************
 660
 661   Synopsis     [Class for BDD vectors.]
 662
 663   Description  []
 664
 665   SeeAlso      [BDD]
 666
 667 ******************************************************************************/
 668 class BDDvector {
 669     struct capsule {
 670         Cudd *manager;
 671         BDD *vect;
 672         int size;
 673         int ref;
 674     };
 675     capsule *p;
 676 public:
 677     BDDvector(int size, Cudd *manager = 0, DdNode **nodes = 0);
 678     BDDvector(const BDDvector &from);
 679     ~BDDvector();
 680     BDDvector& operator=(const BDDvector& right);
 681     BDD& operator[](int i) const;
 682     int count() const {return p->size;}
 683     Cudd *manager() const {return p->manager;}
 684     void DumpDot(char ** inames = 0, char ** onames = 0, FILE * fp = stdout)
 685         const;
 686     void DumpDaVinci(
 687       char ** inames = 0,
 688       char ** onames = 0,
 689       FILE * fp = stdout) const;
 690     void DumpBlif(
 691       char ** inames = 0,
 692       char ** onames = 0,
 693       char * mname = 0,
 694       FILE * fp = stdout,
 695       int mv = 0) const;
 696     void DumpDDcal(char ** inames = 0, char ** onames = 0, FILE * fp = stdout)
 697         const;
 698     void DumpFactoredForm(
 699       char ** inames = 0,
 700       char ** onames = 0,
 701       FILE * fp = stdout) const;
 702     BDD VectorSupport() const;
 703     int nodeCount() const;
 704     int VectorSupportSize() const;
 705
 706 }; // BDDvector
 707
 708
 709 /**Class***********************************************************************
 710
 711   Synopsis     [Class for ADD vectors.]
 712
 713   Description  []
 714
 715   SeeAlso      [ADD]
 716
 717 ******************************************************************************/
 718 class ADDvector {
 719     struct capsule {
 720         Cudd *manager;
 721         ADD *vect;
 722         int size;
 723         int ref;
 724     };
 725     capsule *p;
 726 public:
 727     ADDvector(int size, Cudd *manager = 0, DdNode **nodes = 0);
 728     ADDvector(const ADDvector &from);
 729     ~ADDvector();
 730     ADDvector& operator=(const ADDvector& right);
 731     ADD& operator[](int i) const;
 732     int count() const {return p->size;}
 733     Cudd *manager() const {return p->manager;}
 734     void DumpDot(char ** inames = 0, char ** onames = 0, FILE * fp = stdout)
 735         const;
 736     void DumpDaVinci(
 737       char ** inames = 0,
 738       char ** onames = 0,
 739       FILE * fp = stdout) const;
 740     BDD VectorSupport() const;
 741     int VectorSupportSize() const;
 742
 743 }; // ADDvector
 744
 745
 746 /**Class***********************************************************************
 747
 748   Synopsis     [Class for ZDD vectors.]
 749
 750   Description  []
 751
 752   SeeAlso      [ZDD]
 753
 754 ******************************************************************************/
 755 class ZDDvector {
 756     struct capsule {
 757         Cudd *manager;
 758         ZDD *vect;
 759         int size;
 760         int ref;
 761     };
 762     capsule *p;
 763 public:
 764     ZDDvector(int size, Cudd *manager = 0, DdNode **nodes = 0);
 765     ZDDvector(const ZDDvector &from);
 766     ~ZDDvector();
 767     ZDDvector& operator=(const ZDDvector& right);
 768     ZDD& operator[](int i) const;
 769     int count() const {return p->size;}
 770     Cudd *manager() const {return p->manager;}
 771     void DumpDot(char ** inames = 0, char ** onames = 0, FILE * fp = stdout)
 772         const;
 773
 774 }; // ZDDvector
 775
 776
 777 extern void defaultError(string message);
 778 extern int NextCube(DdGen * gen, int ** cube, CUDD_VALUE_TYPE * value);
 779 extern int GenFree(DdGen * gen);
 780 extern int IsGenEmpty(DdGen * gen);
 781
 782 #endif