bug fix for the order test case ...

diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c
index dee9b26f94959541ee7b9b9910f4e4d5317c7654..36c16f2729a7a43bca7e76ad942d3645c07634b1 100644 (file)
--- a/src/Backend/satorderencoder.c
+++ b/src/Backend/satorderencoder.c
@@ -20,7 +20,7 @@ Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
 Edge getPairConstraint(SATEncoder *This, HashTableOrderPair * table, OrderPair * pair) {
        bool negate = false;
        OrderPair flipped;
-       if (pair->first > pair->second) {
+       if (pair->first < pair->second) {
                negate=true;
                flipped.first=pair->second;
                flipped.second=pair->first;
@@ -79,17 +79,20 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
 
 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){
        ASSERT(pair->first!= pair->second);
-       OrderPair* value = getOrderPair(table, pair);
-       if(value == NULL)
+       bool negate = false;
+       OrderPair flipped;
+       if (pair->first < pair->second) {
+               negate=true;
+               flipped.first=pair->second;
+               flipped.second=pair->first;
+               pair = &flipped;
+       }
+       if (!containsOrderPair(table, pair)) {
                return E_NULL;
-       Edge constraint = value->constraint;
-       model_print("Constraint:\n");
-       printCNF(constraint);
-       model_print("\n***********\n");
-       if(pair->first > pair->second || edgeIsNull(constraint))
-               return constraint;
-       else
-               return constraintNegate(constraint);
+       }
+       Edge constraint= getOrderPair(table, pair)->constraint;
+       ASSERT(!edgeIsNull(constraint));
+       return negate ? constraintNegate(constraint) : constraint;
 }
 
 Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK){

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index ee228798023666ed3f3f5f48a2ea0f9efc0d1069..a3245d85b10a92da0421d49836e0e81133f573a8 100644 (file)
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -82,9 +82,8 @@ bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
 
 HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, Order * order, uint64_t first, uint64_t second){
        ASSERT(order->orderPairTable!= NULL);
-       model_print("Frist:%llu\tSecond:%llu\n", first, second);
        OrderPair pair={first, second, E_NULL};
-       Edge var = getOrderConstraint(order->orderPairTable, & pair);
+       Edge var = getOrderConstraint(order->orderPairTable, &pair); 
        if(edgeIsNull(var))
                return UNORDERED;
        return getValueCNF(This->satEncoder->cnf, var)? FIRST: SECOND;

diff --git a/src/Test/testorder.c b/src/Test/testorder.c
index 0ebd5e22d9a4226705b7710da1db5e222b85f56e..4970cac92891f178268d8cdee6f02576aa98df89 100644 (file)
--- a/src/Test/testorder.c
+++ b/src/Test/testorder.c
@@ -11,11 +11,12 @@ int main(int numargs, char ** argv) {
        addConstraint(solver, b1);
        addConstraint(solver, b2);
        if (startEncoding(solver)==1)
-               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
+               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d O(1111,5)=%d\n", 
                        getOrderConstraintValue(solver, order, 5, 1), 
                        getOrderConstraintValue(solver, order, 1, 4),
                        getOrderConstraintValue(solver, order, 5, 4),
-                       getOrderConstraintValue(solver, order, 1, 5));
+                       getOrderConstraintValue(solver, order, 1, 5),
+                       getOrderConstraintValue(solver, order, 1111, 5));
        else
                printf("UNSAT\n");
        deleteSolver(solver);