More SAT Encoder

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 7d9aec39f8bac6e042b0bb76b415ee189e2bd5c2..1a46ccd6a118c32bbd680119af35a894e51b1052 100644 (file)
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -4,6 +4,7 @@ Boolean* allocBoolean(VarType t) {
        BooleanVar* tmp=(BooleanVar *) ourmalloc(sizeof (BooleanVar));
        GETBOOLEANTYPE(tmp)=BOOLEANVAR;
        tmp->vtype=t;
+       tmp->var=NULL;
        return & tmp->base;
 }
 

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index d00a82cf123fa325eb1d2eadef911272df66302d..860365f891b3b8edff3f628da504ad0dac2fc421 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -24,6 +24,7 @@ struct BooleanOrder {
 struct BooleanVar {
        Boolean base;
        VarType vtype;
+       Constraint * var;
 };
 
 struct BooleanLogic {

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 3b34c3a9fa44fe717548146c89bae0039b56bd55..2918771f7387c3c27c6981f5f52dca6f8f2c9bae 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -6,6 +6,7 @@
 
 SATEncoder * allocSATEncoder() {
        SATEncoder *This=ourmalloc(sizeof (SATEncoder));
+       This->varcount=1;
        return This;
 }
 
@@ -39,8 +40,19 @@ Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint)
        return NULL;
 }
 
+Constraint * getNewVarSATEncoder(SATEncoder *This) {
+       Constraint * var=allocVarConstraint(VAR, This->varcount);
+       Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
+       setNegConstraint(var, varneg);
+       setNegConstraint(varneg, var);
+       return var;
+}
+
 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
-       return NULL;
+       if (constraint->var == NULL) {
+               constraint->var=getNewVarSATEncoder(This);
+       }
+       return constraint->var;
 }
 
 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index a61293076a2cde8f792cf92973e7af199cda20cc..5d8722ca1415dda78a27ef7bc521dc6e4a63f95d 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -4,13 +4,14 @@
 #include "classlist.h"
 
 struct SATEncoder {
-
+       uint varcount;
 };
 
 
 SATEncoder * allocSATEncoder();
 void deleteSATEncoder(SATEncoder *This);
 void encodeAllSATEncoder(SATEncoder *This, CSolver *csolver);
+Constraint * getNewVarSATEncoder(SATEncoder *This);
 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);