Adding new API for defining an order constraint on two orders...

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 09ec2ae817de133940927287c7e68d65fe0427f7..a984515d03c04e2ea566f4489c06095582e2e4af 100644 (file)
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -28,6 +28,20 @@ Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) {
        return & This -> base;
 }
 
+Boolean * allocBooleanInterOrder(Order * order1, uint64_t first,Order* order2, uint64_t second){
+       BooleanInterOrder* This=(BooleanInterOrder *) ourmalloc(sizeof (BooleanInterOrder));
+       GETBOOLEANTYPE(This)=INTERORDERCONST;
+       GETBOOLEANVALUE(This) = BV_UNDEFINED;
+       GETBOOLEANPOLARITY(This) = P_UNDEFINED;
+       This->order1=order1;
+       This->order2 = order2;
+       This->first=first;
+       This->second=second;
+       pushVectorBoolean(&order1->constraints, &This->base);
+       initDefVectorBoolean(GETBOOLEANPARENTS(This));
+       return & This -> base;
+}
+
 Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus){
        BooleanPredicate* This = (BooleanPredicate*) ourmalloc(sizeof(BooleanPredicate));
        GETBOOLEANTYPE(This)= PREDICATEOP;

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index b24fa3f83e10d9cf093b6478bb515e7710507317..eb3b02cd42d955bd319218a7b0b28a36d8ac4e65 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -31,6 +31,15 @@ struct BooleanOrder {
        uint64_t second;
 };
 
+//I don't like the name, we may want to change it later --HG
+struct BooleanInterOrder{
+       Boolean base;
+       Order* order1;
+       uint64_t first;
+       Order* order2;
+       uint64_t second;
+};
+
 struct BooleanVar {
        Boolean base;
        VarType vtype;
@@ -53,6 +62,7 @@ struct BooleanPredicate {
 
 Boolean * allocBooleanVar(VarType t);
 Boolean * allocBooleanOrder(Order * order, uint64_t first, uint64_t second);
+Boolean * allocBooleanInterOrder(Order * order1, uint64_t first,Order* order2, uint64_t second);
 Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus);
 Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize);
 void deleteBoolean(Boolean * This);

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 9e8113d685ce48bd0e3f8dab0b7e38b1823d3c4b..e607898a723b7c01beab29dd17f4780faa255984 100644 (file)
--- a/src/AST/ops.h
+++ b/src/AST/ops.h
@@ -35,7 +35,7 @@ typedef enum FunctionType FunctionType;
 enum PredicateType {TABLEPRED, OPERATORPRED};
 typedef enum PredicateType PredicateType;
 
-enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, ELEMSET, ELEMFUNCRETURN, ELEMCONST};
+enum ASTNodeType {INTERORDERCONST, ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, ELEMSET, ELEMFUNCRETURN, ELEMCONST};
 typedef enum ASTNodeType ASTNodeType;
 
 enum Polarity {P_UNDEFINED, P_TRUE, P_FALSE, P_BOTHTRUEFALSE};

diff --git a/src/classlist.h b/src/classlist.h
index 2079d9b92fed4557146908af1af85b7a087273d0..0e3d28744166fce399a4a661f30879293fe3d573 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -22,6 +22,7 @@ struct SATEncoder;
 typedef struct SATEncoder SATEncoder;
 
 typedef struct BooleanOrder BooleanOrder;
+typedef struct BooleanInterOrder BooleanInterOrder;
 typedef struct BooleanVar BooleanVar;
 typedef struct BooleanLogic BooleanLogic;
 typedef struct BooleanPredicate BooleanPredicate;

diff --git a/src/csolver.c b/src/csolver.c
index d440aadc593c1d8ce9ec0b4e0b846cc6f8d976aa..126caa6f4a8e47937008bdc5c947e770c4395754 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -193,6 +193,12 @@ Boolean * orderConstraint(CSolver *This, Order * order, uint64_t first, uint64_t
        return constraint;
 }
 
+Boolean * interOrderConstraint(CSolver * This, Order * order1, uint64_t first, Order* order2, uint64_t second){
+       Boolean* constraint = allocBooleanInterOrder(order1, first, order2, second);
+       pushVectorBoolean(This->allBooleans, constraint);
+       return constraint;
+}
+
 int startEncoding(CSolver* This){
        naiveEncodingDecision(This);
        SATEncoder* satEncoder = This->satEncoder;

diff --git a/src/csolver.h b/src/csolver.h
index b35f80100b278d6846b77eaefaa3e3aded85e134..1c76ac8eee69a6fb55518a7caccbb2b597d8f8e3 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -121,6 +121,8 @@ Order * createOrder(CSolver *, OrderType type, Set * set);
 /** This function instantiates a boolean on two items in an order. */
 Boolean * orderConstraint(CSolver *, Order * order, uint64_t first, uint64_t second);
 
+Boolean * interOrderConstraint(CSolver *, Order * order1, uint64_t first, Order* order2, uint64_t second);
+
 /** When everything is done, the client calls this function and then csolver starts to encode*/
 int startEncoding(CSolver*);