e053d78514f0b3d2b33868837aa2bd5ca97fb1c0
[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
15 SATEncoder::SATEncoder(CSolver * _solver) :
16         cnf(createCNF()),
17         solver(_solver) {
18 }
19
20 SATEncoder::~SATEncoder() {
21         deleteCNF(cnf);
22 }
23
24 int SATEncoder::solve() {
25         return solveCNF(cnf);
26 }
27
28 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
29         SetIteratorBoolean *iterator = csolver->getConstraints();
30         while (iterator->hasNext()) {
31                 Boolean *constraint = iterator->next();
32                 Edge c = encodeConstraintSATEncoder(constraint);
33                 addConstraintCNF(cnf, c);
34         }
35         delete iterator;
36 }
37
38 Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
39         Edge result;
40         if (booledgeMap.contains(constraint)) {
41                 Edge e={(Node *) booledgeMap.get(constraint)};
42                 return e;
43         }
44         
45         switch (constraint->type) {
46         case ORDERCONST:
47                 result=encodeOrderSATEncoder((BooleanOrder *) constraint);
48                 break;
49         case BOOLEANVAR:
50                 result=encodeVarSATEncoder((BooleanVar *) constraint);
51                 break;
52         case LOGICOP:
53                 result=encodeLogicSATEncoder((BooleanLogic *) constraint);
54                 break;
55         case PREDICATEOP:
56                 result=encodePredicateSATEncoder((BooleanPredicate *) constraint);
57                 break;
58         default:
59                 model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
60                 exit(-1);
61         }
62         booledgeMap.put(constraint, result.node_ptr);
63         return result;
64 }
65
66 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
67         for (uint i = 0; i < num; i++)
68                 carray[i] = getNewVarSATEncoder();
69 }
70
71 Edge SATEncoder::getNewVarSATEncoder() {
72         return constraintNewVar(cnf);
73 }
74
75 Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
76         if (edgeIsNull(constraint->var)) {
77                 constraint->var = getNewVarSATEncoder();
78         }
79         return constraint->var;
80 }
81
82 Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
83         Edge array[constraint->inputs.getSize()];
84         for (uint i = 0; i < constraint->inputs.getSize(); i++)
85                 array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
86
87         switch (constraint->op) {
88         case SATC_AND:
89                 return constraintAND(cnf, constraint->inputs.getSize(), array);
90         case SATC_OR:
91                 return constraintOR(cnf, constraint->inputs.getSize(), array);
92         case SATC_NOT:
93                 return constraintNegate(array[0]);
94         case SATC_XOR:
95                 return constraintXOR(cnf, array[0], array[1]);
96         case SATC_IMPLIES:
97                 return constraintIMPLIES(cnf, array[0], array[1]);
98         default:
99                 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
100                 exit(-1);
101         }
102 }
103
104 Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
105         switch (constraint->predicate->type) {
106         case TABLEPRED:
107                 return encodeTablePredicateSATEncoder(constraint);
108         case OPERATORPRED:
109                 return encodeOperatorPredicateSATEncoder(constraint);
110         default:
111                 ASSERT(0);
112         }
113         return E_BOGUS;
114 }
115
116 Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
117         switch (constraint->encoding.type) {
118         case ENUMERATEIMPLICATIONS:
119         case ENUMERATEIMPLICATIONSNEGATE:
120                 return encodeEnumTablePredicateSATEncoder(constraint);
121         case CIRCUIT:
122                 ASSERT(0);
123                 break;
124         default:
125                 ASSERT(0);
126         }
127         return E_BOGUS;
128 }
129
130 void SATEncoder::encodeElementSATEncoder(Element *element) {
131         /* Check to see if we have already encoded this element. */
132         if (getElementEncoding(element)->variables != NULL)
133                 return;
134         
135         /* Need to encode. */
136         switch ( element->type) {
137         case ELEMFUNCRETURN:
138                 generateElementEncoding(element);
139                 encodeElementFunctionSATEncoder((ElementFunction *) element);
140                 break;
141         case ELEMSET:
142                 generateElementEncoding(element);
143                 return;
144         case ELEMCONST:
145                 return;
146         default:
147                 ASSERT(0);
148         }
149 }
150
151 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
152         switch (function->function->type) {
153         case TABLEFUNC:
154                 encodeTableElementFunctionSATEncoder(function);
155                 break;
156         case OPERATORFUNC:
157                 encodeOperatorElementFunctionSATEncoder(function);
158                 break;
159         default:
160                 ASSERT(0);
161         }
162 }
163
164 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
165         switch (getElementFunctionEncoding(function)->type) {
166         case ENUMERATEIMPLICATIONS:
167                 encodeEnumTableElemFunctionSATEncoder(function);
168                 break;
169         case CIRCUIT:
170                 ASSERT(0);
171                 break;
172         default:
173                 ASSERT(0);
174         }
175 }