1c5e58cb425baa1adce1b993c358309e7563689f
[satune.git] / src / Backend / satfunctableencoder.cc
1 #include "satencoder.h"
2 #include "common.h"
3 #include "function.h"
4 #include "ops.h"
5 #include "predicate.h"
6 #include "boolean.h"
7 #include "table.h"
8 #include "tableentry.h"
9 #include "set.h"
10 #include "element.h"
11 #include "common.h"
12
13 Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
14         ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
15         UndefinedBehavior undefStatus = ((PredicateTable *)constraint->predicate)->undefinedbehavior;
16         ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
17         Table *table = ((PredicateTable *)constraint->predicate)->table;
18         FunctionEncodingType encType = constraint->encoding.type;
19         Array<Element *> *inputs = &constraint->inputs;
20         uint inputNum = inputs->getSize();
21         uint size = table->entries->getSize();
22         bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
23         Edge constraints[size];
24         Edge undefConst = This->encodeConstraintSATEncoder(constraint->undefStatus);
25         printCNF(undefConst);
26         model_print("**\n");
27         HSIteratorTableEntry *iterator = table->entries->iterator();
28         uint i = 0;
29         while (iterator->hasNext()) {
30                 TableEntry *entry = iterator->next();
31                 if (generateNegation == (entry->output != 0) && undefStatus == IGNOREBEHAVIOR) {
32                         //Skip the irrelevant entries
33                         continue;
34                 }
35                 Edge carray[inputNum];
36                 for (uint j = 0; j < inputNum; j++) {
37                         Element *el = inputs->get(j);
38                         carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
39                         printCNF(carray[j]);
40                         model_print("\n");
41                 }
42                 Edge row;
43                 switch (undefStatus) {
44                 case IGNOREBEHAVIOR:
45                         row = constraintAND(This->cnf, inputNum, carray);
46                         break;
47                 case FLAGFORCEUNDEFINED: {
48                         addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray),  constraintNegate(undefConst)));
49                         if (generateNegation == (entry->output != 0)) {
50                                 continue;
51                         }
52                         row = constraintAND(This->cnf, inputNum, carray);
53                         break;
54                 }
55                 default:
56                         ASSERT(0);
57                 }
58                 constraints[i++] = row;
59                 printCNF(row);
60
61                 model_print("\n\n");
62         }
63         delete iterator;
64         ASSERT(i != 0);
65         Edge result = generateNegation ? constraintNegate(constraintOR(This->cnf, i, constraints))
66                                                                 : constraintOR(This->cnf, i, constraints);
67         printCNF(result);
68         return result;
69 }
70 Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
71 #ifdef TRACE_DEBUG
72         model_print("Enumeration Table Predicate ...\n");
73 #endif
74         ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
75         //First encode children
76         Array<Element *> *inputs = &constraint->inputs;
77         uint inputNum = inputs->getSize();
78         //Encode all the inputs first ...
79         for (uint i = 0; i < inputNum; i++) {
80                 encodeElementSATEncoder(This, inputs->get(i));
81         }
82         PredicateTable *predicate = (PredicateTable *)constraint->predicate;
83         switch (predicate->undefinedbehavior) {
84         case IGNOREBEHAVIOR:
85         case FLAGFORCEUNDEFINED:
86                 return encodeEnumEntriesTablePredicateSATEncoder(This, constraint);
87         default:
88                 break;
89         }
90         bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
91         uint numDomains = predicate->table->domains.getSize();
92
93         VectorEdge *clauses = allocDefVectorEdge();
94
95         uint indices[numDomains];       //setup indices
96         bzero(indices, sizeof(uint) * numDomains);
97
98         uint64_t vals[numDomains];//setup value array
99         for (uint i = 0; i < numDomains; i++) {
100                 Set *set = predicate->table->domains.get(i);
101                 vals[i] = set->getElement(indices[i]);
102         }
103         bool hasOverflow = false;
104         Edge undefConstraint = This->encodeConstraintSATEncoder(constraint->undefStatus);
105         printCNF(undefConstraint);
106         bool notfinished = true;
107         while (notfinished) {
108                 Edge carray[numDomains];
109                 TableEntry *tableEntry = predicate->table->getTableEntry(vals, numDomains);
110                 bool isInRange = tableEntry != NULL;
111                 if (!isInRange && !hasOverflow) {
112                         hasOverflow = true;
113                 }
114                 Edge clause;
115                 for (uint i = 0; i < numDomains; i++) {
116                         Element *elem = constraint->inputs.get(i);
117                         carray[i] = getElementValueConstraint(This, elem, vals[i]);
118                 }
119
120                 switch (predicate->undefinedbehavior) {
121                 case UNDEFINEDSETSFLAG:
122                         if (isInRange) {
123                                 clause = constraintAND(This->cnf, numDomains, carray);
124                         } else {
125                                 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint) );
126                         }
127                         break;
128                 case FLAGIFFUNDEFINED:
129                         if (isInRange) {
130                                 clause = constraintAND(This->cnf, numDomains, carray);
131                                 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint)));
132                         } else {
133                                 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint) );
134                         }
135                         break;
136
137                 default:
138                         ASSERT(0);
139                 }
140
141                 if (isInRange) {
142 #ifdef TRACE_DEBUG
143                         model_print("added clause in predicate table enumeration ...\n");
144                         printCNF(clause);
145                         model_print("\n");
146 #endif
147                         pushVectorEdge(clauses, clause);
148                 }
149
150                 notfinished = false;
151                 for (uint i = 0; i < numDomains; i++) {
152                         uint index = ++indices[i];
153                         Set *set = predicate->table->domains.get(i);
154
155                         if (index < set->getSize()) {
156                                 vals[i] = set->getElement(index);
157                                 notfinished = true;
158                                 break;
159                         } else {
160                                 indices[i] = 0;
161                                 vals[i] = set->getElement(0);
162                         }
163                 }
164         }
165         Edge result = E_NULL;
166         ASSERT(getSizeVectorEdge(clauses) != 0);
167         result = constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
168         if (hasOverflow) {
169                 result = constraintOR2(This->cnf, result, undefConstraint);
170         }
171         if (generateNegation) {
172                 ASSERT(!hasOverflow);
173                 result = constraintNegate(result);
174         }
175         deleteVectorEdge(clauses);
176         return result;
177 }
178
179 void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction *func) {
180         UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior;
181         ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
182         Array<Element *> *elements = &func->inputs;
183         Table *table = ((FunctionTable *) (func->function))->table;
184         uint size = table->entries->getSize();
185         Edge constraints[size];
186         HSIteratorTableEntry *iterator = table->entries->iterator();
187         uint i = 0;
188         while (iterator->hasNext()) {
189                 TableEntry *entry = iterator->next();
190                 ASSERT(entry != NULL);
191                 uint inputNum = elements->getSize();
192                 Edge carray[inputNum];
193                 for (uint j = 0; j < inputNum; j++) {
194                         Element *el = elements->get(j);
195                         carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
196                 }
197                 Edge output = getElementValueConstraint(This, (Element *)func, entry->output);
198                 Edge row;
199                 switch (undefStatus ) {
200                 case IGNOREBEHAVIOR: {
201                         row = constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output);
202                         break;
203                 }
204                 case FLAGFORCEUNDEFINED: {
205                         Edge undefConst = This->encodeConstraintSATEncoder(func->overflowstatus);
206                         row = constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
207                         break;
208                 }
209                 default:
210                         ASSERT(0);
211
212                 }
213                 constraints[i++] = row;
214         }
215         delete iterator;
216         addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
217 }
218
219 void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *elemFunc) {
220 #ifdef TRACE_DEBUG
221         model_print("Enumeration Table functions ...\n");
222 #endif
223         ASSERT(GETFUNCTIONTYPE(elemFunc->function) == TABLEFUNC);
224         //First encode children
225         Array<Element *> *elements = &elemFunc->inputs;
226         for (uint i = 0; i < elements->getSize(); i++) {
227                 Element *elem = elements->get(i);
228                 encodeElementSATEncoder(This, elem);
229         }
230
231         FunctionTable *function = (FunctionTable *)elemFunc->function;
232         switch (function->undefBehavior) {
233         case IGNOREBEHAVIOR:
234         case FLAGFORCEUNDEFINED:
235                 return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
236         default:
237                 break;
238         }
239
240         uint numDomains = function->table->domains.getSize();
241
242         VectorEdge *clauses = allocDefVectorEdge();     // Setup array of clauses
243
244         uint indices[numDomains];       //setup indices
245         bzero(indices, sizeof(uint) * numDomains);
246
247         uint64_t vals[numDomains];//setup value array
248         for (uint i = 0; i < numDomains; i++) {
249                 Set *set = function->table->domains.get(i);
250                 vals[i] = set->getElement(indices[i]);
251         }
252
253         Edge undefConstraint = This->encodeConstraintSATEncoder(elemFunc->overflowstatus);
254         bool notfinished = true;
255         while (notfinished) {
256                 Edge carray[numDomains + 1];
257                 TableEntry *tableEntry = function->table->getTableEntry(vals, numDomains);
258                 bool isInRange = tableEntry != NULL;
259                 ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
260                 for (uint i = 0; i < numDomains; i++) {
261                         Element *elem = elemFunc->inputs.get(i);
262                         carray[i] = getElementValueConstraint(This, elem, vals[i]);
263                 }
264                 if (isInRange) {
265                         carray[numDomains] = getElementValueConstraint(This, (Element *)elemFunc, tableEntry->output);
266                 }
267
268                 Edge clause;
269                 switch (function->undefBehavior) {
270                 case UNDEFINEDSETSFLAG: {
271                         if (isInRange) {
272                                 //FIXME: Talk to Brian, It should be IFF not only IMPLY. --HG
273                                 clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
274                         } else {
275                                 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint));
276                         }
277                         break;
278                 }
279                 case FLAGIFFUNDEFINED: {
280                         if (isInRange) {
281                                 clause = constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
282                                 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint) ));
283                         } else {
284                                 addConstraintCNF(This->cnf,constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), undefConstraint));
285                         }
286                         break;
287                 }
288                 default:
289                         ASSERT(0);
290                 }
291                 if (isInRange) {
292 #ifdef TRACE_DEBUG
293                         model_print("added clause in function table enumeration ...\n");
294                         printCNF(clause);
295                         model_print("\n");
296 #endif
297                         pushVectorEdge(clauses, clause);
298                 }
299
300                 notfinished = false;
301                 for (uint i = 0; i < numDomains; i++) {
302                         uint index = ++indices[i];
303                         Set *set = function->table->domains.get(i);
304
305                         if (index < set->getSize()) {
306                                 vals[i] = set->getElement(index);
307                                 notfinished = true;
308                                 break;
309                         } else {
310                                 indices[i] = 0;
311                                 vals[i] = set->getElement(0);
312                         }
313                 }
314         }
315         if (getSizeVectorEdge(clauses) == 0) {
316                 deleteVectorEdge(clauses);
317                 return;
318         }
319         Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
320         addConstraintCNF(This->cnf, cor);
321         deleteVectorEdge(clauses);
322 }