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