Bug Fixes + add more tracing prints + turning off some optimizations
authorHamed Gorjiara <hgorjiar@uci.edu>
Tue, 17 Oct 2017 18:56:36 +0000 (11:56 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Tue, 17 Oct 2017 18:56:36 +0000 (11:56 -0700)
src/AST/boolean.cc
src/AST/boolean.h
src/AST/rewriter.cc
src/ASTAnalyses/Order/orderanalysis.cc
src/ASTAnalyses/Order/ordergraph.cc
src/Backend/constraint.cc
src/Backend/satencoder.cc
src/Backend/satorderencoder.cc
src/common.h
src/csolver.cc
src/csolver.h

index 0f699f7..9196d07 100644 (file)
@@ -110,7 +110,11 @@ void BooleanVar::serialize(Serializer* serializer){
 }
 
 void BooleanVar::print(){
-        model_println("BooleanVar");
+        model_println("BooleanVar:%lu", (uintptr_t)this);
+}
+
+void BooleanConst::print(){
+        model_println("BooleanConst:%s", istrue?"TRUE" :"FALSE");
 }
 
 void BooleanOrder::serialize(Serializer* serializer){
@@ -198,6 +202,8 @@ void BooleanLogic::print(){
         uint size = inputs.getSize();
        for(uint i=0; i<size; i++){
                BooleanEdge input = inputs.get(i);
+                if(input.isNegated())
+                        model_print("!");
                 input.getBoolean()->print();
        }
         model_println("}\n");
index 6a81429..3674d9f 100644 (file)
@@ -34,7 +34,7 @@ public:
        bool isTrue() {return istrue;}
        bool isFalse() {return !istrue;}
        void serialize(Serializer *serializer ){};
-        virtual void print(){};
+        virtual void print();
        bool istrue;
        CMEMALLOC;
 };
index b6908e1..c508185 100644 (file)
@@ -6,6 +6,9 @@
 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
        if (constraints.contains(bexpr.negate())) {
                constraints.remove(bexpr.negate());
+#ifdef TRACE_DEBUG
+                model_println("replaceBooleanWithTrue");
+#endif
                setUnSAT();
        }       
        if (constraints.contains(bexpr)) {
index a77a1a8..8bffb4e 100644 (file)
@@ -1,3 +1,5 @@
+#include <stdint.h>
+
 #include "orderanalysis.h"
 #include "structs.h"
 #include "csolver.h"
@@ -40,9 +42,15 @@ void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
 
 void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
        SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
+#ifdef TRACE_DEBUG
+        model_print("Node:%lu=>", node->id);
+#endif
        while (iterator->hasNext()) {
                OrderEdge *edge = iterator->next();
-               if (mustvisit) {
+#ifdef TRACE_DEBUG
+                model_print("Edge:%lu=>",(uintptr_t) edge);
+#endif
+                if (mustvisit) {
                        if (!edge->mustPos)
                                continue;
                } else
@@ -50,8 +58,10 @@ void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReve
                        continue;
 
                OrderNode *child = isReverse ? edge->source : edge->sink;
-
-               if (child->status == NOTVISITED) {
+#ifdef TRACE_DEBUG
+                model_println("NodeChild:%lu", child->id);
+#endif
+                if (child->status == NOTVISITED) {
                        child->status = VISITED;
                        DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
                        child->status = FINISHED;
@@ -115,6 +125,9 @@ void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
                        sinkNode->inEdges.remove(outEdge);
                        //Adding new edge to new sink and src nodes ...
                        if(srcNode == sinkNode){
+#ifdef TRACE_DEBUG
+                                model_println("bypassMustBe 1");
+#endif
                                This->setUnSAT();
                                delete iterout;
                                delete iterin;
@@ -124,6 +137,9 @@ void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
                        newEdge->mustPos = true;
                        newEdge->polPos = true;
                        if (newEdge->mustNeg){
+#ifdef TRACE_DEBUG
+                                model_println("BypassMustBe 2");
+#endif
                                This->setUnSAT();
                        }
                        srcNode->outEdges.add(newEdge);
@@ -266,8 +282,12 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                                OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
                                newedge->mustPos = true;
                                newedge->polPos = true;
-                               if (newedge->mustNeg)
+                               if (newedge->mustNeg){
+#ifdef TRACE_DEBUG
+                                        model_println("DFS clear 1");
+#endif
                                        solver->setUnSAT();
+                                }
                                srcnode->outEdges.add(newedge);
                                node->inEdges.add(newedge);
                        }
@@ -282,8 +302,12 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                                if (!edge->mustPos && sources->contains(parent)) {
                                        edge->mustPos = true;
                                        edge->polPos = true;
-                                       if (edge->mustNeg)
-                                               solver->setUnSAT();
+                                       if (edge->mustNeg){
+#ifdef TRACE_DEBUG
+                                                model_println("DFS clear 2");
+#endif
+                                                solver->setUnSAT();
+                                        }
                                }
                        }
                        delete iterator;
@@ -297,8 +321,12 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                                if (!edge->mustNeg && sources->contains(child)) {
                                        edge->mustNeg = true;
                                        edge->polNeg = true;
-                                       if (edge->mustPos)
-                                               solver->setUnSAT();
+                                       if (edge->mustPos){
+#ifdef TRACE_DEBUG
+                                                model_println("DFS clear 3: NodeFrom:%lu=>edge%lu=>NodeTo:%lu", node->id, (uintptr_t) edge, child->id);
+#endif
+                                                solver->setUnSAT();
+                                        }
                                }
                        }
                        delete iterator;
@@ -338,6 +366,9 @@ void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
                                if (!invEdge->mustPos) {
                                        invEdge->polPos = false;
                                } else {
+#ifdef TRACE_DEBUG
+                                        model_println("localMustAnalysis Total");
+#endif
                                        solver->setUnSAT();
                                }
                                invEdge->mustNeg = true;
@@ -360,16 +391,22 @@ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
                if (edge->mustPos) {
                        if (!edge->mustNeg) {
                                edge->polNeg = false;
-                       } else
+                       } else{
+#ifdef TRACE_DEBUG
+                                model_println("Local must analysis partial");
+#endif
                                solver->setUnSAT();
-
+                        }
                        OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
                        if (invEdge != NULL) {
                                if (!invEdge->mustPos)
                                        invEdge->polPos = false;
-                               else
+                               else{
+#ifdef TRACE_DEBUG
+                                        model_println("Local must analysis partial 2");
+#endif
                                        solver->setUnSAT();
-
+                                }
                                invEdge->mustNeg = true;
                                invEdge->polNeg = true;
                        }
index ce9a071..822af1f 100644 (file)
@@ -12,6 +12,7 @@ OrderGraph::OrderGraph(Order *_order) :
 }
 
 OrderGraph *buildOrderGraph(Order *order) {
+        ASSERT(order->graph == NULL);
        OrderGraph *orderGraph = new OrderGraph(order);
        order->graph = orderGraph;
        uint constrSize = order->constraints.getSize();
@@ -23,6 +24,7 @@ OrderGraph *buildOrderGraph(Order *order) {
 
 //Builds only the subgraph for the must order graph.
 OrderGraph *buildMustOrderGraph(Order *order) {
+        ASSERT(order->graph == NULL);
        OrderGraph *orderGraph = new OrderGraph(order);
        uint constrSize = order->constraints.getSize();
        for (uint j = 0; j < constrSize; j++) {
index 7c3a094..f018c6c 100644 (file)
@@ -341,7 +341,11 @@ int solveCNF(CNF *cnf) {
        convertPass(cnf, false);
        finishedClauses(cnf->solver);
        long long startSolve = getTimeNano();
-       int result = solve(cnf->solver);
+#ifdef TRACE_DEBUG
+        model_println("Backend: Calling the SAT Solver from CSolver ...");
+#endif
+        int result = solve(cnf->solver);
+        model_print("Backend: Result got from SATSolver: %d", result);
        long long finishTime = getTimeNano();
        cnf->encodeTime = startSolve - startTime;
        cnf->solveTime = finishTime - startSolve;
index 3a30362..720375d 100644 (file)
@@ -29,7 +29,7 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
        SetIteratorBooleanEdge *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();
-                constraint.getBoolean()->print();
+//                constraint.getBoolean()->print();
                Edge c = encodeConstraintSATEncoder(constraint);
                addConstraintCNF(cnf, c);
        }
index c90dcf1..d525bda 100644 (file)
@@ -104,6 +104,7 @@ Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
                boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
                bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
                if (doOptOrderStructure) {
+                        ASSERT(boolOrder->order->graph == NULL);
                        boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
                        reachMustAnalysis(solver, boolOrder->order->graph, true);
                }
index d52924c..58ad1f1 100644 (file)
 #include "time.h"
 
 
-   extern int model_out;
-   extern int model_err;
-   extern int switch_alloc;
+extern int model_out;
+extern int model_err;
+extern int switch_alloc;
 
- #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
+#define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
 
- #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
+#define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
 #define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
- #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
+#define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
 
 
 
index fe21110..f1c39e0 100644 (file)
@@ -260,11 +260,11 @@ BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs,
 }
 
 bool CSolver::isTrue(BooleanEdge b) {
-       return b.isNegated()?b->isFalse():b->isTrue();
+        return b.isNegated()?b->isFalse():b->isTrue();
 }
 
 bool CSolver::isFalse(BooleanEdge b) {
-       return b.isNegated()?b->isTrue():b->isFalse();
+        return b.isNegated()?b->isTrue():b->isFalse();
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
@@ -289,7 +289,8 @@ static int ptrcompares(const void *p1, const void *p2) {
 }
 
 BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge * array, uint asize) {
-       BooleanEdge newarray[asize];
+  return applyLogicalOperation(op, array, asize);
+  /*  BooleanEdge newarray[asize];
        memcpy(newarray, array, asize * sizeof(BooleanEdge));
        for(uint i=0; i < asize; i++) {
                BooleanEdge b=newarray[i];
@@ -300,7 +301,7 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge * array, ui
                        }
                }
        }
-       return applyLogicalOperation(op, newarray, asize);
+       return applyLogicalOperation(op, newarray, asize);*/
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
@@ -312,9 +313,9 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
        case SATC_IFF: {
                for (uint i = 0; i < 2; i++) {
                        if (array[i]->type == BOOLCONST) {
-                               if (array[i]->isTrue()) {
+                               if (isTrue(array[i])) { // It can be undefined
                                        return array[1 - i];
-                               } else {
+                               } else if(isFalse(array[i])) {
                                        newarray[0] = array[1 - i];
                                        return applyLogicalOperation(SATC_NOT, newarray, 1);
                                }
@@ -337,15 +338,20 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
                uint newindex = 0;
                for (uint i = 0; i < asize; i++) {
                        BooleanEdge b = array[i];
+//                        model_print("And: Argument %u:", i);
+//                        if(b.isNegated())
+//                                model_print("!");
+//                        b->print();
                        if (b->type == LOGICOP) {
                                if (((BooleanLogic *)b.getBoolean())->replaced)
                                        return rewriteLogicalOperation(op, array, asize);
                        }
                        if (b->type == BOOLCONST) {
-                               if (b->isTrue())
+                               if (isTrue(b))
                                        continue;
-                               else
+                               else{
                                        return boolFalse;
+                                }
                        } else
                                newarray[newindex++] = b;
                }
@@ -366,47 +372,78 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
        }
        case SATC_IMPLIES: {
                //handle by translation
+//                model_print("Implies: first:");
+//                if(array[0].isNegated())
+//                        model_print("!");
+//                array[0]->print();
+//                model_print("Implies: second:");
+//                if(array[1].isNegated())
+//                        model_print("!");
+//                array[1]->print();
+//                model_println("##### OK let's get the operation done");
                return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
        }
        }
 
        ASSERT(asize != 0);
        Boolean *boolean = new BooleanLogic(this, op, array, asize);
-       Boolean *b = boolMap.get(boolean);
+       /*      Boolean *b = boolMap.get(boolean);
        if (b == NULL) {
                boolean->updateParents();
                boolMap.put(boolean, boolean);
                allBooleans.push(boolean);
                return BooleanEdge(boolean);
        } else {
-               delete boolean;
-               return BooleanEdge(b);
-       }
+       delete boolean;*/
+               return BooleanEdge(boolean);
+               /*      }*/
 }
 
 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
+#ifdef TRACE_DEBUG
+        model_println("Creating order: From:%lu => To:%lu", first, second);
+#endif
+        if(first == second)
+                return boolFalse;
        Boolean *constraint = new BooleanOrder(order, first, second);
        allBooleans.push(constraint);
        return BooleanEdge(constraint);
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
+#ifdef TRACE_DEBUG
+        model_println("****New Constraint******");
+#endif
+        if(constraint.isNegated())
+                model_print("!");
+        constraint.getBoolean()->print();
        if (isTrue(constraint))
                return;
-       else if (isFalse(constraint))
-               setUnSAT();
+       else if (isFalse(constraint)){
+                int t=0;
+#ifdef TRACE_DEBUG
+               model_println("Adding constraint which is false :|");
+#endif
+                setUnSAT();
+        }
        else {
                if (constraint->type == LOGICOP) {
                        BooleanLogic *b=(BooleanLogic *) constraint.getBoolean();
                        if (!constraint.isNegated()) {
                                if (b->op==SATC_AND) {
                                        for(uint i=0;i<b->inputs.getSize();i++) {
+#ifdef TRACE_DEBUG
+                                                model_println("In loop");
+#endif
                                                addConstraint(b->inputs.get(i));
                                        }
                                        return;
                                }
                        }
                        if (b->replaced) {
+#ifdef TRACE_DEBUG
+                                model_println("While rewriting");
+#endif
                                addConstraint(doRewrite(constraint));
                                return;
                        }
@@ -414,8 +451,12 @@ void CSolver::addConstraint(BooleanEdge constraint) {
                constraints.add(constraint);
                Boolean *ptr=constraint.getBoolean();
                
-               if (ptr->boolVal == BV_UNSAT)
-                       setUnSAT();
+               if (ptr->boolVal == BV_UNSAT){
+#ifdef TRACE_DEBUG
+                       model_println("BooleanValue is Set to UnSAT");
+#endif
+                        setUnSAT();
+                }
                
                replaceBooleanWithTrueNoRemove(constraint);
                constraint->parents.clear();
@@ -442,11 +483,11 @@ int CSolver::solve() {
 //     Preprocess pp(this);
 //     pp.doTransform();
        
-       DecomposeOrderTransform dot(this);
-       dot.doTransform();
+//     DecomposeOrderTransform dot(this);
+//     dot.doTransform();
 
-       IntegerEncodingTransform iet(this);
-       iet.doTransform();
+//     IntegerEncodingTransform iet(this);
+//     iet.doTransform();
 
 //     EncodingGraph eg(this);
 //     eg.buildGraph();
@@ -454,7 +495,9 @@ int CSolver::solve() {
        
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
+        model_println("Is problem UNSAT after encoding: %d", unsat);
        int result = unsat ? IS_UNSAT : satEncoder->solve();
+        model_println("Result Computed in CSolver: %d", result);
        long long finishTime = getTimeNano();
        elapsedTime = finishTime - startTime;
        if (deleteTuner) {
index 15da42e..b826258 100644 (file)
@@ -5,6 +5,7 @@
 #include "corestructs.h"
 #include "asthash.h"
 #include "solver_interface.h"
+#include "common.h"
 
 class CSolver {
 public:
@@ -130,7 +131,7 @@ public:
        bool isTrue(BooleanEdge b);
        bool isFalse(BooleanEdge b);
 
-       void setUnSAT() { unsat = true; }
+       void setUnSAT() { model_println("Setting UNSAT %%%%%%"); unsat = true; }
 
        bool isUnSAT() { return unsat; }