1 #include "satencoder.h"
8 #include "tableentry.h"
13 Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint) {
14 ASSERT(constraint->predicate->type == 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 = encodeConstraintSATEncoder(constraint->undefStatus);
27 HSIteratorTableEntry *iterator = table->entries->iterator();
29 while (iterator->hasNext()) {
30 TableEntry *entry = iterator->next();
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 = inputs->get(j);
38 carray[j] = getElementValueConstraint(el, entry->inputs[j]);
43 switch (undefStatus) {
45 row = constraintAND(cnf, inputNum, carray);
47 case FLAGFORCEUNDEFINED: {
48 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintNegate(undefConst)));
49 if (generateNegation == (entry->output != 0)) {
52 row = constraintAND(cnf, inputNum, carray);
58 constraints[i++] = row;
65 Edge result = generateNegation ? constraintNegate(constraintOR(cnf, i, constraints))
66 : constraintOR(cnf, i, constraints);
70 Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint) {
72 model_print("Enumeration Table Predicate ...\n");
74 ASSERT(constraint->predicate->type == 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(inputs->get(i));
82 PredicateTable *predicate = (PredicateTable *)constraint->predicate;
83 switch (predicate->undefinedbehavior) {
85 case FLAGFORCEUNDEFINED:
86 return encodeEnumEntriesTablePredicateSATEncoder(constraint);
90 bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
91 uint numDomains = predicate->table->domains.getSize();
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 = predicate->table->domains.get(i);
101 vals[i] = set->getElement(indices[i]);
103 bool hasOverflow = false;
104 Edge undefConstraint = 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) {
115 for (uint i = 0; i < numDomains; i++) {
116 Element *elem = constraint->inputs.get(i);
117 carray[i] = getElementValueConstraint(elem, vals[i]);
120 switch (predicate->undefinedbehavior) {
121 case UNDEFINEDSETSFLAG:
123 clause = constraintAND(cnf, numDomains, carray);
125 addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), undefConstraint) );
128 case FLAGIFFUNDEFINED:
130 clause = constraintAND(cnf, numDomains, carray);
131 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint)));
133 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(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 = predicate->table->domains.get(i);
155 if (index < set->getSize()) {
156 vals[i] = set->getElement(index);
161 vals[i] = set->getElement(0);
165 Edge result = E_NULL;
166 ASSERT(getSizeVectorEdge(clauses) != 0);
167 result = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
169 result = constraintOR2(cnf, result, undefConstraint);
171 if (generateNegation) {
172 ASSERT(!hasOverflow);
173 result = constraintNegate(result);
175 deleteVectorEdge(clauses);
179 void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(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();
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(el, entry->inputs[j]);
197 Edge output = getElementValueConstraint(func, entry->output);
199 switch (undefStatus ) {
200 case IGNOREBEHAVIOR: {
201 row = constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output);
204 case FLAGFORCEUNDEFINED: {
205 Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
206 row = constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst)));
213 constraints[i++] = row;
216 addConstraintCNF(cnf, constraintAND(cnf, size, constraints));
219 void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc) {
221 model_print("Enumeration Table functions ...\n");
223 ASSERT(elemFunc->function->type == 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(elem);
231 FunctionTable *function = (FunctionTable *)elemFunc->function;
232 switch (function->undefBehavior) {
234 case FLAGFORCEUNDEFINED:
235 return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc);
240 uint numDomains = function->table->domains.getSize();
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 = function->table->domains.get(i);
250 vals[i] = set->getElement(indices[i]);
253 Edge undefConstraint = 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(elem, vals[i]);
265 carray[numDomains] = getElementValueConstraint(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(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
275 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
279 case FLAGIFFUNDEFINED: {
281 clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
282 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint) ));
284 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(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 = function->table->domains.get(i);
305 if (index < set->getSize()) {
306 vals[i] = set->getElement(index);
311 vals[i] = set->getElement(0);
315 if (getSizeVectorEdge(clauses) == 0) {
316 deleteVectorEdge(clauses);
319 Edge cor = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
320 addConstraintCNF(cnf, cor);
321 deleteVectorEdge(clauses);