edits

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 35418088be0ff31e624a3f72fbcf2acf650a42f4..3b3e3c39bd11bf6ae9f2275d4b72de4d3e353716 100644 (file)
--- a/src/AST/ops.h
+++ b/src/AST/ops.h
@@ -1,6 +1,6 @@
 #ifndef OPS_H
 #define OPS_H
-enum LogicOp {AND, OR, NOT, XOR, IMPLIES};
+enum LogicOp {L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES};
 typedef enum LogicOp LogicOp;
 
 enum ArithOp {ADD, SUB};

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 4b59812d91fe1c5b0ea95e05bd1d58b63c9ae303..d6e7e868dfd0b6006d4b8d5a4bade77957374829 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -33,15 +33,15 @@ Constraint * allocVarConstraint(CType t, uint var);
 void deleteConstraint(Constraint *);
 void printConstraint(Constraint * c);
 void dumpConstraint(Constraint * c, IncrementalSolver *solver);
-uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;}
+inline uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;}
 VectorConstraint * simplify(Constraint * c);
-CType getType(Constraint * c) {return c->type;}
-bool isFalse(Constraint * c) {return c->type==FALSE;}
-bool isTrue(Constraint * c) {return c->type==TRUE;}
+inline CType getType(Constraint * c) {return c->type;}
+inline bool isFalse(Constraint * c) {return c->type==FALSE;}
+inline bool isTrue(Constraint * c) {return c->type==TRUE;}
 void internalfreeConstraint(Constraint * c);
 void freerecConstraint(Constraint * c);
 Constraint * cloneConstraint(Constraint * c);
-void setNegConstraint(Constraint * This, Constraint *c) {This->neg=c;}
+inline void setNegConstraint(Constraint * This, Constraint *c) {This->neg=c;}
 Constraint *negateConstraint(Constraint * c);
 
 extern Constraint ctrue;

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index a2f96d5457bb8f0d7b717466c22f2fff480fa7fa..3b34c3a9fa44fe717548146c89bae0039b56bd55 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -1,6 +1,8 @@
 #include "satencoder.h"
 #include "structs.h"
 #include "csolver.h"
+#include "boolean.h"
+#include "constraint.h"
 
 SATEncoder * allocSATEncoder() {
        SATEncoder *This=ourmalloc(sizeof (SATEncoder));
@@ -20,6 +22,52 @@ void encodeAllSATEncoder(SATEncoder * This, CSolver *csolver) {
        }
 }
 
-void encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
+Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
+       switch(constraint->btype) {
+       case ORDERCONST:
+               return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
+       case BOOLEANVAR:
+               return encodeVarSATEncoder(This, (BooleanVar *) constraint);
+       case LOGICOP:
+               return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
+       case COMPARE:
+               return encodeCompareSATEncoder(This, (BooleanComp *) constraint);
+       }
+}
+
+Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
+       return NULL;
+}
+
+Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
+       return NULL;
+}
+
+Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
+       Constraint *left=encodeConstraintSATEncoder(This, constraint->left);
+       Constraint *right=NULL;
+       if (constraint->right!=NULL)
+               right=encodeConstraintSATEncoder(This, constraint->right);
+       switch(constraint->op) {
+       case L_AND:
+               return allocConstraint(AND, left, right);
+       case L_OR:
+               return allocConstraint(OR, left, right);
+       case L_NOT:
+               return negateConstraint(allocConstraint(OR, left, NULL));
+       case L_XOR: {
+               Constraint * nleft=negateConstraint(cloneConstraint(left));
+               Constraint * nright=negateConstraint(cloneConstraint(right));
+               return allocConstraint(OR,
+                                                                                                        allocConstraint(AND, left, nright),
+                                                                                                        allocConstraint(AND, nleft, right));
+       }
+       case L_IMPLIES:
+               return allocConstraint(IMPLIES, left, right);
+       }
+       return NULL;
+}
 
+Constraint * encodeCompareSATEncoder(SATEncoder *This, BooleanComp * constraint) {
+       return NULL;
 }

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 9145e2b40ab56dd9ec8308fdff368215939b04c0..a61293076a2cde8f792cf92973e7af199cda20cc 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -11,5 +11,10 @@ struct SATEncoder {
 SATEncoder * allocSATEncoder();
 void deleteSATEncoder(SATEncoder *This);
 void encodeAllSATEncoder(SATEncoder *This, CSolver *csolver);
-void encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
+Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
+Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
+Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
+Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint);
+Constraint * encodeCompareSATEncoder(SATEncoder *This, BooleanComp * constraint);
+
 #endif

diff --git a/src/Encoders/orderencoding.c b/src/Encoders/orderencoding.c
index fcef2f365c5e581d600f277834a6b545742f3acc..3cd78e15df06eab51a25a752d40bfeb17c8f922a 100644 (file)
--- a/src/Encoders/orderencoding.c
+++ b/src/Encoders/orderencoding.c
@@ -1,7 +1,9 @@
 #include "orderencoding.h"
 
-OrderEncoding * allocOrderEncoding() {
+OrderEncoding * allocOrderEncoding(OrderEncodingType type, Order *order) {
        OrderEncoding *This=ourmalloc(sizeof(OrderEncoding));
+       This->type=type;
+       This->order=order;
        return This;
 }
 

diff --git a/src/Encoders/orderencoding.h b/src/Encoders/orderencoding.h
index c0e4c00d5f6441ee1b4cf92b85dc8fc89789a8d5..89c436a38237535935a037a235e0f2156695b8f4 100644 (file)
--- a/src/Encoders/orderencoding.h
+++ b/src/Encoders/orderencoding.h
@@ -2,11 +2,18 @@
 #define ORDERENCODING_H
 #include "classlist.h"
 
-struct OrderEncoding {
+enum OrderEncodingType {
+       PAIRWISE
+};
 
+typedef enum OrderEncodingType OrderEncodingType;
+
+struct OrderEncoding {
+       OrderEncodingType type;
+       Order *order;
 };
 
-OrderEncoding * allocOrderEncoding();
+OrderEncoding * allocOrderEncoding(OrderEncodingType type, Order *order);
 void deleteOrderEncoding(OrderEncoding *This);
 
 #endif