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::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
26 PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
27 uint numDomains = constraint->inputs.getSize();
28 Polarity polarity = constraint->polarity;
29 FunctionEncodingType encType = constraint->encoding.type;
30 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
32 polarity = negatePolarity(polarity);
34 /* Call base encoders for children */
35 for (uint i = 0; i < numDomains; i++) {
36 Element *elem = constraint->inputs.get(i);
37 encodeElementSATEncoder(elem);
39 VectorEdge *clauses = vector;
41 uint indices[numDomains]; //setup indices
42 bzero(indices, sizeof(uint) * numDomains);
44 uint64_t vals[numDomains];//setup value array
45 for (uint i = 0; i < numDomains; i++) {
46 Set *set = constraint->inputs.get(i)->getRange();
47 vals[i] = set->getElement(indices[i]);
50 bool notfinished = true;
51 Edge carray[numDomains];
53 if (predicate->evalPredicateOperator(vals) != generateNegation) {
54 //Include this in the set of terms
55 for (uint i = 0; i < numDomains; i++) {
56 Element *elem = constraint->inputs.get(i);
57 carray[i] = getElementValueConstraint(elem, polarity, vals[i]);
59 Edge term = constraintAND(cnf, numDomains, carray);
60 pushVectorEdge(clauses, term);
61 ASSERT(getSizeVectorEdge(clauses) > 0);
65 for (uint i = 0; i < numDomains; i++) {
66 uint index = ++indices[i];
67 Set *set = constraint->inputs.get(i)->getRange();
69 if (index < set->getSize()) {
70 vals[i] = set->getElement(index);
75 vals[i] = set->getElement(0);
79 if (getSizeVectorEdge(clauses) == 0) {
82 Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
83 clearVectorEdge(clauses);
84 return generateNegation ? constraintNegate(cor) : cor;
88 void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) {
90 model_print("Operator Function ...\n");
92 FunctionOperator *function = (FunctionOperator *) func->getFunction();
93 uint numDomains = func->inputs.getSize();
95 /* Call base encoders for children */
96 for (uint i = 0; i < numDomains; i++) {
97 Element *elem = func->inputs.get(i);
98 encodeElementSATEncoder(elem);
101 VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
103 uint indices[numDomains]; //setup indices
104 bzero(indices, sizeof(uint) * numDomains);
106 uint64_t vals[numDomains];//setup value array
107 for (uint i = 0; i < numDomains; i++) {
108 Set *set = func->inputs.get(i)->getRange();
109 vals[i] = set->getElement(indices[i]);
112 bool notfinished = true;
113 Edge carray[numDomains + 1];
114 while (notfinished) {
115 uint64_t result = function->applyFunctionOperator(numDomains, vals);
116 bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
117 bool needClause = isInRange;
118 if (function->overflowbehavior == SATC_OVERFLOWSETSFLAG || function->overflowbehavior == SATC_FLAGIFFOVERFLOW) {
123 //Include this in the set of terms
124 for (uint i = 0; i < numDomains; i++) {
125 Element *elem = func->inputs.get(i);
126 carray[i] = getElementValueConstraint(elem, P_FALSE, vals[i]);
129 carray[numDomains] = getElementValueConstraint(func, P_TRUE, result);
133 switch (function->overflowbehavior) {
135 case SATC_NOOVERFLOW:
136 case SATC_WRAPAROUND: {
137 clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
140 case SATC_FLAGFORCESOVERFLOW: {
141 Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
142 clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
145 case SATC_OVERFLOWSETSFLAG: {
147 clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
149 Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
150 clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint);
154 case SATC_FLAGIFFOVERFLOW: {
155 Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
157 clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
159 clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), overFlowConstraint);
167 model_print("added clause in operator function\n");
171 pushVectorEdge(clauses, clause);
175 for (uint i = 0; i < numDomains; i++) {
176 uint index = ++indices[i];
177 Set *set = func->inputs.get(i)->getRange();
179 if (index < set->getSize()) {
180 vals[i] = set->getElement(index);
185 vals[i] = set->getElement(0);
189 if (getSizeVectorEdge(clauses) == 0) {
190 deleteVectorEdge(clauses);
193 Edge cand = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
194 addConstraintCNF(cnf, cand);
195 deleteVectorEdge(clauses);
198 Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constraint) {
199 PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
200 Element *elem0 = constraint->inputs.get(0);
201 encodeElementSATEncoder(elem0);
202 Element *elem1 = constraint->inputs.get(1);
203 encodeElementSATEncoder(elem1);
204 ElementEncoding *ee0 = elem0->getElementEncoding();
205 ElementEncoding *ee1 = elem1->getElementEncoding();
206 ASSERT(ee0->numVars == ee1->numVars);
207 uint numVars = ee0->numVars;
208 switch (predicate->getOp()) {
210 return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
212 return generateLTConstraint(cnf, numVars, ee0->variables, ee1->variables);
214 return generateLTConstraint(cnf, numVars, ee1->variables, ee0->variables);