Adding timeout for SATTune
[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         return solveCNF(cnf);
35 }
36
37 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
38         if (csolver->isUnSAT()) {
39                 return;
40         }
41         SetIteratorBooleanEdge *iterator = csolver->getConstraints();
42         while (iterator->hasNext()) {
43                 BooleanEdge constraint = iterator->next();
44                 Edge c = encodeConstraintSATEncoder(constraint);
45                 addConstraintCNF(cnf, c);
46         }
47         delete iterator;
48 }
49
50 Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
51         Edge result;
52         Boolean *constraint = c.getBoolean();
53
54         if (booledgeMap.contains(constraint)) {
55                 Edge e = {(Node *) booledgeMap.get(constraint)};
56                 return c.isNegated() ? constraintNegate(e) : e;
57         }
58
59         switch (constraint->type) {
60         case ORDERCONST:
61                 result = encodeOrderSATEncoder((BooleanOrder *) constraint);
62                 break;
63         case BOOLEANVAR:
64                 result = encodeVarSATEncoder((BooleanVar *) constraint);
65                 break;
66         case LOGICOP:
67                 result = encodeLogicSATEncoder((BooleanLogic *) constraint);
68                 break;
69         case PREDICATEOP:
70                 result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
71                 break;
72         case BOOLCONST:
73                 result = ((BooleanConst *) constraint)->isTrue() ? E_True : E_False;
74                 break;
75         default:
76                 model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
77                 exit(-1);
78         }
79         Polarity p = constraint->polarity;
80         uint pSize = constraint->parents.getSize();
81
82         if ( !edgeIsVarConst(result) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter) ) {
83                 Edge e = getNewVarSATEncoder();
84                 generateProxy(cnf, result, e, p);
85                 booledgeMap.put(constraint, e.node_ptr);
86                 result = e;
87         }
88
89         return c.isNegated() ? constraintNegate(result) : result;
90 }
91
92 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
93         for (uint i = 0; i < num; i++)
94                 carray[i] = getNewVarSATEncoder();
95 }
96
97 Edge SATEncoder::getNewVarSATEncoder() {
98         return constraintNewVar(cnf);
99 }
100
101 Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
102         if (edgeIsNull(constraint->var)) {
103                 constraint->var = getNewVarSATEncoder();
104         }
105         return constraint->var;
106 }
107
108 Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
109         Edge array[constraint->inputs.getSize()];
110         for (uint i = 0; i < constraint->inputs.getSize(); i++)
111                 array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
112
113         switch (constraint->op) {
114         case SATC_AND:
115                 return constraintAND(cnf, constraint->inputs.getSize(), array);
116         case SATC_NOT:
117                 return constraintNegate(array[0]);
118         case SATC_IFF:
119                 ASSERT(constraint->inputs.getSize() == 2);
120                 return constraintIFF(cnf, array[0], array[1]);
121         case SATC_OR:
122         case SATC_XOR:
123         case SATC_IMPLIES:
124         //Don't handle, translate these away...
125         default:
126                 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
127                 exit(-1);
128         }
129 }
130
131 Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
132         switch (constraint->predicate->type) {
133         case TABLEPRED:
134                 return encodeTablePredicateSATEncoder(constraint);
135         case OPERATORPRED:
136                 return encodeOperatorPredicateSATEncoder(constraint);
137         default:
138                 ASSERT(0);
139         }
140         return E_BOGUS;
141 }
142
143 Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
144         switch (constraint->encoding.type) {
145         case ENUMERATEIMPLICATIONS:
146         case ENUMERATEIMPLICATIONSNEGATE:
147                 return encodeEnumTablePredicateSATEncoder(constraint);
148         case CIRCUIT:
149                 ASSERT(0);
150                 break;
151         default:
152                 ASSERT(0);
153         }
154         return E_BOGUS;
155 }
156
157 void SATEncoder::encodeElementSATEncoder(Element *element) {
158         /* Check to see if we have already encoded this element. */
159         if (element->getElementEncoding()->variables != NULL)
160                 return;
161
162         /* Need to encode. */
163         switch ( element->type) {
164         case ELEMFUNCRETURN:
165                 generateElementEncoding(element);
166                 encodeElementFunctionSATEncoder((ElementFunction *) element);
167                 break;
168         case ELEMSET:
169                 generateElementEncoding(element);
170                 return;
171         case ELEMCONST:
172                 return;
173         default:
174                 ASSERT(0);
175         }
176 }
177
178 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
179         switch (function->getFunction()->type) {
180         case TABLEFUNC:
181                 encodeTableElementFunctionSATEncoder(function);
182                 break;
183         case OPERATORFUNC:
184                 encodeOperatorElementFunctionSATEncoder(function);
185                 break;
186         default:
187                 ASSERT(0);
188         }
189 }
190
191 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
192         switch (function->getElementFunctionEncoding()->type) {
193         case ENUMERATEIMPLICATIONS:
194                 encodeEnumTableElemFunctionSATEncoder(function);
195                 break;
196         case CIRCUIT:
197                 ASSERT(0);
198                 break;
199         default:
200                 ASSERT(0);
201         }
202 }