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 SetIteratorBoolean *iterator = csolver->getConstraints();
30 while (iterator->hasNext()) {
31 Boolean *constraint = iterator->next();
32 Edge c = encodeConstraintSATEncoder(constraint);
33 addConstraintCNF(cnf, c);
38 Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
40 if (booledgeMap.contains(constraint)) {
41 Edge e={(Node *) booledgeMap.get(constraint)};
45 switch (constraint->type) {
47 result=encodeOrderSATEncoder((BooleanOrder *) constraint);
50 result=encodeVarSATEncoder((BooleanVar *) constraint);
53 result=encodeLogicSATEncoder((BooleanLogic *) constraint);
56 result=encodePredicateSATEncoder((BooleanPredicate *) constraint);
59 model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
62 booledgeMap.put(constraint, result.node_ptr);
66 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
67 for (uint i = 0; i < num; i++)
68 carray[i] = getNewVarSATEncoder();
71 Edge SATEncoder::getNewVarSATEncoder() {
72 return constraintNewVar(cnf);
75 Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
76 if (edgeIsNull(constraint->var)) {
77 constraint->var = getNewVarSATEncoder();
79 return constraint->var;
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));
87 switch (constraint->op) {
89 return constraintAND(cnf, constraint->inputs.getSize(), array);
91 return constraintOR(cnf, constraint->inputs.getSize(), array);
93 return constraintNegate(array[0]);
95 return constraintXOR(cnf, array[0], array[1]);
97 return constraintIMPLIES(cnf, array[0], array[1]);
99 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
104 Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
105 switch (constraint->predicate->type) {
107 return encodeTablePredicateSATEncoder(constraint);
109 return encodeOperatorPredicateSATEncoder(constraint);
116 Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
117 switch (constraint->encoding.type) {
118 case ENUMERATEIMPLICATIONS:
119 case ENUMERATEIMPLICATIONSNEGATE:
120 return encodeEnumTablePredicateSATEncoder(constraint);
130 void SATEncoder::encodeElementSATEncoder(Element *element) {
131 /* Check to see if we have already encoded this element. */
132 if (getElementEncoding(element)->variables != NULL)
135 /* Need to encode. */
136 switch ( element->type) {
138 generateElementEncoding(element);
139 encodeElementFunctionSATEncoder((ElementFunction *) element);
142 generateElementEncoding(element);
151 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
152 switch (function->function->type) {
154 encodeTableElementFunctionSATEncoder(function);
157 encodeOperatorElementFunctionSATEncoder(function);
164 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
165 switch (getElementFunctionEncoding(function)->type) {
166 case ENUMERATEIMPLICATIONS:
167 encodeEnumTableElemFunctionSATEncoder(function);