1 #include "satencoder.h"
5 #include "constraint.h"
9 #include "tableentry.h"
12 #include "predicate.h"
14 #include "satfuncopencoder.h"
16 //TODO: Should handle sharing of AST Nodes without recoding them a second time
18 SATEncoder::SATEncoder(CSolver * _solver) :
23 SATEncoder::~SATEncoder() {
27 int SATEncoder::solve() {
31 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
32 HSIteratorBoolean *iterator = csolver->getConstraints();
33 while (iterator->hasNext()) {
34 Boolean *constraint = iterator->next();
35 model_print("Encoding All ...\n\n");
36 Edge c = encodeConstraintSATEncoder(constraint);
37 model_print("Returned Constraint in EncodingAll:\n");
38 ASSERT( !equalsEdge(c, E_BOGUS));
39 addConstraintCNF(cnf, c);
44 Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
45 switch (GETBOOLEANTYPE(constraint)) {
47 return encodeOrderSATEncoder(this, (BooleanOrder *) constraint);
49 return encodeVarSATEncoder(this, (BooleanVar *) constraint);
51 return encodeLogicSATEncoder(this, (BooleanLogic *) constraint);
53 return encodePredicateSATEncoder(this, (BooleanPredicate *) constraint);
55 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
60 void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray) {
61 for (uint i = 0; i < num; i++)
62 carray[i] = getNewVarSATEncoder(encoder);
65 Edge getNewVarSATEncoder(SATEncoder *This) {
66 return constraintNewVar(This->getCNF());
69 Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint) {
70 if (edgeIsNull(constraint->var)) {
71 constraint->var = getNewVarSATEncoder(This);
73 return constraint->var;
76 Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint) {
77 Edge array[constraint->inputs.getSize()];
78 for (uint i = 0; i < constraint->inputs.getSize(); i++)
79 array[i] = This->encodeConstraintSATEncoder(constraint->inputs.get(i));
81 switch (constraint->op) {
83 return constraintAND(This->getCNF(), constraint->inputs.getSize(), array);
85 return constraintOR(This->getCNF(), constraint->inputs.getSize(), array);
87 return constraintNegate(array[0]);
89 return constraintXOR(This->getCNF(), array[0], array[1]);
91 return constraintIMPLIES(This->getCNF(), array[0], array[1]);
93 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
98 Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
99 switch (GETPREDICATETYPE(constraint->predicate) ) {
101 return encodeTablePredicateSATEncoder(This, constraint);
103 return encodeOperatorPredicateSATEncoder(This, constraint);
110 Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
111 switch (constraint->encoding.type) {
112 case ENUMERATEIMPLICATIONS:
113 case ENUMERATEIMPLICATIONSNEGATE:
114 return encodeEnumTablePredicateSATEncoder(This, constraint);
124 void encodeElementSATEncoder(SATEncoder *encoder, Element *This) {
125 switch ( GETELEMENTTYPE(This) ) {
127 generateElementEncoding(encoder, This);
128 encodeElementFunctionSATEncoder(encoder, (ElementFunction *) This);
131 generateElementEncoding(encoder, This);
140 void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
141 switch (GETFUNCTIONTYPE(This->function)) {
143 encodeTableElementFunctionSATEncoder(encoder, This);
146 encodeOperatorElementFunctionSATEncoder(encoder, This);
153 void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
154 switch (getElementFunctionEncoding(This)->type) {
155 case ENUMERATEIMPLICATIONS:
156 encodeEnumTableElemFunctionSATEncoder(encoder, This);