source: vis_dev/glu-2.3/src/mdd/mdd_case.c @ 102

Last change on this file since 102 was 13, checked in by cecile, 13 years ago

library glu 2.3

File size: 4.2 KB
Line 
1#include "mdd.h"
2
3/*
4 * MDD Package
5 *
6 * $Id: mdd_case.c,v 1.10 2002/08/24 20:44:27 fabio Exp $
7 *
8 * Author: Timothy Kam
9 *
10 * Copyright 1992 by the Regents of the University of California.
11 *
12 * All rights reserved.  Permission to use, copy, modify and distribute
13 * this software is hereby granted, provided that the above copyright
14 * notice and this permission notice appear in all copies.  This software
15 * is made available as is, with no warranties.
16 */
17
18mdd_t *
19mdd_case(
20  mdd_manager *mgr,
21  int mvar,
22  array_t *child_list)
23{
24    mvar_type mv;
25    mdd_t *mnode;
26    mdd_t *tmp;
27    array_t *mvar_list = mdd_ret_mvar_list(mgr);
28
29    mv = array_fetch(mvar_type, mvar_list, mvar);
30
31    if (mv.values != array_n(child_list)) 
32        fail("mdd_case: mvar.values different from length of child_list\n");
33
34    if (mv.status == MDD_BUNDLED) {
35        (void) fprintf(stderr, 
36        "\nmdd_andsmooth: bundled variable %s used\n",mv.name);
37        fail("");
38    }
39
40    if (mv.values == 1) {
41        tmp = array_fetch(mdd_t *, child_list, 0);
42        mnode = mdd_dup(tmp);
43    }
44    else {
45        mnode = mdd_encode(mgr, child_list, &mv, mv.encode_length-1);
46    }
47    return mnode;
48}
49
50
51mdd_t *
52mdd_encode(
53  mdd_manager *mgr,
54  array_t *child_list,
55  mvar_type *mv_ptr,
56  int index)
57{
58    array_t *new_child_list;
59    int i;
60    int child_count = 0;
61    int q = array_n(child_list);
62    bvar_type bv;
63    mdd_t *f, *g, *h, *t;
64    mdd_t *one, *zero;
65    array_t *bvar_list;
66
67    if (q == 1) {
68        f =  array_fetch(mdd_t *, child_list, 0);
69        h = mdd_dup(f);
70        if (!mdd_is_tautology(f,1) && !mdd_is_tautology(f,0)) mdd_free(f);
71        return h;
72    }
73    one = mdd_one(mgr);
74    zero = mdd_zero(mgr);
75    bvar_list = mdd_ret_bvar_list(mgr);
76
77    new_child_list = array_alloc(mdd_t *, 0);
78
79    bv = mdd_ret_bvar(mv_ptr, index, bvar_list);
80
81    for (i=0; i<(q/2); i++) {
82
83        f = mdd_dup(bv.node);
84        h = array_fetch(mdd_t *, child_list, child_count++);
85        g = array_fetch(mdd_t *, child_list, child_count++);
86#if USE_ITE
87#if BYPASS
88        /* bypasses cases       */
89        /* 1  = ite(F,1,1)      */
90        /* 0  = ite(F,0,0)      */
91        /* F  = ite(F,1,0)      */
92        /* !F = ite(F,0,1)      */
93        /* G  = ite(F,G,G)      */
94        if (mdd_is_tautology(g,0) && mdd_is_tautology(h,0)) {
95            array_insert_last(mdd_t *, new_child_list, zero);
96        }
97        else if (mdd_is_tautology(g,0) && mdd_is_tautology(h,1)) {
98            t = mdd_not(f);
99            array_insert_last(mdd_t *, new_child_list, t);
100        }
101        else if (mdd_is_tautology(g,1) && mdd_is_tautology(h,1)) {
102            array_insert_last(mdd_t *, new_child_list, one);
103        }
104        else if (mdd_is_tautology(g,1) && mdd_is_tautology(h,0)) {
105            t = mdd_dup(f);
106            array_insert_last(mdd_t *, new_child_list, t);
107        }
108        else if (mdd_equal(f,g)) {
109            t = mdd_dup(f);
110            array_insert_last(mdd_t *, new_child_list, t);
111        }
112        else {
113            t = mdd_ite(f, g, h, 1, 1, 1);
114            array_insert_last(mdd_t *, new_child_list, t);
115        }
116        if (!mdd_is_tautology(g,1) && !mdd_is_tautology(g,0)) mdd_free(g);
117        if (!mdd_is_tautology(h,1) && !mdd_is_tautology(h,0)) mdd_free(h);
118#else
119        t = mdd_ite(f, g, h, 1, 1, 1);
120        if (!mdd_is_tautology(g,1) && !mdd_is_tautology(g,0)) mdd_free(g);
121        if (!mdd_is_tautology(h,1) && !mdd_is_tautology(h,0)) mdd_free(h);
122        array_insert_last(mdd_t *, new_child_list, t);
123#endif
124#else
125        a1 = mdd_and(f,g,1,1);
126        if (!mdd_is_tautology(g,1) && !mdd_is_tautology(g,0)) mdd_free(g);
127        a2 = mdd_and(f,h,0,1);
128        if (!mdd_is_tautology(h,1) && !mdd_is_tautology(h,0)) mdd_free(h);
129        t = mdd_or(a1,a2,1,1);
130        /* t = mdd_or(mdd_and(f,g,1,1), mdd_and(f,h,0,1), 1, 1); */
131        if (!mdd_is_tautology(a1,1) && !mdd_is_tautology(a1,0)) mdd_free(a1);
132        if (!mdd_is_tautology(a2,1) && !mdd_is_tautology(a2,0)) mdd_free(a2);
133        array_insert_last(mdd_t *, new_child_list, t);
134#endif
135
136        mdd_free(f);
137    }
138
139    if (q & 1) { /* if q is odd */
140        t = array_fetch(mdd_t *, child_list, child_count);
141        array_insert_last(mdd_t *, new_child_list, t);
142    }
143    f =  mdd_encode(mgr, new_child_list, mv_ptr, index - 1);
144    array_free(new_child_list);
145    mdd_free(one);
146    mdd_free(zero);
147    return f;
148}
149
150
151/*---------------------------------------------------------------------------*/
152/* Static function prototypes                                                */
153/*---------------------------------------------------------------------------*/
154
155
Note: See TracBrowser for help on using the repository browser.