Merge with branch master ...

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index a3262330f238519514fefbdc8a86b3c045e16e9d..ff384cbb67bb451d8023c051befaa0560a88bf72 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -5,6 +5,8 @@
 #include "csolver.h"
 #include "predicate.h"
 #include "element.h"
+#include "rewriter.h"
+
 /*
 void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
        Order* order = boolOrder->order;
@@ -25,6 +27,7 @@ void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
                This->solver->allElements.push(elem2);
                This->solver->constraints.add(boolean);
        }
+       replaceBooleanWithBoolean(This->solver, boolOrder, boolean);
 }
 
 

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 2e24629b62e8db7d6679c81e7da8af065ae7fae5..9061f76f432aa1ff3af7c3df490aaa65f9779824 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -14,29 +14,16 @@
 #include "orderelement.h"
 
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
-       switch (constraint->order->order.type){
-               case PAIRWISE:
-                       switch ( constraint->order->type) {
-                               case PARTIAL:
-                                       return encodePartialOrderSATEncoder(This, constraint);
-                               case TOTAL:
-                                       return encodeTotalOrderSATEncoder(This, constraint);
-                               default:
-                                       ASSERT(0);
-                       }
-               case INTEGERENCODING:{
-                       //Infer the value from graph ...
-                       Order* order = constraint->order;
-                       Edge gvalue = inferOrderConstraintFromGraph(order, constraint->first, constraint->second);
-                       if(!edgeIsNull(gvalue))
-                               return gvalue;
-                       //If we couldn't infer the value from graph, we have already generated a predicate for that ...
-                       // So, we should do nothing
-                       return E_BOGUS;
-               }
+       switch ( constraint->order->type) {
+               case PARTIAL:
+                       return encodePartialOrderSATEncoder(This, constraint);
+               case TOTAL:
+                       return encodeTotalOrderSATEncoder(This, constraint);
                default:
                        ASSERT(0);
        }
+       default:
+               ASSERT(0);
        return E_BOGUS;
 }