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 * allocSATEncoder() {
18 SATEncoder *This=ourmalloc(sizeof (SATEncoder));
20 This->cnf=createCNF();
24 void deleteSATEncoder(SATEncoder *This) {
29 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
30 VectorBoolean *constraints=csolver->constraints;
31 uint size=getSizeVectorBoolean(constraints);
32 for(uint i=0;i<size;i++) {
33 Boolean *constraint=getVectorBoolean(constraints, i);
34 Edge c= encodeConstraintSATEncoder(This, constraint);
37 addConstraintCNF(This->cnf, c);
41 Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
42 switch(GETBOOLEANTYPE(constraint)) {
44 return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
46 return encodeVarSATEncoder(This, (BooleanVar *) constraint);
48 return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
50 return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint);
52 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
57 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Edge * carray) {
58 for(uint i=0;i<num;i++)
59 carray[i]=getNewVarSATEncoder(encoder);
62 Edge getNewVarSATEncoder(SATEncoder *This) {
63 return constraintNewVar(This->cnf);
66 Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
67 if (edgeIsNull(constraint->var)) {
68 constraint->var=getNewVarSATEncoder(This);
70 return constraint->var;
73 Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
74 Edge array[getSizeArrayBoolean(&constraint->inputs)];
75 for(uint i=0;i<getSizeArrayBoolean(&constraint->inputs);i++)
76 array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
78 switch(constraint->op) {
80 return constraintAND(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
82 return constraintOR(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
84 ASSERT( getSizeArrayBoolean(&constraint->inputs)==1);
85 return constraintNegate(array[0]);
87 ASSERT( getSizeArrayBoolean(&constraint->inputs)==2);
88 return constraintXOR(This->cnf, array[0], array[1]);
90 ASSERT( getSizeArrayBoolean( &constraint->inputs)==2);
91 return constraintIMPLIES(This->cnf, 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 encodeElementFunctionSATEncoder(encoder, (ElementFunction*) This);
136 void encodeElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction *This){
137 switch(GETFUNCTIONTYPE(This->function)){
139 encodeTableElementFunctionSATEncoder(encoder, This);
142 encodeOperatorElementFunctionSATEncoder(encoder, This);
149 void encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
150 switch(getElementFunctionEncoding(This)->type){
151 case ENUMERATEIMPLICATIONS:
152 encodeEnumTableElemFunctionSATEncoder(encoder, This);