From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 18 Jul 2017 01:07:24 +0000 (-0700)
Subject: Modify API to work for partial order as well + adding order test case
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=7013b7621b5e9efc22d99d066d52bd2fb40d688a;p=satune.git

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 5a7f092..32febff 100644
--- 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 5ab5355..4d6f639 100644
--- 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 a72617f..3bfc06b 100644
--- 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 aad1c29..0b1a996 100644
--- 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
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 67e2589..c92aee6 100644
--- 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 1e69794..23c35e0 100644
--- 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