1 #include "satencoder.h"
8 #include "tableentry.h"
13 Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
14 Table* table = ((PredicateTable*)constraint->predicate)->table;
15 FunctionEncodingType encType = constraint->encoding.type;
16 ArrayElement* inputs = &constraint->inputs;
17 uint inputNum =getSizeArrayElement(inputs);
18 //Encode all the inputs first ...
19 for(uint i=0; i<inputNum; i++){
20 encodeElementSATEncoder(This, getArrayElement(inputs, i));
22 uint size = getSizeHashSetTableEntry(table->entrie);
23 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
24 Edge constraints[size];
25 HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie);
27 while(hasNextTableEntry(iterator)){
28 TableEntry* entry = nextTableEntry(iterator);
29 if(generateNegation == entry->output) {
30 //Skip the irrelevant entries
33 Edge carray[inputNum];
34 for(uint j=0; j<inputNum; j++){
35 Element* el = getArrayElement(inputs, j);
36 carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
38 constraints[i++]=constraintAND(This->cnf, inputNum, carray);
40 Edge result=constraintOR(This->cnf, size, constraints);
42 return generateNegation ? constraintNegate(result) : result;
44 Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
49 Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
50 switch(constraint->encoding.type){
51 case ENUMERATEIMPLICATIONS:
52 return encodeEnumOperatorPredicateSATEncoder(This, constraint);
54 return encodeCircuitOperatorPredicateEncoder(This, constraint);
61 Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint) {
62 PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
64 switch(predicate->op) {
66 return encodeCircuitEquals(This, constraint);
74 Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint) {
75 PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
76 ASSERT(getSizeArraySet(&predicate->domains) == 2);
77 Element *elem0 = getArrayElement( &constraint->inputs, 0);
78 Element *elem1 = getArrayElement( &constraint->inputs, 1);
79 ElementEncoding *ee0=getElementEncoding(elem0);
80 ElementEncoding *ee1=getElementEncoding(elem1);
81 ASSERT(ee0->numVars==ee1->numVars);
82 uint numVars=ee0->numVars;
84 for (uint i=0; i<numVars; i++) {
85 carray[i]=constraintIFF(This->cnf, ee0->variables[i], ee1->variables[i]);
87 return constraintAND(This->cnf, numVars, carray);
90 Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
91 PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
92 uint numDomains=getSizeArraySet(&predicate->domains);
94 FunctionEncodingType encType = constraint->encoding.type;
95 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
97 /* Call base encoders for children */
98 for(uint i=0;i<numDomains;i++) {
99 Element *elem = getArrayElement( &constraint->inputs, i);
100 encodeElementSATEncoder(This, elem);
102 VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
104 uint indices[numDomains]; //setup indices
105 bzero(indices, sizeof(uint)*numDomains);
107 uint64_t vals[numDomains]; //setup value array
108 for(uint i=0;i<numDomains; i++) {
109 Set * set=getArraySet(&predicate->domains, i);
110 vals[i]=getSetElement(set, indices[i]);
113 bool notfinished=true;
115 Edge carray[numDomains];
117 if (evalPredicateOperator(predicate, vals) ^ generateNegation) {
118 //Include this in the set of terms
119 for(uint i=0;i<numDomains;i++) {
120 Element * elem = getArrayElement(&constraint->inputs, i);
121 carray[i] = getElementValueConstraint(This, elem, vals[i]);
123 Edge term=constraintAND(This->cnf, numDomains, carray);
124 pushVectorEdge(clauses, term);
128 for(uint i=0;i<numDomains; i++) {
129 uint index=++indices[i];
130 Set * set=getArraySet(&predicate->domains, i);
132 if (index < getSetSize(set)) {
133 vals[i]=getSetElement(set, index);
138 vals[i]=getSetElement(set, 0);
142 if(getSizeVectorEdge(clauses) == 0)
144 Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
145 deleteVectorEdge(clauses);
146 return generateNegation ? constraintNegate(cor) : cor;
150 void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
152 model_print("Operator Function ...\n");
154 FunctionOperator * function = (FunctionOperator *) func->function;
155 uint numDomains=getSizeArrayElement(&func->inputs);
157 /* Call base encoders for children */
158 for(uint i=0;i<numDomains;i++) {
159 Element *elem = getArrayElement( &func->inputs, i);
160 encodeElementSATEncoder(This, elem);
163 VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
165 uint indices[numDomains]; //setup indices
166 bzero(indices, sizeof(uint)*numDomains);
168 uint64_t vals[numDomains]; //setup value array
169 for(uint i=0;i<numDomains; i++) {
170 Set * set=getElementSet(getArrayElement(&func->inputs, i));
171 vals[i]=getSetElement(set, indices[i]);
174 Edge overFlowConstraint = ((BooleanVar*) func->overflowstatus)->var;
176 bool notfinished=true;
178 Edge carray[numDomains+1];
180 uint64_t result=applyFunctionOperator(function, numDomains, vals);
181 bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result);
182 bool needClause = isInRange;
183 if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
188 //Include this in the set of terms
189 for(uint i=0;i<numDomains;i++) {
190 Element * elem = getArrayElement(&func->inputs, i);
191 carray[i] = getElementValueConstraint(This, elem, vals[i]);
194 carray[numDomains] = getElementValueConstraint(This, &func->base, result);
198 switch(function->overflowbehavior) {
202 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
205 case FLAGFORCESOVERFLOW: {
206 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
209 case OVERFLOWSETSFLAG: {
211 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
213 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
217 case FLAGIFFOVERFLOW: {
219 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
221 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
229 model_print("added clause in operator function\n");
233 pushVectorEdge(clauses, clause);
237 for(uint i=0;i<numDomains; i++) {
238 uint index=++indices[i];
239 Set * set=getElementSet(getArrayElement(&func->inputs, i));
241 if (index < getSetSize(set)) {
242 vals[i]=getSetElement(set, index);
247 vals[i]=getSetElement(set, 0);
252 Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
253 addConstraintCNF(This->cnf, cor);
254 deleteVectorEdge(clauses);
257 void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){
258 UndefinedBehavior undefStatus = ((FunctionTable*) func->function)->undefBehavior;
259 ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
260 ArrayElement* elements= &func->inputs;
261 Table* table = ((FunctionTable*) (func->function))->table;
262 uint size = getSizeHashSetTableEntry(table->entrie);
263 Edge constraints[size];
264 HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie);
266 while(hasNextTableEntry(iterator)) {
267 TableEntry* entry = nextTableEntry(iterator);
269 uint inputNum = getSizeArrayElement(elements);
270 Edge carray[inputNum];
271 for(uint j=0; j<inputNum; j++){
272 Element* el= getArrayElement(elements, j);
273 carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
275 Edge output = getElementValueConstraint(This, (Element*)func, entry->output);
277 switch(undefStatus ){
278 case IGNOREBEHAVIOR: {
279 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output);
282 case FLAGFORCEUNDEFINED: {
283 Edge undefConst = ((BooleanVar*)func->overflowstatus)->var;
284 row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
291 constraints[i++]=row;
293 deleteIterTableEntry(iterator);
294 addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
297 void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* elemFunc){
299 model_print("Enumeration Table functions ...\n");
301 ASSERT(GETFUNCTIONTYPE(elemFunc->function)==TABLEFUNC);
302 //First encode children
303 ArrayElement* elements= &elemFunc->inputs;
304 for(uint i=0; i<getSizeArrayElement(elements); i++){
305 Element *elem = getArrayElement( elements, i);
306 encodeElementSATEncoder(This, elem);
309 FunctionTable* function =(FunctionTable*)elemFunc;
310 switch(function->undefBehavior){
312 case FLAGFORCEUNDEFINED:
313 return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
318 uint numDomains=getSizeArraySet(&function->table->domains);
320 VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
322 uint indices[numDomains]; //setup indices
323 bzero(indices, sizeof(uint)*numDomains);
325 uint64_t vals[numDomains]; //setup value array
326 for(uint i=0;i<numDomains; i++) {
327 Set * set=getArraySet(&function->table->domains, i);
328 vals[i]=getSetElement(set, indices[i]);
331 Edge undefConstraint = ((BooleanVar*) elemFunc->overflowstatus)->var;
333 bool notfinished=true;
335 Edge carray[numDomains+1];
336 TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains);
337 bool isInRange = tableEntry!=NULL;
338 bool needClause = isInRange;
339 if (function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED) {
344 //Include this in the set of terms
345 for(uint i=0;i<numDomains;i++) {
346 Element * elem = getArrayElement(&elemFunc->inputs, i);
347 carray[i] = getElementValueConstraint(This, elem, vals[i]);
350 carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output);
354 switch(function->undefBehavior) {
355 case UNDEFINEDSETSFLAG: {
357 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
359 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
363 case FLAGIFFUNDEFINED: {
365 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
367 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
375 model_print("added clause in table enumeration ...\n");
379 pushVectorEdge(clauses, clause);
383 for(uint i=0;i<numDomains; i++) {
384 uint index=++indices[i];
385 Set * set=getArraySet(&function->table->domains, i);
387 if (index < getSetSize(set)) {
388 vals[i]=getSetElement(set, index);
393 vals[i]=getSetElement(set, 0);
398 Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
399 addConstraintCNF(This->cnf, cor);
400 deleteVectorEdge(clauses);