distr/obj/cuddObj.cc

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddObj.cc]
   4
   5   PackageName [cuddObj]
   6
   7   Synopsis    [Functions for the C++ object-oriented encapsulation of CUDD.]
   8
   9   Description []
  10
  11   SeeAlso     []
  12
  13   Author      [Fabio Somenzi]
  14
  15   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  16
  17   All rights reserved.
  18
  19   Redistribution and use in source and binary forms, with or without
  20   modification, are permitted provided that the following conditions
  21   are met:
  22
  23   Redistributions of source code must retain the above copyright
  24   notice, this list of conditions and the following disclaimer.
  25
  26   Redistributions in binary form must reproduce the above copyright
  27   notice, this list of conditions and the following disclaimer in the
  28   documentation and/or other materials provided with the distribution.
  29
  30   Neither the name of the University of Colorado nor the names of its
  31   contributors may be used to endorse or promote products derived from
  32   this software without specific prior written permission.
  33
  34   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  35   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  36   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  37   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  38   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  39   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  40   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  41   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  42   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  43   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  44   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  45   POSSIBILITY OF SUCH DAMAGE.]
  46
  47 ******************************************************************************/
  48
  49 #include "cuddObj.hh"
  50
  51 // ---------------------------------------------------------------------------
  52 // Variable declarations
  53 // ---------------------------------------------------------------------------
  54
  55 #ifndef lint
  56 static char rcsid[] UTIL_UNUSED = "$Id: cuddObj.cc,v 1.13 2009/02/21 19:41:38 fabio Exp fabio $";
  57 #endif
  58
  59 // ---------------------------------------------------------------------------
  60 // Members of class DD
  61 // ---------------------------------------------------------------------------
  62
  63
  64 DD::DD(Cudd *ddManager, DdNode *ddNode) {
  65     ddMgr = ddManager;
  66     node = ddNode;
  67     if (node != 0) Cudd_Ref(node);
  68     if (ddMgr->isVerbose()) {
  69         cout << "Standard DD constructor for node " << hex << long(node) <<
  70             " ref = " << Cudd_Regular(node)->ref << "\n";
  71     }
  72
  73 } // DD::DD
  74
  75
  76 DD::DD() {
  77     ddMgr = 0;
  78     node = 0;
  79
  80 } // DD::DD
  81
  82
  83 DD::DD(const DD &from) {
  84     ddMgr = from.ddMgr;
  85     node = from.node;
  86     if (node != 0) {
  87         Cudd_Ref(node);
  88         if (ddMgr->isVerbose()) {
  89             cout << "Copy DD constructor for node " << hex << long(node) <<
  90                 " ref = " << Cudd_Regular(node)->ref << "\n";
  91         }
  92     }
  93
  94 } // DD::DD
  95
  96
  97 DD::~DD() {}
  98
  99
 100 inline DdManager *
 101 DD::checkSameManager(
 102   const DD &other) const
 103 {
 104     DdManager *mgr = ddMgr->p->manager;
 105     if (mgr != other.ddMgr->p->manager) {
 106         ddMgr->p->errorHandler("Operands come from different manager.");
 107     }
 108     return mgr;
 109
 110 } // DD::checkSameManager
 111
 112
 113 inline void
 114 DD::checkReturnValue(
 115   const DdNode *result) const
 116 {
 117     if (result == 0) {
 118         DdManager *mgr = ddMgr->p->manager;
 119         Cudd_ErrorType errType = Cudd_ReadErrorCode(mgr);
 120         switch (errType) {
 121         case CUDD_MEMORY_OUT:
 122             ddMgr->p->errorHandler("Out of memory.");
 123             break;
 124         case CUDD_TOO_MANY_NODES:
 125             break;
 126         case CUDD_MAX_MEM_EXCEEDED:
 127             ddMgr->p->errorHandler("Maximum memory exceeded.");
 128             break;
 129         case CUDD_INVALID_ARG:
 130             ddMgr->p->errorHandler("Invalid argument.");
 131             break;
 132         case CUDD_INTERNAL_ERROR:
 133             ddMgr->p->errorHandler("Internal error.");
 134             break;
 135         case CUDD_NO_ERROR:
 136         default:
 137             ddMgr->p->errorHandler("Unexpected error.");
 138             break;
 139         }
 140     }
 141
 142 } // DD::checkReturnValue
 143
 144
 145 inline void
 146 DD::checkReturnValue(
 147   const int result,
 148   const int expected) const
 149 {
 150     if (result != expected) {
 151         DdManager *mgr = ddMgr->p->manager;
 152         Cudd_ErrorType errType = Cudd_ReadErrorCode(mgr);
 153         switch (errType) {
 154         case CUDD_MEMORY_OUT:
 155             ddMgr->p->errorHandler("Out of memory.");
 156             break;
 157         case CUDD_TOO_MANY_NODES:
 158             break;
 159         case CUDD_MAX_MEM_EXCEEDED:
 160             ddMgr->p->errorHandler("Maximum memory exceeded.");
 161             break;
 162         case CUDD_INVALID_ARG:
 163             ddMgr->p->errorHandler("Invalid argument.");
 164             break;
 165         case CUDD_INTERNAL_ERROR:
 166             ddMgr->p->errorHandler("Internal error.");
 167             break;
 168         case CUDD_NO_ERROR:
 169         default:
 170             ddMgr->p->errorHandler("Unexpected error.");
 171             break;
 172         }
 173     }
 174
 175 } // DD::checkReturnValue
 176
 177
 178 Cudd *
 179 DD::manager() const
 180 {
 181     return ddMgr;
 182
 183 } // DD::manager
 184
 185
 186 inline DdNode *
 187 DD::getNode() const
 188 {
 189     return node;
 190
 191 } // DD::getNode
 192
 193
 194 int
 195 DD::nodeCount() const
 196 {
 197     return Cudd_DagSize(node);
 198
 199 } // DD::nodeCount
 200
 201
 202 // ---------------------------------------------------------------------------
 203 // Members of class ABDD
 204 // ---------------------------------------------------------------------------
 205
 206
 207 ABDD::ABDD(Cudd *bddManager, DdNode *bddNode) : DD(bddManager,bddNode) {}
 208 ABDD::ABDD() : DD() {}
 209 ABDD::ABDD(const ABDD &from) : DD(from) {}
 210
 211
 212 ABDD::~ABDD() {
 213     if (node != 0) {
 214         Cudd_RecursiveDeref(ddMgr->p->manager,node);
 215         if (ddMgr->isVerbose()) {
 216             cout << "ADD/BDD destructor called for node " << hex <<
 217                 long(node) << " ref = " << Cudd_Regular(node)->ref << "\n";
 218         }
 219     }
 220
 221 } // ABDD::~ABDD
 222
 223
 224 int
 225 ABDD::operator==(
 226   const ABDD& other) const
 227 {
 228     this->checkSameManager(other);
 229     return node == other.node;
 230
 231 } // ABDD::operator==
 232
 233
 234 int
 235 ABDD::operator!=(
 236   const ABDD& other) const
 237 {
 238     this->checkSameManager(other);
 239     return node != other.node;
 240
 241 } // ABDD::operator!=
 242
 243
 244 void
 245 ABDD::print(
 246   int nvars,
 247   int verbosity) const
 248 {
 249     cout.flush();
 250     int retval = Cudd_PrintDebug(ddMgr->p->manager,node,nvars,verbosity);
 251     if (retval == 0) ddMgr->p->errorHandler("print failed");
 252
 253 } // ABDD::print
 254
 255
 256 // ---------------------------------------------------------------------------
 257 // Members of class BDD
 258 // ---------------------------------------------------------------------------
 259
 260 BDD::BDD(Cudd *bddManager, DdNode *bddNode) : ABDD(bddManager,bddNode) {}
 261 BDD::BDD() : ABDD() {}
 262 BDD::BDD(const BDD &from) : ABDD(from) {}
 263
 264
 265 int
 266 BDD::operator==(
 267   const BDD& other) const
 268 {
 269     this->checkSameManager(other);
 270     return node == other.node;
 271
 272 } // BDD::operator==
 273
 274
 275 int
 276 BDD::operator!=(
 277   const BDD& other) const
 278 {
 279     this->checkSameManager(other);
 280     return node != other.node;
 281
 282 } // BDD::operator!=
 283
 284
 285 BDD
 286 BDD::operator=(
 287   const BDD& right)
 288 {
 289     if (this == &right) return *this;
 290     if (right.node != 0) Cudd_Ref(right.node);
 291     if (node != 0) {
 292         Cudd_RecursiveDeref(ddMgr->p->manager,node);
 293         if (ddMgr->isVerbose()) {
 294             cout << "BDD dereferencing for node " << hex << long(node) <<
 295                 " ref = " << Cudd_Regular(node)->ref << "\n";
 296         }
 297     }
 298     node = right.node;
 299     ddMgr = right.ddMgr;
 300     if (node != 0 && ddMgr->isVerbose()) {
 301         cout << "BDD assignment for node " << hex << long(node) <<
 302             " ref = " << Cudd_Regular(node)->ref << "\n";
 303     }
 304     return *this;
 305
 306 } // BDD::operator=
 307
 308
 309 int
 310 BDD::operator<=(
 311   const BDD& other) const
 312 {
 313     DdManager *mgr = this->checkSameManager(other);
 314     return Cudd_bddLeq(mgr,node,other.node);
 315
 316 } // BDD::operator<=
 317
 318
 319 int
 320 BDD::operator>=(
 321   const BDD& other) const
 322 {
 323     DdManager *mgr = this->checkSameManager(other);
 324     return Cudd_bddLeq(mgr,other.node,node);
 325
 326 } // BDD::operator>=
 327
 328
 329 int
 330 BDD::operator<(
 331   const BDD& other) const
 332 {
 333     DdManager *mgr = this->checkSameManager(other);
 334     return node != other.node && Cudd_bddLeq(mgr,node,other.node);
 335
 336 } // BDD::operator<
 337
 338
 339 int
 340 BDD::operator>(
 341   const BDD& other) const
 342 {
 343     DdManager *mgr = this->checkSameManager(other);
 344     return node != other.node && Cudd_bddLeq(mgr,other.node,node);
 345
 346 } // BDD::operator>
 347
 348
 349 BDD
 350 BDD::operator!() const
 351 {
 352     return BDD(ddMgr, Cudd_Not(node));
 353
 354 } // BDD::operator!
 355
 356
 357 BDD
 358 BDD::operator~() const
 359 {
 360     return BDD(ddMgr, Cudd_Not(node));
 361
 362 } // BDD::operator~
 363
 364
 365 BDD
 366 BDD::operator*(
 367   const BDD& other) const
 368 {
 369     DdManager *mgr = this->checkSameManager(other);
 370     DdNode *result = Cudd_bddAnd(mgr,node,other.node);
 371     this->checkReturnValue(result);
 372     return BDD(ddMgr, result);
 373
 374 } // BDD::operator*
 375
 376
 377 BDD
 378 BDD::operator*=(
 379   const BDD& other)
 380 {
 381     DdManager *mgr = this->checkSameManager(other);
 382     DdNode *result = Cudd_bddAnd(mgr,node,other.node);
 383     this->checkReturnValue(result);
 384     Cudd_Ref(result);
 385     Cudd_RecursiveDeref(mgr,node);
 386     node = result;
 387     return *this;
 388
 389 } // BDD::operator*=
 390
 391
 392 BDD
 393 BDD::operator&(
 394   const BDD& other) const
 395 {
 396     DdManager *mgr = this->checkSameManager(other);
 397     DdNode *result = Cudd_bddAnd(mgr,node,other.node);
 398     this->checkReturnValue(result);
 399     return BDD(ddMgr, result);
 400
 401 } // BDD::operator&
 402
 403
 404 BDD
 405 BDD::operator&=(
 406   const BDD& other)
 407 {
 408     DdManager *mgr = this->checkSameManager(other);
 409     DdNode *result = Cudd_bddAnd(mgr,node,other.node);
 410     this->checkReturnValue(result);
 411     Cudd_Ref(result);
 412     Cudd_RecursiveDeref(mgr,node);
 413     node = result;
 414     return *this;
 415
 416 } // BDD::operator&=
 417
 418
 419 BDD
 420 BDD::operator+(
 421   const BDD& other) const
 422 {
 423     DdManager *mgr = this->checkSameManager(other);
 424     DdNode *result = Cudd_bddOr(mgr,node,other.node);
 425     this->checkReturnValue(result);
 426     return BDD(ddMgr, result);
 427
 428 } // BDD::operator+
 429
 430
 431 BDD
 432 BDD::operator+=(
 433   const BDD& other)
 434 {
 435     DdManager *mgr = this->checkSameManager(other);
 436     DdNode *result = Cudd_bddOr(mgr,node,other.node);
 437     this->checkReturnValue(result);
 438     Cudd_Ref(result);
 439     Cudd_RecursiveDeref(mgr,node);
 440     node = result;
 441     return *this;
 442
 443 } // BDD::operator+=
 444
 445
 446 BDD
 447 BDD::operator|(
 448   const BDD& other) const
 449 {
 450     DdManager *mgr = this->checkSameManager(other);
 451     DdNode *result = Cudd_bddOr(mgr,node,other.node);
 452     this->checkReturnValue(result);
 453     return BDD(ddMgr, result);
 454
 455 } // BDD::operator|
 456
 457
 458 BDD
 459 BDD::operator|=(
 460   const BDD& other)
 461 {
 462     DdManager *mgr = this->checkSameManager(other);
 463     DdNode *result = Cudd_bddOr(mgr,node,other.node);
 464     this->checkReturnValue(result);
 465     Cudd_Ref(result);
 466     Cudd_RecursiveDeref(mgr,node);
 467     node = result;
 468     return *this;
 469
 470 } // BDD::operator|=
 471
 472
 473 BDD
 474 BDD::operator^(
 475   const BDD& other) const
 476 {
 477     DdManager *mgr = this->checkSameManager(other);
 478     DdNode *result = Cudd_bddXor(mgr,node,other.node);
 479     this->checkReturnValue(result);
 480     return BDD(ddMgr, result);
 481
 482 } // BDD::operator^
 483
 484
 485 BDD
 486 BDD::operator^=(
 487   const BDD& other)
 488 {
 489     DdManager *mgr = this->checkSameManager(other);
 490     DdNode *result = Cudd_bddXor(mgr,node,other.node);
 491     this->checkReturnValue(result);
 492     Cudd_Ref(result);
 493     Cudd_RecursiveDeref(mgr,node);
 494     node = result;
 495     return *this;
 496
 497 } // BDD::operator^=
 498
 499
 500 BDD
 501 BDD::operator-(
 502   const BDD& other) const
 503 {
 504     DdManager *mgr = this->checkSameManager(other);
 505     DdNode *result = Cudd_bddAnd(mgr,node,Cudd_Not(other.node));
 506     this->checkReturnValue(result);
 507     return BDD(ddMgr, result);
 508
 509 } // BDD::operator-
 510
 511
 512 BDD
 513 BDD::operator-=(
 514   const BDD& other)
 515 {
 516     DdManager *mgr = this->checkSameManager(other);
 517     DdNode *result = Cudd_bddAnd(mgr,node,Cudd_Not(other.node));
 518     this->checkReturnValue(result);
 519     Cudd_Ref(result);
 520     Cudd_RecursiveDeref(mgr,node);
 521     node = result;
 522     return *this;
 523
 524 } // BDD::operator-=
 525
 526
 527 // ---------------------------------------------------------------------------
 528 // Members of class ADD
 529 // ---------------------------------------------------------------------------
 530
 531
 532 ADD::ADD(Cudd *bddManager, DdNode *bddNode) : ABDD(bddManager,bddNode) {}
 533 ADD::ADD() : ABDD() {}
 534 ADD::ADD(const ADD &from) : ABDD(from) {}
 535
 536
 537 int
 538 ADD::operator==(
 539   const ADD& other) const
 540 {
 541     this->checkSameManager(other);
 542     return node == other.node;
 543
 544 } // ADD::operator==
 545
 546
 547 int
 548 ADD::operator!=(
 549   const ADD& other) const
 550 {
 551     this->checkSameManager(other);
 552     return node != other.node;
 553
 554 } // ADD::operator!=
 555
 556
 557 ADD
 558 ADD::operator=(
 559   const ADD& right)
 560 {
 561     if (this == &right) return *this;
 562     if (right.node != 0) Cudd_Ref(right.node);
 563     if (node != 0) {
 564         Cudd_RecursiveDeref(ddMgr->p->manager,node);
 565     }
 566     node = right.node;
 567     ddMgr = right.ddMgr;
 568     return *this;
 569
 570 } // ADD::operator=
 571
 572
 573 int
 574 ADD::operator<=(
 575   const ADD& other) const
 576 {
 577     DdManager *mgr = this->checkSameManager(other);
 578     return Cudd_addLeq(mgr,node,other.node);
 579
 580 } // ADD::operator<=
 581
 582
 583 int
 584 ADD::operator>=(
 585   const ADD& other) const
 586 {
 587     DdManager *mgr = this->checkSameManager(other);
 588     return Cudd_addLeq(mgr,other.node,node);
 589
 590 } // ADD::operator>=
 591
 592
 593 int
 594 ADD::operator<(
 595   const ADD& other) const
 596 {
 597     DdManager *mgr = this->checkSameManager(other);
 598     return node != other.node && Cudd_addLeq(mgr,node,other.node);
 599
 600 } // ADD::operator<
 601
 602
 603 int
 604 ADD::operator>(
 605   const ADD& other) const
 606 {
 607     DdManager *mgr = this->checkSameManager(other);
 608     return node != other.node && Cudd_addLeq(mgr,other.node,node);
 609
 610 } // ADD::operator>
 611
 612
 613 ADD
 614 ADD::operator-() const
 615 {
 616     return ADD(ddMgr, Cudd_addNegate(ddMgr->p->manager,node));
 617
 618 } // ADD::operator-
 619
 620
 621 ADD
 622 ADD::operator*(
 623   const ADD& other) const
 624 {
 625     DdManager *mgr = this->checkSameManager(other);
 626     DdNode *result = Cudd_addApply(mgr,Cudd_addTimes,node,other.node);
 627     this->checkReturnValue(result);
 628     return ADD(ddMgr, result);
 629
 630 } // ADD::operator*
 631
 632
 633 ADD
 634 ADD::operator*=(
 635   const ADD& other)
 636 {
 637     DdManager *mgr = this->checkSameManager(other);
 638     DdNode *result = Cudd_addApply(mgr,Cudd_addTimes,node,other.node);
 639     this->checkReturnValue(result);
 640     Cudd_Ref(result);
 641     Cudd_RecursiveDeref(mgr,node);
 642     node = result;
 643     return *this;
 644
 645 } // ADD::operator*=
 646
 647
 648 ADD
 649 ADD::operator+(
 650   const ADD& other) const
 651 {
 652     DdManager *mgr = this->checkSameManager(other);
 653     DdNode *result = Cudd_addApply(mgr,Cudd_addPlus,node,other.node);
 654     this->checkReturnValue(result);
 655     return ADD(ddMgr, result);
 656
 657 } // ADD::operator+
 658
 659
 660 ADD
 661 ADD::operator+=(
 662   const ADD& other)
 663 {
 664     DdManager *mgr = this->checkSameManager(other);
 665     DdNode *result = Cudd_addApply(mgr,Cudd_addPlus,node,other.node);
 666     this->checkReturnValue(result);
 667     Cudd_Ref(result);
 668     Cudd_RecursiveDeref(mgr,node);
 669     node = result;
 670     return *this;
 671
 672 } // ADD::operator+=
 673
 674
 675 ADD
 676 ADD::operator-(
 677   const ADD& other) const
 678 {
 679     DdManager *mgr = this->checkSameManager(other);
 680     DdNode *result = Cudd_addApply(mgr,Cudd_addMinus,node,other.node);
 681     this->checkReturnValue(result);
 682     return ADD(ddMgr, result);
 683
 684 } // ADD::operator-
 685
 686
 687 ADD
 688 ADD::operator-=(
 689   const ADD& other)
 690 {
 691     DdManager *mgr = this->checkSameManager(other);
 692     DdNode *result = Cudd_addApply(mgr,Cudd_addMinus,node,other.node);
 693     this->checkReturnValue(result);
 694     Cudd_Ref(result);
 695     Cudd_RecursiveDeref(mgr,node);
 696     node = result;
 697     return *this;
 698
 699 } // ADD::operator-=
 700
 701
 702 ADD
 703 ADD::operator~() const
 704 {
 705     return ADD(ddMgr, Cudd_addCmpl(ddMgr->p->manager,node));
 706
 707 } // ADD::operator~
 708
 709
 710 ADD
 711 ADD::operator&(
 712   const ADD& other) const
 713 {
 714     DdManager *mgr = this->checkSameManager(other);
 715     DdNode *result = Cudd_addApply(mgr,Cudd_addTimes,node,other.node);
 716     this->checkReturnValue(result);
 717     return ADD(ddMgr, result);
 718
 719 } // ADD::operator&
 720
 721
 722 ADD
 723 ADD::operator&=(
 724   const ADD& other)
 725 {
 726     DdManager *mgr = this->checkSameManager(other);
 727     DdNode *result = Cudd_addApply(mgr,Cudd_addTimes,node,other.node);
 728     this->checkReturnValue(result);
 729     Cudd_Ref(result);
 730     Cudd_RecursiveDeref(mgr,node);
 731     node = result;
 732     return *this;
 733
 734 } // ADD::operator&=
 735
 736
 737 ADD
 738 ADD::operator|(
 739   const ADD& other) const
 740 {
 741     DdManager *mgr = this->checkSameManager(other);
 742     DdNode *result = Cudd_addApply(mgr,Cudd_addOr,node,other.node);
 743     this->checkReturnValue(result);
 744     return ADD(ddMgr, result);
 745
 746 } // ADD::operator|
 747
 748
 749 ADD
 750 ADD::operator|=(
 751   const ADD& other)
 752 {
 753     DdManager *mgr = this->checkSameManager(other);
 754     DdNode *result = Cudd_addApply(mgr,Cudd_addOr,node,other.node);
 755     this->checkReturnValue(result);
 756     Cudd_Ref(result);
 757     Cudd_RecursiveDeref(mgr,node);
 758     node = result;
 759     return *this;
 760
 761 } // ADD::operator|=
 762
 763
 764 // ---------------------------------------------------------------------------
 765 // Members of class ZDD
 766 // ---------------------------------------------------------------------------
 767
 768
 769 ZDD::ZDD(Cudd *bddManager, DdNode *bddNode) : DD(bddManager,bddNode) {}
 770 ZDD::ZDD() : DD() {}
 771 ZDD::ZDD(const ZDD &from) : DD(from) {}
 772
 773
 774 ZDD::~ZDD() {
 775     if (node != 0) {
 776         Cudd_RecursiveDerefZdd(ddMgr->p->manager,node);
 777         if (ddMgr->isVerbose()) {
 778             cout << "ZDD destructor called for node " << hex << long(node) <<
 779                 " ref = " << Cudd_Regular(node)->ref << "\n";
 780         }
 781     }
 782
 783 } // ZDD::~ZDD
 784
 785
 786 ZDD
 787 ZDD::operator=(
 788   const ZDD& right)
 789 {
 790     if (this == &right) return *this;
 791     if (right.node != 0) Cudd_Ref(right.node);
 792     if (node != 0) {
 793         Cudd_RecursiveDerefZdd(ddMgr->p->manager,node);
 794         if (ddMgr->isVerbose()) {
 795             cout << "ZDD dereferencing for node " << hex << long(node) <<
 796                 " ref = " << node->ref << "\n";
 797         }
 798     }
 799     node = right.node;
 800     ddMgr = right.ddMgr;
 801     if (node != 0 && ddMgr->isVerbose()) {
 802         cout << "ZDD assignment for node " << hex << long(node) <<
 803             " ref = " << node->ref << "\n";
 804     }
 805     return *this;
 806
 807 } // ZDD::operator=
 808
 809
 810 int
 811 ZDD::operator==(
 812   const ZDD& other) const
 813 {
 814     this->checkSameManager(other);
 815     return node == other.node;
 816
 817 } // ZDD::operator==
 818
 819
 820 int
 821 ZDD::operator!=(
 822   const ZDD& other) const
 823 {
 824     this->checkSameManager(other);
 825     return node != other.node;
 826
 827 } // ZDD::operator!=
 828
 829
 830 int
 831 ZDD::operator<=(
 832   const ZDD& other) const
 833 {
 834     DdManager *mgr = this->checkSameManager(other);
 835     return Cudd_zddDiffConst(mgr,node,other.node) == Cudd_ReadZero(mgr);
 836
 837 } // ZDD::operator<=
 838
 839
 840 int
 841 ZDD::operator>=(
 842   const ZDD& other) const
 843 {
 844     DdManager *mgr = this->checkSameManager(other);
 845     return Cudd_zddDiffConst(mgr,other.node,node) == Cudd_ReadZero(mgr);
 846
 847 } // ZDD::operator>=
 848
 849
 850 int
 851 ZDD::operator<(
 852   const ZDD& other) const
 853 {
 854     DdManager *mgr = this->checkSameManager(other);
 855     return node != other.node &&
 856         Cudd_zddDiffConst(mgr,node,other.node) == Cudd_ReadZero(mgr);
 857
 858 } // ZDD::operator<
 859
 860
 861 int
 862 ZDD::operator>(
 863   const ZDD& other) const
 864 {
 865     DdManager *mgr = this->checkSameManager(other);
 866     return node != other.node &&
 867         Cudd_zddDiffConst(mgr,other.node,node) == Cudd_ReadZero(mgr);
 868
 869 } // ZDD::operator>
 870
 871
 872 void
 873 ZDD::print(
 874   int nvars,
 875   int verbosity) const
 876 {
 877     cout.flush();
 878     int retval = Cudd_zddPrintDebug(ddMgr->p->manager,node,nvars,verbosity);
 879     if (retval == 0) ddMgr->p->errorHandler("print failed");
 880
 881 } // ZDD::print
 882
 883
 884 ZDD
 885 ZDD::operator*(
 886   const ZDD& other) const
 887 {
 888     DdManager *mgr = this->checkSameManager(other);
 889     DdNode *result = Cudd_zddIntersect(mgr,node,other.node);
 890     this->checkReturnValue(result);
 891     return ZDD(ddMgr, result);
 892
 893 } // ZDD::operator*
 894
 895
 896 ZDD
 897 ZDD::operator*=(
 898   const ZDD& other)
 899 {
 900     DdManager *mgr = this->checkSameManager(other);
 901     DdNode *result = Cudd_zddIntersect(mgr,node,other.node);
 902     this->checkReturnValue(result);
 903     Cudd_Ref(result);
 904     Cudd_RecursiveDerefZdd(mgr,node);
 905     node = result;
 906     return *this;
 907
 908 } // ZDD::operator*=
 909
 910
 911 ZDD
 912 ZDD::operator&(
 913   const ZDD& other) const
 914 {
 915     DdManager *mgr = this->checkSameManager(other);
 916     DdNode *result = Cudd_zddIntersect(mgr,node,other.node);
 917     this->checkReturnValue(result);
 918     return ZDD(ddMgr, result);
 919
 920 } // ZDD::operator&
 921
 922
 923 ZDD
 924 ZDD::operator&=(
 925   const ZDD& other)
 926 {
 927     DdManager *mgr = this->checkSameManager(other);
 928     DdNode *result = Cudd_zddIntersect(mgr,node,other.node);
 929     this->checkReturnValue(result);
 930     Cudd_Ref(result);
 931     Cudd_RecursiveDerefZdd(mgr,node);
 932     node = result;
 933     return *this;
 934
 935 } // ZDD::operator&=
 936
 937
 938 ZDD
 939 ZDD::operator+(
 940   const ZDD& other) const
 941 {
 942     DdManager *mgr = this->checkSameManager(other);
 943     DdNode *result = Cudd_zddUnion(mgr,node,other.node);
 944     this->checkReturnValue(result);
 945     return ZDD(ddMgr, result);
 946
 947 } // ZDD::operator+
 948
 949
 950 ZDD
 951 ZDD::operator+=(
 952   const ZDD& other)
 953 {
 954     DdManager *mgr = this->checkSameManager(other);
 955     DdNode *result = Cudd_zddUnion(mgr,node,other.node);
 956     this->checkReturnValue(result);
 957     Cudd_Ref(result);
 958     Cudd_RecursiveDerefZdd(mgr,node);
 959     node = result;
 960     return *this;
 961
 962 } // ZDD::operator+=
 963
 964
 965 ZDD
 966 ZDD::operator|(
 967   const ZDD& other) const
 968 {
 969     DdManager *mgr = this->checkSameManager(other);
 970     DdNode *result = Cudd_zddUnion(mgr,node,other.node);
 971     this->checkReturnValue(result);
 972     return ZDD(ddMgr, result);
 973
 974 } // ZDD::operator|
 975
 976
 977 ZDD
 978 ZDD::operator|=(
 979   const ZDD& other)
 980 {
 981     DdManager *mgr = this->checkSameManager(other);
 982     DdNode *result = Cudd_zddUnion(mgr,node,other.node);
 983     this->checkReturnValue(result);
 984     Cudd_Ref(result);
 985     Cudd_RecursiveDerefZdd(mgr,node);
 986     node = result;
 987     return *this;
 988
 989 } // ZDD::operator|=
 990
 991
 992 ZDD
 993 ZDD::operator-(
 994   const ZDD& other) const
 995 {
 996     DdManager *mgr = this->checkSameManager(other);
 997     DdNode *result = Cudd_zddDiff(mgr,node,other.node);
 998     this->checkReturnValue(result);
 999     return ZDD(ddMgr, result);
1000
1001 } // ZDD::operator-
1002
1003
1004 ZDD
1005 ZDD::operator-=(
1006   const ZDD& other)
1007 {
1008     DdManager *mgr = this->checkSameManager(other);
1009     DdNode *result = Cudd_zddDiff(mgr,node,other.node);
1010     this->checkReturnValue(result);
1011     Cudd_Ref(result);
1012     Cudd_RecursiveDerefZdd(mgr,node);
1013     node = result;
1014     return *this;
1015
1016 } // ZDD::operator-=
1017
1018
1019 // ---------------------------------------------------------------------------
1020 // Members of class Cudd
1021 // ---------------------------------------------------------------------------
1022
1023
1024 Cudd::Cudd(
1025   unsigned int numVars,
1026   unsigned int numVarsZ,
1027   unsigned int numSlots,
1028   unsigned int cacheSize,
1029   unsigned long maxMemory)
1030 {
1031     p = new capsule;
1032     p->manager = Cudd_Init(numVars,numVarsZ,numSlots,cacheSize,maxMemory);
1033     p->errorHandler = defaultError;
1034     p->verbose = 0;             // initially terse
1035     p->ref = 1;
1036
1037 } // Cudd::Cudd
1038
1039
1040 Cudd::Cudd(
1041   Cudd& x)
1042 {
1043     p = x.p;
1044     x.p->ref++;
1045
1046 } // Cudd::Cudd
1047
1048
1049 Cudd::~Cudd()
1050 {
1051     if (--p->ref == 0) {
1052         int retval = Cudd_CheckZeroRef(p->manager);
1053         if (retval != 0) {
1054             cerr << retval << " unexpected non-zero reference counts\n";
1055         } else if (p->verbose) {
1056             cerr << "All went well\n";
1057         }
1058         Cudd_Quit(p->manager);
1059         delete p;
1060     }
1061
1062 } // Cudd::~Cudd
1063
1064
1065 Cudd&
1066 Cudd::operator=(
1067   const Cudd& right)
1068 {
1069     right.p->ref++;
1070     if (--p->ref == 0) {        // disconnect self
1071         int retval = Cudd_CheckZeroRef(p->manager);
1072         if (retval != 0) {
1073             cerr << retval << " unexpected non-zero reference counts\n";
1074         }
1075         Cudd_Quit(p->manager);
1076         delete p;
1077     }
1078     p = right.p;
1079     return *this;
1080
1081 } // Cudd::operator=
1082
1083
1084 PFC
1085 Cudd::setHandler(
1086   PFC newHandler)
1087 {
1088     PFC oldHandler = p->errorHandler;
1089     p->errorHandler = newHandler;
1090     return oldHandler;
1091
1092 } // Cudd::setHandler
1093
1094
1095 PFC
1096 Cudd::getHandler() const
1097 {
1098     return p->errorHandler;
1099
1100 } // Cudd::getHandler
1101
1102
1103 inline void
1104 Cudd::checkReturnValue(
1105   const DdNode *result) const
1106 {
1107     if (result == 0) {
1108         if (Cudd_ReadErrorCode(p->manager) == CUDD_MEMORY_OUT) {
1109             p->errorHandler("Out of memory.");
1110         } else {
1111             p->errorHandler("Internal error.");
1112         }
1113     }
1114
1115 } // Cudd::checkReturnValue
1116
1117
1118 inline void
1119 Cudd::checkReturnValue(
1120   const int result) const
1121 {
1122     if (result == 0) {
1123         if (Cudd_ReadErrorCode(p->manager) == CUDD_MEMORY_OUT) {
1124             p->errorHandler("Out of memory.");
1125         } else {
1126             p->errorHandler("Internal error.");
1127         }
1128     }
1129
1130 } // Cudd::checkReturnValue
1131
1132
1133 void
1134 Cudd::info() const
1135 {
1136     cout.flush();
1137     int retval = Cudd_PrintInfo(p->manager,stdout);
1138     this->checkReturnValue(retval);
1139
1140 } // Cudd::info
1141
1142
1143 BDD
1144 Cudd::bddVar()
1145 {
1146     DdNode *result = Cudd_bddNewVar(p->manager);
1147     this->checkReturnValue(result);
1148     return BDD(this, result);
1149
1150 } // Cudd::bddVar
1151
1152
1153 BDD
1154 Cudd::bddVar(
1155   int index)
1156 {
1157     DdNode *result = Cudd_bddIthVar(p->manager,index);
1158     this->checkReturnValue(result);
1159     return BDD(this, result);
1160
1161 } // Cudd::bddVar
1162
1163
1164 BDD
1165 Cudd::bddOne()
1166 {
1167     DdNode *result = Cudd_ReadOne(p->manager);
1168     this->checkReturnValue(result);
1169     return BDD(this, result);
1170
1171 } // Cudd::bddOne
1172
1173
1174 BDD
1175 Cudd::bddZero()
1176 {
1177     DdNode *result = Cudd_ReadLogicZero(p->manager);
1178     this->checkReturnValue(result);
1179     return BDD(this, result);
1180
1181 } // Cudd::bddZero
1182
1183
1184 ADD
1185 Cudd::addVar()
1186 {
1187     DdNode *result = Cudd_addNewVar(p->manager);
1188     this->checkReturnValue(result);
1189     return ADD(this, result);
1190
1191 } // Cudd::addVar
1192
1193
1194 ADD
1195 Cudd::addVar(
1196   int index)
1197 {
1198     DdNode *result = Cudd_addIthVar(p->manager,index);
1199     this->checkReturnValue(result);
1200     return ADD(this, result);
1201
1202 } // Cudd::addVar
1203
1204
1205 ADD
1206 Cudd::addOne()
1207 {
1208     DdNode *result = Cudd_ReadOne(p->manager);
1209     this->checkReturnValue(result);
1210     return ADD(this, result);
1211
1212 } // Cudd::addOne
1213
1214
1215 ADD
1216 Cudd::addZero()
1217 {
1218     DdNode *result = Cudd_ReadZero(p->manager);
1219     this->checkReturnValue(result);
1220     return ADD(this, result);
1221
1222 } // Cudd::addZero
1223
1224
1225 ADD
1226 Cudd::constant(
1227   CUDD_VALUE_TYPE c)
1228 {
1229     DdNode *result = Cudd_addConst(p->manager, c);
1230     this->checkReturnValue(result);
1231     return ADD(this, result);
1232
1233 } // Cudd::constant
1234
1235
1236 ADD
1237 Cudd::plusInfinity()
1238 {
1239     DdNode *result = Cudd_ReadPlusInfinity(p->manager);
1240     this->checkReturnValue(result);
1241     return ADD(this, result);
1242
1243 } // Cudd::plusInfinity
1244
1245
1246 ADD
1247 Cudd::minusInfinity()
1248 {
1249     DdNode *result = Cudd_ReadMinusInfinity(p->manager);
1250     this->checkReturnValue(result);
1251     return ADD(this, result);
1252
1253 } // Cudd::minusInfinity
1254
1255
1256 ZDD
1257 Cudd::zddVar(
1258   int index)
1259 {
1260     DdNode *result = Cudd_zddIthVar(p->manager,index);
1261     this->checkReturnValue(result);
1262     return ZDD(this, result);
1263
1264 } // Cudd::zddVar
1265
1266
1267 ZDD
1268 Cudd::zddOne(
1269   int i)
1270 {
1271     DdNode *result = Cudd_ReadZddOne(p->manager,i);
1272     this->checkReturnValue(result);
1273     return ZDD(this, result);
1274
1275 } // Cudd::zddOne
1276
1277
1278 ZDD
1279 Cudd::zddZero()
1280 {
1281     DdNode *result = Cudd_ReadZero(p->manager);
1282     this->checkReturnValue(result);
1283     return ZDD(this, result);
1284
1285 } // Cudd::zddZero
1286
1287
1288 void
1289 defaultError(
1290   string message)
1291 {
1292     cerr << message << "\n";
1293     exit(1);
1294
1295 } // defaultError
1296
1297
1298 // ---------------------------------------------------------------------------
1299 // Members of class BDDvector
1300 // ---------------------------------------------------------------------------
1301
1302
1303 BDDvector::BDDvector(int size, Cudd *manager, DdNode **nodes)
1304 {
1305     if (manager == 0 && nodes != 0) defaultError("Nodes with no manager");
1306     p = new capsule;
1307     p->size = size;
1308     p->manager = manager;
1309     p->vect = new BDD[size];
1310     p->ref = 1;
1311     for (int i = 0; i < size; i++) {
1312         if (nodes == 0) {
1313             p->vect[i] = BDD();
1314         } else {
1315             p->vect[i] = BDD(manager, nodes[i]);
1316         }
1317     }
1318     if (manager != 0 && manager->isVerbose()) {
1319         cout << "Standard BDDvector constructor for vector " << hex << long(p)
1320              << "\n";
1321     }
1322
1323 } // BDDvector::BDDvector
1324
1325
1326 BDDvector::BDDvector(const BDDvector &from)
1327 {
1328     p = from.p;
1329     p->ref++;
1330     if (p->manager != 0 && p->manager->isVerbose()) {
1331         cout << "Copy BDDvector constructor for vector " << hex << long(p)
1332              << "\n";
1333     }
1334
1335 } // BDDvector::BDDvector
1336
1337
1338 BDDvector::~BDDvector()
1339 {
1340     if (p->manager != 0 && p->manager->isVerbose()) {
1341         cout << "BDDvector destructor for vector " << hex << long(p) <<
1342             " ref = " << p->ref << "\n";
1343     }
1344     if (--p->ref == 0) {
1345         delete [] p->vect;
1346         delete p;
1347     }
1348
1349 } // BDDvector::~BDDvector
1350
1351
1352 BDDvector&
1353 BDDvector::operator=(
1354   const BDDvector& right)
1355 {
1356     right.p->ref++;
1357     if (--p->ref == 0) {        // disconnect self
1358         for (int i = 1; i < p->size; i++) {
1359             delete &(p->vect[i]);
1360         }
1361         delete p->vect;
1362         delete p;
1363     }
1364     p = right.p;
1365     return *this;
1366
1367 } // BDDvector::operator=
1368
1369
1370 BDD&
1371 BDDvector::operator[](int i) const
1372 {
1373     if (i >= p->size)
1374         (p->manager->getHandler())("Out-of-bounds access attempted");
1375     return p->vect[i];
1376
1377 } // BDDvector::operator[]
1378
1379
1380 // ---------------------------------------------------------------------------
1381 // Members of class ADDvector
1382 // ---------------------------------------------------------------------------
1383
1384
1385 ADDvector::ADDvector(int size, Cudd *manager, DdNode **nodes)
1386 {
1387     if (manager == 0 && nodes != 0) defaultError("Nodes with no manager");
1388     p = new capsule;
1389     p->size = size;
1390     p->manager = manager;
1391     p->vect = new ADD[size];
1392     p->ref = 1;
1393     for (int i = 0; i < size; i++) {
1394         if (nodes == 0) {
1395             p->vect[i] = ADD();
1396         } else {
1397             p->vect[i] = ADD(manager, nodes[i]);
1398         }
1399     }
1400     if (manager != 0 && manager->isVerbose()) {
1401         cout << "Standard ADDvector constructor for vector " << hex << long(p)
1402              << "\n";
1403     }
1404
1405 } // ADDvector::ADDvector
1406
1407
1408 ADDvector::ADDvector(const ADDvector &from)
1409 {
1410     p = from.p;
1411     p->ref++;
1412     if (p->manager != 0 && p->manager->isVerbose()) {
1413         cout << "Copy ADDvector constructor for vector " << hex << long(p)
1414              << "\n";
1415     }
1416
1417 } // ADDvector::ADDvector
1418
1419
1420 ADDvector::~ADDvector()
1421 {
1422     if (p->manager != 0 && p->manager->isVerbose()) {
1423         cout << "ADDvector destructor for vector " << hex << long(p) <<
1424             " ref = " << p->ref << "\n";
1425     }
1426     if (--p->ref == 0) {
1427         delete [] p->vect;
1428         delete p;
1429     }
1430
1431 } // ADDvector::~ADDvector
1432
1433
1434 ADDvector&
1435 ADDvector::operator=(
1436   const ADDvector& right)
1437 {
1438     right.p->ref++;
1439     if (--p->ref == 0) {        // disconnect self
1440         for (int i = 1; i < p->size; i++) {
1441             delete &(p->vect[i]);
1442         }
1443         delete p->vect;
1444         delete p;
1445     }
1446     p = right.p;
1447     return *this;
1448
1449 } // ADDvector::operator=
1450
1451
1452 ADD&
1453 ADDvector::operator[](int i) const
1454 {
1455     if (i >= p->size)
1456         (p->manager->getHandler())("Out-of-bounds access attempted");
1457     return p->vect[i];
1458
1459 } // ADDvector::operator[]
1460
1461
1462 // ---------------------------------------------------------------------------
1463 // Members of class ZDDvector
1464 // ---------------------------------------------------------------------------
1465
1466
1467 ZDDvector::ZDDvector(int size, Cudd *manager, DdNode **nodes)
1468 {
1469     if (manager == 0 && nodes != 0) defaultError("Nodes with no manager");
1470     p = new capsule;
1471     p->size = size;
1472     p->manager = manager;
1473     p->vect = new ZDD[size];
1474     p->ref = 1;
1475     for (int i = 0; i < size; i++) {
1476         if (nodes == 0) {
1477             p->vect[i] = ZDD();
1478         } else {
1479             p->vect[i] = ZDD(manager, nodes[i]);
1480         }
1481     }
1482     if (manager != 0 && manager->isVerbose()) {
1483         cout << "Standard ZDDvector constructor for vector " << hex << long(p)
1484              << "\n";
1485     }
1486
1487 } // ZDDvector::ZDDvector
1488
1489
1490 ZDDvector::ZDDvector(const ZDDvector &from)
1491 {
1492     p = from.p;
1493     p->ref++;
1494     if (p->manager != 0 && p->manager->isVerbose()) {
1495         cout << "Copy ZDDvector constructor for vector " << hex << long(p)
1496              << "\n";
1497     }
1498
1499 } // ZDDvector::ZDDvector
1500
1501
1502 ZDDvector::~ZDDvector()
1503 {
1504     if (p->manager != 0 && p->manager->isVerbose()) {
1505         cout << "ZDDvector destructor for vector " << hex << long(p) <<
1506             " ref = " << p->ref << "\n";
1507     }
1508     if (--p->ref == 0) {
1509         delete [] p->vect;
1510         delete p;
1511     }
1512
1513 } // ZDDvector::~ZDDvector
1514
1515
1516 ZDDvector&
1517 ZDDvector::operator=(
1518   const ZDDvector& right)
1519 {
1520     right.p->ref++;
1521     if (--p->ref == 0) {        // disconnect self
1522         for (int i = 1; i < p->size; i++) {
1523             delete &(p->vect[i]);
1524         }
1525         delete p->vect;
1526         delete p;
1527     }
1528     p = right.p;
1529     return *this;
1530
1531 } // ZDDvector::operator=
1532
1533
1534 ZDD&
1535 ZDDvector::operator[](int i) const
1536 {
1537     if (i >= p->size)
1538         (p->manager->getHandler())("Out-of-bounds access attempted");
1539     return p->vect[i];
1540
1541 } // ZDDvector::operator[]
1542
1543
1544 // ---------------------------------------------------------------------------
1545 // All the rest
1546 // ---------------------------------------------------------------------------
1547
1548
1549 ADD
1550 Cudd::addNewVarAtLevel(
1551   int level)
1552 {
1553     DdNode *result = Cudd_addNewVarAtLevel(p->manager, level);
1554     this->checkReturnValue(result);
1555     return ADD(this, result);
1556
1557 } // Cudd::addNewVarAtLevel
1558
1559
1560 BDD
1561 Cudd::bddNewVarAtLevel(
1562   int level)
1563 {
1564     DdNode *result = Cudd_bddNewVarAtLevel(p->manager, level);
1565     this->checkReturnValue(result);
1566     return BDD(this, result);
1567
1568 } // Cudd::bddNewVarAtLevel
1569
1570
1571 void
1572 Cudd::zddVarsFromBddVars(
1573   int multiplicity)
1574 {
1575     int result = Cudd_zddVarsFromBddVars(p->manager, multiplicity);
1576     this->checkReturnValue(result);
1577
1578 } // Cudd::zddVarsFromBddVars
1579
1580
1581 void
1582 Cudd::AutodynEnable(
1583   Cudd_ReorderingType method)
1584 {
1585     Cudd_AutodynEnable(p->manager, method);
1586
1587 } // Cudd::AutodynEnable
1588
1589
1590 void
1591 Cudd::AutodynDisable()
1592 {
1593     Cudd_AutodynDisable(p->manager);
1594
1595 } // Cudd::AutodynDisable
1596
1597
1598 int
1599 Cudd::ReorderingStatus(
1600   Cudd_ReorderingType * method) const
1601 {
1602     return Cudd_ReorderingStatus(p->manager, method);
1603
1604 } // Cudd::ReorderingStatus
1605
1606
1607 void
1608 Cudd::AutodynEnableZdd(
1609   Cudd_ReorderingType method)
1610 {
1611     Cudd_AutodynEnableZdd(p->manager, method);
1612
1613 } // Cudd::AutodynEnableZdd
1614
1615
1616 void
1617 Cudd::AutodynDisableZdd()
1618 {
1619     Cudd_AutodynDisableZdd(p->manager);
1620
1621 } // Cudd::AutodynDisableZdd
1622
1623
1624 int
1625 Cudd::ReorderingStatusZdd(
1626   Cudd_ReorderingType * method) const
1627 {
1628     return Cudd_ReorderingStatusZdd(p->manager, method);
1629
1630 } // Cudd::ReorderingStatusZdd
1631
1632
1633 int
1634 Cudd::zddRealignmentEnabled() const
1635 {
1636     return Cudd_zddRealignmentEnabled(p->manager);
1637
1638 } // Cudd::zddRealignmentEnabled
1639
1640
1641 void
1642 Cudd::zddRealignEnable()
1643 {
1644     Cudd_zddRealignEnable(p->manager);
1645
1646 } // Cudd::zddRealignEnable
1647
1648
1649 void
1650 Cudd::zddRealignDisable()
1651 {
1652     Cudd_zddRealignDisable(p->manager);
1653
1654 } // Cudd::zddRealignDisable
1655
1656
1657 int
1658 Cudd::bddRealignmentEnabled() const
1659 {
1660     return Cudd_bddRealignmentEnabled(p->manager);
1661
1662 } // Cudd::bddRealignmentEnabled
1663
1664
1665 void
1666 Cudd::bddRealignEnable()
1667 {
1668     Cudd_bddRealignEnable(p->manager);
1669
1670 } // Cudd::bddRealignEnable
1671
1672
1673 void
1674 Cudd::bddRealignDisable()
1675 {
1676     Cudd_bddRealignDisable(p->manager);
1677
1678 } // Cudd::bddRealignDisable
1679
1680
1681 ADD
1682 Cudd::background()
1683 {
1684     DdNode *result = Cudd_ReadBackground(p->manager);
1685     this->checkReturnValue(result);
1686     return ADD(this, result);
1687
1688 } // Cudd::background
1689
1690
1691 void
1692 Cudd::SetBackground(
1693   ADD bg)
1694 {
1695     DdManager *mgr = p->manager;
1696     if (mgr != bg.manager()->p->manager) {
1697         p->errorHandler("Background comes from different manager.");
1698     }
1699     Cudd_SetBackground(mgr, bg.getNode());
1700
1701 } // Cudd::SetBackground
1702
1703
1704 unsigned int
1705 Cudd::ReadCacheSlots() const
1706 {
1707     return Cudd_ReadCacheSlots(p->manager);
1708
1709 } // Cudd::ReadCacheSlots
1710
1711
1712 double
1713 Cudd::ReadCacheLookUps() const
1714 {
1715     return Cudd_ReadCacheLookUps(p->manager);
1716
1717 } // Cudd::ReadCacheLookUps
1718
1719
1720 double
1721 Cudd::ReadCacheUsedSlots() const
1722 {
1723     return Cudd_ReadCacheUsedSlots(p->manager);
1724
1725 } // Cudd::ReadCacheUsedSlots
1726
1727
1728 double
1729 Cudd::ReadCacheHits() const
1730 {
1731     return Cudd_ReadCacheHits(p->manager);
1732
1733 } // Cudd::ReadCacheHits
1734
1735
1736 unsigned int
1737 Cudd::ReadMinHit() const
1738 {
1739     return Cudd_ReadMinHit(p->manager);
1740
1741 } // Cudd::ReadMinHit
1742
1743
1744 void
1745 Cudd::SetMinHit(
1746   unsigned int hr)
1747 {
1748     Cudd_SetMinHit(p->manager, hr);
1749
1750 } // Cudd::SetMinHit
1751
1752
1753 unsigned int
1754 Cudd::ReadLooseUpTo() const
1755 {
1756     return Cudd_ReadLooseUpTo(p->manager);
1757
1758 } // Cudd::ReadLooseUpTo
1759
1760
1761 void
1762 Cudd::SetLooseUpTo(
1763   unsigned int lut)
1764 {
1765     Cudd_SetLooseUpTo(p->manager, lut);
1766
1767 } // Cudd::SetLooseUpTo
1768
1769
1770 unsigned int
1771 Cudd::ReadMaxCache() const
1772 {
1773     return Cudd_ReadMaxCache(p->manager);
1774
1775 } // Cudd::ReadMaxCache
1776
1777
1778 unsigned int
1779 Cudd::ReadMaxCacheHard() const
1780 {
1781     return Cudd_ReadMaxCacheHard(p->manager);
1782
1783 } // Cudd::ReadMaxCacheHard
1784
1785
1786 void
1787 Cudd::SetMaxCacheHard(
1788   unsigned int mc)
1789 {
1790     Cudd_SetMaxCacheHard(p->manager, mc);
1791
1792 } // Cudd::SetMaxCacheHard
1793
1794
1795 int
1796 Cudd::ReadSize() const
1797 {
1798     return Cudd_ReadSize(p->manager);
1799
1800 } // Cudd::ReadSize
1801
1802
1803 int
1804 Cudd::ReadZddSize() const
1805 {
1806     return Cudd_ReadZddSize(p->manager);
1807
1808 } // Cudd::ReadZddSize
1809
1810
1811 unsigned int
1812 Cudd::ReadSlots() const
1813 {
1814     return Cudd_ReadSlots(p->manager);
1815
1816 } // Cudd::ReadSlots
1817
1818
1819 unsigned int
1820 Cudd::ReadKeys() const
1821 {
1822     return Cudd_ReadKeys(p->manager);
1823
1824 } // Cudd::ReadKeys
1825
1826
1827 unsigned int
1828 Cudd::ReadDead() const
1829 {
1830     return Cudd_ReadDead(p->manager);
1831
1832 } // Cudd::ReadDead
1833
1834
1835 unsigned int
1836 Cudd::ReadMinDead() const
1837 {
1838     return Cudd_ReadMinDead(p->manager);
1839
1840 } // Cudd::ReadMinDead
1841
1842
1843 int
1844 Cudd::ReadReorderings() const
1845 {
1846     return Cudd_ReadReorderings(p->manager);
1847
1848 } // Cudd::ReadReorderings
1849
1850
1851 long
1852 Cudd::ReadReorderingTime() const
1853 {
1854     return Cudd_ReadReorderingTime(p->manager);
1855
1856 } // Cudd::ReadReorderingTime
1857
1858
1859 int
1860 Cudd::ReadGarbageCollections() const
1861 {
1862     return Cudd_ReadGarbageCollections(p->manager);
1863
1864 } // Cudd::ReadGarbageCollections
1865
1866
1867 long
1868 Cudd::ReadGarbageCollectionTime() const
1869 {
1870     return Cudd_ReadGarbageCollectionTime(p->manager);
1871
1872 } // Cudd::ReadGarbageCollectionTime
1873
1874
1875 int
1876 Cudd::ReadSiftMaxVar() const
1877 {
1878     return Cudd_ReadSiftMaxVar(p->manager);
1879
1880 } // Cudd::ReadSiftMaxVar
1881
1882
1883 void
1884 Cudd::SetSiftMaxVar(
1885   int smv)
1886 {
1887     Cudd_SetSiftMaxVar(p->manager, smv);
1888
1889 } // Cudd::SetSiftMaxVar
1890
1891
1892 int
1893 Cudd::ReadSiftMaxSwap() const
1894 {
1895     return Cudd_ReadSiftMaxSwap(p->manager);
1896
1897 } // Cudd::ReadSiftMaxSwap
1898
1899
1900 void
1901 Cudd::SetSiftMaxSwap(
1902   int sms)
1903 {
1904     Cudd_SetSiftMaxSwap(p->manager, sms);
1905
1906 } // Cudd::SetSiftMaxSwap
1907
1908
1909 double
1910 Cudd::ReadMaxGrowth() const
1911 {
1912     return Cudd_ReadMaxGrowth(p->manager);
1913
1914 } // Cudd::ReadMaxGrowth
1915
1916
1917 void
1918 Cudd::SetMaxGrowth(
1919   double mg)
1920 {
1921     Cudd_SetMaxGrowth(p->manager, mg);
1922
1923 } // Cudd::SetMaxGrowth
1924
1925
1926 MtrNode *
1927 Cudd::ReadTree() const
1928 {
1929     return Cudd_ReadTree(p->manager);
1930
1931 } // Cudd::ReadTree
1932
1933
1934 void
1935 Cudd::SetTree(
1936   MtrNode * tree)
1937 {
1938     Cudd_SetTree(p->manager, tree);
1939
1940 } // Cudd::SetTree
1941
1942
1943 void
1944 Cudd::FreeTree()
1945 {
1946     Cudd_FreeTree(p->manager);
1947
1948 } // Cudd::FreeTree
1949
1950
1951 MtrNode *
1952 Cudd::ReadZddTree() const
1953 {
1954     return Cudd_ReadZddTree(p->manager);
1955
1956 } // Cudd::ReadZddTree
1957
1958
1959 void
1960 Cudd::SetZddTree(
1961   MtrNode * tree)
1962 {
1963     Cudd_SetZddTree(p->manager, tree);
1964
1965 } // Cudd::SetZddTree
1966
1967
1968 void
1969 Cudd::FreeZddTree()
1970 {
1971     Cudd_FreeZddTree(p->manager);
1972
1973 } // Cudd::FreeZddTree
1974
1975
1976 unsigned int
1977 DD::NodeReadIndex() const
1978 {
1979     return Cudd_NodeReadIndex(node);
1980
1981 } // DD::NodeReadIndex
1982
1983
1984 int
1985 Cudd::ReadPerm(
1986   int i) const
1987 {
1988     return Cudd_ReadPerm(p->manager, i);
1989
1990 } // Cudd::ReadPerm
1991
1992
1993 int
1994 Cudd::ReadPermZdd(
1995   int i) const
1996 {
1997     return Cudd_ReadPermZdd(p->manager, i);
1998
1999 } // Cudd::ReadPermZdd
2000
2001
2002 int
2003 Cudd::ReadInvPerm(
2004   int i) const
2005 {
2006     return Cudd_ReadInvPerm(p->manager, i);
2007
2008 } // Cudd::ReadInvPerm
2009
2010
2011 int
2012 Cudd::ReadInvPermZdd(
2013   int i) const
2014 {
2015     return Cudd_ReadInvPermZdd(p->manager, i);
2016
2017 } // Cudd::ReadInvPermZdd
2018
2019
2020 BDD
2021 Cudd::ReadVars(
2022   int i)
2023 {
2024     DdNode *result = Cudd_ReadVars(p->manager, i);
2025     this->checkReturnValue(result);
2026     return BDD(this, result);
2027
2028 } // Cudd::ReadVars
2029
2030
2031 CUDD_VALUE_TYPE
2032 Cudd::ReadEpsilon() const
2033 {
2034     return Cudd_ReadEpsilon(p->manager);
2035
2036 } // Cudd::ReadEpsilon
2037
2038
2039 void
2040 Cudd::SetEpsilon(
2041   CUDD_VALUE_TYPE ep)
2042 {
2043     Cudd_SetEpsilon(p->manager, ep);
2044
2045 } // Cudd::SetEpsilon
2046
2047
2048 Cudd_AggregationType
2049 Cudd::ReadGroupcheck() const
2050 {
2051     return Cudd_ReadGroupcheck(p->manager);
2052
2053 } // Cudd::ReadGroupcheck
2054
2055
2056 void
2057 Cudd::SetGroupcheck(
2058   Cudd_AggregationType gc)
2059 {
2060     Cudd_SetGroupcheck(p->manager, gc);
2061
2062 } // Cudd::SetGroupcheck
2063
2064
2065 int
2066 Cudd::GarbageCollectionEnabled() const
2067 {
2068     return Cudd_GarbageCollectionEnabled(p->manager);
2069
2070 } // Cudd::GarbageCollectionEnabled
2071
2072
2073 void
2074 Cudd::EnableGarbageCollection()
2075 {
2076     Cudd_EnableGarbageCollection(p->manager);
2077
2078 } // Cudd::EnableGarbageCollection
2079
2080
2081 void
2082 Cudd::DisableGarbageCollection()
2083 {
2084     Cudd_DisableGarbageCollection(p->manager);
2085
2086 } // Cudd::DisableGarbageCollection
2087
2088
2089 int
2090 Cudd::DeadAreCounted() const
2091 {
2092     return Cudd_DeadAreCounted(p->manager);
2093
2094 } // Cudd::DeadAreCounted
2095
2096
2097 void
2098 Cudd::TurnOnCountDead()
2099 {
2100     Cudd_TurnOnCountDead(p->manager);
2101
2102 } // Cudd::TurnOnCountDead
2103
2104
2105 void
2106 Cudd::TurnOffCountDead()
2107 {
2108     Cudd_TurnOffCountDead(p->manager);
2109
2110 } // Cudd::TurnOffCountDead
2111
2112
2113 int
2114 Cudd::ReadRecomb() const
2115 {
2116     return Cudd_ReadRecomb(p->manager);
2117
2118 } // Cudd::ReadRecomb
2119
2120
2121 void
2122 Cudd::SetRecomb(
2123   int recomb)
2124 {
2125     Cudd_SetRecomb(p->manager, recomb);
2126
2127 } // Cudd::SetRecomb
2128
2129
2130 int
2131 Cudd::ReadSymmviolation() const
2132 {
2133     return Cudd_ReadSymmviolation(p->manager);
2134
2135 } // Cudd::ReadSymmviolation
2136
2137
2138 void
2139 Cudd::SetSymmviolation(
2140   int symmviolation)
2141 {
2142     Cudd_SetSymmviolation(p->manager, symmviolation);
2143
2144 } // Cudd::SetSymmviolation
2145
2146
2147 int
2148 Cudd::ReadArcviolation() const
2149 {
2150     return Cudd_ReadArcviolation(p->manager);
2151
2152 } // Cudd::ReadArcviolation
2153
2154
2155 void
2156 Cudd::SetArcviolation(
2157   int arcviolation)
2158 {
2159     Cudd_SetArcviolation(p->manager, arcviolation);
2160
2161 } // Cudd::SetArcviolation
2162
2163
2164 int
2165 Cudd::ReadPopulationSize() const
2166 {
2167     return Cudd_ReadPopulationSize(p->manager);
2168
2169 } // Cudd::ReadPopulationSize
2170
2171
2172 void
2173 Cudd::SetPopulationSize(
2174   int populationSize)
2175 {
2176     Cudd_SetPopulationSize(p->manager, populationSize);
2177
2178 } // Cudd::SetPopulationSize
2179
2180
2181 int
2182 Cudd::ReadNumberXovers() const
2183 {
2184     return Cudd_ReadNumberXovers(p->manager);
2185
2186 } // Cudd::ReadNumberXovers
2187
2188
2189 void
2190 Cudd::SetNumberXovers(
2191   int numberXovers)
2192 {
2193     Cudd_SetNumberXovers(p->manager, numberXovers);
2194
2195 } // Cudd::SetNumberXovers
2196
2197
2198 unsigned long
2199 Cudd::ReadMemoryInUse() const
2200 {
2201     return Cudd_ReadMemoryInUse(p->manager);
2202
2203 } // Cudd::ReadMemoryInUse
2204
2205
2206 long
2207 Cudd::ReadPeakNodeCount() const
2208 {
2209     return Cudd_ReadPeakNodeCount(p->manager);
2210
2211 } // Cudd::ReadPeakNodeCount
2212
2213
2214 long
2215 Cudd::ReadNodeCount() const
2216 {
2217     return Cudd_ReadNodeCount(p->manager);
2218
2219 } // Cudd::ReadNodeCount
2220
2221
2222 long
2223 Cudd::zddReadNodeCount() const
2224 {
2225     return Cudd_zddReadNodeCount(p->manager);
2226
2227 } // Cudd::zddReadNodeCount
2228
2229
2230 void
2231 Cudd::AddHook(
2232   DD_HFP f,
2233   Cudd_HookType where)
2234 {
2235     int result = Cudd_AddHook(p->manager, f, where);
2236     this->checkReturnValue(result);
2237
2238 } // Cudd::AddHook
2239
2240
2241 void
2242 Cudd::RemoveHook(
2243   DD_HFP f,
2244   Cudd_HookType where)
2245 {
2246     int result = Cudd_RemoveHook(p->manager, f, where);
2247     this->checkReturnValue(result);
2248
2249 } // Cudd::RemoveHook
2250
2251
2252 int
2253 Cudd::IsInHook(
2254   DD_HFP f,
2255   Cudd_HookType where) const
2256 {
2257     return Cudd_IsInHook(p->manager, f, where);
2258
2259 } // Cudd::IsInHook
2260
2261
2262 void
2263 Cudd::EnableReorderingReporting()
2264 {
2265     int result = Cudd_EnableReorderingReporting(p->manager);
2266     this->checkReturnValue(result);
2267
2268 } // Cudd::EnableReorderingReporting
2269
2270
2271 void
2272 Cudd::DisableReorderingReporting()
2273 {
2274     int result = Cudd_DisableReorderingReporting(p->manager);
2275     this->checkReturnValue(result);
2276
2277 } // Cudd::DisableReorderingReporting
2278
2279
2280 int
2281 Cudd::ReorderingReporting()
2282 {
2283     return Cudd_ReorderingReporting(p->manager);
2284
2285 } // Cudd::ReorderingReporting
2286
2287
2288 int
2289 Cudd::ReadErrorCode() const
2290 {
2291     return Cudd_ReadErrorCode(p->manager);
2292
2293 } // Cudd::ReadErrorCode
2294
2295
2296 void
2297 Cudd::ClearErrorCode()
2298 {
2299     Cudd_ClearErrorCode(p->manager);
2300
2301 } // Cudd::ClearErrorCode
2302
2303
2304 FILE *
2305 Cudd::ReadStdout() const
2306 {
2307     return Cudd_ReadStdout(p->manager);
2308
2309 } // Cudd::ReadStdout
2310
2311
2312 void
2313 Cudd::SetStdout(FILE *fp)
2314 {
2315     Cudd_SetStdout(p->manager, fp);
2316
2317 } // Cudd::SetStdout
2318
2319
2320 FILE *
2321 Cudd::ReadStderr() const
2322 {
2323     return Cudd_ReadStderr(p->manager);
2324
2325 } // Cudd::ReadStderr
2326
2327
2328 void
2329 Cudd::SetStderr(FILE *fp)
2330 {
2331     Cudd_SetStderr(p->manager, fp);
2332
2333 } // Cudd::SetStderr
2334
2335
2336 unsigned int
2337 Cudd::ReadNextReordering() const
2338 {
2339     return Cudd_ReadNextReordering(p->manager);
2340
2341 } // Cudd::ReadNextReordering
2342
2343
2344 double
2345 Cudd::ReadSwapSteps() const
2346 {
2347     return Cudd_ReadSwapSteps(p->manager);
2348
2349 } // Cudd::ReadSwapSteps
2350
2351
2352 unsigned int
2353 Cudd::ReadMaxLive() const
2354 {
2355     return Cudd_ReadMaxLive(p->manager);
2356
2357 } // Cudd::ReadMaxLive
2358
2359
2360 void
2361 Cudd::SetMaxLive(unsigned int maxLive)
2362 {
2363     Cudd_SetMaxLive(p->manager, maxLive);
2364
2365 } // Cudd::SetMaxLive
2366
2367
2368 unsigned long
2369 Cudd::ReadMaxMemory() const
2370 {
2371     return Cudd_ReadMaxMemory(p->manager);
2372
2373 } // Cudd::ReadMaxMemory
2374
2375
2376 void
2377 Cudd::SetMaxMemory(unsigned long maxMem)
2378 {
2379     Cudd_SetMaxMemory(p->manager, maxMem);
2380
2381 } // Cudd::SetMaxMemory
2382
2383
2384 int
2385 Cudd::bddBindVar(int index)
2386 {
2387     return Cudd_bddBindVar(p->manager, index);
2388
2389 } // Cudd::bddBindVar
2390
2391
2392 int
2393 Cudd::bddUnbindVar(int index)
2394 {
2395     return Cudd_bddUnbindVar(p->manager, index);
2396
2397 } // Cudd::bddUnbindVar
2398
2399
2400 int
2401 Cudd::bddVarIsBound(int index) const
2402 {
2403     return Cudd_bddVarIsBound(p->manager, index);
2404
2405 } // Cudd::bddVarIsBound
2406
2407
2408 ADD
2409 ADD::ExistAbstract(
2410   const ADD& cube) const
2411 {
2412     DdManager *mgr = this->checkSameManager(cube);
2413     DdNode *result = Cudd_addExistAbstract(mgr, node, cube.node);
2414     this->checkReturnValue(result);
2415     return ADD(ddMgr, result);
2416
2417 } // ADD::ExistAbstract
2418
2419
2420 ADD
2421 ADD::UnivAbstract(
2422   const ADD& cube) const
2423 {
2424     DdManager *mgr = this->checkSameManager(cube);
2425     DdNode *result = Cudd_addUnivAbstract(mgr, node, cube.node);
2426     this->checkReturnValue(result);
2427     return ADD(ddMgr, result);
2428
2429 } // ADD::UnivAbstract
2430
2431
2432 ADD
2433 ADD::OrAbstract(
2434   const ADD& cube) const
2435 {
2436     DdManager *mgr = this->checkSameManager(cube);
2437     DdNode *result = Cudd_addOrAbstract(mgr, node, cube.node);
2438     this->checkReturnValue(result);
2439     return ADD(ddMgr, result);
2440
2441 } // ADD::OrAbstract
2442
2443
2444 ADD
2445 ADD::Plus(
2446   const ADD& g) const
2447 {
2448     DdManager *mgr = this->checkSameManager(g);
2449     DdNode *result = Cudd_addApply(mgr, Cudd_addPlus, node, g.node);
2450     this->checkReturnValue(result);
2451     return ADD(ddMgr, result);
2452
2453 } // ADD::Plus
2454
2455
2456 ADD
2457 ADD::Times(
2458   const ADD& g) const
2459 {
2460     DdManager *mgr = this->checkSameManager(g);
2461     DdNode *result = Cudd_addApply(mgr, Cudd_addTimes, node, g.node);
2462     this->checkReturnValue(result);
2463     return ADD(ddMgr, result);
2464
2465 } // ADD::Times
2466
2467
2468 ADD
2469 ADD::Threshold(
2470   const ADD& g) const
2471 {
2472     DdManager *mgr = this->checkSameManager(g);
2473     DdNode *result = Cudd_addApply(mgr, Cudd_addThreshold, node, g.node);
2474     this->checkReturnValue(result);
2475     return ADD(ddMgr, result);
2476
2477 } // ADD::Threshold
2478
2479
2480 ADD
2481 ADD::SetNZ(
2482   const ADD& g) const
2483 {
2484     DdManager *mgr = this->checkSameManager(g);
2485     DdNode *result = Cudd_addApply(mgr, Cudd_addSetNZ, node, g.node);
2486     this->checkReturnValue(result);
2487     return ADD(ddMgr, result);
2488
2489 } // ADD::SetNZ
2490
2491
2492 ADD
2493 ADD::Divide(
2494   const ADD& g) const
2495 {
2496     DdManager *mgr = this->checkSameManager(g);
2497     DdNode *result = Cudd_addApply(mgr, Cudd_addDivide, node, g.node);
2498     this->checkReturnValue(result);
2499     return ADD(ddMgr, result);
2500
2501 } // ADD::Divide
2502
2503
2504 ADD
2505 ADD::Minus(
2506   const ADD& g) const
2507 {
2508     DdManager *mgr = this->checkSameManager(g);
2509     DdNode *result = Cudd_addApply(mgr, Cudd_addMinus, node, g.node);
2510     this->checkReturnValue(result);
2511     return ADD(ddMgr, result);
2512
2513 } // ADD::Minus
2514
2515
2516 ADD
2517 ADD::Minimum(
2518   const ADD& g) const
2519 {
2520     DdManager *mgr = this->checkSameManager(g);
2521     DdNode *result = Cudd_addApply(mgr, Cudd_addMinimum, node, g.node);
2522     this->checkReturnValue(result);
2523     return ADD(ddMgr, result);
2524
2525 } // ADD::Minimum
2526
2527
2528 ADD
2529 ADD::Maximum(
2530   const ADD& g) const
2531 {
2532     DdManager *mgr = this->checkSameManager(g);
2533     DdNode *result = Cudd_addApply(mgr, Cudd_addMaximum, node, g.node);
2534     this->checkReturnValue(result);
2535     return ADD(ddMgr, result);
2536
2537 } // ADD::Maximum
2538
2539
2540 ADD
2541 ADD::OneZeroMaximum(
2542   const ADD& g) const
2543 {
2544     DdManager *mgr = this->checkSameManager(g);
2545     DdNode *result = Cudd_addApply(mgr, Cudd_addOneZeroMaximum, node, g.node);
2546     this->checkReturnValue(result);
2547     return ADD(ddMgr, result);
2548
2549 } // ADD::OneZeroMaximum
2550
2551
2552 ADD
2553 ADD::Diff(
2554   const ADD& g) const
2555 {
2556     DdManager *mgr = this->checkSameManager(g);
2557     DdNode *result = Cudd_addApply(mgr, Cudd_addDiff, node, g.node);
2558     this->checkReturnValue(result);
2559     return ADD(ddMgr, result);
2560
2561 } // ADD::Diff
2562
2563
2564 ADD
2565 ADD::Agreement(
2566   const ADD& g) const
2567 {
2568     DdManager *mgr = this->checkSameManager(g);
2569     DdNode *result = Cudd_addApply(mgr, Cudd_addAgreement, node, g.node);
2570     this->checkReturnValue(result);
2571     return ADD(ddMgr, result);
2572
2573 } // ADD::Agreement
2574
2575
2576 ADD
2577 ADD::Or(
2578   const ADD& g) const
2579 {
2580     DdManager *mgr = this->checkSameManager(g);
2581     DdNode *result = Cudd_addApply(mgr, Cudd_addOr, node, g.node);
2582     this->checkReturnValue(result);
2583     return ADD(ddMgr, result);
2584
2585 } // ADD::Or
2586
2587
2588 ADD
2589 ADD::Nand(
2590   const ADD& g) const
2591 {
2592     DdManager *mgr = this->checkSameManager(g);
2593     DdNode *result = Cudd_addApply(mgr, Cudd_addNand, node, g.node);
2594     this->checkReturnValue(result);
2595     return ADD(ddMgr, result);
2596
2597 } // ADD::Nand
2598
2599
2600 ADD
2601 ADD::Nor(
2602   const ADD& g) const
2603 {
2604     DdManager *mgr = this->checkSameManager(g);
2605     DdNode *result = Cudd_addApply(mgr, Cudd_addNor, node, g.node);
2606     this->checkReturnValue(result);
2607     return ADD(ddMgr, result);
2608
2609 } // ADD::Nor
2610
2611
2612 ADD
2613 ADD::Xor(
2614   const ADD& g) const
2615 {
2616     DdManager *mgr = this->checkSameManager(g);
2617     DdNode *result = Cudd_addApply(mgr, Cudd_addXor, node, g.node);
2618     this->checkReturnValue(result);
2619     return ADD(ddMgr, result);
2620
2621 } // ADD::Xor
2622
2623
2624 ADD
2625 ADD::Xnor(
2626   const ADD& g) const
2627 {
2628     DdManager *mgr = this->checkSameManager(g);
2629     DdNode *result = Cudd_addApply(mgr, Cudd_addXnor, node, g.node);
2630     this->checkReturnValue(result);
2631     return ADD(ddMgr, result);
2632
2633 } // ADD::Xnor
2634
2635
2636 ADD
2637 ADD::Log() const
2638 {
2639     DdManager *mgr = ddMgr->p->manager;
2640     DdNode *result = Cudd_addMonadicApply(mgr, Cudd_addLog, node);
2641     this->checkReturnValue(result);
2642     return ADD(ddMgr, result);
2643
2644 } // ADD::Log
2645
2646
2647 ADD
2648 ADD::FindMax() const
2649 {
2650     DdManager *mgr = ddMgr->p->manager;
2651     DdNode *result = Cudd_addFindMax(mgr, node);
2652     this->checkReturnValue(result);
2653     return ADD(ddMgr, result);
2654
2655 } // ADD::FindMax
2656
2657
2658 ADD
2659 ADD::FindMin() const
2660 {
2661     DdManager *mgr = ddMgr->p->manager;
2662     DdNode *result = Cudd_addFindMin(mgr, node);
2663     this->checkReturnValue(result);
2664     return ADD(ddMgr, result);
2665
2666 } // ADD::FindMin
2667
2668
2669 ADD
2670 ADD::IthBit(
2671   int bit) const
2672 {
2673     DdManager *mgr = ddMgr->p->manager;
2674     DdNode *result = Cudd_addIthBit(mgr, node, bit);
2675     this->checkReturnValue(result);
2676     return ADD(ddMgr, result);
2677
2678 } // ADD::IthBit
2679
2680
2681 ADD
2682 ADD::ScalarInverse(
2683   const ADD& epsilon) const
2684 {
2685     DdManager *mgr = this->checkSameManager(epsilon);
2686     DdNode *result = Cudd_addScalarInverse(mgr, node, epsilon.node);
2687     this->checkReturnValue(result);
2688     return ADD(ddMgr, result);
2689
2690 } // ADD::ScalarInverse
2691
2692
2693 ADD
2694 ADD::Ite(
2695   const ADD& g,
2696   const ADD& h) const
2697 {
2698     DdManager *mgr = this->checkSameManager(g);
2699     this->checkSameManager(h);
2700     DdNode *result = Cudd_addIte(mgr, node, g.node, h.node);
2701     this->checkReturnValue(result);
2702     return ADD(ddMgr, result);
2703
2704 } // ADD::Ite
2705
2706
2707 ADD
2708 ADD::IteConstant(
2709   const ADD& g,
2710   const ADD& h) const
2711 {
2712     DdManager *mgr = this->checkSameManager(g);
2713     this->checkSameManager(h);
2714     DdNode *result = Cudd_addIteConstant(mgr, node, g.node, h.node);
2715     this->checkReturnValue(result);
2716     return ADD(ddMgr, result);
2717
2718 } // ADD::IteConstant
2719
2720
2721 ADD
2722 ADD::EvalConst(
2723   const ADD& g) const
2724 {
2725     DdManager *mgr = this->checkSameManager(g);
2726     DdNode *result = Cudd_addEvalConst(mgr, node, g.node);
2727     this->checkReturnValue(result);
2728     return ADD(ddMgr, result);
2729
2730 } // ADD::EvalConst
2731
2732
2733 int
2734 ADD::Leq(
2735   const ADD& g) const
2736 {
2737     DdManager *mgr = this->checkSameManager(g);
2738     return Cudd_addLeq(mgr, node, g.node);
2739
2740 } // ADD::Leq
2741
2742
2743 ADD
2744 ADD::Cmpl() const
2745 {
2746     DdManager *mgr = ddMgr->p->manager;
2747     DdNode *result = Cudd_addCmpl(mgr, node);
2748     this->checkReturnValue(result);
2749     return ADD(ddMgr, result);
2750
2751 } // ADD::Cmpl
2752
2753
2754 ADD
2755 ADD::Negate() const
2756 {
2757     DdManager *mgr = ddMgr->p->manager;
2758     DdNode *result = Cudd_addNegate(mgr, node);
2759     this->checkReturnValue(result);
2760     return ADD(ddMgr, result);
2761
2762 } // ADD::Negate
2763
2764
2765 ADD
2766 ADD::RoundOff(
2767   int N) const
2768 {
2769     DdManager *mgr = ddMgr->p->manager;
2770     DdNode *result = Cudd_addRoundOff(mgr, node, N);
2771     this->checkReturnValue(result);
2772     return ADD(ddMgr, result);
2773
2774 } // ADD::RoundOff
2775
2776
2777 ADD
2778 Cudd::Walsh(
2779   ADDvector x,
2780   ADDvector y)
2781 {
2782     int n = x.count();
2783     DdNode **X = ALLOC(DdNode *,n);
2784     DdNode **Y = ALLOC(DdNode *,n);
2785     for (int i = 0; i < n; i++) {
2786         X[i] = x[i].getNode();
2787         Y[i] = y[i].getNode();
2788     }
2789     DdNode *result = Cudd_addWalsh(p->manager, X, Y, n);
2790     FREE(X);
2791     FREE(Y);
2792     this->checkReturnValue(result);
2793     return ADD(this, result);
2794
2795 } // ADD::Walsh
2796
2797
2798 ADD
2799 Cudd::addResidue(
2800   int n,
2801   int m,
2802   int options,
2803   int top)
2804 {
2805     DdNode *result = Cudd_addResidue(p->manager, n, m, options, top);
2806     this->checkReturnValue(result);
2807     return ADD(this, result);
2808
2809 } // Cudd::addResidue
2810
2811
2812 BDD
2813 BDD::AndAbstract(
2814   const BDD& g,
2815   const BDD& cube) const
2816 {
2817     DdManager *mgr = this->checkSameManager(g);
2818     this->checkSameManager(cube);
2819     DdNode *result = Cudd_bddAndAbstract(mgr, node, g.node, cube.node);
2820     this->checkReturnValue(result);
2821     return BDD(ddMgr, result);
2822
2823 } // BDD::AndAbstract
2824
2825
2826 BDD
2827 BDD::AndAbstractLimit(
2828   const BDD& g,
2829   const BDD& cube,
2830   unsigned int limit) const
2831 {
2832     DdManager *mgr = this->checkSameManager(g);
2833     this->checkSameManager(cube);
2834     DdNode *result = Cudd_bddAndAbstractLimit(mgr, node, g.node,
2835                                               cube.node, limit);
2836     this->checkReturnValue(result);
2837     return BDD(ddMgr, result);
2838
2839 } // BDD::AndAbstractLimit
2840
2841
2842 int
2843 Cudd::ApaNumberOfDigits(
2844   int binaryDigits) const
2845 {
2846     return Cudd_ApaNumberOfDigits(binaryDigits);
2847
2848 } // Cudd::ApaNumberOfDigits
2849
2850
2851 DdApaNumber
2852 Cudd::NewApaNumber(
2853   int digits) const
2854 {
2855     return Cudd_NewApaNumber(digits);
2856
2857 } // Cudd::NewApaNumber
2858
2859
2860 void
2861 Cudd::ApaCopy(
2862   int digits,
2863   DdApaNumber source,
2864   DdApaNumber dest) const
2865 {
2866     Cudd_ApaCopy(digits, source, dest);
2867
2868 } // Cudd::ApaCopy
2869
2870
2871 DdApaDigit
2872 Cudd::ApaAdd(
2873   int digits,
2874   DdApaNumber a,
2875   DdApaNumber b,
2876   DdApaNumber sum) const
2877 {
2878     return Cudd_ApaAdd(digits, a, b, sum);
2879
2880 } // Cudd::ApaAdd
2881
2882
2883 DdApaDigit
2884 Cudd::ApaSubtract(
2885   int digits,
2886   DdApaNumber a,
2887   DdApaNumber b,
2888   DdApaNumber diff) const
2889 {
2890     return Cudd_ApaSubtract(digits, a, b, diff);
2891
2892 } // Cudd::ApaSubtract
2893
2894
2895 DdApaDigit
2896 Cudd::ApaShortDivision(
2897   int digits,
2898   DdApaNumber dividend,
2899   DdApaDigit divisor,
2900   DdApaNumber quotient) const
2901 {
2902     return Cudd_ApaShortDivision(digits, dividend, divisor, quotient);
2903
2904 } // Cudd::ApaShortDivision
2905
2906
2907 void
2908 Cudd::ApaShiftRight(
2909   int digits,
2910   DdApaDigit in,
2911   DdApaNumber a,
2912   DdApaNumber b) const
2913 {
2914     Cudd_ApaShiftRight(digits, in, a, b);
2915
2916 } // Cudd::ApaShiftRight
2917
2918
2919 void
2920 Cudd::ApaSetToLiteral(
2921   int digits,
2922   DdApaNumber number,
2923   DdApaDigit literal) const
2924 {
2925     Cudd_ApaSetToLiteral(digits, number, literal);
2926
2927 } // Cudd::ApaSetToLiteral
2928
2929
2930 void
2931 Cudd::ApaPowerOfTwo(
2932   int digits,
2933   DdApaNumber number,
2934   int power) const
2935 {
2936     Cudd_ApaPowerOfTwo(digits, number, power);
2937
2938 } // Cudd::ApaPowerOfTwo
2939
2940
2941 void
2942 Cudd::ApaPrintHex(
2943   FILE * fp,
2944   int digits,
2945   DdApaNumber number) const
2946 {
2947     cout.flush();
2948     int result = Cudd_ApaPrintHex(fp, digits, number);
2949     this->checkReturnValue(result);
2950
2951 } // Cudd::ApaPrintHex
2952
2953
2954 void
2955 Cudd::ApaPrintDecimal(
2956   FILE * fp,
2957   int digits,
2958   DdApaNumber number) const
2959 {
2960     cout.flush();
2961     int result = Cudd_ApaPrintDecimal(fp, digits, number);
2962     this->checkReturnValue(result);
2963
2964 } // Cudd::ApaPrintDecimal
2965
2966
2967 DdApaNumber
2968 ABDD::ApaCountMinterm(
2969   int nvars,
2970   int * digits) const
2971 {
2972     DdManager *mgr = ddMgr->p->manager;
2973     return Cudd_ApaCountMinterm(mgr, node, nvars, digits);
2974
2975 } // ABDD::ApaCountMinterm
2976
2977
2978 void
2979 ABDD::ApaPrintMinterm(
2980   int nvars,
2981   FILE * fp) const
2982 {
2983     cout.flush();
2984     DdManager *mgr = ddMgr->p->manager;
2985     int result = Cudd_ApaPrintMinterm(fp, mgr, node, nvars);
2986     this->checkReturnValue(result);
2987
2988 } // ABDD::ApaPrintMinterm
2989
2990
2991 void
2992 ABDD::EpdPrintMinterm(
2993   int nvars,
2994   FILE * fp) const
2995 {
2996     EpDouble count;
2997     char str[24];
2998     cout.flush();
2999     DdManager *mgr = ddMgr->p->manager;
3000     int result = Cudd_EpdCountMinterm(mgr, node, nvars, &count);
3001     this->checkReturnValue(result,0);
3002     EpdGetString(&count, str);
3003     fprintf(fp, "%s\n", str);
3004
3005 } // ABDD::ApaPrintMinterm
3006
3007
3008 BDD
3009 BDD::UnderApprox(
3010   int numVars,
3011   int threshold,
3012   int safe,
3013   double quality) const
3014 {
3015     DdManager *mgr = ddMgr->p->manager;
3016     DdNode *result = Cudd_UnderApprox(mgr, node, numVars, threshold, safe, quality);
3017     this->checkReturnValue(result);
3018     return BDD(ddMgr, result);
3019
3020 } // BDD::UnderApprox
3021
3022
3023 BDD
3024 BDD::OverApprox(
3025   int numVars,
3026   int threshold,
3027   int safe,
3028   double quality) const
3029 {
3030     DdManager *mgr = ddMgr->p->manager;
3031     DdNode *result = Cudd_OverApprox(mgr, node, numVars, threshold, safe, quality);
3032     this->checkReturnValue(result);
3033     return BDD(ddMgr, result);
3034
3035 } // BDD::OverApprox
3036
3037
3038 BDD
3039 BDD::RemapUnderApprox(
3040   int numVars,
3041   int threshold,
3042   double quality) const
3043 {
3044     DdManager *mgr = ddMgr->p->manager;
3045     DdNode *result = Cudd_RemapUnderApprox(mgr, node, numVars, threshold, quality);
3046     this->checkReturnValue(result);
3047     return BDD(ddMgr, result);
3048
3049 } // BDD::RemapUnderApprox
3050
3051
3052 BDD
3053 BDD::RemapOverApprox(
3054   int numVars,
3055   int threshold,
3056   double quality) const
3057 {
3058     DdManager *mgr = ddMgr->p->manager;
3059     DdNode *result = Cudd_RemapOverApprox(mgr, node, numVars, threshold, quality);
3060     this->checkReturnValue(result);
3061     return BDD(ddMgr, result);
3062
3063 } // BDD::RemapOverApprox
3064
3065
3066 BDD
3067 BDD::ExistAbstract(
3068   const BDD& cube) const
3069 {
3070     DdManager *mgr = this->checkSameManager(cube);
3071     DdNode *result = Cudd_bddExistAbstract(mgr, node, cube.node);
3072     this->checkReturnValue(result);
3073     return BDD(ddMgr, result);
3074
3075 } // BDD::ExistAbstract
3076
3077
3078 BDD
3079 BDD::XorExistAbstract(
3080   const BDD& g,
3081   const BDD& cube) const
3082 {
3083     DdManager *mgr = this->checkSameManager(g);
3084     this->checkSameManager(cube);
3085     DdNode *result = Cudd_bddXorExistAbstract(mgr, node, g.node, cube.node);
3086     this->checkReturnValue(result);
3087     return BDD(ddMgr, result);
3088
3089 } // BDD::XorExistAbstract
3090
3091
3092 BDD
3093 BDD::UnivAbstract(
3094   const BDD& cube) const
3095 {
3096     DdManager *mgr = this->checkSameManager(cube);
3097     DdNode *result = Cudd_bddUnivAbstract(mgr, node, cube.node);
3098     this->checkReturnValue(result);
3099     return BDD(ddMgr, result);
3100
3101 } // BDD::UnivAbstract
3102
3103
3104 BDD
3105 BDD::BooleanDiff(
3106   int x) const
3107 {
3108     DdManager *mgr = ddMgr->p->manager;
3109     DdNode *result = Cudd_bddBooleanDiff(mgr, node, x);
3110     this->checkReturnValue(result);
3111     return BDD(ddMgr, result);
3112
3113 } // BDD::BooleanDiff
3114
3115
3116 int
3117 BDD::VarIsDependent(
3118   const BDD& var) const
3119 {
3120     DdManager *mgr = ddMgr->p->manager;
3121     return Cudd_bddVarIsDependent(mgr, node, var.node);
3122
3123 } // BDD::VarIsDependent
3124
3125
3126 double
3127 BDD::Correlation(
3128   const BDD& g) const
3129 {
3130     DdManager *mgr = this->checkSameManager(g);
3131     return Cudd_bddCorrelation(mgr, node, g.node);
3132
3133 } // BDD::Correlation
3134
3135
3136 double
3137 BDD::CorrelationWeights(
3138   const BDD& g,
3139   double * prob) const
3140 {
3141     DdManager *mgr = this->checkSameManager(g);
3142     return Cudd_bddCorrelationWeights(mgr, node, g.node, prob);
3143
3144 } // BDD::CorrelationWeights
3145
3146
3147 BDD
3148 BDD::Ite(
3149   const BDD& g,
3150   const BDD& h) const
3151 {
3152     DdManager *mgr = this->checkSameManager(g);
3153     this->checkSameManager(h);
3154     DdNode *result = Cudd_bddIte(mgr, node, g.node, h.node);
3155     this->checkReturnValue(result);
3156     return BDD(ddMgr, result);
3157
3158 } // BDD::Ite
3159
3160
3161 BDD
3162 BDD::IteConstant(
3163   const BDD& g,
3164   const BDD& h) const
3165 {
3166     DdManager *mgr = this->checkSameManager(g);
3167     this->checkSameManager(h);
3168     DdNode *result = Cudd_bddIteConstant(mgr, node, g.node, h.node);
3169     this->checkReturnValue(result);
3170     return BDD(ddMgr, result);
3171
3172 } // BDD::IteConstant
3173
3174
3175 BDD
3176 BDD::Intersect(
3177   const BDD& g) const
3178 {
3179     DdManager *mgr = this->checkSameManager(g);
3180     DdNode *result = Cudd_bddIntersect(mgr, node, g.node);
3181     this->checkReturnValue(result);
3182     return BDD(ddMgr, result);
3183
3184 } // BDD::Intersect
3185
3186
3187 BDD
3188 BDD::And(
3189   const BDD& g) const
3190 {
3191     DdManager *mgr = this->checkSameManager(g);
3192     DdNode *result = Cudd_bddAnd(mgr, node, g.node);
3193     this->checkReturnValue(result);
3194     return BDD(ddMgr, result);
3195
3196 } // BDD::And
3197
3198
3199 BDD
3200 BDD::AndLimit(
3201   const BDD& g,
3202   unsigned int limit) const
3203 {
3204     DdManager *mgr = this->checkSameManager(g);
3205     DdNode *result = Cudd_bddAndLimit(mgr, node, g.node, limit);
3206     this->checkReturnValue(result);
3207     return BDD(ddMgr, result);
3208
3209 } // BDD::AndLimit
3210
3211
3212 BDD
3213 BDD::Or(
3214   const BDD& g) const
3215 {
3216     DdManager *mgr = this->checkSameManager(g);
3217     DdNode *result = Cudd_bddOr(mgr, node, g.node);
3218     this->checkReturnValue(result);
3219     return BDD(ddMgr, result);
3220
3221 } // BDD::Or
3222
3223
3224 BDD
3225 BDD::Nand(
3226   const BDD& g) const
3227 {
3228     DdManager *mgr = this->checkSameManager(g);
3229     DdNode *result = Cudd_bddNand(mgr, node, g.node);
3230     this->checkReturnValue(result);
3231     return BDD(ddMgr, result);
3232
3233 } // BDD::Nand
3234
3235
3236 BDD
3237 BDD::Nor(
3238   const BDD& g) const
3239 {
3240     DdManager *mgr = this->checkSameManager(g);
3241     DdNode *result = Cudd_bddNor(mgr, node, g.node);
3242     this->checkReturnValue(result);
3243     return BDD(ddMgr, result);
3244
3245 } // BDD::Nor
3246
3247
3248 BDD
3249 BDD::Xor(
3250   const BDD& g) const
3251 {
3252     DdManager *mgr = this->checkSameManager(g);
3253     DdNode *result = Cudd_bddXor(mgr, node, g.node);
3254     this->checkReturnValue(result);
3255     return BDD(ddMgr, result);
3256
3257 } // BDD::Xor
3258
3259
3260 BDD
3261 BDD::Xnor(
3262   const BDD& g) const
3263 {
3264     DdManager *mgr = this->checkSameManager(g);
3265     DdNode *result = Cudd_bddXnor(mgr, node, g.node);
3266     this->checkReturnValue(result);
3267     return BDD(ddMgr, result);
3268
3269 } // BDD::Xnor
3270
3271
3272 int
3273 BDD::Leq(
3274   const BDD& g) const
3275 {
3276     DdManager *mgr = this->checkSameManager(g);
3277     return Cudd_bddLeq(mgr, node, g.node);
3278
3279 } // BDD::Leq
3280
3281
3282 BDD
3283 ADD::BddThreshold(
3284   CUDD_VALUE_TYPE value) const
3285 {
3286     DdManager *mgr = ddMgr->p->manager;
3287     DdNode *result = Cudd_addBddThreshold(mgr, node, value);
3288     this->checkReturnValue(result);
3289     return BDD(ddMgr, result);
3290
3291 } // ADD::BddThreshold
3292
3293
3294 BDD
3295 ADD::BddStrictThreshold(
3296   CUDD_VALUE_TYPE value) const
3297 {
3298     DdManager *mgr = ddMgr->p->manager;
3299     DdNode *result = Cudd_addBddStrictThreshold(mgr, node, value);
3300     this->checkReturnValue(result);
3301     return BDD(ddMgr, result);
3302
3303 } // ADD::BddStrictThreshold
3304
3305
3306 BDD
3307 ADD::BddInterval(
3308   CUDD_VALUE_TYPE lower,
3309   CUDD_VALUE_TYPE upper) const
3310 {
3311     DdManager *mgr = ddMgr->p->manager;
3312     DdNode *result = Cudd_addBddInterval(mgr, node, lower, upper);
3313     this->checkReturnValue(result);
3314     return BDD(ddMgr, result);
3315
3316 } // ADD::BddInterval
3317
3318
3319 BDD
3320 ADD::BddIthBit(
3321   int bit) const
3322 {
3323     DdManager *mgr = ddMgr->p->manager;
3324     DdNode *result = Cudd_addBddIthBit(mgr, node, bit);
3325     this->checkReturnValue(result);
3326     return BDD(ddMgr, result);
3327
3328 } // ADD::BddIthBit
3329
3330
3331 ADD
3332 BDD::Add() const
3333 {
3334     DdManager *mgr = ddMgr->p->manager;
3335     DdNode *result = Cudd_BddToAdd(mgr, node);
3336     this->checkReturnValue(result);
3337     return ADD(ddMgr, result);
3338
3339 } // BDD::Add
3340
3341
3342 BDD
3343 ADD::BddPattern() const
3344 {
3345     DdManager *mgr = ddMgr->p->manager;
3346     DdNode *result = Cudd_addBddPattern(mgr, node);
3347     this->checkReturnValue(result);
3348     return BDD(ddMgr, result);
3349
3350 } // ADD::BddPattern
3351
3352
3353 BDD
3354 BDD::Transfer(
3355   Cudd& destination) const
3356 {
3357     DdManager *mgr = ddMgr->p->manager;
3358     DdNode *result = Cudd_bddTransfer(mgr, destination.p->manager, node);
3359     this->checkReturnValue(result);
3360     return BDD(&destination, result);
3361
3362 } // BDD::Transfer
3363
3364
3365 void
3366 Cudd::DebugCheck()
3367 {
3368     int result = Cudd_DebugCheck(p->manager);
3369     this->checkReturnValue(result == 0);
3370
3371 } // Cudd::DebugCheck
3372
3373
3374 void
3375 Cudd::CheckKeys()
3376 {
3377     int result = Cudd_CheckKeys(p->manager);
3378     this->checkReturnValue(result == 0);
3379
3380 } // Cudd::CheckKeys
3381
3382
3383 BDD
3384 BDD::ClippingAnd(
3385   const BDD& g,
3386   int maxDepth,
3387   int direction) const
3388 {
3389     DdManager *mgr = this->checkSameManager(g);
3390     DdNode *result = Cudd_bddClippingAnd(mgr, node, g.node, maxDepth,
3391                                          direction);
3392     this->checkReturnValue(result);
3393     return BDD(ddMgr, result);
3394
3395 } // BDD::ClippingAnd
3396
3397
3398 BDD
3399 BDD::ClippingAndAbstract(
3400   const BDD& g,
3401   const BDD& cube,
3402   int maxDepth,
3403   int direction) const
3404 {
3405     DdManager *mgr = this->checkSameManager(g);
3406     this->checkSameManager(cube);
3407     DdNode *result = Cudd_bddClippingAndAbstract(mgr, node, g.node, cube.node,
3408                                                  maxDepth, direction);
3409     this->checkReturnValue(result);
3410     return BDD(ddMgr, result);
3411
3412 } // BDD::ClippingAndAbstract
3413
3414
3415 ADD
3416 ADD::Cofactor(
3417   const ADD& g) const
3418 {
3419     DdManager *mgr = this->checkSameManager(g);
3420     DdNode *result = Cudd_Cofactor(mgr, node, g.node);
3421     this->checkReturnValue(result);
3422     return ADD(ddMgr, result);
3423
3424 } // ADD::Cofactor
3425
3426
3427 BDD
3428 BDD::Cofactor(
3429   const BDD& g) const
3430 {
3431     DdManager *mgr = this->checkSameManager(g);
3432     DdNode *result = Cudd_Cofactor(mgr, node, g.node);
3433     this->checkReturnValue(result);
3434     return BDD(ddMgr, result);
3435
3436 } // BDD::Cofactor
3437
3438
3439 BDD
3440 BDD::Compose(
3441   const BDD& g,
3442   int v) const
3443 {
3444     DdManager *mgr = this->checkSameManager(g);
3445     DdNode *result = Cudd_bddCompose(mgr, node, g.node, v);
3446     this->checkReturnValue(result);
3447     return BDD(ddMgr, result);
3448
3449 } // BDD::Compose
3450
3451
3452 ADD
3453 ADD::Compose(
3454   const ADD& g,
3455   int v) const
3456 {
3457     DdManager *mgr = this->checkSameManager(g);
3458     DdNode *result = Cudd_addCompose(mgr, node, g.node, v);
3459     this->checkReturnValue(result);
3460     return ADD(ddMgr, result);
3461
3462 } // ADD::Compose
3463
3464
3465 ADD
3466 ADD::Permute(
3467   int * permut) const
3468 {
3469     DdManager *mgr = ddMgr->p->manager;
3470     DdNode *result = Cudd_addPermute(mgr, node, permut);
3471     this->checkReturnValue(result);
3472     return ADD(ddMgr, result);
3473
3474 } // ADD::Permute
3475
3476
3477 ADD
3478 ADD::SwapVariables(
3479   ADDvector x,
3480   ADDvector y) const
3481 {
3482     int n = x.count();
3483     DdManager *mgr = ddMgr->p->manager;
3484     DdNode **X = ALLOC(DdNode *,n);
3485     DdNode **Y = ALLOC(DdNode *,n);
3486     for (int i = 0; i < n; i++) {
3487         X[i] = x[i].node;
3488         Y[i] = y[i].node;
3489     }
3490     DdNode *result = Cudd_addSwapVariables(mgr, node, X, Y, n);
3491     FREE(X);
3492     FREE(Y);
3493     this->checkReturnValue(result);
3494     return ADD(ddMgr, result);
3495
3496 } // ADD::SwapVariables
3497
3498
3499 BDD
3500 BDD::Permute(
3501   int * permut) const
3502 {
3503     DdManager *mgr = ddMgr->p->manager;
3504     DdNode *result = Cudd_bddPermute(mgr, node, permut);
3505     this->checkReturnValue(result);
3506     return BDD(ddMgr, result);
3507
3508 } // BDD::Permute
3509
3510
3511 BDD
3512 BDD::SwapVariables(
3513   BDDvector x,
3514   BDDvector y) const
3515 {
3516     int n = x.count();
3517     DdManager *mgr = ddMgr->p->manager;
3518     DdNode **X = ALLOC(DdNode *,n);
3519     DdNode **Y = ALLOC(DdNode *,n);
3520     for (int i = 0; i < n; i++) {
3521         X[i] = x[i].node;
3522         Y[i] = y[i].node;
3523     }
3524     DdNode *result = Cudd_bddSwapVariables(mgr, node, X, Y, n);
3525     FREE(X);
3526     FREE(Y);
3527     this->checkReturnValue(result);
3528     return BDD(ddMgr, result);
3529
3530 } // BDD::SwapVariables
3531
3532
3533 BDD
3534 BDD::AdjPermuteX(
3535   BDDvector x) const
3536 {
3537     int n = x.count();
3538     DdManager *mgr = ddMgr->p->manager;
3539     DdNode **X = ALLOC(DdNode *,n);
3540     for (int i = 0; i < n; i++) {
3541         X[i] = x[i].node;
3542     }
3543     DdNode *result = Cudd_bddAdjPermuteX(mgr, node, X, n);
3544     FREE(X);
3545     this->checkReturnValue(result);
3546     return BDD(ddMgr, result);
3547
3548 } // BDD::AdjPermuteX
3549
3550
3551 ADD
3552 ADD::VectorCompose(
3553   ADDvector vector) const
3554 {
3555     DdManager *mgr = ddMgr->p->manager;
3556     int n = Cudd_ReadSize(mgr);
3557     DdNode **X = ALLOC(DdNode *,n);
3558     for (int i = 0; i < n; i++) {
3559         X[i] = vector[i].node;
3560     }
3561     DdNode *result = Cudd_addVectorCompose(mgr, node, X);
3562     FREE(X);
3563     this->checkReturnValue(result);
3564     return ADD(ddMgr, result);
3565
3566 } // ADD::VectorCompose
3567
3568
3569 ADD
3570 ADD::NonSimCompose(
3571   ADDvector vector) const
3572 {
3573     DdManager *mgr = ddMgr->p->manager;
3574     int n = Cudd_ReadSize(mgr);
3575     DdNode **X = ALLOC(DdNode *,n);
3576     for (int i = 0; i < n; i++) {
3577         X[i] = vector[i].node;
3578     }
3579     DdNode *result = Cudd_addNonSimCompose(mgr, node, X);
3580     FREE(X);
3581     this->checkReturnValue(result);
3582     return ADD(ddMgr, result);
3583
3584 } // ADD::NonSimCompose
3585
3586
3587 BDD
3588 BDD::VectorCompose(
3589   BDDvector vector) const
3590 {
3591     DdManager *mgr = ddMgr->p->manager;
3592     int n = Cudd_ReadSize(mgr);
3593     DdNode **X = ALLOC(DdNode *,n);
3594     for (int i = 0; i < n; i++) {
3595         X[i] = vector[i].node;
3596     }
3597     DdNode *result = Cudd_bddVectorCompose(mgr, node, X);
3598     FREE(X);
3599     this->checkReturnValue(result);
3600     return BDD(ddMgr, result);
3601
3602 } // BDD::VectorCompose
3603
3604
3605 void
3606 BDD::ApproxConjDecomp(
3607   BDD* g,
3608   BDD* h) const
3609 {
3610     DdManager *mgr = ddMgr->p->manager;
3611     DdNode **pieces;
3612     int result = Cudd_bddApproxConjDecomp(mgr, node, &pieces);
3613     this->checkReturnValue(result == 2);
3614     *g = BDD(ddMgr, pieces[0]);
3615     *h = BDD(ddMgr, pieces[1]);
3616     Cudd_RecursiveDeref(mgr,pieces[0]);
3617     Cudd_RecursiveDeref(mgr,pieces[1]);
3618     FREE(pieces);
3619
3620 } // BDD::ApproxConjDecomp
3621
3622
3623 void
3624 BDD::ApproxDisjDecomp(
3625   BDD* g,
3626   BDD* h) const
3627 {
3628     DdManager *mgr = ddMgr->p->manager;
3629     DdNode **pieces;
3630     int result = Cudd_bddApproxDisjDecomp(mgr, node, &pieces);
3631     this->checkReturnValue(result == 2);
3632     *g = BDD(ddMgr, pieces[0]);
3633     *h = BDD(ddMgr, pieces[1]);
3634     Cudd_RecursiveDeref(mgr,pieces[0]);
3635     Cudd_RecursiveDeref(mgr,pieces[1]);
3636     FREE(pieces);
3637
3638 } // BDD::ApproxDisjDecomp
3639
3640
3641 void
3642 BDD::IterConjDecomp(
3643   BDD* g,
3644   BDD* h) const
3645 {
3646     DdManager *mgr = ddMgr->p->manager;
3647     DdNode **pieces;
3648     int result = Cudd_bddIterConjDecomp(mgr, node, &pieces);
3649     this->checkReturnValue(result == 2);
3650     *g = BDD(ddMgr, pieces[0]);
3651     *h = BDD(ddMgr, pieces[1]);
3652     Cudd_RecursiveDeref(mgr,pieces[0]);
3653     Cudd_RecursiveDeref(mgr,pieces[1]);
3654     FREE(pieces);
3655
3656 } // BDD::IterConjDecomp
3657
3658
3659 void
3660 BDD::IterDisjDecomp(
3661   BDD* g,
3662   BDD* h) const
3663 {
3664     DdManager *mgr = ddMgr->p->manager;
3665     DdNode **pieces;
3666     int result = Cudd_bddIterDisjDecomp(mgr, node, &pieces);
3667     this->checkReturnValue(result == 2);
3668     *g = BDD(ddMgr, pieces[0]);
3669     *h = BDD(ddMgr, pieces[1]);
3670     Cudd_RecursiveDeref(mgr,pieces[0]);
3671     Cudd_RecursiveDeref(mgr,pieces[1]);
3672     FREE(pieces);
3673
3674 } // BDD::IterDisjDecomp
3675
3676
3677 void
3678 BDD::GenConjDecomp(
3679   BDD* g,
3680   BDD* h) const
3681 {
3682     DdManager *mgr = ddMgr->p->manager;
3683     DdNode **pieces;
3684     int result = Cudd_bddGenConjDecomp(mgr, node, &pieces);
3685     this->checkReturnValue(result == 2);
3686     *g = BDD(ddMgr, pieces[0]);
3687     *h = BDD(ddMgr, pieces[1]);
3688     Cudd_RecursiveDeref(mgr,pieces[0]);
3689     Cudd_RecursiveDeref(mgr,pieces[1]);
3690     FREE(pieces);
3691
3692 } // BDD::GenConjDecomp
3693
3694
3695 void
3696 BDD::GenDisjDecomp(
3697   BDD* g,
3698   BDD* h) const
3699 {
3700     DdManager *mgr = ddMgr->p->manager;
3701     DdNode **pieces;
3702     int result = Cudd_bddGenDisjDecomp(mgr, node, &pieces);
3703     this->checkReturnValue(result == 2);
3704     *g = BDD(ddMgr, pieces[0]);
3705     *h = BDD(ddMgr, pieces[1]);
3706     Cudd_RecursiveDeref(mgr,pieces[0]);
3707     Cudd_RecursiveDeref(mgr,pieces[1]);
3708     FREE(pieces);
3709
3710 } // BDD::GenDisjDecomp
3711
3712
3713 void
3714 BDD::VarConjDecomp(
3715   BDD* g,
3716   BDD* h) const
3717 {
3718     DdManager *mgr = ddMgr->p->manager;
3719     DdNode **pieces;
3720     int result = Cudd_bddVarConjDecomp(mgr, node, &pieces);
3721     this->checkReturnValue(result == 2);
3722     *g = BDD(ddMgr, pieces[0]);
3723     *h = BDD(ddMgr, pieces[1]);
3724     Cudd_RecursiveDeref(mgr,pieces[0]);
3725     Cudd_RecursiveDeref(mgr,pieces[1]);
3726     FREE(pieces);
3727
3728 } // BDD::VarConjDecomp
3729
3730
3731 void
3732 BDD::VarDisjDecomp(
3733   BDD* g,
3734   BDD* h) const
3735 {
3736     DdManager *mgr = ddMgr->p->manager;
3737     DdNode **pieces;
3738     int result = Cudd_bddVarDisjDecomp(mgr, node, &pieces);
3739     this->checkReturnValue(result == 2);
3740     *g = BDD(ddMgr, pieces[0]);
3741     *h = BDD(ddMgr, pieces[1]);
3742     Cudd_RecursiveDeref(mgr,pieces[0]);
3743     Cudd_RecursiveDeref(mgr,pieces[1]);
3744     FREE(pieces);
3745
3746 } // BDD::VarDisjDecomp
3747
3748
3749 BDD
3750 ABDD::FindEssential() const
3751 {
3752     DdManager *mgr = ddMgr->p->manager;
3753     DdNode *result = Cudd_FindEssential(mgr, node);
3754     this->checkReturnValue(result);
3755     return BDD(ddMgr, result);
3756
3757 } // ABDD::FindEssential
3758
3759
3760 int
3761 BDD::IsVarEssential(
3762   int id,
3763   int phase) const
3764 {
3765     DdManager *mgr = ddMgr->p->manager;
3766     return Cudd_bddIsVarEssential(mgr, node, id, phase);
3767
3768 } // BDD::IsVarEssential
3769
3770
3771 void
3772 ABDD::PrintTwoLiteralClauses(
3773   char **names,
3774   FILE *fp) const
3775 {
3776     DdManager *mgr = ddMgr->p->manager;
3777     int result = Cudd_PrintTwoLiteralClauses(mgr, node, names, fp);
3778     this->checkReturnValue(result);
3779
3780 } // ABDD::PrintTwoLiteralClauses
3781
3782
3783 void
3784 BDDvector::DumpBlif(
3785   char ** inames,
3786   char ** onames,
3787   char * mname,
3788   FILE * fp,
3789   int mv) const
3790 {
3791     DdManager *mgr = p->manager->getManager();
3792     int n = p->size;
3793     DdNode **F = ALLOC(DdNode *,n);
3794     for (int i = 0; i < n; i ++) {
3795         F[i] = p->vect[i].getNode();
3796     }
3797     int result = Cudd_DumpBlif(mgr, n, F, inames, onames, mname, fp, mv);
3798     FREE(F);
3799     p->manager->checkReturnValue(result);
3800
3801 } // BDDvector::DumpBlif
3802
3803
3804 void
3805 BDDvector::DumpDot(
3806   char ** inames,
3807   char ** onames,
3808   FILE * fp) const
3809 {
3810     DdManager *mgr = p->manager->getManager();
3811     int n = p->size;
3812     DdNode **F = ALLOC(DdNode *,n);
3813     for (int i = 0; i < n; i ++) {
3814         F[i] = p->vect[i].getNode();
3815     }
3816     int result = Cudd_DumpDot(mgr, n, F, inames, onames, fp);
3817     FREE(F);
3818     p->manager->checkReturnValue(result);
3819
3820 } // BDDvector::DumpDot
3821
3822
3823 void
3824 ADDvector::DumpDot(
3825   char ** inames,
3826   char ** onames,
3827   FILE * fp) const
3828 {
3829     DdManager *mgr = p->manager->getManager();
3830     int n = p->size;
3831     DdNode **F = ALLOC(DdNode *,n);
3832     for (int i = 0; i < n; i ++) {
3833         F[i] = p->vect[i].getNode();
3834     }
3835     int result = Cudd_DumpDot(mgr, n, F, inames, onames, fp);
3836     FREE(F);
3837     p->manager->checkReturnValue(result);
3838
3839 } // ADDvector::DumpDot
3840
3841
3842 void
3843 BDDvector::DumpDaVinci(
3844   char ** inames,
3845   char ** onames,
3846   FILE * fp) const
3847 {
3848     DdManager *mgr = p->manager->getManager();
3849     int n = p->size;
3850     DdNode **F = ALLOC(DdNode *,n);
3851     for (int i = 0; i < n; i ++) {
3852         F[i] = p->vect[i].getNode();
3853     }
3854     int result = Cudd_DumpDaVinci(mgr, n, F, inames, onames, fp);
3855     FREE(F);
3856     p->manager->checkReturnValue(result);
3857
3858 } // BDDvector::DumpDaVinci
3859
3860
3861 void
3862 ADDvector::DumpDaVinci(
3863   char ** inames,
3864   char ** onames,
3865   FILE * fp) const
3866 {
3867     DdManager *mgr = p->manager->getManager();
3868     int n = p->size;
3869     DdNode **F = ALLOC(DdNode *,n);
3870     for (int i = 0; i < n; i ++) {
3871         F[i] = p->vect[i].getNode();
3872     }
3873     int result = Cudd_DumpDaVinci(mgr, n, F, inames, onames, fp);
3874     FREE(F);
3875     p->manager->checkReturnValue(result);
3876
3877 } // ADDvector::DumpDaVinci
3878
3879
3880 void
3881 BDDvector::DumpDDcal(
3882   char ** inames,
3883   char ** onames,
3884   FILE * fp) const
3885 {
3886     DdManager *mgr = p->manager->getManager();
3887     int n = p->size;
3888     DdNode **F = ALLOC(DdNode *,n);
3889     for (int i = 0; i < n; i ++) {
3890         F[i] = p->vect[i].getNode();
3891     }
3892     int result = Cudd_DumpDDcal(mgr, n, F, inames, onames, fp);
3893     FREE(F);
3894     p->manager->checkReturnValue(result);
3895
3896 } // BDDvector::DumpDDcal
3897
3898
3899 void
3900 BDDvector::DumpFactoredForm(
3901   char ** inames,
3902   char ** onames,
3903   FILE * fp) const
3904 {
3905     DdManager *mgr = p->manager->getManager();
3906     int n = p->size;
3907     DdNode **F = ALLOC(DdNode *,n);
3908     for (int i = 0; i < n; i ++) {
3909         F[i] = p->vect[i].getNode();
3910     }
3911     int result = Cudd_DumpFactoredForm(mgr, n, F, inames, onames, fp);
3912     FREE(F);
3913     p->manager->checkReturnValue(result);
3914
3915 } // BDDvector::DumpFactoredForm
3916
3917
3918 BDD
3919 BDD::Constrain(
3920   const BDD& c) const
3921 {
3922     DdManager *mgr = this->checkSameManager(c);
3923     DdNode *result = Cudd_bddConstrain(mgr, node, c.node);
3924     this->checkReturnValue(result);
3925     return BDD(ddMgr, result);
3926
3927 } // BDD::Constrain
3928
3929
3930 BDD
3931 BDD::Restrict(
3932   const BDD& c) const
3933 {
3934     DdManager *mgr = this->checkSameManager(c);
3935     DdNode *result = Cudd_bddRestrict(mgr, node, c.node);
3936     this->checkReturnValue(result);
3937     return BDD(ddMgr, result);
3938
3939 } // BDD::Restrict
3940
3941
3942 BDD
3943 BDD::NPAnd(
3944   const BDD& g) const
3945 {
3946     DdManager *mgr = this->checkSameManager(g);
3947     DdNode *result = Cudd_bddNPAnd(mgr, node, g.node);
3948     this->checkReturnValue(result);
3949     return BDD(ddMgr, result);
3950
3951 } // BDD::NPAnd
3952
3953
3954 ADD
3955 ADD::Constrain(
3956   const ADD& c) const
3957 {
3958     DdManager *mgr = this->checkSameManager(c);
3959     DdNode *result = Cudd_addConstrain(mgr, node, c.node);
3960     this->checkReturnValue(result);
3961     return ADD(ddMgr, result);
3962
3963 } // ADD::Constrain
3964
3965
3966 BDDvector
3967 BDD::ConstrainDecomp() const
3968 {
3969     DdManager *mgr = ddMgr->p->manager;
3970     DdNode **result = Cudd_bddConstrainDecomp(mgr, node);
3971     this->checkReturnValue((DdNode *)result);
3972     int size = Cudd_ReadSize(mgr);
3973     for (int i = 0; i < size; i++) {
3974         Cudd_Deref(result[i]);
3975     }
3976     BDDvector vect(size, ddMgr, result);
3977     FREE(result);
3978     return vect;
3979
3980 } // BDD::ConstrainDecomp
3981
3982
3983 ADD
3984 ADD::Restrict(
3985   const ADD& c) const
3986 {
3987     DdManager *mgr = this->checkSameManager(c);
3988     DdNode *result = Cudd_addRestrict(mgr, node, c.node);
3989     this->checkReturnValue(result);
3990     return ADD(ddMgr, result);
3991
3992 } // ADD::Restrict
3993
3994
3995 BDDvector
3996 BDD::CharToVect() const
3997 {
3998     DdManager *mgr = ddMgr->p->manager;
3999     DdNode **result = Cudd_bddCharToVect(mgr, node);
4000     this->checkReturnValue((DdNode *)result);
4001     int size = Cudd_ReadSize(mgr);
4002     for (int i = 0; i < size; i++) {
4003         Cudd_Deref(result[i]);
4004     }
4005     BDDvector vect(size, ddMgr, result);
4006     FREE(result);
4007     return vect;
4008
4009 } // BDD::CharToVect
4010
4011
4012 BDD
4013 BDD::LICompaction(
4014   const BDD& c) const
4015 {
4016     DdManager *mgr = this->checkSameManager(c);
4017     DdNode *result = Cudd_bddLICompaction(mgr, node, c.node);
4018     this->checkReturnValue(result);
4019     return BDD(ddMgr, result);
4020
4021 } // BDD::LICompaction
4022
4023
4024 BDD
4025 BDD::Squeeze(
4026   const BDD& u) const
4027 {
4028     DdManager *mgr = this->checkSameManager(u);
4029     DdNode *result = Cudd_bddSqueeze(mgr, node, u.node);
4030     this->checkReturnValue(result);
4031     return BDD(ddMgr, result);
4032
4033 } // BDD::Squeeze
4034
4035
4036 BDD
4037 BDD::Minimize(
4038   const BDD& c) const
4039 {
4040     DdManager *mgr = this->checkSameManager(c);
4041     DdNode *result = Cudd_bddMinimize(mgr, node, c.node);
4042     this->checkReturnValue(result);
4043     return BDD(ddMgr, result);
4044
4045 } // BDD::Minimize
4046
4047
4048 BDD
4049 BDD::SubsetCompress(
4050   int nvars,
4051   int threshold) const
4052 {
4053     DdManager *mgr = ddMgr->p->manager;
4054     DdNode *result = Cudd_SubsetCompress(mgr, node, nvars, threshold);
4055     this->checkReturnValue(result);
4056     return BDD(ddMgr, result);
4057
4058 } // BDD::SubsetCompress
4059
4060
4061 BDD
4062 BDD::SupersetCompress(
4063   int nvars,
4064   int threshold) const
4065 {
4066     DdManager *mgr = ddMgr->p->manager;
4067     DdNode *result = Cudd_SupersetCompress(mgr, node, nvars, threshold);
4068     this->checkReturnValue(result);
4069     return BDD(ddMgr, result);
4070
4071 } // BDD::SupersetCompress
4072
4073
4074 MtrNode *
4075 Cudd::MakeTreeNode(
4076   unsigned int low,
4077   unsigned int size,
4078   unsigned int type)
4079 {
4080     return Cudd_MakeTreeNode(p->manager, low, size, type);
4081
4082 } // Cudd::MakeTreeNode
4083
4084
4085 /* This is incorrect, but we'll wait for this one.
4086 void
4087 Cudd::Harwell(
4088   FILE * fp,
4089   DdManager * dd,
4090   ADD* E,
4091   ADD** x,
4092   ADD** y,
4093   ADD** xn,
4094   ADD** yn_,
4095   int * nx,
4096   int * ny,
4097   int * m,
4098   int * n,
4099   int bx,
4100   int sx,
4101   int by,
4102   int sy,
4103   int pr)
4104 {
4105     DdManager *mgr = p->manager;
4106     int result = Cudd_addHarwell(fp, mgr, E, x, y, xn, yn_, nx, ny, m, n, bx, sx, by, sy, pr);
4107     this->checkReturnValue(result);
4108
4109 } // Cudd::Harwell
4110 */
4111
4112
4113 void
4114 Cudd::PrintLinear()
4115 {
4116     cout.flush();
4117     int result = Cudd_PrintLinear(p->manager);
4118     this->checkReturnValue(result);
4119
4120 } // Cudd::PrintLinear
4121
4122
4123 int
4124 Cudd::ReadLinear(
4125   int x,
4126   int y)
4127 {
4128     return Cudd_ReadLinear(p->manager, x, y);
4129
4130 } // Cudd::ReadLinear
4131
4132
4133 BDD
4134 BDD::LiteralSetIntersection(
4135   const BDD& g) const
4136 {
4137     DdManager *mgr = this->checkSameManager(g);
4138     DdNode *result = Cudd_bddLiteralSetIntersection(mgr, node, g.node);
4139     this->checkReturnValue(result);
4140     return BDD(ddMgr, result);
4141
4142 } // BDD::LiteralSetIntersection
4143
4144
4145 ADD
4146 ADD::MatrixMultiply(
4147   const ADD& B,
4148   ADDvector z) const
4149 {
4150     int nz = z.count();
4151     DdManager *mgr = this->checkSameManager(B);
4152     DdNode **Z = ALLOC(DdNode *,nz);
4153     for (int i = 0; i < nz; i++) {
4154         Z[i] = z[i].node;
4155     }
4156     DdNode *result = Cudd_addMatrixMultiply(mgr, node, B.node, Z, nz);
4157     FREE(Z);
4158     this->checkReturnValue(result);
4159     return ADD(ddMgr, result);
4160
4161 } // ADD::MatrixMultiply
4162
4163
4164 ADD
4165 ADD::TimesPlus(
4166   const ADD& B,
4167   ADDvector z) const
4168 {
4169     int nz = z.count();
4170     DdManager *mgr = this->checkSameManager(B);
4171     DdNode **Z = ALLOC(DdNode *,nz);
4172     for (int i = 0; i < nz; i++) {
4173         Z[i] = z[i].node;
4174     }
4175     DdNode *result = Cudd_addTimesPlus(mgr, node, B.node, Z, nz);
4176     FREE(Z);
4177     this->checkReturnValue(result);
4178     return ADD(ddMgr, result);
4179
4180 } // ADD::TimesPlus
4181
4182
4183 ADD
4184 ADD::Triangle(
4185   const ADD& g,
4186   ADDvector z) const
4187 {
4188     int nz = z.count();
4189     DdManager *mgr = this->checkSameManager(g);
4190     DdNode **Z = ALLOC(DdNode *,nz);
4191     for (int i = 0; i < nz; i++) {
4192         Z[i] = z[i].node;
4193     }
4194     DdNode *result = Cudd_addTriangle(mgr, node, g.node, Z, nz);
4195     FREE(Z);
4196     this->checkReturnValue(result);
4197     return ADD(ddMgr, result);
4198
4199 } // ADD::Triangle
4200
4201
4202 BDD
4203 BDD::PrioritySelect(
4204   BDDvector x,
4205   BDDvector y,
4206   BDDvector z,
4207   const BDD& Pi,
4208   DD_PRFP Pifunc) const
4209 {
4210     int n = x.count();
4211     DdManager *mgr = ddMgr->p->manager;
4212     DdNode **X = ALLOC(DdNode *,n);
4213     DdNode **Y = ALLOC(DdNode *,n);
4214     DdNode **Z = ALLOC(DdNode *,n);
4215     for (int i = 0; i < n; i++) {
4216         X[i] = x[i].node;
4217         Y[i] = y[i].node;
4218         Z[i] = z[i].node;
4219     }
4220     DdNode *result = Cudd_PrioritySelect(mgr, node, X, Y, Z, Pi.node, n, Pifunc);
4221     FREE(X);
4222     FREE(Y);
4223     FREE(Z);
4224     this->checkReturnValue(result);
4225     return BDD(ddMgr, result);
4226
4227 } // BDD::PrioritySelect
4228
4229
4230 BDD
4231 Cudd::Xgty(
4232   BDDvector z,
4233   BDDvector x,
4234   BDDvector y)
4235 {
4236     int N = z.count();
4237     DdManager *mgr = p->manager;
4238     DdNode **X = ALLOC(DdNode *,N);
4239     DdNode **Y = ALLOC(DdNode *,N);
4240     DdNode **Z = ALLOC(DdNode *,N);
4241     for (int i = 0; i < N; i++) {
4242         X[i] = x[i].getNode();
4243         Y[i] = y[i].getNode();
4244         Z[i] = z[i].getNode();
4245     }
4246     DdNode *result = Cudd_Xgty(mgr, N, Z, X, Y);
4247     FREE(X);
4248     FREE(Y);
4249     FREE(Z);
4250     this->checkReturnValue(result);
4251     return BDD(this, result);
4252
4253 } // Cudd::Xgty
4254
4255
4256 BDD
4257 Cudd::Xeqy(
4258   BDDvector x,
4259   BDDvector y)
4260 {
4261     int N = x.count();
4262     DdManager *mgr = p->manager;
4263     DdNode **X = ALLOC(DdNode *,N);
4264     DdNode **Y = ALLOC(DdNode *,N);
4265     for (int i = 0; i < N; i++) {
4266         X[i] = x[i].getNode();
4267         Y[i] = y[i].getNode();
4268     }
4269     DdNode *result = Cudd_Xeqy(mgr, N, X, Y);
4270     FREE(X);
4271     FREE(Y);
4272     this->checkReturnValue(result);
4273     return BDD(this, result);
4274
4275 } // BDD::Xeqy
4276
4277
4278 ADD
4279 Cudd::Xeqy(
4280   ADDvector x,
4281   ADDvector y)
4282 {
4283     int N = x.count();
4284     DdManager *mgr = p->manager;
4285     DdNode **X = ALLOC(DdNode *,N);
4286     DdNode **Y = ALLOC(DdNode *,N);
4287     for (int i = 0; i < N; i++) {
4288         X[i] = x[i].getNode();
4289         Y[i] = y[i].getNode();
4290     }
4291     DdNode *result = Cudd_addXeqy(mgr, N, X, X);
4292     FREE(X);
4293     FREE(Y);
4294     this->checkReturnValue(result);
4295     return ADD(this, result);
4296
4297 } // ADD::Xeqy
4298
4299
4300 BDD
4301 Cudd::Dxygtdxz(
4302   BDDvector x,
4303   BDDvector y,
4304   BDDvector z)
4305 {
4306     int N = x.count();
4307     DdManager *mgr = p->manager;
4308     DdNode **X = ALLOC(DdNode *,N);
4309     DdNode **Y = ALLOC(DdNode *,N);
4310     DdNode **Z = ALLOC(DdNode *,N);
4311     for (int i = 0; i < N; i++) {
4312         X[i] = x[i].getNode();
4313         Y[i] = y[i].getNode();
4314         Z[i] = z[i].getNode();
4315     }
4316     DdNode *result = Cudd_Dxygtdxz(mgr, N, X, Y, Z);
4317     FREE(X);
4318     FREE(Y);
4319     FREE(Z);
4320     this->checkReturnValue(result);
4321     return BDD(this, result);
4322
4323 } // Cudd::Dxygtdxz
4324
4325
4326 BDD
4327 Cudd::Dxygtdyz(
4328   BDDvector x,
4329   BDDvector y,
4330   BDDvector z)
4331 {
4332     int N = x.count();
4333     DdManager *mgr = p->manager;
4334     DdNode **X = ALLOC(DdNode *,N);
4335     DdNode **Y = ALLOC(DdNode *,N);
4336     DdNode **Z = ALLOC(DdNode *,N);
4337     for (int i = 0; i < N; i++) {
4338         X[i] = x[i].getNode();
4339         Y[i] = y[i].getNode();
4340         Z[i] = z[i].getNode();
4341     }
4342     DdNode *result = Cudd_Dxygtdyz(mgr, N, X, Y, Z);
4343     FREE(X);
4344     FREE(Y);
4345     FREE(Z);
4346     this->checkReturnValue(result);
4347     return BDD(this, result);
4348
4349 } // Cudd::Dxygtdyz
4350
4351
4352 BDD
4353 Cudd::Inequality(
4354   int c,
4355   BDDvector x,
4356   BDDvector y)
4357 {
4358     int N = x.count();
4359     DdManager *mgr = p->manager;
4360     DdNode **X = ALLOC(DdNode *,N);
4361     DdNode **Y = ALLOC(DdNode *,N);
4362     for (int i = 0; i < N; i++) {
4363         X[i] = x[i].getNode();
4364         Y[i] = y[i].getNode();
4365     }
4366     DdNode *result = Cudd_Inequality(mgr, N, c, X, Y);
4367     FREE(X);
4368     FREE(Y);
4369     this->checkReturnValue(result);
4370     return BDD(this, result);
4371
4372 } // Cudd::Inequality
4373
4374
4375 BDD
4376 Cudd::Disequality(
4377   int c,
4378   BDDvector x,
4379   BDDvector y)
4380 {
4381     int N = x.count();
4382     DdManager *mgr = p->manager;
4383     DdNode **X = ALLOC(DdNode *,N);
4384     DdNode **Y = ALLOC(DdNode *,N);
4385     for (int i = 0; i < N; i++) {
4386         X[i] = x[i].getNode();
4387         Y[i] = y[i].getNode();
4388     }
4389     DdNode *result = Cudd_Disequality(mgr, N, c, X, Y);
4390     FREE(X);
4391     FREE(Y);
4392     this->checkReturnValue(result);
4393     return BDD(this, result);
4394
4395 } // Cudd::Disequality
4396
4397
4398 BDD
4399 Cudd::Interval(
4400   BDDvector x,
4401   unsigned int lowerB,
4402   unsigned int upperB)
4403 {
4404     int N = x.count();
4405     DdManager *mgr = p->manager;
4406     DdNode **X = ALLOC(DdNode *,N);
4407     for (int i = 0; i < N; i++) {
4408         X[i] = x[i].getNode();
4409     }
4410     DdNode *result = Cudd_bddInterval(mgr, N, X, lowerB, upperB);
4411     FREE(X);
4412     this->checkReturnValue(result);
4413     return BDD(this, result);
4414
4415 } // Cudd::Interval
4416
4417
4418 BDD
4419 BDD::CProjection(
4420   const BDD& Y) const
4421 {
4422     DdManager *mgr = this->checkSameManager(Y);
4423     DdNode *result = Cudd_CProjection(mgr, node, Y.node);
4424     this->checkReturnValue(result);
4425     return BDD(ddMgr, result);
4426
4427 } // BDD::CProjection
4428
4429
4430 int
4431 BDD::MinHammingDist(
4432   int *minterm,
4433   int upperBound) const
4434 {
4435     DdManager *mgr = ddMgr->p->manager;
4436     int result = Cudd_MinHammingDist(mgr, node, minterm, upperBound);
4437     return result;
4438
4439 } // BDD::MinHammingDist
4440
4441
4442 ADD
4443 Cudd::Hamming(
4444   ADDvector xVars,
4445   ADDvector yVars)
4446 {
4447     int nVars = xVars.count();
4448     DdManager *mgr = p->manager;
4449     DdNode **X = ALLOC(DdNode *,nVars);
4450     DdNode **Y = ALLOC(DdNode *,nVars);
4451     for (int i = 0; i < nVars; i++) {
4452         X[i] = xVars[i].getNode();
4453         Y[i] = yVars[i].getNode();
4454     }
4455     DdNode *result = Cudd_addHamming(mgr, X, Y, nVars);
4456     FREE(X);
4457     FREE(Y);
4458     this->checkReturnValue(result);
4459     return ADD(this, result);
4460
4461 } // Cudd::Hamming
4462
4463
4464 /* We'll leave these two out for the time being.
4465 void
4466 Cudd::Read(
4467   FILE * fp,
4468   ADD* E,
4469   ADD** x,
4470   ADD** y,
4471   ADD** xn,
4472   ADD** yn_,
4473   int * nx,
4474   int * ny,
4475   int * m,
4476   int * n,
4477   int bx,
4478   int sx,
4479   int by,
4480   int sy)
4481 {
4482     DdManager *mgr = p->manager;
4483     int result = Cudd_addRead(fp, mgr, E, x, y, xn, yn_, nx, ny, m, n, bx, sx, by, sy);
4484     this->checkReturnValue(result);
4485
4486 } // Cudd::Read
4487
4488
4489 void
4490 Cudd::Read(
4491   FILE * fp,
4492   BDD* E,
4493   BDD** x,
4494   BDD** y,
4495   int * nx,
4496   int * ny,
4497   int * m,
4498   int * n,
4499   int bx,
4500   int sx,
4501   int by,
4502   int sy)
4503 {
4504     DdManager *mgr = p->manager;
4505     int result = Cudd_bddRead(fp, mgr, E, x, y, nx, ny, m, n, bx, sx, by, sy);
4506     this->checkReturnValue(result);
4507
4508 } // Cudd::Read
4509 */
4510
4511
4512 void
4513 Cudd::ReduceHeap(
4514   Cudd_ReorderingType heuristic,
4515   int minsize)
4516 {
4517     int result = Cudd_ReduceHeap(p->manager, heuristic, minsize);
4518     this->checkReturnValue(result);
4519
4520 } // Cudd::ReduceHeap
4521
4522
4523 void
4524 Cudd::ShuffleHeap(
4525   int * permutation)
4526 {
4527     int result = Cudd_ShuffleHeap(p->manager, permutation);
4528     this->checkReturnValue(result);
4529
4530 } // Cudd::ShuffleHeap
4531
4532
4533 ADD
4534 ADD::Eval(
4535   int * inputs) const
4536 {
4537     DdManager *mgr = ddMgr->p->manager;
4538     DdNode *result = Cudd_Eval(mgr, node, inputs);
4539     this->checkReturnValue(result);
4540     return ADD(ddMgr, result);
4541
4542 } // ADD::Eval
4543
4544
4545 BDD
4546 BDD::Eval(
4547   int * inputs) const
4548 {
4549     DdManager *mgr = ddMgr->p->manager;
4550     DdNode *result = Cudd_Eval(mgr, node, inputs);
4551     this->checkReturnValue(result);
4552     return BDD(ddMgr, result);
4553
4554 } // BDD::Eval
4555
4556
4557 BDD
4558 ABDD::ShortestPath(
4559   int * weight,
4560   int * support,
4561   int * length) const
4562 {
4563     DdManager *mgr = ddMgr->p->manager;
4564     DdNode *result = Cudd_ShortestPath(mgr, node, weight, support, length);
4565     this->checkReturnValue(result);
4566     return BDD(ddMgr, result);
4567
4568 } // ABDD::ShortestPath
4569
4570
4571 BDD
4572 ABDD::LargestCube(
4573   int * length) const
4574 {
4575     DdManager *mgr = ddMgr->p->manager;
4576     DdNode *result = Cudd_LargestCube(mgr, node, length);
4577     this->checkReturnValue(result);
4578     return BDD(ddMgr, result);
4579
4580 } // ABDD::LargestCube
4581
4582
4583 int
4584 ABDD::ShortestLength(
4585   int * weight) const
4586 {
4587     DdManager *mgr = ddMgr->p->manager;
4588     int result = Cudd_ShortestLength(mgr, node, weight);
4589     this->checkReturnValue(result != CUDD_OUT_OF_MEM);
4590     return result;
4591
4592 } // ABDD::ShortestLength
4593
4594
4595 BDD
4596 BDD::Decreasing(
4597   int i) const
4598 {
4599     DdManager *mgr = ddMgr->p->manager;
4600     DdNode *result = Cudd_Decreasing(mgr, node, i);
4601     this->checkReturnValue(result);
4602     return BDD(ddMgr, result);
4603
4604 } // BDD::Decreasing
4605
4606
4607 BDD
4608 BDD::Increasing(
4609   int i) const
4610 {
4611     DdManager *mgr = ddMgr->p->manager;
4612     DdNode *result = Cudd_Increasing(mgr, node, i);
4613     this->checkReturnValue(result);
4614     return BDD(ddMgr, result);
4615
4616 } // BDD::Increasing
4617
4618
4619 int
4620 ABDD::EquivDC(
4621   const ABDD& G,
4622   const ABDD& D) const
4623 {
4624     DdManager *mgr = this->checkSameManager(G);
4625     this->checkSameManager(D);
4626     return Cudd_EquivDC(mgr, node, G.node, D.node);
4627
4628 } // ABDD::EquivDC
4629
4630
4631 int
4632 ADD::EqualSupNorm(
4633   const ADD& g,
4634   CUDD_VALUE_TYPE tolerance,
4635   int pr) const
4636 {
4637     DdManager *mgr = this->checkSameManager(g);
4638     return Cudd_EqualSupNorm(mgr, node, g.node, tolerance, pr);
4639
4640 } // ADD::EqualSupNorm
4641
4642
4643 double *
4644 ABDD::CofMinterm() const
4645 {
4646     DdManager *mgr = ddMgr->p->manager;
4647     double *result = Cudd_CofMinterm(mgr, node);
4648     this->checkReturnValue((DdNode *)result);
4649     return result;
4650
4651 } // ABDD::CofMinterm
4652
4653
4654 BDD
4655 BDD::SolveEqn(
4656   const BDD& Y,
4657   BDD* G,
4658   int ** yIndex,
4659   int n) const
4660 {
4661     DdManager *mgr = this->checkSameManager(Y);
4662     DdNode **g = ALLOC(DdNode *,n);
4663     DdNode *result = Cudd_SolveEqn(mgr, node, Y.node, g, yIndex, n);
4664     this->checkReturnValue(result);
4665     for (int i = 0; i < n; i++) {
4666         G[i] = BDD(ddMgr, g[i]);
4667         Cudd_RecursiveDeref(mgr,g[i]);
4668     }
4669     FREE(g);
4670     return BDD(ddMgr, result);
4671
4672 } // BDD::SolveEqn
4673
4674
4675 BDD
4676 BDD::VerifySol(
4677   BDD* G,
4678   int * yIndex,
4679   int n) const
4680 {
4681     DdManager *mgr = ddMgr->p->manager;
4682     DdNode **g = ALLOC(DdNode *,n);
4683     for (int i = 0; i < n; i++) {
4684         g[i] = G[i].node;
4685     }
4686     DdNode *result = Cudd_VerifySol(mgr, node, g, yIndex, n);
4687     FREE(g);
4688     this->checkReturnValue(result);
4689     return BDD(ddMgr, result);
4690
4691 } // BDD::VerifySol
4692
4693
4694 BDD
4695 BDD::SplitSet(
4696   BDDvector xVars,
4697   double m) const
4698 {
4699     int n = xVars.count();
4700     DdManager *mgr = ddMgr->p->manager;
4701     DdNode **X = ALLOC(DdNode *,n);
4702     for (int i = 0; i < n; i++) {
4703         X[i] = xVars[i].node;
4704     }
4705     DdNode *result = Cudd_SplitSet(mgr, node, X, n, m);
4706     FREE(X);
4707     this->checkReturnValue(result);
4708     return BDD(ddMgr, result);
4709
4710 } // BDD::SplitSet
4711
4712
4713 BDD
4714 BDD::SubsetHeavyBranch(
4715   int numVars,
4716   int threshold) const
4717 {
4718     DdManager *mgr = ddMgr->p->manager;
4719     DdNode *result = Cudd_SubsetHeavyBranch(mgr, node, numVars, threshold);
4720     this->checkReturnValue(result);
4721     return BDD(ddMgr, result);
4722
4723 } // BDD::SubsetHeavyBranch
4724
4725
4726 BDD
4727 BDD::SupersetHeavyBranch(
4728   int numVars,
4729   int threshold) const
4730 {
4731     DdManager *mgr = ddMgr->p->manager;
4732     DdNode *result = Cudd_SupersetHeavyBranch(mgr, node, numVars, threshold);
4733     this->checkReturnValue(result);
4734     return BDD(ddMgr, result);
4735
4736 } // BDD::SupersetHeavyBranch
4737
4738
4739 BDD
4740 BDD::SubsetShortPaths(
4741   int numVars,
4742   int threshold,
4743   int hardlimit) const
4744 {
4745     DdManager *mgr = ddMgr->p->manager;
4746     DdNode *result = Cudd_SubsetShortPaths(mgr, node, numVars, threshold, hardlimit);
4747     this->checkReturnValue(result);
4748     return BDD(ddMgr, result);
4749
4750 } // BDD::SubsetShortPaths
4751
4752
4753 BDD
4754 BDD::SupersetShortPaths(
4755   int numVars,
4756   int threshold,
4757   int hardlimit) const
4758 {
4759     DdManager *mgr = ddMgr->p->manager;
4760     DdNode *result = Cudd_SupersetShortPaths(mgr, node, numVars, threshold, hardlimit);
4761     this->checkReturnValue(result);
4762     return BDD(ddMgr, result);
4763
4764 } // BDD::SupersetShortPaths
4765
4766
4767 void
4768 Cudd::SymmProfile(
4769   int lower,
4770   int upper) const
4771 {
4772     Cudd_SymmProfile(p->manager, lower, upper);
4773
4774 } // Cudd::SymmProfile
4775
4776
4777 unsigned int
4778 Cudd::Prime(
4779   unsigned int pr) const
4780 {
4781     return Cudd_Prime(pr);
4782
4783 } // Cudd::Prime
4784
4785
4786 void
4787 ABDD::PrintMinterm() const
4788 {
4789     cout.flush();
4790     DdManager *mgr = ddMgr->p->manager;
4791     int result = Cudd_PrintMinterm(mgr, node);
4792     this->checkReturnValue(result);
4793
4794 } // ABDD::PrintMinterm
4795
4796
4797 void
4798 BDD::PrintCover() const
4799 {
4800     cout.flush();
4801     DdManager *mgr = ddMgr->p->manager;
4802     int result = Cudd_bddPrintCover(mgr, node, node);
4803     this->checkReturnValue(result);
4804
4805 } // BDD::PrintCover
4806
4807
4808 void
4809 BDD::PrintCover(
4810   const BDD& u) const
4811 {
4812     this->checkSameManager(u);
4813     cout.flush();
4814     DdManager *mgr = ddMgr->p->manager;
4815     int result = Cudd_bddPrintCover(mgr, node, u.node);
4816     this->checkReturnValue(result);
4817
4818 } // BDD::PrintCover
4819
4820
4821 int
4822 BDD::EstimateCofactor(
4823   int i,
4824   int phase) const
4825 {
4826     DdManager *mgr = ddMgr->p->manager;
4827     int result = Cudd_EstimateCofactor(mgr, node, i, phase);
4828     this->checkReturnValue(result != CUDD_OUT_OF_MEM);
4829     return result;
4830
4831 } // BDD::EstimateCofactor
4832
4833
4834 int
4835 BDD::EstimateCofactorSimple(
4836   int i) const
4837 {
4838     int result = Cudd_EstimateCofactorSimple(node, i);
4839     return result;
4840
4841 } // BDD::EstimateCofactorSimple
4842
4843
4844 int
4845 Cudd::SharingSize(
4846   DD* nodes,
4847   int n) const
4848 {
4849     DdNode **nodeArray = ALLOC(DdNode *,n);
4850     for (int i = 0; i < n; i++) {
4851         nodeArray[i] = nodes[i].getNode();
4852     }
4853     int result = Cudd_SharingSize(nodeArray, n);
4854     FREE(nodeArray);
4855     this->checkReturnValue(result > 0);
4856     return result;
4857
4858 } // Cudd::SharingSize
4859
4860
4861 double
4862 ABDD::CountMinterm(
4863   int nvars) const
4864 {
4865     DdManager *mgr = ddMgr->p->manager;
4866     double result = Cudd_CountMinterm(mgr, node, nvars);
4867     this->checkReturnValue(result != (double) CUDD_OUT_OF_MEM);
4868     return result;
4869
4870 } // ABDD::CountMinterm
4871
4872
4873 double
4874 ABDD::CountPath() const
4875 {
4876     double result = Cudd_CountPath(node);
4877     this->checkReturnValue(result != (double) CUDD_OUT_OF_MEM);
4878     return result;
4879
4880 } // ABDD::CountPath
4881
4882
4883 BDD
4884 ABDD::Support() const
4885 {
4886     DdManager *mgr = ddMgr->p->manager;
4887     DdNode *result = Cudd_Support(mgr, node);
4888     this->checkReturnValue(result);
4889     return BDD(ddMgr, result);
4890
4891 } // ABDD::Support
4892
4893
4894 int
4895 ABDD::SupportSize() const
4896 {
4897     DdManager *mgr = ddMgr->p->manager;
4898     int result = Cudd_SupportSize(mgr, node);
4899     this->checkReturnValue(result != CUDD_OUT_OF_MEM);
4900     return result;
4901
4902 } // ABDD::SupportSize
4903
4904
4905 BDD
4906 BDDvector::VectorSupport() const
4907 {
4908     int n = p->size;
4909     DdManager *mgr = p->manager->getManager();
4910     DdNode **F = ALLOC(DdNode *,n);
4911     for (int i = 0; i < n; i++) {
4912         F[i] = p->vect[i].getNode();
4913     }
4914     DdNode *result = Cudd_VectorSupport(mgr, F, n);
4915     FREE(F);
4916     p->manager->checkReturnValue(result);
4917     return BDD(p->manager, result);
4918
4919 } // BDDvector::VectorSupport
4920
4921
4922 int
4923 BDDvector::nodeCount() const
4924 {
4925     int n = p->size;
4926     DdNode **nodeArray = ALLOC(DdNode *,n);
4927     for (int i = 0; i < n; i++) {
4928         nodeArray[i] = p->vect[i].getNode();
4929     }
4930     int result = Cudd_SharingSize(nodeArray, n);
4931     FREE(nodeArray);
4932     p->manager->checkReturnValue(result > 0);
4933     return result;
4934
4935 } // BDDvector::nodeCount
4936
4937
4938 BDD
4939 ADDvector::VectorSupport() const
4940 {
4941     int n = p->size;
4942     DdManager *mgr = p->manager->getManager();
4943     DdNode **F = ALLOC(DdNode *,n);
4944     for (int i = 0; i < n; i++) {
4945         F[i] = p->vect[i].getNode();
4946     }
4947     DdNode *result = Cudd_VectorSupport(mgr, F, n);
4948     FREE(F);
4949     p->manager->checkReturnValue(result);
4950     return BDD(p->manager, result);
4951
4952 } // ADDvector::VectorSupport
4953
4954
4955 int
4956 BDDvector::VectorSupportSize() const
4957 {
4958     int n = p->size;
4959     DdManager *mgr = p->manager->getManager();
4960     DdNode **F = ALLOC(DdNode *,n);
4961     for (int i = 0; i < n; i++) {
4962         F[i] = p->vect[i].getNode();
4963     }
4964     int result = Cudd_VectorSupportSize(mgr, F, n);
4965     FREE(F);
4966     p->manager->checkReturnValue(result != CUDD_OUT_OF_MEM);
4967     return result;
4968
4969 } // BDDvector::VectorSupportSize
4970
4971
4972 int
4973 ADDvector::VectorSupportSize() const
4974 {
4975     int n = p->size;
4976     DdManager *mgr = p->manager->getManager();
4977     DdNode **F = ALLOC(DdNode *,n);
4978     for (int i = 0; i < n; i++) {
4979         F[i] = p->vect[i].getNode();
4980     }
4981     int result = Cudd_VectorSupportSize(mgr, F, n);
4982     FREE(F);
4983     p->manager->checkReturnValue(result != CUDD_OUT_OF_MEM);
4984     return result;
4985
4986 } // ADDvector::VectorSupportSize
4987
4988
4989 void
4990 ABDD::ClassifySupport(
4991   const ABDD& g,
4992   BDD* common,
4993   BDD* onlyF,
4994   BDD* onlyG) const
4995 {
4996     DdManager *mgr = this->checkSameManager(g);
4997     DdNode *C, *F, *G;
4998     int result = Cudd_ClassifySupport(mgr, node, g.node, &C, &F, &G);
4999     this->checkReturnValue(result);
5000     *common = BDD(ddMgr, C);
5001     *onlyF = BDD(ddMgr, F);
5002     *onlyG = BDD(ddMgr, G);
5003
5004 } // ABDD::ClassifySupport
5005
5006
5007 int
5008 ABDD::CountLeaves() const
5009 {
5010     return Cudd_CountLeaves(node);
5011
5012 } // ABDD::CountLeaves
5013
5014
5015 void
5016 BDD::PickOneCube(
5017   char * string) const
5018 {
5019     DdManager *mgr = ddMgr->p->manager;
5020     int result = Cudd_bddPickOneCube(mgr, node, string);
5021     this->checkReturnValue(result);
5022
5023 } // BDD::PickOneCube
5024
5025
5026 BDD
5027 BDD::PickOneMinterm(
5028   BDDvector vars) const
5029 {
5030     int n = vars.count();
5031     DdManager *mgr = ddMgr->p->manager;
5032     DdNode **V = ALLOC(DdNode *,n);
5033     for (int i = 0; i < n; i++) {
5034         V[i] = vars[i].node;
5035     }
5036     DdNode *result = Cudd_bddPickOneMinterm(mgr, node, V, n);
5037     FREE(V);
5038     this->checkReturnValue(result);
5039     return BDD(ddMgr, result);
5040
5041 } // BDD::PickOneMinterm
5042
5043
5044 DdGen *
5045 ABDD::FirstCube(
5046   int ** cube,
5047   CUDD_VALUE_TYPE * value) const
5048 {
5049     DdManager *mgr = ddMgr->p->manager;
5050     DdGen *result = Cudd_FirstCube(mgr, node, cube, value);
5051     this->checkReturnValue((DdNode *)result);
5052     return result;
5053
5054 } // ABDD::FirstCube
5055
5056
5057 int
5058 NextCube(
5059   DdGen * gen,
5060   int ** cube,
5061   CUDD_VALUE_TYPE * value)
5062 {
5063     return Cudd_NextCube(gen, cube, value);
5064
5065 } // NextCube
5066
5067
5068 BDD
5069 Cudd::bddComputeCube(
5070   BDD * vars,
5071   int * phase,
5072   int n)
5073 {
5074     DdManager *mgr = p->manager;
5075     DdNode **V = ALLOC(DdNode *,n);
5076     for (int i = 0; i < n; i++) {
5077         V[i] = vars[i].getNode();
5078     }
5079     DdNode *result = Cudd_bddComputeCube(mgr, V, phase, n);
5080     FREE(V);
5081     this->checkReturnValue(result);
5082     return BDD(this, result);
5083
5084 } // Cudd::bddComputeCube
5085
5086
5087 ADD
5088 Cudd::addComputeCube(
5089   ADD * vars,
5090   int * phase,
5091   int n)
5092 {
5093     DdManager *mgr = p->manager;
5094     DdNode **V = ALLOC(DdNode *,n);
5095     for (int i = 0; i < n; i++) {
5096         V[i] = vars[i].getNode();
5097     }
5098     DdNode *result = Cudd_addComputeCube(mgr, V, phase, n);
5099     FREE(V);
5100     this->checkReturnValue(result);
5101     return ADD(this, result);
5102
5103 } // Cudd::addComputeCube
5104
5105
5106 DdGen *
5107 BDD::FirstNode(
5108   BDD* fnode) const
5109 {
5110     DdManager *mgr = ddMgr->p->manager;
5111     DdNode *Fn;
5112     DdGen *result = Cudd_FirstNode(mgr, node, &Fn);
5113     this->checkReturnValue((DdNode *)result);
5114     *fnode = BDD(ddMgr, Fn);
5115     return result;
5116
5117 } // DD::FirstNode
5118
5119
5120 int
5121 Cudd::NextNode(
5122   DdGen * gen,
5123   BDD * nnode)
5124 {
5125     DdNode *nn;
5126     int result = Cudd_NextNode(gen, &nn);
5127     *nnode = BDD(this, nn);
5128     return result;
5129
5130 } // Cudd::NextNode
5131
5132
5133 int
5134 GenFree(
5135   DdGen * gen)
5136 {
5137     return Cudd_GenFree(gen);
5138
5139 } // GenFree
5140
5141
5142 int
5143 IsGenEmpty(
5144   DdGen * gen)
5145 {
5146     return Cudd_IsGenEmpty(gen);
5147
5148 } // IsGenEmpty
5149
5150
5151 BDD
5152 Cudd::IndicesToCube(
5153   int * array,
5154   int n)
5155 {
5156     DdNode *result = Cudd_IndicesToCube(p->manager, array, n);
5157     this->checkReturnValue(result);
5158     return BDD(this, result);
5159
5160 } // Cudd::IndicesToCube
5161
5162
5163 void
5164 Cudd::PrintVersion(
5165   FILE * fp) const
5166 {
5167     cout.flush();
5168     Cudd_PrintVersion(fp);
5169
5170 } // Cudd::PrintVersion
5171
5172
5173 double
5174 Cudd::AverageDistance() const
5175 {
5176     return Cudd_AverageDistance(p->manager);
5177
5178 } // Cudd::AverageDistance
5179
5180
5181 long
5182 Cudd::Random()
5183 {
5184     return Cudd_Random();
5185
5186 } // Cudd::Random
5187
5188
5189 void
5190 Cudd::Srandom(
5191   long seed)
5192 {
5193     Cudd_Srandom(seed);
5194
5195 } // Cudd::Srandom
5196
5197
5198 double
5199 ABDD::Density(
5200   int nvars) const
5201 {
5202     DdManager *mgr = ddMgr->p->manager;
5203     double result = Cudd_Density(mgr, node, nvars);
5204     this->checkReturnValue(result != (double) CUDD_OUT_OF_MEM);
5205     return result;
5206
5207 } // ABDD::Density
5208
5209
5210 int
5211 ZDD::Count() const
5212 {
5213     DdManager *mgr = ddMgr->p->manager;
5214     int result = Cudd_zddCount(mgr, node);
5215     this->checkReturnValue(result != CUDD_OUT_OF_MEM);
5216     return result;
5217
5218 } // ZDD::Count
5219
5220
5221 double
5222 ZDD::CountDouble() const
5223 {
5224     DdManager *mgr = ddMgr->p->manager;
5225     double result = Cudd_zddCountDouble(mgr, node);
5226     this->checkReturnValue(result != (double) CUDD_OUT_OF_MEM);
5227     return result;
5228
5229 } // ZDD::CountDouble
5230
5231
5232 ZDD
5233 ZDD::Product(
5234   const ZDD& g) const
5235 {
5236     DdManager *mgr = this->checkSameManager(g);
5237     DdNode *result = Cudd_zddProduct(mgr, node, g.node);
5238     this->checkReturnValue(result);
5239     return ZDD(ddMgr, result);
5240
5241 } // ZDD::Product
5242
5243
5244 ZDD
5245 ZDD::UnateProduct(
5246   const ZDD& g) const
5247 {
5248     DdManager *mgr = this->checkSameManager(g);
5249     DdNode *result = Cudd_zddUnateProduct(mgr, node, g.node);
5250     this->checkReturnValue(result);
5251     return ZDD(ddMgr, result);
5252
5253 } // ZDD::UnateProduct
5254
5255
5256 ZDD
5257 ZDD::WeakDiv(
5258   const ZDD& g) const
5259 {
5260     DdManager *mgr = this->checkSameManager(g);
5261     DdNode *result = Cudd_zddWeakDiv(mgr, node, g.node);
5262     this->checkReturnValue(result);
5263     return ZDD(ddMgr, result);
5264
5265 } // ZDD::WeakDiv
5266
5267
5268 ZDD
5269 ZDD::Divide(
5270   const ZDD& g) const
5271 {
5272     DdManager *mgr = this->checkSameManager(g);
5273     DdNode *result = Cudd_zddDivide(mgr, node, g.node);
5274     this->checkReturnValue(result);
5275     return ZDD(ddMgr, result);
5276
5277 } // ZDD::Divide
5278
5279
5280 ZDD
5281 ZDD::WeakDivF(
5282   const ZDD& g) const
5283 {
5284     DdManager *mgr = this->checkSameManager(g);
5285     DdNode *result = Cudd_zddWeakDivF(mgr, node, g.node);
5286     this->checkReturnValue(result);
5287     return ZDD(ddMgr, result);
5288
5289 } // ZDD::WeakDivF
5290
5291
5292 ZDD
5293 ZDD::DivideF(
5294   const ZDD& g) const
5295 {
5296     DdManager *mgr = this->checkSameManager(g);
5297     DdNode *result = Cudd_zddDivideF(mgr, node, g.node);
5298     this->checkReturnValue(result);
5299     return ZDD(ddMgr, result);
5300
5301 } // ZDD::DivideF
5302
5303
5304 MtrNode *
5305 Cudd::MakeZddTreeNode(
5306   unsigned int low,
5307   unsigned int size,
5308   unsigned int type)
5309 {
5310     return Cudd_MakeZddTreeNode(p->manager, low, size, type);
5311
5312 } // Cudd::MakeZddTreeNode
5313
5314
5315 BDD
5316 BDD::zddIsop(
5317   const BDD& U,
5318   ZDD* zdd_I) const
5319 {
5320     DdManager *mgr = this->checkSameManager(U);
5321     DdNode *Z;
5322     DdNode *result = Cudd_zddIsop(mgr, node, U.node, &Z);
5323     this->checkReturnValue(result);
5324     *zdd_I = ZDD(ddMgr, Z);
5325     return BDD(ddMgr, result);
5326
5327 } // BDD::Isop
5328
5329
5330 BDD
5331 BDD::Isop(
5332   const BDD& U) const
5333 {
5334     DdManager *mgr = this->checkSameManager(U);
5335     DdNode *result = Cudd_bddIsop(mgr, node, U.node);
5336     this->checkReturnValue(result);
5337     return BDD(ddMgr, result);
5338
5339 } // BDD::Isop
5340
5341
5342 double
5343 ZDD::CountMinterm(
5344   int path) const
5345 {
5346     DdManager *mgr = ddMgr->p->manager;
5347     double result = Cudd_zddCountMinterm(mgr, node, path);
5348     this->checkReturnValue(result != (double) CUDD_OUT_OF_MEM);
5349     return result;
5350
5351 } // ZDD::CountMinterm
5352
5353
5354 void
5355 Cudd::zddPrintSubtable() const
5356 {
5357     cout.flush();
5358     Cudd_zddPrintSubtable(p->manager);
5359
5360 } // Cudd::zddPrintSubtable
5361
5362
5363 ZDD
5364 BDD::PortToZdd() const
5365 {
5366     DdManager *mgr = ddMgr->p->manager;
5367     DdNode *result = Cudd_zddPortFromBdd(mgr, node);
5368     this->checkReturnValue(result);
5369     return ZDD(ddMgr, result);
5370
5371 } // BDD::PortToZdd
5372
5373
5374 BDD
5375 ZDD::PortToBdd() const
5376 {
5377     DdManager *mgr = ddMgr->p->manager;
5378     DdNode *result = Cudd_zddPortToBdd(mgr, node);
5379     this->checkReturnValue(result);
5380     return BDD(ddMgr, result);
5381
5382 } // ZDD::PortToBdd
5383
5384
5385 void
5386 Cudd::zddReduceHeap(
5387   Cudd_ReorderingType heuristic,
5388   int minsize)
5389 {
5390     int result = Cudd_zddReduceHeap(p->manager, heuristic, minsize);
5391     this->checkReturnValue(result);
5392
5393 } // Cudd::zddReduceHeap
5394
5395
5396 void
5397 Cudd::zddShuffleHeap(
5398   int * permutation)
5399 {
5400     int result = Cudd_zddShuffleHeap(p->manager, permutation);
5401     this->checkReturnValue(result);
5402
5403 } // Cudd::zddShuffleHeap
5404
5405
5406 ZDD
5407 ZDD::Ite(
5408   const ZDD& g,
5409   const ZDD& h) const
5410 {
5411     DdManager *mgr = this->checkSameManager(g);
5412     this->checkSameManager(h);
5413     DdNode *result = Cudd_zddIte(mgr, node, g.node, h.node);
5414     this->checkReturnValue(result);
5415     return ZDD(ddMgr, result);
5416
5417 } // ZDD::Ite
5418
5419
5420 ZDD
5421 ZDD::Union(
5422   const ZDD& Q) const
5423 {
5424     DdManager *mgr = this->checkSameManager(Q);
5425     DdNode *result = Cudd_zddUnion(mgr, node, Q.node);
5426     this->checkReturnValue(result);
5427     return ZDD(ddMgr, result);
5428
5429 } // ZDD::Union
5430
5431
5432 ZDD
5433 ZDD::Intersect(
5434   const ZDD& Q) const
5435 {
5436     DdManager *mgr = this->checkSameManager(Q);
5437     DdNode *result = Cudd_zddIntersect(mgr, node, Q.node);
5438     this->checkReturnValue(result);
5439     return ZDD(ddMgr, result);
5440
5441 } // ZDD::Intersect
5442
5443
5444 ZDD
5445 ZDD::Diff(
5446   const ZDD& Q) const
5447 {
5448     DdManager *mgr = this->checkSameManager(Q);
5449     DdNode *result = Cudd_zddDiff(mgr, node, Q.node);
5450     this->checkReturnValue(result);
5451     return ZDD(ddMgr, result);
5452
5453 } // ZDD::Diff
5454
5455
5456 ZDD
5457 ZDD::DiffConst(
5458   const ZDD& Q) const
5459 {
5460     DdManager *mgr = this->checkSameManager(Q);
5461     DdNode *result = Cudd_zddDiffConst(mgr, node, Q.node);
5462     this->checkReturnValue(result);
5463     return ZDD(ddMgr, result);
5464
5465 } // ZDD::DiffConst
5466
5467
5468 ZDD
5469 ZDD::Subset1(
5470   int var) const
5471 {
5472     DdManager *mgr = ddMgr->p->manager;
5473     DdNode *result = Cudd_zddSubset1(mgr, node, var);
5474     this->checkReturnValue(result);
5475     return ZDD(ddMgr, result);
5476
5477 } // ZDD::Subset1
5478
5479
5480 ZDD
5481 ZDD::Subset0(
5482   int var) const
5483 {
5484     DdManager *mgr = ddMgr->p->manager;
5485     DdNode *result = Cudd_zddSubset0(mgr, node, var);
5486     this->checkReturnValue(result);
5487     return ZDD(ddMgr, result);
5488
5489 } // ZDD::Subset0
5490
5491
5492 ZDD
5493 ZDD::Change(
5494   int var) const
5495 {
5496     DdManager *mgr = ddMgr->p->manager;
5497     DdNode *result = Cudd_zddChange(mgr, node, var);
5498     this->checkReturnValue(result);
5499     return ZDD(ddMgr, result);
5500
5501 } // ZDD::Change
5502
5503
5504 void
5505 Cudd::zddSymmProfile(
5506   int lower,
5507   int upper) const
5508 {
5509     Cudd_zddSymmProfile(p->manager, lower, upper);
5510
5511 } // Cudd::zddSymmProfile
5512
5513
5514 void
5515 ZDD::PrintMinterm() const
5516 {
5517     cout.flush();
5518     DdManager *mgr = ddMgr->p->manager;
5519     int result = Cudd_zddPrintMinterm(mgr, node);
5520     this->checkReturnValue(result);
5521
5522 } // ZDD::PrintMinterm
5523
5524
5525 void
5526 ZDD::PrintCover() const
5527 {
5528     cout.flush();
5529     DdManager *mgr = ddMgr->p->manager;
5530     int result = Cudd_zddPrintCover(mgr, node);
5531     this->checkReturnValue(result);
5532
5533 } // ZDD::PrintCover
5534
5535
5536 void
5537 ZDDvector::DumpDot(
5538   char ** inames,
5539   char ** onames,
5540   FILE * fp) const
5541 {
5542     DdManager *mgr = p->manager->getManager();
5543     int n = p->size;
5544     DdNode **F = ALLOC(DdNode *,n);
5545     for (int i = 0; i < n; i ++) {
5546         F[i] = p->vect[i].getNode();
5547     }
5548     int result = Cudd_zddDumpDot(mgr, n, F, inames, onames, fp);
5549     FREE(F);
5550     p->manager->checkReturnValue(result);
5551
5552 } // ZDDvector::DumpDot