Adding an API for translating the value of an BooleanOrder

diff --git a/src/AST/ops.h b/src/AST/ops.h
index 39fc024b2d88c34eaaa5e0c05b003a3282c01883..5a7f092271868fbc13c82a166a1639fee8ad12e5 100644 (file)
--- 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 2693455a0ba0f85da0c731709482c5b2de67d152..8d3d675940d3bca6ebc86653216a5859dd059a72 100644 (file)
--- 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 01cb65a2845a4b29cbf84c015d0923847e08b133..c16ba491ee2d22318a1eea12546b2f802e13b53d 100644 (file)
--- 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 52e40a7bcd2854c7590736789b64c3766485ee7c..aad1c29d6a3ef52751c6d4157fc9677553ac15e0 100644 (file)
--- 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 36e1d91a0cfad786628c4f160b09c6b1a4cfefd1..67e25899bd6b8b059c3e7d3b69897e060baff6c9 100644 (file)
--- 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 c45d7ee38c3ab33c9ead806ff1dffe4e10cbd454..1e697948e83518465a9c7412c8cdace3c9b24d99 100644 (file)
--- 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