1 #include "satencoder.h"
8 #include "tableentry.h"
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 ArrayElement *inputs = &constraint->inputs;
20 uint inputNum = getSizeArrayElement(inputs);
21 uint size = getSizeHashSetTableEntry(table->entries);
22 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
23 Edge constraints[size];
24 Edge undefConst = encodeConstraintSATEncoder(This, constraint->undefStatus);
27 HSIteratorTableEntry *iterator = iteratorTableEntry(table->entries);
29 while (hasNextTableEntry(iterator)) {
30 TableEntry *entry = nextTableEntry(iterator);
31 if (generateNegation == (entry->output != 0) && undefStatus == IGNOREBEHAVIOR) {
32 //Skip the irrelevant entries
35 Edge carray[inputNum];
36 for (uint j = 0; j < inputNum; j++) {
37 Element *el = getArrayElement(inputs, j);
38 carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
43 switch (undefStatus) {
45 row = constraintAND(This->cnf, inputNum, carray);
47 case FLAGFORCEUNDEFINED: {
48 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintNegate(undefConst)));
49 if (generateNegation == (entry->output != 0)) {
52 row = constraintAND(This->cnf, inputNum, carray);
58 constraints[i++] = row;
63 deleteIterTableEntry(iterator);
65 Edge result = generateNegation ? constraintNegate(constraintOR(This->cnf, i, constraints))
66 : constraintOR(This->cnf, i, constraints);
70 Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
72 model_print("Enumeration Table Predicate ...\n");
74 ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
75 //First encode children
76 ArrayElement *inputs = &constraint->inputs;
77 uint inputNum = getSizeArrayElement(inputs);
78 //Encode all the inputs first ...
79 for (uint i = 0; i < inputNum; i++) {
80 encodeElementSATEncoder(This, getArrayElement(inputs, i));
82 PredicateTable *predicate = (PredicateTable *)constraint->predicate;
83 switch (predicate->undefinedbehavior) {
85 case FLAGFORCEUNDEFINED:
86 return encodeEnumEntriesTablePredicateSATEncoder(This, constraint);
90 bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
91 uint numDomains = getSizeArraySet(&predicate->table->domains);
93 VectorEdge *clauses = allocDefVectorEdge();
95 uint indices[numDomains]; //setup indices
96 bzero(indices, sizeof(uint) * numDomains);
98 uint64_t vals[numDomains];//setup value array
99 for (uint i = 0; i < numDomains; i++) {
100 Set *set = getArraySet(&predicate->table->domains, i);
101 vals[i] = getSetElement(set, indices[i]);
103 bool hasOverflow = false;
104 Edge undefConstraint = encodeConstraintSATEncoder (This, constraint->undefStatus);
105 printCNF(undefConstraint);
106 bool notfinished = true;
107 while (notfinished) {
108 Edge carray[numDomains];
109 TableEntry *tableEntry = getTableEntryFromTable(predicate->table, vals, numDomains);
110 bool isInRange = tableEntry != NULL;
111 if (!isInRange && !hasOverflow) {
115 for (uint i = 0; i < numDomains; i++) {
116 Element *elem = getArrayElement(&constraint->inputs, i);
117 carray[i] = getElementValueConstraint(This, elem, vals[i]);
120 switch (predicate->undefinedbehavior) {
121 case UNDEFINEDSETSFLAG:
123 clause = constraintAND(This->cnf, numDomains, carray);
125 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint) );
128 case FLAGIFFUNDEFINED:
130 clause = constraintAND(This->cnf, numDomains, carray);
131 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint)));
133 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint) );
143 model_print("added clause in predicate table enumeration ...\n");
147 pushVectorEdge(clauses, clause);
151 for (uint i = 0; i < numDomains; i++) {
152 uint index = ++indices[i];
153 Set *set = getArraySet(&predicate->table->domains, i);
155 if (index < getSetSize(set)) {
156 vals[i] = getSetElement(set, index);
161 vals[i] = getSetElement(set, 0);
165 Edge result = E_NULL;
166 ASSERT(getSizeVectorEdge(clauses) != 0);
167 result = constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
169 result = constraintOR2(This->cnf, result, undefConstraint);
171 if (generateNegation) {
172 ASSERT(!hasOverflow);
173 result = constraintNegate(result);
175 deleteVectorEdge(clauses);
179 void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction *func) {
180 UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior;
181 ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
182 ArrayElement *elements = &func->inputs;
183 Table *table = ((FunctionTable *) (func->function))->table;
184 uint size = getSizeHashSetTableEntry(table->entries);
185 Edge constraints[size];
186 HSIteratorTableEntry *iterator = iteratorTableEntry(table->entries);
188 while (hasNextTableEntry(iterator)) {
189 TableEntry *entry = nextTableEntry(iterator);
190 ASSERT(entry != NULL);
191 uint inputNum = getSizeArrayElement(elements);
192 Edge carray[inputNum];
193 for (uint j = 0; j < inputNum; j++) {
194 Element *el = getArrayElement(elements, j);
195 carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
197 Edge output = getElementValueConstraint(This, (Element *)func, entry->output);
199 switch (undefStatus ) {
200 case IGNOREBEHAVIOR: {
201 row = constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output);
204 case FLAGFORCEUNDEFINED: {
205 Edge undefConst = encodeConstraintSATEncoder(This, func->overflowstatus);
206 row = constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
213 constraints[i++] = row;
215 deleteIterTableEntry(iterator);
216 addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
219 void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *elemFunc) {
221 model_print("Enumeration Table functions ...\n");
223 ASSERT(GETFUNCTIONTYPE(elemFunc->function) == TABLEFUNC);
224 //First encode children
225 ArrayElement *elements = &elemFunc->inputs;
226 for (uint i = 0; i < getSizeArrayElement(elements); i++) {
227 Element *elem = getArrayElement( elements, i);
228 encodeElementSATEncoder(This, elem);
231 FunctionTable *function = (FunctionTable *)elemFunc->function;
232 switch (function->undefBehavior) {
234 case FLAGFORCEUNDEFINED:
235 return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
240 uint numDomains = getSizeArraySet(&function->table->domains);
242 VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
244 uint indices[numDomains]; //setup indices
245 bzero(indices, sizeof(uint) * numDomains);
247 uint64_t vals[numDomains];//setup value array
248 for (uint i = 0; i < numDomains; i++) {
249 Set *set = getArraySet(&function->table->domains, i);
250 vals[i] = getSetElement(set, indices[i]);
253 Edge undefConstraint = encodeConstraintSATEncoder(This, elemFunc->overflowstatus);
254 bool notfinished = true;
255 while (notfinished) {
256 Edge carray[numDomains + 1];
257 TableEntry *tableEntry = getTableEntryFromTable(function->table, 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 = getArrayElement(&elemFunc->inputs, i);
262 carray[i] = getElementValueConstraint(This, elem, vals[i]);
265 carray[numDomains] = getElementValueConstraint(This, (Element *)elemFunc, tableEntry->output);
269 switch (function->undefBehavior) {
270 case UNDEFINEDSETSFLAG: {
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]);
275 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint));
279 case FLAGIFFUNDEFINED: {
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) ));
284 addConstraintCNF(This->cnf,constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), undefConstraint));
293 model_print("added clause in function table enumeration ...\n");
297 pushVectorEdge(clauses, clause);
301 for (uint i = 0; i < numDomains; i++) {
302 uint index = ++indices[i];
303 Set *set = getArraySet(&function->table->domains, i);
305 if (index < getSetSize(set)) {
306 vals[i] = getSetElement(set, index);
311 vals[i] = getSetElement(set, 0);
315 if (getSizeVectorEdge(clauses) == 0) {
316 deleteVectorEdge(clauses);
319 Edge cor = constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
320 addConstraintCNF(This->cnf, cor);
321 deleteVectorEdge(clauses);