From b37b46536ba2d34a104147f7a627acc83184cca8 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Tue, 17 Oct 2017 11:56:36 -0700 Subject: [PATCH] Bug Fixes + add more tracing prints + turning off some optimizations --- src/AST/boolean.cc | 8 ++- src/AST/boolean.h | 2 +- src/AST/rewriter.cc | 3 + src/ASTAnalyses/Order/orderanalysis.cc | 61 +++++++++++++++---- src/ASTAnalyses/Order/ordergraph.cc | 2 + src/Backend/constraint.cc | 6 +- src/Backend/satencoder.cc | 2 +- src/Backend/satorderencoder.cc | 1 + src/common.h | 12 ++-- src/csolver.cc | 83 +++++++++++++++++++------- src/csolver.h | 3 +- 11 files changed, 140 insertions(+), 43 deletions(-) diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index 0f699f7..9196d07 100644 --- a/src/AST/boolean.cc +++ b/src/AST/boolean.cc @@ -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; iprint(); } model_println("}\n"); diff --git a/src/AST/boolean.h b/src/AST/boolean.h index 6a81429..3674d9f 100644 --- 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 ){}; - virtual void print(){}; + virtual void print(); bool istrue; CMEMALLOC; }; diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index b6908e1..c508185 100644 --- 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()); +#ifdef TRACE_DEBUG + model_println("replaceBooleanWithTrue"); +#endif setUnSAT(); } if (constraints.contains(bexpr)) { diff --git a/src/ASTAnalyses/Order/orderanalysis.cc b/src/ASTAnalyses/Order/orderanalysis.cc index a77a1a8..8bffb4e 100644 --- a/src/ASTAnalyses/Order/orderanalysis.cc +++ b/src/ASTAnalyses/Order/orderanalysis.cc @@ -1,3 +1,5 @@ +#include + #include "orderanalysis.h" #include "structs.h" #include "csolver.h" @@ -40,9 +42,15 @@ void DFSReverse(OrderGraph *graph, Vector *finishNodes) { void DFSNodeVisit(OrderNode *node, Vector *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 *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, VectorgetOrderEdgeFromOrderGraph(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, VectormustPos && 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, VectormustNeg && 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; } diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc index ce9a071..822af1f 100644 --- a/src/ASTAnalyses/Order/ordergraph.cc +++ b/src/ASTAnalyses/Order/ordergraph.cc @@ -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++) { diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index 7c3a094..f018c6c 100644 --- 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(); - 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; diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 3a30362..720375d 100644 --- 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(); - constraint.getBoolean()->print(); +// constraint.getBoolean()->print(); Edge c = encodeConstraintSATEncoder(constraint); addConstraintCNF(cnf, c); } diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index c90dcf1..d525bda 100644 --- 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) { + ASSERT(boolOrder->order->graph == NULL); boolOrder->order->graph = buildMustOrderGraph(boolOrder->order); reachMustAnalysis(solver, boolOrder->order->graph, true); } diff --git a/src/common.h b/src/common.h index d52924c..58ad1f1 100644 --- a/src/common.h +++ b/src/common.h @@ -19,15 +19,15 @@ #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) diff --git a/src/csolver.cc b/src/csolver.cc index fe21110..f1c39e0 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -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;iinputs.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) { diff --git a/src/csolver.h b/src/csolver.h index 15da42e..b826258 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -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; } -- 2.34.1