fix tabbing
[satune.git] / src / Backend / satencoder.cc
1 #include "satencoder.h"
2 #include "structs.h"
3 #include "csolver.h"
4 #include "boolean.h"
5 #include "constraint.h"
6 #include "common.h"
7 #include "element.h"
8 #include "function.h"
9 #include "tableentry.h"
10 #include "table.h"
11 #include "order.h"
12 #include "predicate.h"
13 #include "set.h"
14 #include "tunable.h"
15
16 SATEncoder::SATEncoder(CSolver *_solver) :
17         cnf(createCNF()),
18         solver(_solver),
19         vector(allocDefVectorEdge()) {
20 }
21
22 SATEncoder::~SATEncoder() {
23         deleteCNF(cnf);
24         deleteVectorEdge(vector);
25 }
26
27 void SATEncoder::resetSATEncoder() {
28         resetCNF(cnf);
29         booledgeMap.reset();
30 }
31
32 int SATEncoder::solve(long timeout) {
33         cnf->solver->timeout = timeout;
34         long long startTime = getTimeNano();
35         finishedClauses(cnf->solver);
36         cnf->encodeTime = getTimeNano() - startTime;
37         if (solver->isIncrementalMode()) {
38                 solver->freezeElementsVariables();
39         }
40         return solveCNF(cnf);
41 }
42
43 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
44         if (csolver->isUnSAT()) {
45                 return;
46         }
47         SetIteratorBooleanEdge *iterator = csolver->getConstraints();
48         while (iterator->hasNext()) {
49                 BooleanEdge constraint = iterator->next();
50                 if (!csolver->isConstraintEncoded(constraint)) {
51                         Edge c = encodeConstraintSATEncoder(constraint);
52                         addConstraintCNF(cnf, c);
53                         csolver->addEncodedConstraint(constraint);
54                 }
55         }
56         delete iterator;
57 }
58
59 Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
60         Edge result;
61         Boolean *constraint = c.getBoolean();
62
63         if (booledgeMap.contains(constraint)) {
64                 Edge e = {(Node *) booledgeMap.get(constraint)};
65                 return c.isNegated() ? constraintNegate(e) : e;
66         }
67
68         switch (constraint->type) {
69         case ORDERCONST:
70                 result = encodeOrderSATEncoder((BooleanOrder *) constraint);
71                 break;
72         case BOOLEANVAR:
73                 result = encodeVarSATEncoder((BooleanVar *) constraint);
74                 break;
75         case LOGICOP:
76                 result = encodeLogicSATEncoder((BooleanLogic *) constraint);
77                 break;
78         case PREDICATEOP:
79                 result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
80                 break;
81         case BOOLCONST:
82                 result = ((BooleanConst *) constraint)->isTrue() ? E_True : E_False;
83                 break;
84         default:
85                 model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
86                 exit(-1);
87         }
88         Polarity p = constraint->polarity;
89         uint pSize = constraint->parents.getSize();
90
91         if ( !edgeIsVarConst(result) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter) ) {
92                 Edge e = getNewVarSATEncoder();
93                 generateProxy(cnf, result, e, p);
94                 booledgeMap.put(constraint, e.node_ptr);
95                 result = e;
96         }
97
98         return c.isNegated() ? constraintNegate(result) : result;
99 }
100
101 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
102         for (uint i = 0; i < num; i++)
103                 carray[i] = getNewVarSATEncoder();
104 }
105
106 Edge SATEncoder::getNewVarSATEncoder() {
107         return constraintNewVar(cnf);
108 }
109
110 Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
111         if (edgeIsNull(constraint->var)) {
112                 constraint->var = getNewVarSATEncoder();
113         }
114         return constraint->var;
115 }
116
117 Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
118         Edge array[constraint->inputs.getSize()];
119         for (uint i = 0; i < constraint->inputs.getSize(); i++)
120                 array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
121
122         switch (constraint->op) {
123         case SATC_AND:
124                 return constraintAND(cnf, constraint->inputs.getSize(), array);
125         case SATC_NOT:
126                 return constraintNegate(array[0]);
127         case SATC_IFF:
128                 ASSERT(constraint->inputs.getSize() == 2);
129                 return constraintIFF(cnf, array[0], array[1]);
130         case SATC_OR:
131         case SATC_XOR:
132         case SATC_IMPLIES:
133         //Don't handle, translate these away...
134         default:
135                 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
136                 exit(-1);
137         }
138 }
139
140 Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
141         switch (constraint->predicate->type) {
142         case TABLEPRED:
143                 return encodeTablePredicateSATEncoder(constraint);
144         case OPERATORPRED:
145                 return encodeOperatorPredicateSATEncoder(constraint);
146         default:
147                 ASSERT(0);
148         }
149         return E_BOGUS;
150 }
151
152 Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
153         switch (constraint->encoding.type) {
154         case ENUMERATEIMPLICATIONS:
155         case ENUMERATEIMPLICATIONSNEGATE:
156                 return encodeEnumTablePredicateSATEncoder(constraint);
157         case CIRCUIT:
158                 ASSERT(0);
159                 break;
160         default:
161                 ASSERT(0);
162         }
163         return E_BOGUS;
164 }
165
166 void SATEncoder::encodeElementSATEncoder(Element *element) {
167         /* Check to see if we have already encoded this element. */
168         if (element->getElementEncoding()->variables != NULL)
169                 return;
170
171         /* Need to encode. */
172         switch ( element->type) {
173         case ELEMFUNCRETURN:
174                 generateElementEncoding(element);
175                 encodeElementFunctionSATEncoder((ElementFunction *) element);
176                 break;
177         case ELEMSET:
178                 generateElementEncoding(element);
179                 return;
180         case ELEMCONST:
181                 return;
182         default:
183                 ASSERT(0);
184         }
185 }
186
187 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
188         switch (function->getFunction()->type) {
189         case TABLEFUNC:
190                 encodeTableElementFunctionSATEncoder(function);
191                 break;
192         case OPERATORFUNC:
193                 encodeOperatorElementFunctionSATEncoder(function);
194                 break;
195         default:
196                 ASSERT(0);
197         }
198 }
199
200 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
201         switch (function->getElementFunctionEncoding()->type) {
202         case ENUMERATEIMPLICATIONS:
203                 encodeEnumTableElemFunctionSATEncoder(function);
204                 break;
205         case CIRCUIT:
206                 ASSERT(0);
207                 break;
208         default:
209                 ASSERT(0);
210         }
211 }