From 0703630a40f4fcfd8c8dcad336472907f125c86c Mon Sep 17 00:00:00 2001 From: bdemsky Date: Wed, 18 Oct 2017 16:54:21 -0700 Subject: [PATCH] Edits to merge --- src/AST/boolean.cc | 34 +++++----- src/AST/element.cc | 12 ++-- src/AST/function.cc | 13 ++-- src/AST/order.cc | 6 +- src/AST/predicate.cc | 8 +-- src/AST/rewriter.cc | 3 - src/AST/set.cc | 22 +++---- src/AST/table.cc | 14 ++--- src/ASTAnalyses/Order/orderanalysis.cc | 64 ++++--------------- src/Backend/constraint.cc | 6 +- src/Backend/satencoder.cc | 1 - src/common.h | 27 ++++---- src/csolver.cc | 87 ++++++++------------------ src/csolver.h | 2 +- src/mymemory.h | 2 +- 15 files changed, 111 insertions(+), 190 deletions(-) diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index 9196d07..fff3658 100644 --- a/src/AST/boolean.cc +++ b/src/AST/boolean.cc @@ -110,11 +110,11 @@ void BooleanVar::serialize(Serializer* serializer){ } void BooleanVar::print(){ - model_println("BooleanVar:%lu", (uintptr_t)this); + model_print("BooleanVar:%lu\n", (uintptr_t)this); } void BooleanConst::print(){ - model_println("BooleanConst:%s", istrue?"TRUE" :"FALSE"); + model_print("BooleanConst:%s\n", istrue?"TRUE" :"FALSE"); } void BooleanOrder::serialize(Serializer* serializer){ @@ -132,9 +132,9 @@ void BooleanOrder::serialize(Serializer* serializer){ } void BooleanOrder::print(){ - model_println("{BooleanOrder: First= %lu, Second = %lu on Order:", first, second); + model_print("{BooleanOrder: First= %lu, Second = %lu on Order:\n", first, second); order->print(); - model_println("}\n"); + model_print("}\n"); } void BooleanPredicate::serialize(Serializer* serializer){ @@ -164,15 +164,15 @@ void BooleanPredicate::serialize(Serializer* serializer){ } void BooleanPredicate::print(){ - model_println("{BooleanPredicate:"); - predicate->print(); - model_println("elements:"); - uint size = inputs.getSize(); + model_print("{BooleanPredicate:\n"); + predicate->print(); + model_print("elements:\n"); + uint size = inputs.getSize(); for(uint i=0; iprint(); } - model_println("}\n"); + model_print("}\n"); } void BooleanLogic::serialize(Serializer* serializer){ @@ -196,16 +196,16 @@ void BooleanLogic::serialize(Serializer* serializer){ } void BooleanLogic::print(){ - model_println("{BooleanLogic: %s", - op ==SATC_AND? "AND": op == SATC_OR? "OR": op==SATC_NOT? "NOT": - op == SATC_XOR? "XOR" : op==SATC_IFF? "IFF" : "IMPLIES"); - uint size = inputs.getSize(); + model_print("{BooleanLogic: %s\n", + op ==SATC_AND? "AND": op == SATC_OR? "OR": op==SATC_NOT? "NOT": + op == SATC_XOR? "XOR" : op==SATC_IFF? "IFF" : "IMPLIES"); + uint size = inputs.getSize(); for(uint i=0; iprint(); + if(input.isNegated()) + model_print("!"); + input.getBoolean()->print(); } - model_println("}\n"); + model_print("}\n"); } diff --git a/src/AST/element.cc b/src/AST/element.cc index fb5b822..205d31f 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -78,9 +78,9 @@ void ElementSet::serialize(Serializer* serializer){ } void ElementSet::print(){ - model_println("{ElementSet:"); + model_print("{ElementSet:\n"); set->print(); - model_println("}\n"); + model_print("}\n"); } void ElementConst::serialize(Serializer* serializer){ @@ -99,7 +99,7 @@ void ElementConst::serialize(Serializer* serializer){ } void ElementConst::print(){ - model_println("{ElementConst: %lu}", value); + model_print("{ElementConst: %lu}\n", value); } void ElementFunction::serialize(Serializer* serializer){ @@ -129,13 +129,13 @@ void ElementFunction::serialize(Serializer* serializer){ } void ElementFunction::print(){ - model_println("{ElementFunction:"); + model_print("{ElementFunction:\n"); function->print(); - model_println("Elements:"); + model_print("Elements:\n"); uint size = inputs.getSize(); for(uint i=0; iprint(); } - model_println("}\n"); + model_print("}\n"); } diff --git a/src/AST/function.cc b/src/AST/function.cc index 26decd0..f17fb62 100644 --- a/src/AST/function.cc +++ b/src/AST/function.cc @@ -83,10 +83,9 @@ void FunctionTable::serialize(Serializer* serializer){ } void FunctionTable::print(){ - model_println("{FunctionTable:"); - table->print(); - model_println("}\n"); - + model_print("{FunctionTable:\n"); + table->print(); + model_print("}\n"); } void FunctionOperator::serialize(Serializer* serializer){ @@ -115,6 +114,6 @@ void FunctionOperator::serialize(Serializer* serializer){ serializer->mywrite(&overflowbehavior, sizeof(OverFlowBehavior)); } -void FunctionOperator::print(){ - model_println("{FunctionOperator: %s}", op == SATC_ADD? "ADD": "SUB" ); -} \ No newline at end of file +void FunctionOperator::print() { + model_print("{FunctionOperator: %s}\n", op == SATC_ADD? "ADD": "SUB" ); +} diff --git a/src/AST/order.cc b/src/AST/order.cc index 96e7be5..a28d6c0 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -60,7 +60,7 @@ void Order::serialize(Serializer* serializer){ } void Order::print(){ - model_println("{Order on Set:"); - set->print(); - model_println("}\n"); + model_print("{Order on Set:\n"); + set->print(); + model_print("}\n"); } diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc index f320a4d..1e0bb21 100644 --- a/src/AST/predicate.cc +++ b/src/AST/predicate.cc @@ -67,9 +67,9 @@ void PredicateTable::serialize(Serializer* serializer){ } void PredicateTable::print(){ - model_println("{PredicateTable:"); - table->print(); - model_println("}\n"); + model_print("{PredicateTable:\n"); + table->print(); + model_print("}\n"); } void PredicateOperator::serialize(Serializer* serializer){ @@ -96,7 +96,7 @@ void PredicateOperator::serialize(Serializer* serializer){ } void PredicateOperator::print(){ - model_println("{PredicateOperator: %s }", op ==SATC_EQUALS? "EQUAL": "NOT-EQUAL"); + model_print("{PredicateOperator: %s }\n", op ==SATC_EQUALS? "EQUAL": "NOT-EQUAL"); } diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index c508185..b6908e1 100644 --- a/src/AST/rewriter.cc +++ b/src/AST/rewriter.cc @@ -6,9 +6,6 @@ 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/AST/set.cc b/src/AST/set.cc index 25ccd05..8fa9eda 100644 --- a/src/AST/set.cc +++ b/src/AST/set.cc @@ -145,15 +145,15 @@ void Set::serialize(Serializer* serializer){ void Set::print(){ model_print("{Set:"); - if(isRange){ - model_print("Range: low=%lu, high=%lu}\n\n", low, high); - } else { - uint size = members->getSize(); - model_print("Members: "); - for(uint i=0; iget(i); - model_print("%lu, ", mem); - } - model_println("}\n"); - } + if(isRange){ + model_print("Range: low=%lu, high=%lu}\n\n", low, high); + } else { + uint size = members->getSize(); + model_print("Members: "); + for(uint i=0; iget(i); + model_print("%lu, ", mem); + } + model_print("}\n"); + } } diff --git a/src/AST/table.cc b/src/AST/table.cc index f6494f4..3778767 100644 --- a/src/AST/table.cc +++ b/src/AST/table.cc @@ -98,16 +98,16 @@ void Table::serialize(Serializer* serializer){ void Table::print(){ - model_println("{Table:"); + model_print("{Table:\n"); SetIteratorTableEntry* iterator = getEntries(); while(iterator->hasNext()){ TableEntry* entry = iterator->next(); - model_print("<"); - for(uint i=0; iinputSize; i++){ - model_print("%lu, ", entry->inputs[i]); - } - model_print(" == %lu>", entry->output); + model_print("<"); + for(uint i=0; iinputSize; i++){ + model_print("%lu, ", entry->inputs[i]); + } + model_print(" == %lu>", entry->output); } - model_println("}\n"); + model_print("}\n"); delete iterator; } diff --git a/src/ASTAnalyses/Order/orderanalysis.cc b/src/ASTAnalyses/Order/orderanalysis.cc index 8bffb4e..ae3c752 100644 --- a/src/ASTAnalyses/Order/orderanalysis.cc +++ b/src/ASTAnalyses/Order/orderanalysis.cc @@ -42,15 +42,9 @@ 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(); -#ifdef TRACE_DEBUG - model_print("Edge:%lu=>",(uintptr_t) edge); -#endif - if (mustvisit) { + if (mustvisit) { if (!edge->mustPos) continue; } else @@ -58,10 +52,7 @@ void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReve continue; OrderNode *child = isReverse ? edge->source : edge->sink; -#ifdef TRACE_DEBUG - model_println("NodeChild:%lu", child->id); -#endif - if (child->status == NOTVISITED) { + if (child->status == NOTVISITED) { child->status = VISITED; DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum); child->status = FINISHED; @@ -124,10 +115,7 @@ void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) { OrderNode *sinkNode = outEdge->sink; sinkNode->inEdges.remove(outEdge); //Adding new edge to new sink and src nodes ... - if(srcNode == sinkNode){ -#ifdef TRACE_DEBUG - model_println("bypassMustBe 1"); -#endif + if(srcNode == sinkNode) { This->setUnSAT(); delete iterout; delete iterin; @@ -136,12 +124,8 @@ void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) { OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode); newEdge->mustPos = true; newEdge->polPos = true; - if (newEdge->mustNeg){ -#ifdef TRACE_DEBUG - model_println("BypassMustBe 2"); -#endif + if (newEdge->mustNeg) This->setUnSAT(); - } srcNode->outEdges.add(newEdge); sinkNode->inEdges.add(newEdge); } @@ -282,12 +266,8 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorgetOrderEdgeFromOrderGraph(srcnode, node); newedge->mustPos = true; newedge->polPos = true; - if (newedge->mustNeg){ -#ifdef TRACE_DEBUG - model_println("DFS clear 1"); -#endif + if (newedge->mustNeg) solver->setUnSAT(); - } srcnode->outEdges.add(newedge); node->inEdges.add(newedge); } @@ -302,12 +282,8 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectormustPos && sources->contains(parent)) { edge->mustPos = true; edge->polPos = true; - if (edge->mustNeg){ -#ifdef TRACE_DEBUG - model_println("DFS clear 2"); -#endif - solver->setUnSAT(); - } + if (edge->mustNeg) + solver->setUnSAT(); } } delete iterator; @@ -322,11 +298,8 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectormustNeg = true; edge->polNeg = true; 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(); - } + solver->setUnSAT(); + } } } delete iterator; @@ -365,12 +338,8 @@ void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) { if (invEdge != NULL) { if (!invEdge->mustPos) { invEdge->polPos = false; - } else { -#ifdef TRACE_DEBUG - model_println("localMustAnalysis Total"); -#endif + } else solver->setUnSAT(); - } invEdge->mustNeg = true; invEdge->polNeg = true; } @@ -391,22 +360,15 @@ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) { if (edge->mustPos) { if (!edge->mustNeg) { edge->polNeg = false; - } else{ -#ifdef TRACE_DEBUG - model_println("Local must analysis partial"); -#endif + } else { solver->setUnSAT(); - } + } OrderEdge *invEdge = graph->getInverseOrderEdge(edge); if (invEdge != NULL) { if (!invEdge->mustPos) invEdge->polPos = false; - else{ -#ifdef TRACE_DEBUG - model_println("Local must analysis partial 2"); -#endif + else solver->setUnSAT(); - } invEdge->mustNeg = true; invEdge->polNeg = true; } diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index f018c6c..7c3a094 100644 --- a/src/Backend/constraint.cc +++ b/src/Backend/constraint.cc @@ -341,11 +341,7 @@ int solveCNF(CNF *cnf) { convertPass(cnf, false); finishedClauses(cnf->solver); long long startSolve = getTimeNano(); -#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); + int result = solve(cnf->solver); 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 720375d..fdeee9e 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -29,7 +29,6 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) { SetIteratorBooleanEdge *iterator = csolver->getConstraints(); while (iterator->hasNext()) { BooleanEdge constraint = iterator->next(); -// constraint.getBoolean()->print(); Edge c = encodeConstraintSATEncoder(constraint); addConstraintCNF(cnf, c); } diff --git a/src/common.h b/src/common.h index 58ad1f1..a15f7df 100644 --- a/src/common.h +++ b/src/common.h @@ -18,20 +18,21 @@ #include "config.h" #include "time.h" +/* + 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_print(fmt, ...) do { printf(fmt, ## __VA_ARGS__); } while (0) + #define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0) + + #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0) + + #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0) + */ -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_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 printf +#define model_print printf #define NEXTPOW2(x) ((x == 1) ? 1 : (1 << (sizeof(uint) * 8 - __builtin_clz(x - 1)))) #define NUMBITS(x) ((x == 0) ? 0 : 8 * sizeof(x) - __builtin_clz(x)) diff --git a/src/csolver.cc b/src/csolver.cc index f1c39e0..592d1d5 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -289,8 +289,7 @@ static int ptrcompares(const void *p1, const void *p2) { } BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge * array, uint asize) { - return applyLogicalOperation(op, array, asize); - /* BooleanEdge newarray[asize]; + BooleanEdge newarray[asize]; memcpy(newarray, array, asize * sizeof(BooleanEdge)); for(uint i=0; i < asize; i++) { BooleanEdge b=newarray[i]; @@ -301,7 +300,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) { @@ -338,10 +337,6 @@ 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); @@ -372,78 +367,53 @@ 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;*/ + 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; + ASSERT(first != second); 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(constraint.isNegated()) + model_print("!"); + constraint.getBoolean()->print(); if (isTrue(constraint)) return; - else if (isFalse(constraint)){ - int t=0; -#ifdef TRACE_DEBUG - model_println("Adding constraint which is false :|"); -#endif - setUnSAT(); - } + else if (isFalse(constraint)) { + int t=0; + 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; } @@ -451,12 +421,9 @@ void CSolver::addConstraint(BooleanEdge constraint) { constraints.add(constraint); Boolean *ptr=constraint.getBoolean(); - if (ptr->boolVal == BV_UNSAT){ -#ifdef TRACE_DEBUG - model_println("BooleanValue is Set to UnSAT"); -#endif - setUnSAT(); - } + if (ptr->boolVal == BV_UNSAT) { + setUnSAT(); + } replaceBooleanWithTrueNoRemove(constraint); constraint->parents.clear(); @@ -480,24 +447,24 @@ int CSolver::solve() { long long startTime = getTimeNano(); computePolarities(this); -// 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(); -// eg.encode(); + EncodingGraph eg(this); + eg.buildGraph(); + eg.encode(); naiveEncodingDecision(this); satEncoder->encodeAllSATEncoder(this); - model_println("Is problem UNSAT after encoding: %d", unsat); + model_print("Is problem UNSAT after encoding: %d\n", unsat); int result = unsat ? IS_UNSAT : satEncoder->solve(); - model_println("Result Computed in CSolver: %d", result); + model_print("Result Computed in CSolver: %d\n", result); long long finishTime = getTimeNano(); elapsedTime = finishTime - startTime; if (deleteTuner) { diff --git a/src/csolver.h b/src/csolver.h index b826258..41c4627 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -131,7 +131,7 @@ public: bool isTrue(BooleanEdge b); bool isFalse(BooleanEdge b); - void setUnSAT() { model_println("Setting UNSAT %%%%%%"); unsat = true; } + void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; } bool isUnSAT() { return unsat; } diff --git a/src/mymemory.h b/src/mymemory.h index e0a60bd..7c63aa1 100644 --- a/src/mymemory.h +++ b/src/mymemory.h @@ -26,7 +26,7 @@ void * ourrealloc(void *ptr, size_t size); */ -#if 1 +#if 0 void * model_malloc(size_t size); void model_free(void *ptr); void * model_calloc(size_t count, size_t size); -- 2.34.1