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 && 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]);
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){
52 row=constraintAND(This->cnf, inputNum, carray);
58 constraints[i++] = row;
64 Edge result= generateNegation?constraintNegate(constraintOR(This->cnf, i, constraints))
65 :constraintOR(This->cnf, i, constraints);
69 Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
71 model_print("Enumeration Table Predicate ...\n");
73 ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
74 //First encode children
75 ArrayElement* inputs = &constraint->inputs;
76 uint inputNum =getSizeArrayElement(inputs);
77 //Encode all the inputs first ...
78 for(uint i=0; i<inputNum; i++){
79 encodeElementSATEncoder(This, getArrayElement(inputs, i));
81 PredicateTable* predicate = (PredicateTable*)constraint->predicate;
82 switch(predicate->undefinedbehavior){
84 case FLAGFORCEUNDEFINED:
85 return encodeEnumEntriesTablePredicateSATEncoder(This, constraint);
89 bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
90 uint numDomains=getSizeArraySet(&predicate->table->domains);
92 VectorEdge * clauses=allocDefVectorEdge();
94 uint indices[numDomains]; //setup indices
95 bzero(indices, sizeof(uint)*numDomains);
97 uint64_t vals[numDomains]; //setup value array
98 for(uint i=0;i<numDomains; i++) {
99 Set * set=getArraySet(&predicate->table->domains, i);
100 vals[i]=getSetElement(set, indices[i]);
102 bool hasOverflow = false;
103 Edge undefConstraint = encodeConstraintSATEncoder (This, constraint->undefStatus);
104 printCNF(undefConstraint);
105 bool notfinished=true;
107 Edge carray[numDomains];
108 TableEntry* tableEntry = getTableEntryFromTable(predicate->table, vals, numDomains);
109 bool isInRange = tableEntry!=NULL;
110 if(!isInRange && !hasOverflow){
114 for(uint i=0;i<numDomains;i++) {
115 Element * elem = getArrayElement(&constraint->inputs, i);
116 carray[i] = getElementValueConstraint(This, elem, vals[i]);
119 switch(predicate->undefinedbehavior) {
120 case UNDEFINEDSETSFLAG:
122 clause=constraintAND(This->cnf, numDomains, carray);
124 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint) );
127 case FLAGIFFUNDEFINED:
129 clause=constraintAND(This->cnf, numDomains, carray);
130 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint)));
132 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint) );
142 model_print("added clause in predicate table enumeration ...\n");
146 pushVectorEdge(clauses, clause);
150 for(uint i=0;i<numDomains; i++) {
151 uint index=++indices[i];
152 Set * set=getArraySet(&predicate->table->domains, i);
154 if (index < getSetSize(set)) {
155 vals[i]=getSetElement(set, index);
160 vals[i]=getSetElement(set, 0);
164 Edge result = E_NULL;
165 ASSERT(getSizeVectorEdge(clauses) != 0);
166 result=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
168 result = constraintOR2(This->cnf, result, undefConstraint);
170 if(generateNegation){
171 ASSERT(!hasOverflow);
172 result = constraintNegate(result);
174 deleteVectorEdge(clauses);
178 void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){
179 UndefinedBehavior undefStatus = ((FunctionTable*) func->function)->undefBehavior;
180 ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
181 ArrayElement* elements= &func->inputs;
182 Table* table = ((FunctionTable*) (func->function))->table;
183 uint size = getSizeHashSetTableEntry(table->entries);
184 Edge constraints[size];
185 HSIteratorTableEntry* iterator = iteratorTableEntry(table->entries);
187 while(hasNextTableEntry(iterator)) {
188 TableEntry* entry = nextTableEntry(iterator);
190 uint inputNum = getSizeArrayElement(elements);
191 Edge carray[inputNum];
192 for(uint j=0; j<inputNum; j++){
193 Element* el= getArrayElement(elements, j);
194 carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
196 Edge output = getElementValueConstraint(This, (Element*)func, entry->output);
198 switch(undefStatus ){
199 case IGNOREBEHAVIOR: {
200 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output);
203 case FLAGFORCEUNDEFINED: {
204 Edge undefConst = encodeConstraintSATEncoder(This, func->overflowstatus);
205 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
212 constraints[i++]=row;
214 deleteIterTableEntry(iterator);
215 addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
218 void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* elemFunc){
220 model_print("Enumeration Table functions ...\n");
222 ASSERT(GETFUNCTIONTYPE(elemFunc->function)==TABLEFUNC);
223 //First encode children
224 ArrayElement* elements= &elemFunc->inputs;
225 for(uint i=0; i<getSizeArrayElement(elements); i++){
226 Element *elem = getArrayElement( elements, i);
227 encodeElementSATEncoder(This, elem);
230 FunctionTable* function =(FunctionTable*)elemFunc->function;
231 switch(function->undefBehavior){
233 case FLAGFORCEUNDEFINED:
234 return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
239 uint numDomains=getSizeArraySet(&function->table->domains);
241 VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
243 uint indices[numDomains]; //setup indices
244 bzero(indices, sizeof(uint)*numDomains);
246 uint64_t vals[numDomains]; //setup value array
247 for(uint i=0;i<numDomains; i++) {
248 Set * set=getArraySet(&function->table->domains, i);
249 vals[i]=getSetElement(set, indices[i]);
252 Edge undefConstraint = encodeConstraintSATEncoder(This, elemFunc->overflowstatus);
253 bool notfinished=true;
255 Edge carray[numDomains+1];
256 TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains);
257 bool isInRange = tableEntry!=NULL;
258 ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
259 for(uint i=0;i<numDomains;i++) {
260 Element * elem = getArrayElement(&elemFunc->inputs, i);
261 carray[i] = getElementValueConstraint(This, elem, vals[i]);
264 carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output);
268 switch(function->undefBehavior) {
269 case UNDEFINEDSETSFLAG: {
271 //FIXME: Talk to Brian, It should be IFF not only IMPLY. --HG
272 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
274 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint));
278 case FLAGIFFUNDEFINED: {
280 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
281 addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint) ));
283 addConstraintCNF(This->cnf,constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), undefConstraint));
292 model_print("added clause in function table enumeration ...\n");
296 pushVectorEdge(clauses, clause);
300 for(uint i=0;i<numDomains; i++) {
301 uint index=++indices[i];
302 Set * set=getArraySet(&function->table->domains, i);
304 if (index < getSetSize(set)) {
305 vals[i]=getSetElement(set, index);
310 vals[i]=getSetElement(set, 0);
314 if(getSizeVectorEdge(clauses) == 0){
315 deleteVectorEdge(clauses);
318 Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
319 addConstraintCNF(This->cnf, cor);
320 deleteVectorEdge(clauses);