Performance improvement
[satune.git] / src / Backend / satfuncopencoder.cc
1 #include "satencoder.h"
2 #include "common.h"
3 #include "function.h"
4 #include "ops.h"
5 #include "predicate.h"
6 #include "boolean.h"
7 #include "table.h"
8 #include "tableentry.h"
9 #include "set.h"
10 #include "element.h"
11 #include "common.h"
12
13 Edge SATEncoder::encodeOperatorPredicateSATEncoder(BooleanPredicate *constraint) {
14         switch (constraint->encoding.type) {
15         case ENUMERATEIMPLICATIONS:
16                 return encodeEnumOperatorPredicateSATEncoder(constraint);
17         case CIRCUIT:
18                 return encodeCircuitOperatorPredicateEncoder(constraint);
19         default:
20                 ASSERT(0);
21         }
22         exit(-1);
23 }
24
25 Edge SATEncoder::encodeEnumEqualsPredicateSATEncoder(BooleanPredicate *constraint) {
26         Polarity polarity = constraint->polarity;
27
28         /* Call base encoders for children */
29         for (uint i = 0; i < 2; i++) {
30                 Element *elem = constraint->inputs.get(i);
31                 encodeElementSATEncoder(elem);
32         }
33         VectorEdge *clauses = vector;
34
35         Set *set0 = constraint->inputs.get(0)->getRange();
36         uint size0 = set0->getSize();
37
38         Set *set1 = constraint->inputs.get(1)->getRange();
39         uint size1 = set1->getSize();
40
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; ) {
45                         if (val0 == val1) {
46                                 Edge carray[2];
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);
51                                 i++; j++;
52                                 if (i < size0)
53                                         val0 = set0->getElement(i);
54                                 else
55                                         break;
56                                 if (j < size1)
57                                         val1 = set1->getElement(j);
58                                 else
59                                         break;
60                         } else if (val0 < val1) {
61                                 i++;
62                                 if (i < size0)
63                                         val0 = set0->getElement(i);
64                                 else
65                                         break;
66                         } else {
67                                 j++;
68                                 if (j < size1)
69                                         val1 = set1->getElement(j);
70                                 else
71                                         break;
72                         }
73                 }
74         if (getSizeVectorEdge(clauses) == 0) {
75                 return E_False;
76         }
77         Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
78         clearVectorEdge(clauses);
79         return cor;
80 }
81
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;
88         if (generateNegation)
89                 polarity = negatePolarity(polarity);
90
91         if (!generateNegation && predicate->getOp() == SATC_EQUALS)
92                 return encodeEnumEqualsPredicateSATEncoder(constraint);
93
94         /* Call base encoders for children */
95         for (uint i = 0; i < numDomains; i++) {
96                 Element *elem = constraint->inputs.get(i);
97                 encodeElementSATEncoder(elem);
98         }
99         VectorEdge *clauses = vector;
100
101         uint indices[numDomains];       //setup indices
102         bzero(indices, sizeof(uint) * numDomains);
103
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]);
108         }
109
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]);
118                         }
119                         Edge term = constraintAND(cnf, numDomains, carray);
120                         pushVectorEdge(clauses, term);
121                         ASSERT(getSizeVectorEdge(clauses) > 0);
122                 }
123
124                 notfinished = false;
125                 for (uint i = 0; i < numDomains; i++) {
126                         uint index = ++indices[i];
127                         Set *set = constraint->inputs.get(i)->getRange();
128
129                         if (index < set->getSize()) {
130                                 vals[i] = set->getElement(index);
131                                 notfinished = true;
132                                 break;
133                         } else {
134                                 indices[i] = 0;
135                                 vals[i] = set->getElement(0);
136                         }
137                 }
138         }
139         if (getSizeVectorEdge(clauses) == 0) {
140                 return E_False;
141         }
142         Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
143         clearVectorEdge(clauses);
144         return generateNegation ? constraintNegate(cor) : cor;
145 }
146
147
148 void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func) {
149 #ifdef TRACE_DEBUG
150         model_print("Operator Function ...\n");
151 #endif
152         FunctionOperator *function = (FunctionOperator *) func->getFunction();
153         uint numDomains = func->inputs.getSize();
154
155         /* Call base encoders for children */
156         for (uint i = 0; i < numDomains; i++) {
157                 Element *elem = func->inputs.get(i);
158                 encodeElementSATEncoder(elem);
159         }
160
161         VectorEdge *clauses = allocDefVectorEdge();     // Setup array of clauses
162
163         uint indices[numDomains];       //setup indices
164         bzero(indices, sizeof(uint) * numDomains);
165
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]);
170         }
171
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) {
179                         needClause = true;
180                 }
181
182                 if (needClause) {
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]);
187                         }
188                         if (isInRange) {
189                                 carray[numDomains] = getElementValueConstraint(func, P_TRUE, result);
190                         }
191
192                         Edge clause;
193                         switch (function->overflowbehavior) {
194                         case SATC_IGNORE:
195                         case SATC_NOOVERFLOW:
196                         case SATC_WRAPAROUND: {
197                                 clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
198                                 break;
199                         }
200                         case SATC_FLAGFORCESOVERFLOW: {
201                                 Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
202                                 clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
203                                 break;
204                         }
205                         case SATC_OVERFLOWSETSFLAG: {
206                                 if (isInRange) {
207                                         clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
208                                 } else {
209                                         Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
210                                         clause = constraintIMPLIES(cnf,constraintAND(cnf, numDomains, carray), overFlowConstraint);
211                                 }
212                                 break;
213                         }
214                         case SATC_FLAGIFFOVERFLOW: {
215                                 Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
216                                 if (isInRange) {
217                                         clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), constraintAND2(cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
218                                 } else {
219                                         clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), overFlowConstraint);
220                                 }
221                                 break;
222                         }
223                         default:
224                                 ASSERT(0);
225                         }
226 #ifdef TRACE_DEBUG
227                         model_print("added clause in operator function\n");
228                         printCNF(clause);
229                         model_print("\n");
230 #endif
231                         pushVectorEdge(clauses, clause);
232                 }
233
234                 notfinished = false;
235                 for (uint i = 0; i < numDomains; i++) {
236                         uint index = ++indices[i];
237                         Set *set = func->inputs.get(i)->getRange();
238
239                         if (index < set->getSize()) {
240                                 vals[i] = set->getElement(index);
241                                 notfinished = true;
242                                 break;
243                         } else {
244                                 indices[i] = 0;
245                                 vals[i] = set->getElement(0);
246                         }
247                 }
248         }
249         if (getSizeVectorEdge(clauses) == 0) {
250                 deleteVectorEdge(clauses);
251                 return;
252         }
253         Edge cand = constraintAND(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
254         addConstraintCNF(cnf, cand);
255         deleteVectorEdge(clauses);
256 }
257
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()) {
269         case SATC_EQUALS:
270                 return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
271         case SATC_LT:
272                 return generateLTConstraint(cnf, numVars, ee0->variables, ee1->variables);
273         case SATC_GT:
274                 return generateLTConstraint(cnf, numVars, ee1->variables, ee0->variables);
275         default:
276                 ASSERT(0);
277         }
278         exit(-1);
279 }
280