1 #include "satencoder.h"
5 #include "constraint.h"
7 SATEncoder * allocSATEncoder() {
8 SATEncoder *This=ourmalloc(sizeof (SATEncoder));
13 void deleteSATEncoder(SATEncoder *This) {
17 void encodeAllSATEncoder(SATEncoder * This, CSolver *csolver) {
18 VectorBoolean *constraints=csolver->constraints;
19 uint size=getSizeVectorBoolean(constraints);
20 for(uint i=0;i<size;i++) {
21 Boolean *constraint=getVectorBoolean(constraints, i);
22 encodeConstraintSATEncoder(This, constraint);
26 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
27 switch(constraint->btype) {
29 return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
31 return encodeVarSATEncoder(This, (BooleanVar *) constraint);
33 return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
35 return encodeCompareSATEncoder(This, (BooleanComp *) constraint);
39 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
43 Constraint * getNewVarSATEncoder(SATEncoder *This) {
44 Constraint * var=allocVarConstraint(VAR, This->varcount);
45 Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
46 setNegConstraint(var, varneg);
47 setNegConstraint(varneg, var);
51 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
52 if (constraint->var == NULL) {
53 constraint->var=getNewVarSATEncoder(This);
55 return constraint->var;
58 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
59 Constraint *left=encodeConstraintSATEncoder(This, constraint->left);
60 Constraint *right=NULL;
61 if (constraint->right!=NULL)
62 right=encodeConstraintSATEncoder(This, constraint->right);
63 switch(constraint->op) {
65 return allocConstraint(AND, left, right);
67 return allocConstraint(OR, left, right);
69 return negateConstraint(allocConstraint(OR, left, NULL));
71 Constraint * nleft=negateConstraint(cloneConstraint(left));
72 Constraint * nright=negateConstraint(cloneConstraint(right));
73 return allocConstraint(OR,
74 allocConstraint(AND, left, nright),
75 allocConstraint(AND, nleft, right));
78 return allocConstraint(IMPLIES, left, right);
83 Constraint * encodeCompareSATEncoder(SATEncoder *This, BooleanComp * constraint) {