1 #include "satencoder.h"
8 #include "tableentry.h"
13 Edge SATEncoder::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
14 switch (constraint->encoding.type) {
15 case ENUMERATEIMPLICATIONS:
16 return encodeEnumOperatorPredicateSATEncoder(constraint);
18 return encodeCircuitOperatorPredicateEncoder(constraint);
25 Edge SATEncoder::encodeEnumEqualsPredicateSATEncoder(BooleanPredicate *constraint) {
26 Polarity polarity = constraint->polarity;
28 /* Call base encoders for children */
29 for (uint i = 0; i < 2; i++) {
30 Element *elem = constraint->inputs.get(i);
31 encodeElementSATEncoder(elem);
33 VectorEdge *clauses = vector;
35 Set *set0 = constraint->inputs.get(0)->getRange();
36 uint size0 = set0->getSize();
38 Set *set1 = constraint->inputs.get(1)->getRange();
39 uint size1 = set1->getSize();
41 uint64_t val0 = set0->getElement(0);
42 uint64_t val1 = set1->getElement(0);
43 if (size0 != 0 && size1 != 0)
44 for (uint i = 0, j = 0; true; ) {
47 carray[0] = getElementValueConstraint(constraint->inputs.get(0), polarity, val0);
48 carray[1] = getElementValueConstraint(constraint->inputs.get(1), polarity, val0);
49 Edge term = constraintAND(cnf, 2, carray);
50 pushVectorEdge(clauses, term);
53 val0 = set0->getElement(i);
57 val1 = set1->getElement(j);
60 } else if (val0 < val1) {
63 val0 = set0->getElement(i);
69 val1 = set1->getElement(j);
74 if (getSizeVectorEdge(clauses) == 0) {
77 Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
78 clearVectorEdge(clauses);
82 Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
83 PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
84 uint numDomains = constraint->inputs.getSize();
85 Polarity polarity = constraint->polarity;
86 FunctionEncodingType encType = constraint->encoding.type;
87 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
89 polarity = negatePolarity(polarity);
91 if (!generateNegation && predicate->getOp() == SATC_EQUALS)
92 return encodeEnumEqualsPredicateSATEncoder(constraint);
94 /* Call base encoders for children */
95 for (uint i = 0; i < numDomains; i++) {
96 Element *elem = constraint->inputs.get(i);
97 encodeElementSATEncoder(elem);
99 VectorEdge *clauses = vector;
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 = constraint->inputs.get(i)->getRange();
107 vals[i] = set->getElement(indices[i]);
110 bool notfinished = true;
111 Edge carray[numDomains];
112 while (notfinished) {
113 if (predicate->evalPredicateOperator(vals) != generateNegation) {
114 //Include this in the set of terms
115 for (uint i = 0; i < numDomains; i++) {
116 Element *elem = constraint->inputs.get(i);
117 carray[i] = getElementValueConstraint(elem, polarity, vals[i]);
119 Edge term = constraintAND(cnf, numDomains, carray);
120 pushVectorEdge(clauses, term);
121 ASSERT(getSizeVectorEdge(clauses) > 0);
125 for (uint i = 0; i < numDomains; i++) {
126 uint index = ++indices[i];
127 Set *set = constraint->inputs.get(i)->getRange();
129 if (index < set->getSize()) {
130 vals[i] = set->getElement(index);
135 vals[i] = set->getElement(0);
139 if (getSizeVectorEdge(clauses) == 0) {
142 Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
143 clearVectorEdge(clauses);
144 return generateNegation ? constraintNegate(cor) : cor;
148 void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) {
150 model_print("Operator Function ...\n");
152 FunctionOperator *function = (FunctionOperator *) func->getFunction();
153 uint numDomains = func->inputs.getSize();
155 /* Call base encoders for children */
156 for (uint i = 0; i < numDomains; i++) {
157 Element *elem = func->inputs.get(i);
158 encodeElementSATEncoder(elem);
161 VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
163 uint indices[numDomains]; //setup indices
164 bzero(indices, sizeof(uint) * numDomains);
166 uint64_t vals[numDomains];//setup value array
167 for (uint i = 0; i < numDomains; i++) {
168 Set *set = func->inputs.get(i)->getRange();
169 vals[i] = set->getElement(indices[i]);
172 bool notfinished = true;
173 Edge carray[numDomains + 1];
174 while (notfinished) {
175 uint64_t result = function->applyFunctionOperator(numDomains, vals);
176 bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
177 bool needClause = isInRange;
178 if (function->overflowbehavior == SATC_OVERFLOWSETSFLAG || function->overflowbehavior == SATC_FLAGIFFOVERFLOW) {
183 //Include this in the set of terms
184 for (uint i = 0; i < numDomains; i++) {
185 Element *elem = func->inputs.get(i);
186 carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]);
189 carray[numDomains] = getElementValueConstraint(func, P_TRUE, result);
193 switch (function->overflowbehavior) {
195 case SATC_NOOVERFLOW:
196 case SATC_WRAPAROUND: {
197 clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
200 case SATC_FLAGFORCESOVERFLOW: {
201 Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
202 clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
205 case SATC_OVERFLOWSETSFLAG: {
207 clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
209 Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
210 clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint);
214 case SATC_FLAGIFFOVERFLOW: {
215 Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
217 clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
219 clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), overFlowConstraint);
227 model_print("added clause in operator function\n");
231 pushVectorEdge(clauses, clause);
235 for (uint i = 0; i < numDomains; i++) {
236 uint index = ++indices[i];
237 Set *set = func->inputs.get(i)->getRange();
239 if (index < set->getSize()) {
240 vals[i] = set->getElement(index);
245 vals[i] = set->getElement(0);
249 if (getSizeVectorEdge(clauses) == 0) {
250 deleteVectorEdge(clauses);
253 Edge cand = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
254 addConstraintCNF(cnf, cand);
255 deleteVectorEdge(clauses);
258 Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint) {
259 PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
260 Element *elem0 = constraint->inputs.get(0);
261 encodeElementSATEncoder(elem0);
262 Element *elem1 = constraint->inputs.get(1);
263 encodeElementSATEncoder(elem1);
264 ElementEncoding *ee0 = elem0->getElementEncoding();
265 ElementEncoding *ee1 = elem1->getElementEncoding();
266 ASSERT(ee0->numVars == ee1->numVars);
267 uint numVars = ee0->numVars;
268 switch (predicate->getOp()) {
270 return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
272 return generateLTConstraint(cnf, numVars, ee0->variables, ee1->variables);
274 return generateLTConstraint(cnf, numVars, ee1->variables, ee0->variables);