1 #include "satencoder.h"
5 #include "constraint.h"
9 #include "tableentry.h"
12 #include "predicate.h"
15 SATEncoder::SATEncoder(CSolver *_solver) :
20 SATEncoder::~SATEncoder() {
24 void SATEncoder::resetSATEncoder() {
29 int SATEncoder::solve() {
33 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
34 SetIteratorBooleanEdge *iterator = csolver->getConstraints();
35 while (iterator->hasNext()) {
36 BooleanEdge constraint = iterator->next();
37 Edge c = encodeConstraintSATEncoder(constraint);
38 addConstraintCNF(cnf, c);
43 Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
45 Boolean *constraint = c.getBoolean();
47 if (booledgeMap.contains(constraint)) {
48 Edge e = {(Node *) booledgeMap.get(constraint)};
49 return c.isNegated() ? constraintNegate(e) : e;
52 switch (constraint->type) {
54 result = encodeOrderSATEncoder((BooleanOrder *) constraint);
57 result = encodeVarSATEncoder((BooleanVar *) constraint);
60 result = encodeLogicSATEncoder((BooleanLogic *) constraint);
63 result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
66 model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
69 booledgeMap.put(constraint, result.node_ptr);
70 return c.isNegated() ? constraintNegate(result) : result;
73 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
74 for (uint i = 0; i < num; i++)
75 carray[i] = getNewVarSATEncoder();
78 Edge SATEncoder::getNewVarSATEncoder() {
79 return constraintNewVar(cnf);
82 Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
83 if (edgeIsNull(constraint->var)) {
84 constraint->var = getNewVarSATEncoder();
86 return constraint->var;
89 Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
90 Edge array[constraint->inputs.getSize()];
91 for (uint i = 0; i < constraint->inputs.getSize(); i++)
92 array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
94 switch (constraint->op) {
96 return constraintAND(cnf, constraint->inputs.getSize(), array);
98 return constraintNegate(array[0]);
100 return constraintIFF(cnf, array[0], array[1]);
104 //Don't handle, translate these away...
106 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
111 Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
112 switch (constraint->predicate->type) {
114 return encodeTablePredicateSATEncoder(constraint);
116 return encodeOperatorPredicateSATEncoder(constraint);
123 Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
124 switch (constraint->encoding.type) {
125 case ENUMERATEIMPLICATIONS:
126 case ENUMERATEIMPLICATIONSNEGATE:
127 return encodeEnumTablePredicateSATEncoder(constraint);
137 void SATEncoder::encodeElementSATEncoder(Element *element) {
138 /* Check to see if we have already encoded this element. */
139 if (element->getElementEncoding()->variables != NULL)
142 /* Need to encode. */
143 switch ( element->type) {
145 generateElementEncoding(element);
146 encodeElementFunctionSATEncoder((ElementFunction *) element);
149 generateElementEncoding(element);
158 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
159 switch (function->getFunction()->type) {
161 encodeTableElementFunctionSATEncoder(function);
164 encodeOperatorElementFunctionSATEncoder(function);
171 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
172 switch (function->getElementFunctionEncoding()->type) {
173 case ENUMERATEIMPLICATIONS:
174 encodeEnumTableElemFunctionSATEncoder(function);