Bug Fixes + add more tracing prints + turning off some optimizations

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 0f699f7cf5245db063e9140debcb1ba8b37792e1..9196d07765b84e8db76f6b9582867287adf1f03d 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -110,7 +110,11 @@ void BooleanVar::serialize(Serializer* serializer){
 }
 
 void BooleanVar::print(){
 }
 
 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){
 }
 
 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);
         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");
                 input.getBoolean()->print();
        }
         model_println("}\n");

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 6a814294b91c099e3f6776e4119136f7ff60d7be..3674d9f29d5e934bd94e90ecd1dfe93a488b3e9c 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -34,7 +34,7 @@ public:
        bool isTrue() {return istrue;}
        bool isFalse() {return !istrue;}
        void serialize(Serializer *serializer ){};
        bool isTrue() {return istrue;}
        bool isFalse() {return !istrue;}
        void serialize(Serializer *serializer ){};

-        virtual void print(){};
+        virtual void print();

        bool istrue;
        CMEMALLOC;
 };
        bool istrue;
        CMEMALLOC;
 };

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index b6908e1f1dc1b7435b21fa637345492ad4f98971..c508185f99928cd2eff5d6e67c332510080e15b3 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -6,6 +6,9 @@
 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
        if (constraints.contains(bexpr.negate())) {
                constraints.remove(bexpr.negate());
 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)) {
                setUnSAT();
        }       
        if (constraints.contains(bexpr)) {

diff --git a/src/ASTAnalyses/Order/orderanalysis.cc b/src/ASTAnalyses/Order/orderanalysis.cc
index a77a1a8418b086dd143c3e549034dde836d62988..8bffb4e8f0e7818bed8ea73592ba562381fa19f7 100644 (file)
--- a/src/ASTAnalyses/Order/orderanalysis.cc
+++ b/src/ASTAnalyses/Order/orderanalysis.cc
@@ -1,3 +1,5 @@
+#include <stdint.h>
+

 #include "orderanalysis.h"
 #include "structs.h"
 #include "csolver.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();
 
 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();
        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
                        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;
                        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;
                        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){
                        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;
                                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){
                        newEdge->mustPos = true;
                        newEdge->polPos = true;
                        if (newEdge->mustNeg){

+#ifdef TRACE_DEBUG
+                                model_println("BypassMustBe 2");
+#endif

                                This->setUnSAT();
                        }
                        srcNode->outEdges.add(newEdge);
                                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;
                                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();
                                        solver->setUnSAT();

+                                }

                                srcnode->outEdges.add(newedge);
                                node->inEdges.add(newedge);
                        }
                                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->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;
                                }
                        }
                        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->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;
                                }
                        }
                        delete iterator;


@@ -338,6 +366,9 @@ void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
                                if (!invEdge->mustPos) {
                                        invEdge->polPos = false;
                                } else {
                                if (!invEdge->mustPos) {
                                        invEdge->polPos = false;
                                } else {

+#ifdef TRACE_DEBUG
+                                        model_println("localMustAnalysis Total");
+#endif

                                        solver->setUnSAT();
                                }
                                invEdge->mustNeg = true;
                                        solver->setUnSAT();
                                }
                                invEdge->mustNeg = true;


@@ -360,16 +391,22 @@ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
                if (edge->mustPos) {
                        if (!edge->mustNeg) {
                                edge->polNeg = false;
                if (edge->mustPos) {
                        if (!edge->mustNeg) {
                                edge->polNeg = false;

-                       } else
+                       } else{
+#ifdef TRACE_DEBUG
+                                model_println("Local must analysis partial");
+#endif

                                solver->setUnSAT();
                                solver->setUnSAT();

-
+                        }

                        OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
                        if (invEdge != NULL) {
                                if (!invEdge->mustPos)
                                        invEdge->polPos = false;
                        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();
                                        solver->setUnSAT();

-
+                                }

                                invEdge->mustNeg = true;
                                invEdge->polNeg = true;
                        }
                                invEdge->mustNeg = true;
                                invEdge->polNeg = true;
                        }

diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc
index ce9a0712f0e6f713c8c4bcabedbd59871e7f2306..822af1f517a58ecb9c7d83239f7fa2dd877e4e94 100644 (file)
--- a/src/ASTAnalyses/Order/ordergraph.cc
+++ b/src/ASTAnalyses/Order/ordergraph.cc
@@ -12,6 +12,7 @@ OrderGraph::OrderGraph(Order *_order) :
 }
 
 OrderGraph *buildOrderGraph(Order *order) {
 }
 
 OrderGraph *buildOrderGraph(Order *order) {

+        ASSERT(order->graph == NULL);

        OrderGraph *orderGraph = new OrderGraph(order);
        order->graph = orderGraph;
        uint constrSize = order->constraints.getSize();
        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) {
 
 //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++) {
        OrderGraph *orderGraph = new OrderGraph(order);
        uint constrSize = order->constraints.getSize();
        for (uint j = 0; j < constrSize; j++) {

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 7c3a094701d3c12ffa08d5a3fba5c83dd6b3f4d8..f018c6c433a5baa358e2f8812fbd73b6837a8040 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -341,7 +341,11 @@ int solveCNF(CNF *cnf) {
        convertPass(cnf, false);
        finishedClauses(cnf->solver);
        long long startSolve = getTimeNano();
        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;
        long long finishTime = getTimeNano();
        cnf->encodeTime = startSolve - startTime;
        cnf->solveTime = finishTime - startSolve;

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 3a303628616a4ba4bb0dbba2922e4a536733208c..720375db8b1ab5deedcebdfed70bdc5c90691f74 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -29,7 +29,7 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
        SetIteratorBooleanEdge *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();
        SetIteratorBooleanEdge *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();

-                constraint.getBoolean()->print();
+//                constraint.getBoolean()->print();

                Edge c = encodeConstraintSATEncoder(constraint);
                addConstraintCNF(cnf, c);
        }
                Edge c = encodeConstraintSATEncoder(constraint);
                addConstraintCNF(cnf, c);
        }

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index c90dcf17d44734b5f20948e35c36e22eeeba72d4..d525bdad0ed0b808d192e8a72004282d77b1c549 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -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) {
                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);
                }
                        boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
                        reachMustAnalysis(solver, boolOrder->order->graph, true);
                }

