1 #include "satencoder.h"
8 #include "tableentry.h"
15 Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint) {
16 ASSERT(constraint->predicate->type == TABLEPRED);
17 UndefinedBehavior undefStatus = ((PredicateTable *)constraint->predicate)->undefinedbehavior;
18 ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == SATC_FLAGFORCEUNDEFINED);
19 Table *table = ((PredicateTable *)constraint->predicate)->table;
20 FunctionEncodingType encType = constraint->encoding.type;
21 Array<Element *> *inputs = &constraint->inputs;
22 uint inputNum = inputs->getSize();
23 uint size = table->getSize();
24 Polarity polarity = constraint->polarity;
25 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
27 polarity = negatePolarity(polarity);
28 if (undefStatus ==SATC_FLAGFORCEUNDEFINED)
29 polarity = P_BOTHTRUEFALSE;
31 Edge constraints[size];
33 SetIteratorTableEntry *iterator = table->getEntries();
35 while (iterator->hasNext()) {
36 TableEntry *entry = iterator->next();
37 if (generateNegation == (entry->output != 0) && undefStatus == SATC_IGNOREBEHAVIOR) {
38 //Skip the irrelevant entries
41 Edge carray[inputNum];
42 for (uint j = 0; j < inputNum; j++) {
43 Element *el = inputs->get(j);
44 carray[j] = getElementValueConstraint(el, polarity, entry->inputs[j]);
47 switch (undefStatus) {
48 case SATC_IGNOREBEHAVIOR:
49 row = constraintAND(cnf, inputNum, carray);
51 case SATC_FLAGFORCEUNDEFINED: {
52 row = constraintAND(cnf, inputNum, carray);
53 uint pSize = constraint->parents.getSize();
54 if(!edgeIsVarConst(row) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter)){
55 Edge proxy = constraintNewVar(cnf);
56 generateProxy(cnf, row, proxy, P_BOTHTRUEFALSE);
57 Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
58 addConstraintCNF(cnf, constraintIMPLIES(cnf, proxy, constraintNegate(undefConst)));
59 if (generateNegation == (entry->output != 0)) {
69 constraints[i++] = row;
73 Edge result = generateNegation ? constraintNegate(constraintOR(cnf, i, constraints))
74 : constraintOR(cnf, i, constraints);
78 Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint) {
80 model_print("Enumeration Table Predicate ...\n");
82 ASSERT(constraint->predicate->type == TABLEPRED);
83 Polarity polarity = constraint->polarity;
85 //First encode children
86 Array<Element *> *inputs = &constraint->inputs;
87 uint inputNum = inputs->getSize();
88 //Encode all the inputs first ...
89 for (uint i = 0; i < inputNum; i++) {
90 encodeElementSATEncoder(inputs->get(i));
92 PredicateTable *predicate = (PredicateTable *)constraint->predicate;
93 switch (predicate->undefinedbehavior) {
94 case SATC_IGNOREBEHAVIOR:
95 case SATC_FLAGFORCEUNDEFINED:
96 return encodeEnumEntriesTablePredicateSATEncoder(constraint);
100 bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
101 uint numDomains = constraint->inputs.getSize();
103 if (generateNegation)
104 polarity = negatePolarity(polarity);
106 ASSERT(numDomains != 0);
107 VectorEdge *clauses = allocDefVectorEdge();
109 uint indices[numDomains]; //setup indices
110 bzero(indices, sizeof(uint) * numDomains);
112 uint64_t vals[numDomains];//setup value array
113 for (uint i = 0; i < numDomains; i++) {
114 Set *set = constraint->inputs.get(i)->getRange();
115 vals[i] = set->getElement(indices[i]);
117 bool hasOverflow = false;
119 bool notfinished = true;
120 while (notfinished) {
121 Edge carray[numDomains];
122 TableEntry *tableEntry = predicate->table->getTableEntry(vals, numDomains);
123 bool isInRange = tableEntry != NULL;
124 if (!isInRange && !hasOverflow) {
128 for (uint i = 0; i < numDomains; i++) {
129 Element *elem = constraint->inputs.get(i);
130 carray[i] = getElementValueConstraint(elem, polarity, vals[i]);
133 switch (predicate->undefinedbehavior) {
134 case SATC_UNDEFINEDSETSFLAG:
136 clause = constraintAND(cnf, numDomains, carray);
138 Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
139 addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), undefConstraint) );
142 case SATC_FLAGIFFUNDEFINED: {
143 Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
145 clause = constraintAND(cnf, numDomains, carray);
146 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintNegate(undefConstraint)));
148 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint) );
158 model_print("added clause in predicate table enumeration ...\n");
162 pushVectorEdge(clauses, clause);
166 for (uint i = 0; i < numDomains; i++) {
167 uint index = ++indices[i];
168 Set *set = constraint->inputs.get(i)->getRange();
170 if (index < set->getSize()) {
171 vals[i] = set->getElement(index);
176 vals[i] = set->getElement(0);
180 Edge result = E_NULL;
181 ASSERT(getSizeVectorEdge(clauses) != 0);
182 result = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
184 Edge undefConstraint = encodeConstraintSATEncoder(constraint->undefStatus);
185 result = constraintOR2(cnf, result, undefConstraint);
187 if (generateNegation) {
188 ASSERT(!hasOverflow);
189 result = constraintNegate(result);
191 deleteVectorEdge(clauses);
195 void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func) {
196 UndefinedBehavior undefStatus = ((FunctionTable *) func->getFunction())->undefBehavior;
197 ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == SATC_FLAGFORCEUNDEFINED);
198 Array<Element *> *elements = &func->inputs;
200 Table *table = ((FunctionTable *) (func->getFunction()))->table;
201 uint size = table->getSize();
202 Edge constraints[size];
203 SetIteratorTableEntry *iterator = table->getEntries();
205 while (iterator->hasNext()) {
206 TableEntry *entry = iterator->next();
207 ASSERT(entry != NULL);
208 uint inputNum = elements->getSize();
209 Edge carray[inputNum];
210 for (uint j = 0; j < inputNum; j++) {
211 Element *el = elements->get(j);
212 carray[j] = getElementValueConstraint(el, P_FALSE, entry->inputs[j]);
214 Edge output = getElementValueConstraint(func, P_TRUE, entry->output);
215 switch (undefStatus ) {
216 case SATC_IGNOREBEHAVIOR: {
218 addConstraintCNF(cnf, output);
220 addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
224 case SATC_FLAGFORCEUNDEFINED: {
225 Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
227 addConstraintCNF(cnf, constraintAND2(cnf, output, constraintNegate(undefConst)));
229 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
241 void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc) {
243 model_print("Enumeration Table functions ...\n");
245 ASSERT(elemFunc->getFunction()->type == TABLEFUNC);
247 //First encode children
248 Array<Element *> *elements = &elemFunc->inputs;
249 for (uint i = 0; i < elements->getSize(); i++) {
250 Element *elem = elements->get(i);
251 encodeElementSATEncoder(elem);
254 FunctionTable *function = (FunctionTable *)elemFunc->getFunction();
255 switch (function->undefBehavior) {
256 case SATC_IGNOREBEHAVIOR:
257 case SATC_FLAGFORCEUNDEFINED:
258 return encodeEnumEntriesTableElemFuncSATEncoder(elemFunc);
263 uint numDomains = elemFunc->inputs.getSize();
265 uint indices[numDomains]; //setup indices
266 bzero(indices, sizeof(uint) * numDomains);
268 uint64_t vals[numDomains];//setup value array
269 for (uint i = 0; i < numDomains; i++) {
270 Set *set = elemFunc->inputs.get(i)->getRange();
271 vals[i] = set->getElement(indices[i]);
274 bool notfinished = true;
275 while (notfinished) {
276 Edge carray[numDomains + 1];
277 TableEntry *tableEntry = function->table->getTableEntry(vals, numDomains);
278 bool isInRange = tableEntry != NULL;
279 ASSERT(function->undefBehavior == SATC_UNDEFINEDSETSFLAG || function->undefBehavior == SATC_FLAGIFFUNDEFINED);
280 for (uint i = 0; i < numDomains; i++) {
281 Element *elem = elemFunc->inputs.get(i);
282 carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]);
285 carray[numDomains] = getElementValueConstraint(elemFunc, P_TRUE, tableEntry->output);
288 switch (function->undefBehavior) {
289 case SATC_UNDEFINEDSETSFLAG: {
292 addConstraintCNF(cnf,carray[numDomains]);
294 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
297 Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
298 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
302 case SATC_FLAGIFFUNDEFINED: {
303 Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
306 addConstraintCNF(cnf, constraintAND2(cnf,carray[numDomains], constraintNegate(undefConstraint)) );
308 Edge freshvar = constraintNewVar(cnf);
309 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
310 addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
311 addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
315 addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
324 model_print("added clause in function table enumeration ...\n");
331 for (uint i = 0; i < numDomains; i++) {
332 uint index = ++indices[i];
333 Set *set = elemFunc->inputs.get(i)->getRange();
335 if (index < set->getSize()) {
336 vals[i] = set->getElement(index);
341 vals[i] = set->getElement(0);