1 #include "satencoder.h"
8 #include "tableentry.h"
12 Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
13 VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
14 FunctionEncodingType encType = constraint->encoding.type;
15 ArrayElement* inputs = &constraint->inputs;
16 uint inputNum =getSizeArrayElement(inputs);
17 //Encode all the inputs first ...
18 for(uint i=0; i<inputNum; i++){
19 encodeElementSATEncoder(This, getArrayElement(inputs, i));
22 //WARNING: THIS ASSUMES PREDICATE TABLE IS COMPLETE...SEEMS UNLIKELY TO BE SAFE IN MANY CASES...
23 //WONDER WHAT BEST WAY TO HANDLE THIS IS...
25 uint size = getSizeVectorTableEntry(entries);
26 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
27 Edge constraints[size];
28 for(uint i=0; i<size; i++){
29 TableEntry* entry = getVectorTableEntry(entries, i);
30 if(generateNegation == entry->output) {
31 //Skip the irrelevant entries
34 Edge carray[inputNum];
35 for(uint j=0; j<inputNum; j++){
36 Element* el = getArrayElement(inputs, j);
37 carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
39 constraints[i]=constraintAND(This->cnf, inputNum, carray);
41 Edge result=constraintOR(This->cnf, size, constraints);
43 return generateNegation ? constraintNegate(result) : result;
46 Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
47 switch(constraint->encoding.type){
48 case ENUMERATEIMPLICATIONS:
49 return encodeEnumOperatorPredicateSATEncoder(This, constraint);
51 return encodeCircuitOperatorPredicateEncoder(This, constraint);
58 Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint) {
59 PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
61 switch(predicate->op) {
63 return encodeCircuitEquals(This, constraint);
71 Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint) {
72 PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
73 ASSERT(getSizeArraySet(&predicate->domains) == 2);
74 Element *elem0 = getArrayElement( &constraint->inputs, 0);
75 Element *elem1 = getArrayElement( &constraint->inputs, 1);
76 ElementEncoding *ee0=getElementEncoding(elem0);
77 ElementEncoding *ee1=getElementEncoding(elem1);
78 ASSERT(ee0->numVars==ee1->numVars);
79 uint numVars=ee0->numVars;
81 for (uint i=0; i<numVars; i++) {
82 carray[i]=constraintIFF(This->cnf, ee0->variables[i], ee1->variables[i]);
84 return constraintAND(This->cnf, numVars, carray);
87 Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
88 PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
89 uint numDomains=getSizeArraySet(&predicate->domains);
91 FunctionEncodingType encType = constraint->encoding.type;
92 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
94 /* Call base encoders for children */
95 for(uint i=0;i<numDomains;i++) {
96 Element *elem = getArrayElement( &constraint->inputs, i);
97 encodeElementSATEncoder(This, elem);
99 VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
101 uint indices[numDomains]; //setup indices
102 bzero(indices, sizeof(uint)*numDomains);
104 uint64_t vals[numDomains]; //setup value array
105 for(uint i=0;i<numDomains; i++) {
106 Set * set=getArraySet(&predicate->domains, i);
107 vals[i]=getSetElement(set, indices[i]);
110 bool notfinished=true;
112 Edge carray[numDomains];
114 if (evalPredicateOperator(predicate, vals) ^ generateNegation) {
115 //Include this in the set of terms
116 for(uint i=0;i<numDomains;i++) {
117 Element * elem = getArrayElement(&constraint->inputs, i);
118 carray[i] = getElementValueConstraint(This, elem, vals[i]);
120 Edge term=constraintAND(This->cnf, numDomains, carray);
121 pushVectorEdge(clauses, term);
125 for(uint i=0;i<numDomains; i++) {
126 uint index=++indices[i];
127 Set * set=getArraySet(&predicate->domains, i);
129 if (index < getSetSize(set)) {
130 vals[i]=getSetElement(set, index);
135 vals[i]=getSetElement(set, 0);
139 if(getSizeVectorEdge(clauses) == 0)
141 Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
142 deleteVectorEdge(clauses);
143 return generateNegation ? constraintNegate(cor) : cor;
147 void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
149 model_print("Operator Function ...\n");
151 FunctionOperator * function = (FunctionOperator *) func->function;
152 uint numDomains=getSizeArrayElement(&func->inputs);
154 /* Call base encoders for children */
155 for(uint i=0;i<numDomains;i++) {
156 Element *elem = getArrayElement( &func->inputs, i);
157 encodeElementSATEncoder(This, elem);
160 VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
162 uint indices[numDomains]; //setup indices
163 bzero(indices, sizeof(uint)*numDomains);
165 uint64_t vals[numDomains]; //setup value array
166 for(uint i=0;i<numDomains; i++) {
167 Set * set=getElementSet(getArrayElement(&func->inputs, i));
168 vals[i]=getSetElement(set, indices[i]);
171 Edge overFlowConstraint = ((BooleanVar*) func->overflowstatus)->var;
173 bool notfinished=true;
175 Edge carray[numDomains+1];
177 uint64_t result=applyFunctionOperator(function, numDomains, vals);
178 bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result);
179 bool needClause = isInRange;
180 if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
185 //Include this in the set of terms
186 for(uint i=0;i<numDomains;i++) {
187 Element * elem = getArrayElement(&func->inputs, i);
188 carray[i] = getElementValueConstraint(This, elem, vals[i]);
191 carray[numDomains] = getElementValueConstraint(This, &func->base, result);
195 switch(function->overflowbehavior) {
199 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
202 case FLAGFORCESOVERFLOW: {
203 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
206 case OVERFLOWSETSFLAG: {
208 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
210 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
214 case FLAGIFFOVERFLOW: {
216 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
218 clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
225 pushVectorEdge(clauses, clause);
229 for(uint i=0;i<numDomains; i++) {
230 uint index=++indices[i];
231 Set * set=getElementSet(getArrayElement(&func->inputs, i));
233 if (index < getSetSize(set)) {
234 vals[i]=getSetElement(set, index);
239 vals[i]=getSetElement(set, 0);
244 Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
245 addConstraintCNF(This->cnf, cor);
246 deleteVectorEdge(clauses);
249 void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* func){
251 model_print("Enumeration Table functions ...\n");
253 //FIXME: HANDLE UNDEFINED BEHAVIORS
254 ASSERT(GETFUNCTIONTYPE(func->function)==TABLEFUNC);
255 ArrayElement* elements= &func->inputs;
256 Table* table = ((FunctionTable*) (func->function))->table;
257 uint size = getSizeVectorTableEntry(&table->entries);
258 Edge constraints[size]; //FIXME: should add a space for the case that didn't match any entries
259 for(uint i=0; i<size; i++) {
260 TableEntry* entry = getVectorTableEntry(&table->entries, i);
261 uint inputNum = getSizeArrayElement(elements);
262 Edge carray[inputNum];
263 for(uint j=0; j<inputNum; j++){
264 Element* el= getArrayElement(elements, j);
265 carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
267 Edge output = getElementValueConstraint(This, (Element*)func, entry->output);
268 Edge row= constraintIMPLIES(This->cnf, constraintAND(This->cnf, inputNum, carray), output);
271 addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));