Modify API to work for partial order as well + adding order test case

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 5a7f092271868fbc13c82a166a1639fee8ad12e5..32febff340161729dd67fb0e69312038d02923ab 100644 (file)
--- a/src/AST/ops.h
+++ b/src/AST/ops.h
@@ -12,7 +12,7 @@ typedef enum CompOp CompOp;
 enum OrderType {PARTIAL, TOTAL};
 typedef enum OrderType OrderType;
 
-enum HappenedBefore {UNORDERED, FIRST, SECOND};
+enum HappenedBefore {FIRST, SECOND, UNORDERED};
 typedef enum HappenedBefore HappenedBefore;
 
 /**

diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c
index 5ab535568cb772c0d4f132477545140cde55d381..4d6f639b51750f02c5e7cfc41958e8f22ea4ce7c 100644 (file)
--- a/src/Backend/satorderencoder.c
+++ b/src/Backend/satorderencoder.c
@@ -79,7 +79,10 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
 
 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){
        ASSERT(pair->first!= pair->second);
-       Edge constraint = getOrderPair(table, pair)->constraint;
+       OrderPair* value = getOrderPair(table, pair);
+       if(value == NULL)
+               return E_NULL;
+       Edge constraint = value->constraint;
        if(pair->first > pair->second || edgeIsNull(constraint))
                return constraint;
        else

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index a72617fda658f8682c1f359c730a06db438f0831..3bfc06b75c34d47108c96ce550178ac3df1b417d 100644 (file)
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -80,10 +80,10 @@ bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
        return This->satEncoder->cnf->solver->solution[index] == true;
 }
 
-HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, BooleanOrder* boolOrder){
-       ASSERT(boolOrder->order->orderPairTable!= NULL);
-       OrderPair pair={boolOrder->first, boolOrder->second, E_NULL};
-       Edge var = getOrderConstraint(boolOrder->order->orderPairTable, & pair);
+HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, Order * order, uint64_t first, uint64_t second){
+       ASSERT(order->orderPairTable!= NULL);
+       OrderPair pair={first, second, E_NULL};
+       Edge var = getOrderConstraint(order->orderPairTable, & pair);
        if(edgeIsNull(var))
                return UNORDERED;
        int index = getEdgeVar( var );

diff --git a/src/Backend/sattranslator.h b/src/Backend/sattranslator.h
index aad1c29d6a3ef52751c6d4157fc9677553ac15e0..0b1a996346654721664101bb53942281aaa783d1 100644 (file)
--- a/src/Backend/sattranslator.h
+++ b/src/Backend/sattranslator.h
@@ -13,7 +13,7 @@
 
 
 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean);
-HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, BooleanOrder* boolOrder);
+HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, Order * order, uint64_t first, uint64_t second);
 uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc);
 uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc);
 uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc);

diff --git a/src/Test/testorder.c b/src/Test/testorder.c
new file mode 100644 (file)
index 0000000..37217f0
--- /dev/null
+++ b/src/Test/testorder.c
@@ -0,0 +1,22 @@
+
+#include "csolver.h"
+
+int main(int numargs, char ** argv) {
+       CSolver * solver=allocCSolver();
+       uint64_t set1[]={5, 1, 4};
+       Set * s=createSet(solver, 0, set1, 3);
+       Order* order = createOrder(solver, TOTAL, s);
+       Boolean* b1=  orderConstraint(solver, order, 1, 4);
+       Boolean* b2=  orderConstraint(solver, order, 5, 4);
+       addConstraint(solver, b1);
+       addConstraint(solver, b2);
+       if (startEncoding(solver)==1)
+               printf("O(1,4)=%d O(5,4)=%d O(4,5)=%d O(1,5)=%d\n", 
+                       getOrderConstraintValue(solver, order, 1, 4), 
+                       getOrderConstraintValue(solver, order, 5, 4),
+                       getOrderConstraintValue(solver, order, 4, 5),
+                       getOrderConstraintValue(solver, order, 1, 5));
+       else
+               printf("UNSAT\n");
+       deleteSolver(solver);
+}
\ No newline at end of file

diff --git a/src/csolver.c b/src/csolver.c
index 67e25899bd6b8b059c3e7d3b69897e060baff6c9..c92aee6b6b6b94cdaa47d546d24ca5ee102d099a 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -213,13 +213,7 @@ bool getBooleanValue( CSolver* This , Boolean* boolean){
        exit(-1);
 }
 
-HappenedBefore getOrderConstraintValue(CSolver* This, Boolean* orderConstr){
-       switch(GETBOOLEANTYPE(orderConstr)){
-               case ORDERCONST:
-                       return getOrderConstraintValueSATTranslator(This, (BooleanOrder*)orderConstr);
-               default:
-                       ASSERT(0);
-       }
-       exit(-1);
+HappenedBefore getOrderConstraintValue(CSolver* This, Order * order, uint64_t first, uint64_t second){
+       return getOrderConstraintValueSATTranslator(This, order, first, second);
 }
 

diff --git a/src/csolver.h b/src/csolver.h
index 1e697948e83518465a9c7412c8cdace3c9b24d99..23c35e059811ba3dee0aaabe6907def5478f7107 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -125,6 +125,6 @@ uint64_t getElementValue(CSolver*, Element* element);
 /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
 bool getBooleanValue( CSolver* , Boolean* boolean);
 
-HappenedBefore getOrderConstraintValue(CSolver*, Boolean* orderConstr);
+HappenedBefore getOrderConstraintValue(CSolver*, Order * order, uint64_t first, uint64_t second);
 
 #endif