1 | #include "mdd.h" |
---|
2 | |
---|
3 | /* |
---|
4 | * MDD Package |
---|
5 | * |
---|
6 | * $Id: mdd_func3.c,v 1.10 2002/08/25 05:30:12 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 | |
---|
18 | mdd_t * |
---|
19 | mdd_func3( |
---|
20 | mdd_manager *mgr, |
---|
21 | int mvar1, |
---|
22 | int mvar2, |
---|
23 | int mvar3, |
---|
24 | boolean (*func3)(int, int, int)) |
---|
25 | { |
---|
26 | mvar_type x, y, z; |
---|
27 | array_t *child_list_x, *child_list_y, *child_list_z; |
---|
28 | int i, j, k; |
---|
29 | mdd_t *tx, *ty, *tz; |
---|
30 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
31 | mdd_t *one, *zero; |
---|
32 | |
---|
33 | one = mdd_one(mgr); |
---|
34 | zero = mdd_zero(mgr); |
---|
35 | |
---|
36 | x = array_fetch(mvar_type, mvar_list, mvar1); |
---|
37 | y = array_fetch(mvar_type, mvar_list, mvar2); |
---|
38 | z = array_fetch(mvar_type, mvar_list, mvar3); |
---|
39 | |
---|
40 | if (x.status == MDD_BUNDLED) { |
---|
41 | (void) fprintf(stderr, |
---|
42 | "\nWarning: mdd_func3, bundled variable %s is used\n", x.name); |
---|
43 | fail(""); |
---|
44 | } |
---|
45 | |
---|
46 | if (y.status == MDD_BUNDLED) { |
---|
47 | (void) fprintf(stderr, |
---|
48 | "\nWarning: mdd_func3, bundled variable %s is used\n", y.name); |
---|
49 | fail(""); |
---|
50 | } |
---|
51 | |
---|
52 | if (z.status == MDD_BUNDLED) { |
---|
53 | (void) fprintf(stderr, |
---|
54 | "\nWarning: mdd_func3, bundled variable %s is used\n", z.name); |
---|
55 | fail(""); |
---|
56 | } |
---|
57 | |
---|
58 | |
---|
59 | child_list_x = array_alloc(mdd_t *, 0); |
---|
60 | for (i=0; i<x.values; i++) { |
---|
61 | child_list_y = array_alloc(mdd_t *, 0); |
---|
62 | for (j=0; j<y.values; j++) { |
---|
63 | child_list_z = array_alloc(mdd_t *, 0); |
---|
64 | for (k=0; k<z.values; k++) { |
---|
65 | if (func3(i,j,k)) |
---|
66 | array_insert_last(mdd_t *, child_list_z, one); |
---|
67 | else |
---|
68 | array_insert_last(mdd_t *, child_list_z, zero); |
---|
69 | } |
---|
70 | tz = mdd_case(mgr, mvar3, child_list_z); |
---|
71 | array_insert_last(mdd_t *, child_list_y, tz); |
---|
72 | array_free(child_list_z); |
---|
73 | } |
---|
74 | ty = mdd_case(mgr, mvar2, child_list_y); |
---|
75 | array_insert_last(mdd_t *, child_list_x, ty); |
---|
76 | array_free(child_list_y); |
---|
77 | } |
---|
78 | tx = mdd_case(mgr, mvar1, child_list_x); |
---|
79 | array_free(child_list_x); |
---|
80 | |
---|
81 | mdd_free(one); |
---|
82 | mdd_free(zero); |
---|
83 | |
---|
84 | return tx; |
---|
85 | } |
---|
86 | |
---|
87 | /***** internal functions *****/ |
---|
88 | |
---|
89 | boolean |
---|
90 | eq_plus3(int x, int y, int z) |
---|
91 | { |
---|
92 | return (x == y + z); |
---|
93 | } |
---|
94 | |
---|
95 | boolean |
---|
96 | geq_plus3(int x, int y, int z) |
---|
97 | { |
---|
98 | return (x >= y + z); |
---|
99 | } |
---|
100 | |
---|
101 | boolean |
---|
102 | gt_plus3(int x, int y, int z) |
---|
103 | { |
---|
104 | return (x > y + z); |
---|
105 | } |
---|
106 | |
---|
107 | boolean |
---|
108 | leq_plus3(int x, int y, int z) |
---|
109 | { |
---|
110 | return (x <= y + z); |
---|
111 | } |
---|
112 | |
---|
113 | boolean |
---|
114 | lt_plus3(int x, int y, int z) |
---|
115 | { |
---|
116 | return (x < y + z); |
---|
117 | } |
---|
118 | |
---|
119 | boolean |
---|
120 | neq_plus3(int x, int y, int z) |
---|
121 | { |
---|
122 | return (x != y + z); |
---|
123 | } |
---|
124 | |
---|
125 | boolean |
---|
126 | eq_minus3(int x, int y, int z) |
---|
127 | { |
---|
128 | return (x == y - z); |
---|
129 | } |
---|
130 | |
---|
131 | boolean |
---|
132 | geq_minus3(int x, int y, int z) |
---|
133 | { |
---|
134 | return (x >= y - z); |
---|
135 | } |
---|
136 | |
---|
137 | boolean |
---|
138 | gt_minus3(int x, int y, int z) |
---|
139 | { |
---|
140 | return (x > y - z); |
---|
141 | } |
---|
142 | |
---|
143 | boolean |
---|
144 | leq_minus3(int x, int y, int z) |
---|
145 | { |
---|
146 | return (x <= y - z); |
---|
147 | } |
---|
148 | |
---|
149 | boolean |
---|
150 | lt_minus3(int x, int y, int z) |
---|
151 | { |
---|
152 | return (x < y - z); |
---|
153 | } |
---|
154 | |
---|
155 | boolean |
---|
156 | neq_minus3(int x, int y, int z) |
---|
157 | { |
---|
158 | return (x != y - z); |
---|
159 | } |
---|
160 | |
---|
161 | |
---|
162 | /*---------------------------------------------------------------------------*/ |
---|
163 | /* Static function prototypes */ |
---|
164 | /*---------------------------------------------------------------------------*/ |
---|
165 | |
---|
166 | |
---|