diff --git a/src/common.h b/src/common.h
index d52924c2d91e95904baae0e9fb7bb4d758778b96..58ad1f1acdb2cbacf64c99e7b6576f4d3233134e 100644 (file)
--- a/src/common.h
+++ b/src/common.h
@@ -19,15 +19,15 @@
 #include "time.h"
 
 
 #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_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)

 
 
 
 
 
 

diff --git a/src/csolver.cc b/src/csolver.cc
index fe2111036f1281b8fb366cbf35d3e0f9c7782168..f1c39e0e33229648c39e97bf02460c0e0271c52a 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -260,11 +260,11 @@ BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs,
 }
 
 bool CSolver::isTrue(BooleanEdge b) {
 }
 
 bool CSolver::isTrue(BooleanEdge b) {

-       return b.isNegated()?b->isFalse():b->isTrue();
+        return b.isNegated()?b->isFalse():b->isTrue();

 }
 
 bool CSolver::isFalse(BooleanEdge b) {
 }
 
 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) {
 }
 
 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 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];
        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) {
 }
 
 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) {
        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];
                                        return array[1 - i];

-                               } else {
+                               } else if(isFalse(array[i])) {

                                        newarray[0] = array[1 - i];
                                        return applyLogicalOperation(SATC_NOT, newarray, 1);
                                }
                                        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];
                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->type == LOGICOP) {
                                if (((BooleanLogic *)b.getBoolean())->replaced)
                                        return rewriteLogicalOperation(op, array, asize);
                        }
                        if (b->type == BOOLCONST) {

-                               if (b->isTrue())
+                               if (isTrue(b))

                                        continue;
                                        continue;

-                               else
+                               else{

                                        return boolFalse;
                                        return boolFalse;

+                                }

                        } else
                                newarray[newindex++] = b;
                }
                        } else
                                newarray[newindex++] = b;
                }


@@ -366,47 +372,78 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
        }
        case SATC_IMPLIES: {
                //handle by translation
        }
        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);
                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 {
        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) {
 }
 
 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) {
        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;
        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++) {
        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) {
                                                addConstraint(b->inputs.get(i));
                                        }
                                        return;
                                }
                        }
                        if (b->replaced) {

+#ifdef TRACE_DEBUG
+                                model_println("While rewriting");
+#endif

                                addConstraint(doRewrite(constraint));
                                return;
                        }
                                addConstraint(doRewrite(constraint));
                                return;
                        }


@@ -414,8 +451,12 @@ void CSolver::addConstraint(BooleanEdge constraint) {
                constraints.add(constraint);
                Boolean *ptr=constraint.getBoolean();
                
                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();
                
                replaceBooleanWithTrueNoRemove(constraint);
                constraint->parents.clear();


@@ -442,11 +483,11 @@ int CSolver::solve() {
 //     Preprocess pp(this);
 //     pp.doTransform();
        
 //     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();
 
 //     EncodingGraph eg(this);
 //     eg.buildGraph();


@@ -454,7 +495,9 @@ int CSolver::solve() {
        
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);
        
        naiveEncodingDecision(this);
        satEncoder->encodeAllSATEncoder(this);

+        model_println("Is problem UNSAT after encoding: %d", unsat);

        int result = unsat ? IS_UNSAT : satEncoder->solve();
        int result = unsat ? IS_UNSAT : satEncoder->solve();

+        model_println("Result Computed in CSolver: %d", result);

        long long finishTime = getTimeNano();
        elapsedTime = finishTime - startTime;
        if (deleteTuner) {
        long long finishTime = getTimeNano();
        elapsedTime = finishTime - startTime;
        if (deleteTuner) {

diff --git a/src/csolver.h b/src/csolver.h
index 15da42e58946c1ec8703c6b08300801863144a27..b826258d2aea3b0a7634fb89d2831fed4c4e1b73 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -5,6 +5,7 @@
 #include "corestructs.h"
 #include "asthash.h"
 #include "solver_interface.h"
 #include "corestructs.h"
 #include "asthash.h"
 #include "solver_interface.h"

+#include "common.h"

 
 class CSolver {
 public:
 
 class CSolver {
 public:


@@ -130,7 +131,7 @@ public:
        bool isTrue(BooleanEdge b);
        bool isFalse(BooleanEdge b);
 
        bool isTrue(BooleanEdge b);
        bool isFalse(BooleanEdge b);
 

-       void setUnSAT() { unsat = true; }
+       void setUnSAT() { model_println("Setting UNSAT %%%%%%"); unsat = true; }

 
        bool isUnSAT() { return unsat; }
 
 
        bool isUnSAT() { return unsat; }