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 == SATC_IGNOREBEHAVIOR || undefStatus == SATC_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->getSize();
22 Polarity polarity = constraint->polarity;
23 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
25 polarity = negatePolarity(polarity);
26 if (undefStatus ==SATC_FLAGFORCEUNDEFINED)
27 polarity = P_BOTHTRUEFALSE;
29 Edge constraints[size];
31 SetIteratorTableEntry *iterator = table->getEntries();
33 while (iterator->hasNext()) {
34 TableEntry *entry = iterator->next();
35 if (generateNegation == (entry->output != 0) && undefStatus == SATC_IGNOREBEHAVIOR) {
36 //Skip the irrelevant entries
39 Edge carray[inputNum];
40 for (uint j = 0; j < inputNum; j++) {
41 Element *el = inputs->get(j);
42 carray[j] = getElementValueConstraint(el, polarity, entry->inputs[j]);
45 switch (undefStatus) {
46 case SATC_IGNOREBEHAVIOR:
47 row = constraintAND(cnf, inputNum, carray);
49 case SATC_FLAGFORCEUNDEFINED: {
50 Edge proxy = constraintNewVar(cnf);
51 generateProxy(cnf, constraintAND(cnf, inputNum, carray), proxy, P_BOTHTRUEFALSE);
52 Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
53 addConstraintCNF(cnf, constraintIMPLIES(cnf, proxy, constraintNegate(undefConst)));
54 if (generateNegation == (entry->output != 0)) {
63 constraints[i++] = row;
67 Edge result = generateNegation ? constraintNegate(constraintOR(cnf, i, constraints))
68 : constraintOR(cnf, i, constraints);
72 Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint) {
74 model_print("Enumeration Table Predicate ...\n");
76 ASSERT(constraint->predicate->type == TABLEPRED);
77 Polarity polarity = constraint->polarity;
79 //First encode children
80 Array<Element *> *inputs = &constraint->inputs;
81 uint inputNum = inputs->getSize();
82 //Encode all the inputs first ...
83 for (uint i = 0; i < inputNum; i++) {
84 encodeElementSATEncoder(inputs->get(i));
86 PredicateTable *predicate = (PredicateTable *)constraint->predicate;
87 switch (predicate->undefinedbehavior) {
88 case SATC_IGNOREBEHAVIOR:
89 case SATC_FLAGFORCEUNDEFINED:
90 return encodeEnumEntriesTablePredicateSATEncoder(constraint);
94 bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
95 uint numDomains = predicate->table->numDomains();
98 polarity = negatePolarity(polarity);
100 ASSERT(numDomains != 0);
101 VectorEdge *clauses = allocDefVectorEdge();
103 uint indices[numDomains]; //setup indices
104 bzero(indices, sizeof(uint) * numDomains);
106 uint64_t vals[numDomains];//setup value array
107 for (uint i = 0; i < numDomains; i++) {
108 Set *set = predicate->table->getDomain(i);
109 vals[i] = set->getElement(indices[i]);
111 bool hasOverflow = false;
113 bool notfinished = true;
114 while (notfinished) {
115 Edge carray[numDomains];
116 TableEntry *tableEntry = predicate->table->getTableEntry(vals, numDomains);
117 bool isInRange = tableEntry != NULL;
118 if (!isInRange && !hasOverflow) {
122 for (uint i = 0; i < numDomains; i++) {
123 Element *elem = constraint->inputs.get(i);
124 carray[i] = getElementValueConstraint(elem, polarity, vals[i]);
127 switch (predicate->undefinedbehavior) {
128 case SATC_UNDEFINEDSETSFLAG:
130 clause = constraintAND(cnf, numDomains, carray);
132 Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
133 addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), undefConstraint) );
136 case SATC_FLAGIFFUNDEFINED: {
137 Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
139 clause = constraintAND(cnf, numDomains, carray);
140 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint)));
142 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint) );
152 model_print("added clause in predicate table enumeration ...\n");
156 pushVectorEdge(clauses, clause);
160 for (uint i = 0; i < numDomains; i++) {
161 uint index = ++indices[i];
162 Set *set = predicate->table->getDomain(i);
164 if (index < set->getSize()) {
165 vals[i] = set->getElement(index);
170 vals[i] = set->getElement(0);
174 Edge result = E_NULL;
175 ASSERT(getSizeVectorEdge(clauses) != 0);
176 result = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
178 Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
179 result = constraintOR2(cnf, result, undefConstraint);
181 if (generateNegation) {
182 ASSERT(!hasOverflow);
183 result = constraintNegate(result);
185 deleteVectorEdge(clauses);
189 void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) {
190 UndefinedBehavior undefStatus = ((FunctionTable *) func->getFunction())->undefBehavior;
191 ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == SATC_FLAGFORCEUNDEFINED);
192 Array<Element *> *elements = &func->inputs;
194 Table *table = ((FunctionTable *) (func->getFunction()))->table;
195 uint size = table->getSize();
196 Edge constraints[size];
197 SetIteratorTableEntry *iterator = table->getEntries();
199 while (iterator->hasNext()) {
200 TableEntry *entry = iterator->next();
201 ASSERT(entry != NULL);
202 uint inputNum = elements->getSize();
203 Edge carray[inputNum];
204 for (uint j = 0; j < inputNum; j++) {
205 Element *el = elements->get(j);
206 carray[j] = getElementValueConstraint(el, P_FALSE, entry->inputs[j]);
208 Edge output = getElementValueConstraint(func, P_TRUE, entry->output);
209 switch (undefStatus ) {
210 case SATC_IGNOREBEHAVIOR: {
212 addConstraintCNF(cnf, output);
214 addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
218 case SATC_FLAGFORCEUNDEFINED: {
219 Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
221 addConstraintCNF(cnf, constraintAND2(cnf, output, constraintNegate(undefConst)));
223 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
235 void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc) {
237 model_print("Enumeration Table functions ...\n");
239 ASSERT(elemFunc->getFunction()->type == TABLEFUNC);
241 //First encode children
242 Array<Element *> *elements = &elemFunc->inputs;
243 for (uint i = 0; i < elements->getSize(); i++) {
244 Element *elem = elements->get(i);
245 encodeElementSATEncoder(elem);
248 FunctionTable *function = (FunctionTable *)elemFunc->getFunction();
249 switch (function->undefBehavior) {
250 case SATC_IGNOREBEHAVIOR:
251 case SATC_FLAGFORCEUNDEFINED:
252 return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc);
257 uint numDomains = function->table->numDomains();
259 uint indices[numDomains]; //setup indices
260 bzero(indices, sizeof(uint) * numDomains);
262 uint64_t vals[numDomains];//setup value array
263 for (uint i = 0; i < numDomains; i++) {
264 Set *set = function->table->getDomain(i);
265 vals[i] = set->getElement(indices[i]);
268 bool notfinished = true;
269 while (notfinished) {
270 Edge carray[numDomains + 1];
271 TableEntry *tableEntry = function->table->getTableEntry(vals, numDomains);
272 bool isInRange = tableEntry != NULL;
273 ASSERT(function->undefBehavior == SATC_UNDEFINEDSETSFLAG || function->undefBehavior == SATC_FLAGIFFUNDEFINED);
274 for (uint i = 0; i < numDomains; i++) {
275 Element *elem = elemFunc->inputs.get(i);
276 carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]);
279 carray[numDomains] = getElementValueConstraint(elemFunc, P_TRUE, tableEntry->output);
282 switch (function->undefBehavior) {
283 case SATC_UNDEFINEDSETSFLAG: {
286 addConstraintCNF(cnf,carray[numDomains]);
288 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
291 Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
292 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
296 case SATC_FLAGIFFUNDEFINED: {
297 Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
300 addConstraintCNF(cnf, constraintAND2(cnf,carray[numDomains], constraintNegate(undefConstraint)) );
302 Edge freshvar = constraintNewVar(cnf);
303 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
304 addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
305 addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
309 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
318 model_print("added clause in function table enumeration ...\n");
325 for (uint i = 0; i < numDomains; i++) {
326 uint index = ++indices[i];
327 Set *set = function->table->getDomain(i);
329 if (index < set->getSize()) {
330 vals[i] = set->getElement(index);
335 vals[i] = set->getElement(0);