source: icGREP/icgrep-devel/cudd-2.5.1/obj/testobj.cc @ 6055

Last change on this file since 6055 was 4597, checked in by nmedfort, 4 years ago

Upload of the CUDD library.

File size: 18.3 KB
Line 
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-2012, 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#include <iostream>
52#include <cassert>
53
54using namespace std;
55
56/*---------------------------------------------------------------------------*/
57/* Variable declarations                                                     */
58/*---------------------------------------------------------------------------*/
59
60#ifndef lint
61static char rcsid[] UNUSED = "$Id: testobj.cc,v 1.7 2012/02/05 01:06:40 fabio Exp fabio $";
62#endif
63
64/*---------------------------------------------------------------------------*/
65/* Static function prototypes                                                */
66/*---------------------------------------------------------------------------*/
67
68static void testBdd(Cudd& mgr, int verbosity);
69static void testAdd(Cudd& mgr, int verbosity);
70static void testAdd2(Cudd& mgr, int verbosity);
71static void testZdd(Cudd& mgr, int verbosity);
72static void testBdd2(Cudd& mgr, int verbosity);
73static void testBdd3(Cudd& mgr, int verbosity);
74static void testZdd2(Cudd& mgr, int verbosity);
75static void testBdd4(Cudd& mgr, int verbosity);
76static void testBdd5(Cudd& mgr, int verbosity);
77
78
79/*---------------------------------------------------------------------------*/
80/* Definition of exported functions                                          */
81/*---------------------------------------------------------------------------*/
82
83/**Function********************************************************************
84
85  Synopsis    [Main program for testobj.]
86
87  Description []
88
89  SideEffects [None]
90
91  SeeAlso     []
92
93******************************************************************************/
94int
95main(int argc, char **argv)
96{
97    int verbosity = 0;
98
99    if (argc == 2) {
100        int retval = sscanf(argv[1], "%d", &verbosity);
101        if (retval != 1)
102            return 1;
103    } else if (argc != 1) {
104        return 1;
105    }
106
107    Cudd mgr(0,2);
108    // mgr.makeVerbose();               // trace constructors and destructors
109    testBdd(mgr,verbosity);
110    testAdd(mgr,verbosity);
111    testAdd2(mgr,verbosity);
112    testZdd(mgr,verbosity);
113    testBdd2(mgr,verbosity);
114    testBdd3(mgr,verbosity);
115    testZdd2(mgr,verbosity);
116    testBdd4(mgr,verbosity);
117    testBdd5(mgr,verbosity);
118    if (verbosity) mgr.info();
119    return 0;
120
121} // main
122
123
124/**Function********************************************************************
125
126  Synopsis    [Test basic operators on BDDs.]
127
128  Description [Test basic operators on BDDs. The function returns void
129  because it relies on the error handling done by the interface. The
130  default error handler causes program termination.]
131
132  SideEffects [Creates BDD variables in the manager.]
133
134  SeeAlso     [testBdd2 testBdd3 testBdd4 testBdd5]
135
136******************************************************************************/
137static void
138testBdd(
139  Cudd& mgr,
140  int verbosity)
141{
142    if (verbosity) cout << "Entering testBdd\n";
143    // Create two new variables in the manager. If testBdd is called before
144    // any variable is created in mgr, then x gets index 0 and y gets index 1.
145    BDD x = mgr.bddVar();
146    BDD y = mgr.bddVar();
147
148    BDD f = x * y;
149    if (verbosity) cout << "f"; f.print(2,verbosity);
150
151    BDD g = y + !x;
152    if (verbosity) cout << "g"; g.print(2,verbosity);
153
154    if (verbosity) 
155        cout << "f and g are" << (f == !g ? "" : " not") << " complementary\n";
156    if (verbosity) 
157        cout << "f is" << (f <= g ? "" : " not") << " less than or equal to g\n";
158
159    g = f | ~g;
160    if (verbosity) cout << "g"; g.print(2,verbosity);
161
162    BDD h = f = y;
163    if (verbosity) cout << "h"; h.print(2,verbosity);
164
165    if (verbosity) cout << "x + h has " << (x+h).nodeCount() << " nodes\n";
166
167    h += x;
168    if (verbosity) cout << "h"; h.print(2,verbosity);
169
170} // testBdd
171
172
173/**Function********************************************************************
174
175  Synopsis    [Test basic operators on ADDs.]
176
177  Description [Test basic operators on ADDs. The function returns void
178  because it relies on the error handling done by the interface. The
179  default error handler causes program termination.]
180
181  SideEffects [May create ADD variables in the manager.]
182
183  SeeAlso     [testAdd2]
184
185******************************************************************************/
186static void
187testAdd(
188  Cudd& mgr,
189  int verbosity)
190{
191    if (verbosity) cout << "Entering testAdd\n";
192    // Create two ADD variables. If we called method addVar without an
193    // argument, we would get two new indices. If testAdd is indeed called
194    // after testBdd, then those indices would be 2 and 3. By specifying the
195    // arguments, on the other hand, we avoid creating new unnecessary BDD
196    // variables.
197    ADD p = mgr.addVar(0);
198    ADD q = mgr.addVar(1);
199
200    // Test arithmetic operators.
201    ADD r = p + q;
202    if (verbosity) cout << "r"; r.print(2,verbosity);
203
204    // CUDD_VALUE_TYPE is double.
205    ADD s = mgr.constant(3.0);
206    s *= p * q;
207    if (verbosity) cout << "s"; s.print(2,verbosity);
208
209    s += mgr.plusInfinity();
210    if (verbosity) cout << "s"; s.print(2,verbosity);
211
212    // Test relational operators.
213    if (verbosity) 
214        cout << "p is" << (p <= r ? "" : " not") << " less than or equal to r\n";
215
216    // Test logical operators.
217    r = p | q;
218    if (verbosity) cout << "r"; r.print(2,verbosity);
219
220} // testAdd
221
222
223/**Function********************************************************************
224
225  Synopsis    [Test some more operators on ADDs.]
226
227  Description [Test some more operators on ADDs. The function returns void
228  because it relies on the error handling done by the interface. The
229  default error handler causes program termination.]
230
231  SideEffects [May create ADD variables in the manager.]
232
233  SeeAlso     [testAdd]
234
235******************************************************************************/
236static void
237testAdd2(
238  Cudd& mgr,
239  int verbosity)
240{
241    if (verbosity) cout << "Entering testAdd2\n";
242    // Create two ADD variables. If we called method addVar without an
243    // argument, we would get two new indices.
244    int i;
245    vector<ADD> x(2);
246    for (i = 0; i < 2; i++) {
247        x[i] = mgr.addVar(i);
248    }
249
250    // Build a probability density function: [0.1, 0.2, 0.3, 0.4].
251    ADD f0 = x[1].Ite(mgr.constant(0.2), mgr.constant(0.1));
252    ADD f1 = x[1].Ite(mgr.constant(0.4), mgr.constant(0.3));
253    ADD f  = x[0].Ite(f1, f0);
254    if (verbosity) cout << "f"; f.print(2,verbosity);
255
256    // Compute the entropy.
257    ADD l = f.Log();
258    if (verbosity) cout << "l"; l.print(2,verbosity);
259    ADD r = f * l;
260    if (verbosity) cout << "r"; r.print(2,verbosity);
261
262    ADD e = r.MatrixMultiply(mgr.constant(-1.0/log(2.0)),x);
263    if (verbosity) cout << "e"; e.print(2,verbosity);
264
265} // testAdd2
266
267
268/**Function********************************************************************
269
270  Synopsis    [Test basic operators on ZDDs.]
271
272  Description [Test basic operators on ZDDs. The function returns void
273  because it relies on the error handling done by the interface. The
274  default error handler causes program termination.]
275
276  SideEffects [May create ZDD variables in the manager.]
277
278  SeeAlso     [testZdd2]
279
280******************************************************************************/
281static void
282testZdd(
283  Cudd& mgr,
284  int verbosity)
285{
286    if (verbosity) cout << "Entering testZdd\n";
287    ZDD v = mgr.zddVar(0);
288    ZDD w = mgr.zddVar(1);
289
290    ZDD s = v + w;
291    if (verbosity) cout << "s"; s.print(2,verbosity);
292
293    if (verbosity) cout << "v is" << (v < s ? "" : " not") << " less than s\n";
294
295    s -= v;
296    if (verbosity) cout << "s"; s.print(2,verbosity);
297
298} // testZdd
299
300
301/**Function********************************************************************
302
303  Synopsis    [Test vector operators on BDDs.]
304
305  Description [Test vector operators on BDDs. The function returns void
306  because it relies on the error handling done by the interface. The
307  default error handler causes program termination.]
308
309  SideEffects [May create BDD variables in the manager.]
310
311  SeeAlso     [testBdd testBdd3 testBdd4 testBdd5]
312
313******************************************************************************/
314static void
315testBdd2(
316  Cudd& mgr,
317  int verbosity)
318{
319    if (verbosity) cout << "Entering testBdd2\n";
320    vector<BDD> x(4);
321    for (int i = 0; i < 4; i++) {
322        x[i] = mgr.bddVar(i);
323    }
324
325    // Create the BDD for the Achilles' Heel function.
326    BDD p1 = x[0] * x[2];
327    BDD p2 = x[1] * x[3];
328    BDD f = p1 + p2;
329    const char* inames[] = {"x0", "x1", "x2", "x3"};
330    if (verbosity) {
331        cout << "f"; f.print(4,verbosity);
332        cout << "Irredundant cover of f:" << endl; f.PrintCover();
333        cout << "Number of minterms (arbitrary precision): "; f.ApaPrintMinterm(4);
334        cout << "Number of minterms (extended precision):  "; f.EpdPrintMinterm(4);
335        cout << "Two-literal clauses of f:" << endl;
336        f.PrintTwoLiteralClauses((char **)inames); cout << endl;
337    }
338
339    vector<BDD> vect = f.CharToVect();
340    if (verbosity) {
341        for (size_t i = 0; i < vect.size(); i++) {
342            cout << "vect[" << i << "]" << endl; vect[i].PrintCover();
343        }
344    }
345
346    // v0,...,v3 suffice if testBdd2 is called before testBdd3.
347    if (verbosity) {
348        const char* onames[] = {"v0", "v1", "v2", "v3", "v4", "v5"};
349        mgr.DumpDot(vect, (char **)inames,(char **)onames);
350    }
351
352} // testBdd2
353
354
355/**Function********************************************************************
356
357  Synopsis    [Test additional operators on BDDs.]
358
359  Description [Test additional operators on BDDs. The function returns
360  void because it relies on the error handling done by the
361  interface. The default error handler causes program termination.]
362
363  SideEffects [May create BDD variables in the manager.]
364
365  SeeAlso     [testBdd testBdd2 testBdd4 testBdd5]
366
367******************************************************************************/
368static void
369testBdd3(
370  Cudd& mgr,
371  int verbosity)
372{
373    if (verbosity) cout << "Entering testBdd3\n";
374    vector<BDD> x(6);
375    for (int i = 0; i < 6; i++) {
376        x[i] = mgr.bddVar(i);
377    }
378
379    BDD G = x[4] + !x[5];
380    BDD H = x[4] * x[5];
381    BDD E = x[3].Ite(G,!x[5]);
382    BDD F = x[3] + !H;
383    BDD D = x[2].Ite(F,!H);
384    BDD C = x[2].Ite(E,!F);
385    BDD B = x[1].Ite(C,!F);
386    BDD A = x[0].Ite(B,!D);
387    BDD f = !A;
388    if (verbosity) cout << "f"; f.print(6,verbosity);
389
390    BDD f1 = f.RemapUnderApprox(6);
391    if (verbosity) cout << "f1"; f1.print(6,verbosity);
392    if (verbosity) 
393        cout << "f1 is" << (f1 <= f ? "" : " not") << " less than or equal to f\n";
394
395    BDD g;
396    BDD h;
397    f.GenConjDecomp(&g,&h);
398    if (verbosity) {
399        cout << "g"; g.print(6,verbosity);
400        cout << "h"; h.print(6,verbosity);
401        cout << "g * h " << (g * h == f ? "==" : "!=") << " f\n";
402    }
403
404} // testBdd3
405
406
407/**Function********************************************************************
408
409  Synopsis    [Test cover manipulation with BDDs and ZDDs.]
410
411  Description [Test cover manipulation with BDDs and ZDDs.  The
412  function returns void because it relies on the error handling done by
413  the interface.  The default error handler causes program
414  termination.  This function builds the BDDs for a transformed adder:
415  one in which the inputs are transformations of the original
416  inputs. It then creates ZDDs for the covers from the BDDs.]
417
418  SideEffects [May create BDD and ZDD variables in the manager.]
419
420  SeeAlso     [testZdd]
421
422******************************************************************************/
423static void
424testZdd2(
425  Cudd& mgr,
426  int verbosity)
427{
428    if (verbosity) cout << "Entering testZdd2\n";
429    int N = 3;                  // number of bits
430    // Create variables.
431    vector<BDD> a(N);
432    vector<BDD> b(N);
433    vector<BDD> c(N+1);
434    for (int i = 0; i < N; i++) {
435        a[N-1-i] = mgr.bddVar(2*i);
436        b[N-1-i] = mgr.bddVar(2*i+1);
437    }
438    c[0] = mgr.bddVar(2*N);
439    // Build functions.
440    vector<BDD> s(N);
441    for (int i = 0; i < N; i++) {
442        s[i] = a[i].Xnor(c[i]);
443        c[i+1] = a[i].Ite(b[i],c[i]);
444    }
445
446    // Create array of outputs and print it.
447    vector<BDD> p(N+1);
448    for (int i = 0; i < N; i++) {
449        p[i] = s[i];
450    }
451    p[N] = c[N];
452    if (verbosity) {
453        for (size_t i = 0; i < p.size(); i++) {
454            cout << "p[" << i << "]"; p[i].print(2*N+1,verbosity);
455        }
456    }
457    const char* onames[] = {"s0", "s1", "s2", "c3"};
458    if (verbosity) {
459        const char* inames[] = {"a2", "b2", "a1", "b1", "a0", "b0", "c0"};
460        mgr.DumpDot(p, (char **)inames,(char **)onames);
461    }
462
463    // Create ZDD variables and build ZDD covers from BDDs.
464    mgr.zddVarsFromBddVars(2);
465    vector<ZDD> z(N+1);
466    for (int i = 0; i < N+1; i++) {
467        ZDD temp;
468        BDD dummy = p[i].zddIsop(p[i],&temp);
469        z[i] = temp;
470    }
471
472    // Print out covers.
473    if (verbosity) {
474        for (size_t i = 0; i < z.size(); i++) {
475            cout << "z[" << i << "]"; z[i].print(4*N+2,verbosity);
476        }
477        for (size_t i = 0; i < z.size(); i++) {
478            cout << "z[" << i << "]\n"; z[i].PrintCover();
479        }
480        const char* znames[] = {"a2+", "a2-", "b2+", "b2-", "a1+", "a1-", "b1+",
481                                "b1-", "a0+", "a0-", "b0+", "b0-", "c0+", "c0-"};
482        mgr.DumpDot(z, (char **)znames,(char **)onames);
483    }
484
485} // testZdd2
486
487
488/**Function********************************************************************
489
490  Synopsis    [Test transfer between BDD managers.]
491
492  Description [Test transfer between BDD managers.  The
493  function returns void because it relies on the error handling done by
494  the interface.  The default error handler causes program
495  termination.]
496
497  SideEffects [May create BDD variables in the manager.]
498
499  SeeAlso     [testBdd testBdd2 testBdd3 testBdd5]
500
501******************************************************************************/
502static void
503testBdd4(
504  Cudd& mgr,
505  int verbosity)
506{
507    if (verbosity) cout << "Entering testBdd4\n";
508    BDD x = mgr.bddVar(0);
509    BDD y = mgr.bddVar(1);
510    BDD z = mgr.bddVar(2);
511
512    BDD f = !x * !y * !z + x * y;
513    if (verbosity) cout << "f"; f.print(3,verbosity);
514
515    Cudd otherMgr(0,0);
516    BDD g = f.Transfer(otherMgr);
517    if (verbosity) cout << "g"; g.print(3,verbosity);
518
519    BDD h = g.Transfer(mgr);
520    if (verbosity) 
521        cout << "f and h are" << (f == h ? "" : " not") << " identical\n";
522
523} // testBdd4
524
525
526
527/**Function********************************************************************
528
529  Synopsis    [Test maximal expansion of cubes.]
530
531  Description [Test maximal expansion of cubes.  The function returns
532  void because it relies on the error handling done by the interface.
533  The default error handler causes program termination.]
534
535  SideEffects [May create BDD variables in the manager.]
536
537  SeeAlso     [testBdd testBdd2 testBdd3 testBdd4]
538
539******************************************************************************/
540static void
541testBdd5(
542  Cudd& mgr,
543  int verbosity)
544{
545    if (verbosity) cout << "Entering testBdd5\n";
546    vector<BDD> x;
547    x.reserve(4);
548    for (int i = 0; i < 4; i++) {
549        x.push_back(mgr.bddVar(i));
550    }
551    const char* inames[] = {"a", "b", "c", "d"};
552    BDD f = (x[1] & x[3]) | (x[0] & !x[2] & x[3]) | (!x[0] & x[1] & !x[2]);
553    BDD lb = x[1] & !x[2] & x[3];
554    BDD ub = x[3];
555    BDD primes = lb.MaximallyExpand(ub,f);
556    assert(primes == (x[1] & x[3]));
557    BDD lprime = primes.LargestPrimeUnate(lb);
558    assert(lprime == primes);
559    if (verbosity) {
560      const char * onames[] = {"lb", "ub", "f", "primes", "lprime"};
561        vector<BDD> z;
562        z.reserve(5);
563        z.push_back(lb);
564        z.push_back(ub);
565        z.push_back(f);
566        z.push_back(primes);
567        z.push_back(lprime);
568        mgr.DumpDot(z, (char **)inames, (char **)onames);
569        cout << "primes(1)"; primes.print(4,verbosity);
570    }
571
572    lb = !x[0] & x[2] & x[3];
573    primes = lb.MaximallyExpand(ub,f);
574    assert(primes == mgr.bddZero());
575    if (verbosity) {
576        cout << "primes(2)"; primes.print(4,verbosity);
577    }
578
579    lb = x[0] & !x[2] & x[3];
580    primes = lb.MaximallyExpand(ub,f);
581    assert(primes == lb);
582    lprime = primes.LargestPrimeUnate(lb);
583    assert(lprime == primes);
584    if (verbosity) {
585        cout << "primes(3)"; primes.print(4,verbosity);
586    }
587
588    lb = !x[0] & x[1] & !x[2] & x[3];
589    ub = mgr.bddOne();
590    primes = lb.MaximallyExpand(ub,f);
591    assert(primes == ((x[1] & x[3]) | (!x[0] & x[1] & !x[2])));
592    lprime = primes.LargestPrimeUnate(lb);
593    assert(lprime == (x[1] & x[3]));
594    if (verbosity) {
595        cout << "primes(4)"; primes.print(4,1); primes.PrintCover();
596    }
597
598    ub = !x[0] & x[3];
599    primes = lb.MaximallyExpand(ub,f);
600    assert(primes == (!x[0] & x[1] & x[3]));
601    lprime = primes.LargestPrimeUnate(lb);
602    assert(lprime == primes);
603    if (verbosity) {
604        cout << "primes(5)"; primes.print(4,verbosity);
605    }
606
607} // testBdd5
Note: See TracBrowser for help on using the repository browser.