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);
37 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
41 Constraint * getNewVarSATEncoder(SATEncoder *This) {
42 Constraint * var=allocVarConstraint(VAR, This->varcount);
43 Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
44 setNegConstraint(var, varneg);
45 setNegConstraint(varneg, var);
49 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
50 if (constraint->var == NULL) {
51 constraint->var=getNewVarSATEncoder(This);
53 return constraint->var;
56 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
57 Constraint *left=encodeConstraintSATEncoder(This, constraint->left);
58 Constraint *right=NULL;
59 if (constraint->right!=NULL)
60 right=encodeConstraintSATEncoder(This, constraint->right);
61 switch(constraint->op) {
63 return allocConstraint(AND, left, right);
65 return allocConstraint(OR, left, right);
67 return negateConstraint(allocConstraint(OR, left, NULL));
69 Constraint * nleft=negateConstraint(cloneConstraint(left));
70 Constraint * nright=negateConstraint(cloneConstraint(right));
71 return allocConstraint(OR,
72 allocConstraint(AND, left, nright),
73 allocConstraint(AND, nleft, right));
76 return allocConstraint(IMPLIES, left, right);