1 #include "satencoder.h"
5 #include "constraint.h"
9 #include "tableentry.h"
12 #include "predicate.h"
15 //TODO: Should handle sharing of AST Nodes without recoding them a second time
17 SATEncoder::SATEncoder(CSolver * _solver) :
22 SATEncoder::~SATEncoder() {
26 int SATEncoder::solve() {
30 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
31 HSIteratorBoolean *iterator = csolver->getConstraints();
32 while (iterator->hasNext()) {
33 Boolean *constraint = iterator->next();
35 model_print("Encoding All ...\n\n");
37 Edge c = encodeConstraintSATEncoder(constraint);
39 model_print("Returned Constraint in EncodingAll:\n");
41 ASSERT( !equalsEdge(c, E_BOGUS));
42 addConstraintCNF(cnf, c);
47 Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
48 switch (constraint->type) {
50 return encodeOrderSATEncoder((BooleanOrder *) constraint);
52 return encodeVarSATEncoder((BooleanVar *) constraint);
54 return encodeLogicSATEncoder((BooleanLogic *) constraint);
56 return encodePredicateSATEncoder((BooleanPredicate *) constraint);
58 model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
63 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
64 for (uint i = 0; i < num; i++)
65 carray[i] = getNewVarSATEncoder();
68 Edge SATEncoder::getNewVarSATEncoder() {
69 return constraintNewVar(cnf);
72 Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
73 if (edgeIsNull(constraint->var)) {
74 constraint->var = getNewVarSATEncoder();
76 return constraint->var;
79 Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
80 Edge array[constraint->inputs.getSize()];
81 for (uint i = 0; i < constraint->inputs.getSize(); i++)
82 array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
84 switch (constraint->op) {
86 return constraintAND(cnf, constraint->inputs.getSize(), array);
88 return constraintOR(cnf, constraint->inputs.getSize(), array);
90 return constraintNegate(array[0]);
92 return constraintXOR(cnf, array[0], array[1]);
94 return constraintIMPLIES(cnf, array[0], array[1]);
96 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
101 Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
102 switch (constraint->predicate->type) {
104 return encodeTablePredicateSATEncoder(constraint);
106 return encodeOperatorPredicateSATEncoder(constraint);
113 Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
114 switch (constraint->encoding.type) {
115 case ENUMERATEIMPLICATIONS:
116 case ENUMERATEIMPLICATIONSNEGATE:
117 return encodeEnumTablePredicateSATEncoder(constraint);
127 void SATEncoder::encodeElementSATEncoder(Element *element) {
128 switch ( element->type) {
130 generateElementEncoding(element);
131 encodeElementFunctionSATEncoder((ElementFunction *) element);
134 generateElementEncoding(element);
143 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
144 switch (function->function->type) {
146 encodeTableElementFunctionSATEncoder(function);
149 encodeOperatorElementFunctionSATEncoder(function);
156 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
157 switch (getElementFunctionEncoding(function)->type) {
158 case ENUMERATEIMPLICATIONS:
159 encodeEnumTableElemFunctionSATEncoder(function);