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() {
19 SATEncoder *This=ourmalloc(sizeof (SATEncoder));
21 This->cnf=createCNF();
25 void deleteSATEncoder(SATEncoder *This) {
30 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
31 VectorBoolean *constraints=csolver->constraints;
32 uint size=getSizeVectorBoolean(constraints);
33 for(uint i=0;i<size;i++) {
34 model_print("Encoding All ...\n\n");
35 Boolean *constraint=getVectorBoolean(constraints, i);
36 Edge c= encodeConstraintSATEncoder(This, constraint);
37 model_print("Returned Constraint in EncodingAll:\n");
38 addConstraintCNF(This->cnf, c);
42 Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
43 switch(GETBOOLEANTYPE(constraint)) {
45 return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
47 return encodeVarSATEncoder(This, (BooleanVar *) constraint);
49 return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
51 return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint);
53 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
58 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Edge * carray) {
59 for(uint i=0;i<num;i++)
60 carray[i]=getNewVarSATEncoder(encoder);
63 Edge getNewVarSATEncoder(SATEncoder *This) {
64 return constraintNewVar(This->cnf);
67 Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
68 if (edgeIsNull(constraint->var)) {
69 constraint->var=getNewVarSATEncoder(This);
71 return constraint->var;
74 Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
75 Edge array[getSizeArrayBoolean(&constraint->inputs)];
76 for(uint i=0;i<getSizeArrayBoolean(&constraint->inputs);i++)
77 array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
79 switch(constraint->op) {
81 return constraintAND(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
83 return constraintOR(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
85 ASSERT( getSizeArrayBoolean(&constraint->inputs)==1);
86 return constraintNegate(array[0]);
88 ASSERT( getSizeArrayBoolean(&constraint->inputs)==2);
89 return constraintXOR(This->cnf, array[0], array[1]);
91 ASSERT( getSizeArrayBoolean( &constraint->inputs)==2);
92 return constraintIMPLIES(This->cnf, array[0], array[1]);
94 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
99 Edge encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
100 switch(GETPREDICATETYPE(constraint->predicate) ){
102 return encodeTablePredicateSATEncoder(This, constraint);
104 return encodeOperatorPredicateSATEncoder(This, constraint);
111 Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
112 switch(constraint->encoding.type){
113 case ENUMERATEIMPLICATIONS:
114 case ENUMERATEIMPLICATIONSNEGATE:
115 return encodeEnumTablePredicateSATEncoder(This, constraint);
125 void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
126 switch( GETELEMENTTYPE(This) ){
128 generateElementEncoding(encoder, This);
129 encodeElementFunctionSATEncoder(encoder, (ElementFunction*) This);
132 generateElementEncoding(encoder, This);
141 void encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This){
142 switch(GETFUNCTIONTYPE(This->function)){
144 encodeTableElementFunctionSATEncoder(encoder, This);
147 encodeOperatorElementFunctionSATEncoder(encoder, This);
154 void encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
155 switch(getElementFunctionEncoding(This)->type){
156 case ENUMERATEIMPLICATIONS:
157 encodeEnumTableElemFunctionSATEncoder(encoder, This);