Fixing more bugs
authorHamed <hamed.gorjiara@gmail.com>
Mon, 4 Sep 2017 10:06:13 +0000 (03:06 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Mon, 4 Sep 2017 10:06:13 +0000 (03:06 -0700)
src/AST/order.h
src/ASTAnalyses/ordergraph.cc
src/ASTTransform/decomposeordertransform.cc
src/ASTTransform/integerencoding.cc
src/Encoders/naiveencoder.cc
src/Test/ordertest.cc
src/csolver.cc

index d922235..cc8b45e 100644 (file)
@@ -19,7 +19,7 @@ public:
        Order *clone(CSolver *solver, CloneMap *map);
        Vector<BooleanOrder *> constraints;
        OrderEncoding encoding;
-       void setOrderResolver(OrderResolver *_resolver) { encoding.resolver = _resolver;};
+       void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};
        void initializeOrderHashtable();
        void initializeOrderElementsHashtable();
        void addOrderConstraint(BooleanOrder *constraint);
index fcc9eda..bb241de 100644 (file)
@@ -13,6 +13,7 @@ OrderGraph::OrderGraph(Order *_order) :
 
 OrderGraph *buildOrderGraph(Order *order) {
        OrderGraph *orderGraph = new OrderGraph(order);
+       order->graph = orderGraph;
        uint constrSize = order->constraints.getSize();
        for (uint j = 0; j < constrSize; j++) {
                orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
index 7d276e2..359a3a3 100644 (file)
@@ -60,17 +60,15 @@ void DecomposeOrderTransform::doTransform() {
                        }
                }
 
-               /*
+               
                bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
 
                if (mustReachPrune)
                        removeMustBeTrueNodes(solver, graph);
-               */
                
                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);
                decomposeOrder(order, graph);
-               delete graph;
        }
        delete orderit;
        delete orders;
index a4aacdf..ab88f20 100644 (file)
@@ -35,6 +35,7 @@ void IntegerEncodingTransform::integerEncode(Order *currOrder) {
                encodingRecord = new IntegerEncodingRecord(
                        solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
                orderIntEncoding->put(currOrder, encodingRecord);
+               currOrder->setOrderEncodingType( INTEGERENCODING );
        } else {
                encodingRecord = orderIntEncoding->get(currOrder);
        }
index 466d839..2d77608 100644 (file)
@@ -28,7 +28,8 @@ void naiveEncodingConstraint(Boolean *This) {
                return;
        }
        case ORDERCONST: {
-               ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
+               if(((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
+                       ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
                return;
        }
        case LOGICOP: {
index 8633415..d9ad852 100755 (executable)
@@ -15,9 +15,15 @@ int main(int numargs, char **argv) {
        BooleanEdge b2 =  solver->orderConstraint(order, 1, 4);
        solver->addConstraint(b1);
        solver->addConstraint(b2);
-       if (solver->solve() == 1)
+       if (solver->solve() == 1){
                printf("SAT\n");
-       else
+               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
+                       solver->getOrderConstraintValue(order, 5, 1), 
+                       solver->getOrderConstraintValue(order, 1, 4),
+                       solver->getOrderConstraintValue(order, 5, 4),
+                       solver->getOrderConstraintValue(order, 1, 5));
+       } else {
                printf("UNSAT\n");
+       }
        delete solver;
 }
index b353791..f52c4eb 100644 (file)
@@ -400,12 +400,11 @@ int CSolver::solve() {
        long long startTime = getTimeNano();
        computePolarities(this);
 
-       DecomposeOrderTransform dot(this);
-       dot.doTransform();
+//     DecomposeOrderTransform dot(this);
+//     dot.doTransform();
 
-       //This leaks like crazy
-       //      IntegerEncodingTransform iet(this);
-       //iet.doTransform();
+       IntegerEncodingTransform iet(this);
+       iet.doTransform();
 
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);