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();
34 model_print("Encoding All ...\n\n");
35 Edge c = encodeConstraintSATEncoder(constraint);
36 model_print("Returned Constraint in EncodingAll:\n");
37 ASSERT( !equalsEdge(c, E_BOGUS));
38 addConstraintCNF(cnf, c);
43 Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
44 switch (GETBOOLEANTYPE(constraint)) {
46 return encodeOrderSATEncoder((BooleanOrder *) constraint);
48 return encodeVarSATEncoder((BooleanVar *) constraint);
50 return encodeLogicSATEncoder((BooleanLogic *) constraint);
52 return encodePredicateSATEncoder((BooleanPredicate *) constraint);
54 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
59 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
60 for (uint i = 0; i < num; i++)
61 carray[i] = getNewVarSATEncoder();
64 Edge SATEncoder::getNewVarSATEncoder() {
65 return constraintNewVar(cnf);
68 Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
69 if (edgeIsNull(constraint->var)) {
70 constraint->var = getNewVarSATEncoder();
72 return constraint->var;
75 Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
76 Edge array[constraint->inputs.getSize()];
77 for (uint i = 0; i < constraint->inputs.getSize(); i++)
78 array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
80 switch (constraint->op) {
82 return constraintAND(cnf, constraint->inputs.getSize(), array);
84 return constraintOR(cnf, constraint->inputs.getSize(), array);
86 return constraintNegate(array[0]);
88 return constraintXOR(cnf, array[0], array[1]);
90 return constraintIMPLIES(cnf, array[0], array[1]);
92 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
97 Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
98 switch (GETPREDICATETYPE(constraint->predicate) ) {
100 return encodeTablePredicateSATEncoder(constraint);
102 return encodeOperatorPredicateSATEncoder(constraint);
109 Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
110 switch (constraint->encoding.type) {
111 case ENUMERATEIMPLICATIONS:
112 case ENUMERATEIMPLICATIONSNEGATE:
113 return encodeEnumTablePredicateSATEncoder(constraint);
123 void SATEncoder::encodeElementSATEncoder(Element *element) {
124 switch ( GETELEMENTTYPE(element) ) {
126 generateElementEncoding(element);
127 encodeElementFunctionSATEncoder((ElementFunction *) element);
130 generateElementEncoding(element);
139 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
140 switch (GETFUNCTIONTYPE(function->function)) {
142 encodeTableElementFunctionSATEncoder(function);
145 encodeOperatorElementFunctionSATEncoder(function);
152 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
153 switch (getElementFunctionEncoding(function)->type) {
154 case ENUMERATEIMPLICATIONS:
155 encodeEnumTableElemFunctionSATEncoder(function);