distr/obj/testobj.cc

   1 /**CFile***********************************************************************
   2
   3   FileName    [testobj.cc]
   4
   5   PackageName [cuddObj]
   6
   7   Synopsis    [Test program 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 #include <math.h>
  51
  52 /*---------------------------------------------------------------------------*/
  53 /* Variable declarations                                                     */
  54 /*---------------------------------------------------------------------------*/
  55
  56 #ifndef lint
  57 static char rcsid[] UTIL_UNUSED = "$Id: testobj.cc,v 1.5 2004/08/13 18:11:07 fabio Exp fabio $";
  58 #endif
  59
  60 /*---------------------------------------------------------------------------*/
  61 /* Static function prototypes                                                */
  62 /*---------------------------------------------------------------------------*/
  63
  64 static void testBdd(Cudd& mgr, int verbosity);
  65 static void testAdd(Cudd& mgr, int verbosity);
  66 static void testAdd2(Cudd& mgr, int verbosity);
  67 static void testZdd(Cudd& mgr, int verbosity);
  68 static void testBdd2(Cudd& mgr, int verbosity);
  69 static void testBdd3(Cudd& mgr, int verbosity);
  70 static void testZdd2(Cudd& mgr, int verbosity);
  71 static void testBdd4(Cudd& mgr, int verbosity);
  72
  73
  74 /*---------------------------------------------------------------------------*/
  75 /* Definition of exported functions                                          */
  76 /*---------------------------------------------------------------------------*/
  77
  78 /**Function********************************************************************
  79
  80   Synopsis    [Main program for testobj.]
  81
  82   Description []
  83
  84   SideEffects [None]
  85
  86   SeeAlso     []
  87
  88 ******************************************************************************/
  89 int
  90 main()
  91 {
  92     int verbosity = 2;
  93
  94     Cudd mgr(0,2);
  95     // mgr.makeVerbose();               // trace constructors and destructors
  96     testBdd(mgr,verbosity);
  97     testAdd(mgr,verbosity);
  98     testAdd2(mgr,verbosity);
  99     testZdd(mgr,verbosity);
 100     testBdd2(mgr,verbosity);
 101     testBdd3(mgr,verbosity);
 102     testZdd2(mgr,verbosity);
 103     testBdd4(mgr,verbosity);
 104     mgr.info();
 105     return 0;
 106
 107 } // main
 108
 109
 110 /**Function********************************************************************
 111
 112   Synopsis    [Test basic operators on BDDs.]
 113
 114   Description [Test basic operators on BDDs. The function returns void
 115   because it relies on the error hadling done by the interface. The
 116   default error handler causes program termination.]
 117
 118   SideEffects [Creates BDD variables in the manager.]
 119
 120   SeeAlso     [testBdd2 testBdd3 testBdd4]
 121
 122 ******************************************************************************/
 123 static void
 124 testBdd(
 125   Cudd& mgr,
 126   int verbosity)
 127 {
 128     cout << "Entering testBdd\n";
 129     // Create two new variables in the manager. If testBdd is called before
 130     // any variable is created in mgr, then x gets index 0 and y gets index 1.
 131     BDD x = mgr.bddVar();
 132     BDD y = mgr.bddVar();
 133
 134     BDD f = x * y;
 135     cout << "f"; f.print(2,verbosity);
 136
 137     BDD g = y + !x;
 138     cout << "g"; g.print(2,verbosity);
 139
 140     cout << "f and g are" << (f == !g ? "" : " not") << " complementary\n";
 141     cout << "f is" << (f <= g ? "" : " not") << " less than or equal to g\n";
 142
 143     g = f | ~g;
 144     cout << "g"; g.print(2,verbosity);
 145
 146     BDD h = f = y;
 147     cout << "h"; h.print(2,verbosity);
 148
 149     cout << "x + h has " << (x+h).nodeCount() << " nodes\n";
 150
 151     h += x;
 152     cout << "h"; h.print(2,verbosity);
 153
 154 } // testBdd
 155
 156
 157 /**Function********************************************************************
 158
 159   Synopsis    [Test basic operators on ADDs.]
 160
 161   Description [Test basic operators on ADDs. The function returns void
 162   because it relies on the error hadling done by the interface. The
 163   default error handler causes program termination.]
 164
 165   SideEffects [May create ADD variables in the manager.]
 166
 167   SeeAlso     [testAdd2]
 168
 169 ******************************************************************************/
 170 static void
 171 testAdd(
 172   Cudd& mgr,
 173   int verbosity)
 174 {
 175     cout << "Entering testAdd\n";
 176     // Create two ADD variables. If we called method addVar without an
 177     // argument, we would get two new indices. If testAdd is indeed called
 178     // after testBdd, then those indices would be 2 and 3. By specifying the
 179     // arguments, on the other hand, we avoid creating new unnecessary BDD
 180     // variables.
 181     ADD p = mgr.addVar(0);
 182     ADD q = mgr.addVar(1);
 183
 184     // Test arithmetic operators.
 185     ADD r = p + q;
 186     cout << "r"; r.print(2,verbosity);
 187
 188     // CUDD_VALUE_TYPE is double.
 189     ADD s = mgr.constant(3.0);
 190     s *= p * q;
 191     cout << "s"; s.print(2,verbosity);
 192
 193     s += mgr.plusInfinity();
 194     cout << "s"; s.print(2,verbosity);
 195
 196     // Test relational operators.
 197     cout << "p is" << (p <= r ? "" : " not") << " less than or equal to r\n";
 198
 199     // Test logical operators.
 200     r = p | q;
 201     cout << "r"; r.print(2,verbosity);
 202
 203 } // testAdd
 204
 205
 206 /**Function********************************************************************
 207
 208   Synopsis    [Test some more operators on ADDs.]
 209
 210   Description [Test some more operators on ADDs. The function returns void
 211   because it relies on the error hadling done by the interface. The
 212   default error handler causes program termination.]
 213
 214   SideEffects [May create ADD variables in the manager.]
 215
 216   SeeAlso     [testAdd]
 217
 218 ******************************************************************************/
 219 static void
 220 testAdd2(
 221   Cudd& mgr,
 222   int verbosity)
 223 {
 224     cout << "Entering testAdd2\n";
 225     // Create two ADD variables. If we called method addVar without an
 226     // argument, we would get two new indices.
 227     int i;
 228     ADDvector x(2);
 229     for (i = 0; i < 2; i++) {
 230         x[i] = mgr.addVar(i);
 231     }
 232
 233     // Build a probability density function: [0.1, 0.2, 0.3, 0.4].
 234     ADD f0 = x[1].Ite(mgr.constant(0.2), mgr.constant(0.1));
 235     ADD f1 = x[1].Ite(mgr.constant(0.4), mgr.constant(0.3));
 236     ADD f  = x[0].Ite(f1, f0);
 237     cout << "f"; f.print(2,verbosity);
 238
 239     // Compute the entropy.
 240     ADD l = f.Log();
 241     cout << "l"; l.print(2,verbosity);
 242     ADD r = f * l;
 243     cout << "r"; r.print(2,verbosity);
 244
 245     ADD e = r.MatrixMultiply(mgr.constant(-1.0/log(2.0)),x);
 246     cout << "e"; e.print(2,verbosity);
 247
 248 } // testAdd2
 249
 250
 251 /**Function********************************************************************
 252
 253   Synopsis    [Test basic operators on ZDDs.]
 254
 255   Description [Test basic operators on ZDDs. The function returns void
 256   because it relies on the error hadling done by the interface. The
 257   default error handler causes program termination.]
 258
 259   SideEffects [May create ZDD variables in the manager.]
 260
 261   SeeAlso     [testZdd2]
 262
 263 ******************************************************************************/
 264 static void
 265 testZdd(
 266   Cudd& mgr,
 267   int verbosity)
 268 {
 269     cout << "Entering testZdd\n";
 270     ZDD v = mgr.zddVar(0);
 271     ZDD w = mgr.zddVar(1);
 272
 273     ZDD s = v + w;
 274     cout << "s"; s.print(2,verbosity);
 275
 276     cout << "v is" << (v < s ? "" : " not") << " less than s\n";
 277
 278     s -= v;
 279     cout << "s"; s.print(2,verbosity);
 280
 281 } // testZdd
 282
 283
 284 /**Function********************************************************************
 285
 286   Synopsis    [Test vector operators on BDDs.]
 287
 288   Description [Test vector operators on BDDs. The function returns void
 289   because it relies on the error hadling done by the interface. The
 290   default error handler causes program termination.]
 291
 292   SideEffects [May create BDD variables in the manager.]
 293
 294   SeeAlso     [testBdd testBdd3 testBdd4]
 295
 296 ******************************************************************************/
 297 static void
 298 testBdd2(
 299   Cudd& mgr,
 300   int verbosity)
 301 {
 302     cout << "Entering testBdd2\n";
 303     // Loop indices are best declared in the loops themselves, but
 304     // some compilers won't let us do that.
 305     int i;
 306     BDDvector x(4);
 307     for (i = 0; i < 4; i++) {
 308         x[i] = mgr.bddVar(i);
 309     }
 310
 311     // Create the BDD for the Achilles' Heel function.
 312     BDD p1 = x[0] * x[2];
 313     BDD p2 = x[1] * x[3];
 314     BDD f = p1 + p2;
 315     cout << "f"; f.print(4,verbosity);
 316     cout << "Irredundant cover of f:" << endl; f.PrintCover();
 317     cout << "Number of minterms (arbitrary precision): "; f.ApaPrintMinterm(4);
 318     cout << "Number of minterms (extended precision):  "; f.EpdPrintMinterm(4);
 319     const char* inames[] = {"x0", "x1", "x2", "x3"};
 320     cout << "Two-literal clauses of f:" << endl;
 321     f.PrintTwoLiteralClauses((char **)inames); cout << endl;
 322
 323     BDDvector vect = f.CharToVect();
 324     for (i = 0; i < vect.count(); i++) {
 325         cout << "vect[" << i << "]" << endl; vect[i].PrintCover();
 326     }
 327
 328     // v0,...,v3 suffice if testBdd2 is called before testBdd3.
 329     const char* onames[] = {"v0", "v1", "v2", "v3", "v4", "v5"};
 330     vect.DumpDot((char **)inames,(char **)onames);
 331
 332 } // testBdd2
 333
 334
 335 /**Function********************************************************************
 336
 337   Synopsis    [Test additional operators on BDDs.]
 338
 339   Description [Test additional operators on BDDs. The function returns
 340   void because it relies on the error hadling done by the
 341   interface. The default error handler causes program termination.]
 342
 343   SideEffects [May create BDD variables in the manager.]
 344
 345   SeeAlso     [testBdd testBdd2 testBdd4]
 346
 347 ******************************************************************************/
 348 static void
 349 testBdd3(
 350   Cudd& mgr,
 351   int verbosity)
 352 {
 353     cout << "Entering testBdd3\n";
 354     BDDvector x(6);
 355     for (int i = 0; i < 6; i++) {
 356         x[i] = mgr.bddVar(i);
 357     }
 358
 359     BDD G = x[4] + !x[5];
 360     BDD H = x[4] * x[5];
 361     BDD E = x[3].Ite(G,!x[5]);
 362     BDD F = x[3] + !H;
 363     BDD D = x[2].Ite(F,!H);
 364     BDD C = x[2].Ite(E,!F);
 365     BDD B = x[1].Ite(C,!F);
 366     BDD A = x[0].Ite(B,!D);
 367     BDD f = !A;
 368     cout << "f"; f.print(6,verbosity);
 369
 370     BDD f1 = f.RemapUnderApprox(6);
 371     cout << "f1"; f1.print(6,verbosity);
 372     cout << "f1 is" << (f1 <= f ? "" : " not") << " less than or equal to f\n";
 373
 374     BDD g;
 375     BDD h;
 376     f.GenConjDecomp(&g,&h);
 377     cout << "g"; g.print(6,verbosity);
 378     cout << "h"; h.print(6,verbosity);
 379     cout << "g * h " << (g * h == f ? "==" : "!=") << " f\n";
 380
 381 } // testBdd3
 382
 383
 384 /**Function********************************************************************
 385
 386   Synopsis    [Test cover manipulation with BDDs and ZDDs.]
 387
 388   Description [Test cover manipulation with BDDs and ZDDs.  The
 389   function returns void because it relies on the error hadling done by
 390   the interface.  The default error handler causes program
 391   termination.  This function builds the BDDs for a transformed adder:
 392   one in which the inputs are transformations of the original
 393   inputs. It then creates ZDDs for the covers from the BDDs.]
 394
 395   SideEffects [May create BDD and ZDD variables in the manager.]
 396
 397   SeeAlso     [testZdd]
 398
 399 ******************************************************************************/
 400 static void
 401 testZdd2(
 402   Cudd& mgr,
 403   int verbosity)
 404 {
 405     cout << "Entering testZdd2\n";
 406     int N = 3;                  // number of bits
 407     // Loop indices are best declared in the loops themselves, but
 408     // some compilers won't let us do that.
 409     int i;
 410     // Create variables.
 411     BDDvector a(N,&mgr);
 412     BDDvector b(N,&mgr);
 413     BDDvector c(N+1,&mgr);
 414     for (i = 0; i < N; i++) {
 415         a[N-1-i] = mgr.bddVar(2*i);
 416         b[N-1-i] = mgr.bddVar(2*i+1);
 417     }
 418     c[0] = mgr.bddVar(2*N);
 419     // Build functions.
 420     BDDvector s(N,&mgr);
 421     for (i = 0; i < N; i++) {
 422         s[i] = a[i].Xnor(c[i]);
 423         c[i+1] = a[i].Ite(b[i],c[i]);
 424     }
 425
 426     // Create array of outputs and print it.
 427     BDDvector p(N+1,&mgr);
 428     for (i = 0; i < N; i++) {
 429         p[i] = s[i];
 430     }
 431     p[N] = c[N];
 432     for (i = 0; i < p.count(); i++) {
 433         cout << "p[" << i << "]"; p[i].print(2*N+1,verbosity);
 434     }
 435     const char* inames[] = {"a2", "b2", "a1", "b1", "a0", "b0", "c0"};
 436     const char* onames[] = {"s0", "s1", "s2", "c3"};
 437     p.DumpDot((char **)inames,(char **)onames);
 438
 439     // Create ZDD variables and build ZDD covers from BDDs.
 440     mgr.zddVarsFromBddVars(2);
 441     ZDDvector z(N+1,&mgr);
 442     for (i = 0; i < N+1; i++) {
 443         ZDD temp;
 444         BDD dummy = p[i].zddIsop(p[i],&temp);
 445         z[i] = temp;
 446     }
 447
 448     // Print out covers.
 449     for (i = 0; i < z.count(); i++) {
 450         cout << "z[" << i << "]"; z[i].print(4*N+2,verbosity);
 451     }
 452     for (i = 0; i < z.count(); i++) {
 453         cout << "z[" << i << "]\n"; z[i].PrintCover();
 454     }
 455     const char* znames[] = {"a2+", "a2-", "b2+", "b2-", "a1+", "a1-", "b1+",
 456                             "b1-", "a0+", "a0-", "b0+", "b0-", "c0+", "c0-"};
 457     z.DumpDot((char **)znames,(char **)onames);
 458
 459 } // testZdd2
 460
 461
 462 /**Function********************************************************************
 463
 464   Synopsis    [Test transfer between BDD managers.]
 465
 466   Description [Test transfer between BDD managers.  The
 467   function returns void because it relies on the error hadling done by
 468   the interface.  The default error handler causes program
 469   termination.]
 470
 471   SideEffects [May create BDD variables in the manager.]
 472
 473   SeeAlso     [testBdd testBdd2 testBdd3]
 474
 475 ******************************************************************************/
 476 static void
 477 testBdd4(
 478   Cudd& mgr,
 479   int verbosity)
 480 {
 481     cout << "Entering testBdd4\n";
 482     BDD x = mgr.bddVar(0);
 483     BDD y = mgr.bddVar(1);
 484     BDD z = mgr.bddVar(2);
 485
 486     BDD f = !x * !y * !z + x * y;
 487     cout << "f"; f.print(3,verbosity);
 488
 489     Cudd otherMgr(0,0);
 490     BDD g = f.Transfer(otherMgr);
 491     cout << "g"; g.print(3,verbosity);
 492
 493     BDD h = g.Transfer(mgr);
 494     cout << "f and h are" << (f == h ? "" : " not") << " identical\n";
 495
 496 } // testBdd4