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 int SATEncoder::solve() {
28 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
29 SetIteratorBooleanEdge *iterator = csolver->getConstraints();
30 while (iterator->hasNext()) {
31 BooleanEdge constraint = iterator->next();
32 Edge c = encodeConstraintSATEncoder(constraint);
33 addConstraintCNF(cnf, c);
38 Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
40 Boolean * constraint = c.getBoolean();
42 if (booledgeMap.contains(constraint)) {
43 Edge e = {(Node *) booledgeMap.get(constraint)};
44 return c.isNegated() ? constraintNegate(e) : e;
47 switch (constraint->type) {
49 result = encodeOrderSATEncoder((BooleanOrder *) constraint);
52 result = encodeVarSATEncoder((BooleanVar *) constraint);
55 result = encodeLogicSATEncoder((BooleanLogic *) constraint);
58 result = encodePredicateSATEncoder((BooleanPredicate *) constraint);
61 model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
64 booledgeMap.put(constraint, result.node_ptr);
65 return c.isNegated() ? constraintNegate(result) : result;
68 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
69 for (uint i = 0; i < num; i++)
70 carray[i] = getNewVarSATEncoder();
73 Edge SATEncoder::getNewVarSATEncoder() {
74 return constraintNewVar(cnf);
77 Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
78 if (edgeIsNull(constraint->var)) {
79 constraint->var = getNewVarSATEncoder();
81 return constraint->var;
84 Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
85 Edge array[constraint->inputs.getSize()];
86 for (uint i = 0; i < constraint->inputs.getSize(); i++)
87 array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
89 switch (constraint->op) {
91 return constraintAND(cnf, constraint->inputs.getSize(), array);
93 return constraintNegate(array[0]);
95 return constraintIFF(cnf, array[0], array[1]);
99 //Don't handle, translate these away...
101 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
106 Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
107 switch (constraint->predicate->type) {
109 return encodeTablePredicateSATEncoder(constraint);
111 return encodeOperatorPredicateSATEncoder(constraint);
118 Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
119 switch (constraint->encoding.type) {
120 case ENUMERATEIMPLICATIONS:
121 case ENUMERATEIMPLICATIONSNEGATE:
122 return encodeEnumTablePredicateSATEncoder(constraint);
132 void SATEncoder::encodeElementSATEncoder(Element *element) {
133 /* Check to see if we have already encoded this element. */
134 if (getElementEncoding(element)->variables != NULL)
137 /* Need to encode. */
138 switch ( element->type) {
140 generateElementEncoding(element);
141 encodeElementFunctionSATEncoder((ElementFunction *) element);
144 generateElementEncoding(element);
153 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
154 switch (function->getFunction()->type) {
156 encodeTableElementFunctionSATEncoder(function);
159 encodeOperatorElementFunctionSATEncoder(function);
166 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
167 switch (getElementFunctionEncoding(function)->type) {
168 case ENUMERATEIMPLICATIONS:
169 encodeEnumTableElemFunctionSATEncoder(function);