replacing booleanOrder with booleanPredicate in IntegerEncoding ...
authorHamed <hamed.gorjiara@gmail.com>
Fri, 25 Aug 2017 05:09:26 +0000 (22:09 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Fri, 25 Aug 2017 05:09:26 +0000 (22:09 -0700)
src/ASTTransform/integerencoding.cc
src/Backend/satorderencoder.cc

index f4b17b4..a992f8f 100644 (file)
@@ -5,6 +5,7 @@
 #include "csolver.h"
 #include "predicate.h"
 #include "element.h"
+#include "rewriter.h"
 
 void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
        Order* order = boolOrder->order;
@@ -25,6 +26,7 @@ void orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
                This->solver->allElements.push(elem2);
                This->solver->constraints.add(boolean);
        }
+       replaceBooleanWithBoolean(This->solver, boolOrder, boolean);
 }
 
 
index 2e24629..9061f76 100644 (file)
 #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;
 }