source: vis_dev/glu-2.3/src/mdd/mdd_ineq_s.c @ 50

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

library glu 2.3
File size: 3.0 KB
Line 
1/*
2 * $Id: mdd_ineq_s.c,v 1.4 2002/08/27 16:30:26 fabio Exp $
3 *
4 */
5
6#include "mdd.h"
7
8static int
9mdd_is_care_bit(
10  mvar_type mvar,
11  int index)
12{
13    return ( getbit( ( (int) pow(2.0, (double)mvar.encode_length) ) - mvar.values, mvar.encode_length-index-1));
14}
15
16
17mdd_t *
18mdd_ineq_template_s(
19  mdd_manager *mgr,
20  int mvar1,
21  int mvar2,
22  int zero_then_val /* J in Tim's thesis */,
23  int one_else_val  /* K */,
24  int bottom_val    /* A and B */)
25{
26    mvar_type x, y;
27    bvar_type bx, by;
28    mdd_t *one_top, *zero_top, *zero_then, *one_else,
29          *one_top_else = mdd_one(mgr);
30    mdd_t *one_top_then = mdd_one(mgr);
31    mdd_t *zero_top_else = mdd_one(mgr);
32    mdd_t *zero_top_then = mdd_one(mgr);
33    mdd_t *compare;
34    int i;
35
36    array_t *mvar_list = mdd_ret_mvar_list(mgr);
37    array_t *bvar_list = mdd_ret_bvar_list(mgr);
38
39    if (zero_then_val == 0) 
40        zero_then = mdd_zero(mgr);
41    else 
42        zero_then = mdd_one(mgr);
43
44
45     if (one_else_val == 0) 
46         one_else = mdd_zero(mgr);
47     else 
48         one_else = mdd_one(mgr);
49
50    if (bottom_val == 0) {
51        one_top = mdd_zero(mgr);
52        zero_top = mdd_zero(mgr);
53    }
54    else {
55        one_top = mdd_one(mgr);
56        zero_top = mdd_one(mgr);
57    }
58
59
60    x = array_fetch(mvar_type, mvar_list, mvar1);
61    y = array_fetch(mvar_type, mvar_list, mvar2);
62
63    if (x.values != y.values) 
64        fail("mdd_ineq: 2 mvars have incompatible value ranges\n");
65
66    if (x.status == MDD_BUNDLED) {
67        (void) fprintf(stderr, 
68                "\nWarning: mdd_ineq, bundled variable %s is used\n", x.name);
69        fail("");
70    }
71
72    if (y.status == MDD_BUNDLED) {
73        (void) fprintf(stderr,
74                "\nWarning: mdd_ineq, bundled variable %s is used\n", y.name);
75        fail("");
76    }
77
78
79    for (i=(x.encode_length-1); i>=0; i--) {
80
81        bx = mdd_ret_bvar(&x, i, bvar_list);
82        by = mdd_ret_bvar(&y, i, bvar_list);
83
84        mdd_free(zero_top_else);
85        zero_top_else = mdd_ite(by.node, zero_then, zero_top, 1, 1, 1);
86        mdd_free(zero_top_then);
87        zero_top_then = mdd_ite(by.node, zero_top,  one_else, 1, 1, 1);
88
89        if (mdd_is_care_bit(x,i) == 0) {
90
91                mdd_free(one_top_else);
92                one_top_else = mdd_ite(by.node, zero_then, zero_top, 1, 1, 1);
93                mdd_free(one_top_then);
94                one_top_then = mdd_ite(by.node, one_top, one_else, 1, 1, 1);
95
96                mdd_free(one_top);
97
98                one_top = mdd_ite(bx.node, one_top_then, one_top_else, 1, 1, 1);
99        }
100
101        mdd_free(zero_top);
102        zero_top = mdd_ite(bx.node, zero_top_then, zero_top_else, 1, 1, 1);
103
104    }
105
106    mdd_free(zero_then);
107    mdd_free(one_else);
108
109    mdd_free(zero_top_else);
110    mdd_free(zero_top_then);
111    mdd_free(one_top_else);
112    mdd_free(one_top_then);
113
114    mdd_free(zero_top);
115
116    compare = mdd_eq(mgr, mvar1, mvar2);
117
118    if  ( ( bdd_equal(compare, one_top) == 0) && (zero_then_val == 0) && (one_else_val == 0) && (bottom_val == 1) )
119      printf("Error \n"); 
120
121    mdd_free(compare);
122   
123    return one_top;
124}
125
126/*---------------------------------------------------------------------------*/
127/* Static function prototypes                                                */
128/*---------------------------------------------------------------------------*/
129
130
Note: See TracBrowser for help on using the repository browser.