From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 18 Jul 2017 00:05:22 +0000 (-0700)
Subject: Adding an API for translating the value of an BooleanOrder
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=25cb868e9c7e6327c211f06fea04df896816124c;p=satune.git

Adding an API for translating the value of an BooleanOrder
---

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 39fc024..5a7f092 100644
--- a/src/AST/ops.h
+++ b/src/AST/ops.h
@@ -12,6 +12,9 @@ typedef enum CompOp CompOp;
 enum OrderType {PARTIAL, TOTAL};
 typedef enum OrderType OrderType;
 
+enum HappenedBefore {UNORDERED, FIRST, SECOND};
+typedef enum HappenedBefore HappenedBefore;
+
 /**
  *    FLAGFORCESOVERFLOW forces the operation to overflow if the boolean flag is true
  *  OVERFLOWSETSFLAG -- sets the flag if the operation overflows
diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 2693455..8d3d675 100644
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -79,6 +79,8 @@ static inline void setExpanded(Node *n, int isNegated) {
 }
 
 static inline Edge constraintNegate(Edge e) {
+	if(edgeIsNull(e))
+		return e;
 	Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
 	return enew;
 }
diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index 01cb65a..c16ba49 100644
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -78,3 +78,14 @@ bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
 	int index = getEdgeVar( ((BooleanVar*) boolean)->var );
 	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);
+	if(edgeIsNull(var))
+		return UNORDERED;
+	int index = getEdgeVar( var );
+	return This->satEncoder->cnf->solver->solution[index] ? FIRST: SECOND;
+}
+
diff --git a/src/Backend/sattranslator.h b/src/Backend/sattranslator.h
index 52e40a7..aad1c29 100644
--- a/src/Backend/sattranslator.h
+++ b/src/Backend/sattranslator.h
@@ -9,8 +9,11 @@
 #define SATTRANSLATOR_H
 
 #include "classlist.h"
+#include "ops.h"
+
 
 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean);
+HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, BooleanOrder* boolOrder);
 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/csolver.c b/src/csolver.c
index 36e1d91..67e2589 100644
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -212,3 +212,14 @@ 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);
+}
+
diff --git a/src/csolver.h b/src/csolver.h
index c45d7ee..1e69794 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -125,4 +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);
+
 #endif