bug fixes

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index e4e045293ab1bf846abf2b4a6ffa182e7bd66e5e..b74df47f37c6c22cb20c2e5391b2c0d4e09533ea 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -53,7 +53,7 @@ CSolver::~CSolver() {
 
        size = allElements.getSize();
        for (uint i = 0; i < size; i++) {
-                Element* el = allElements.get(i);
+               Element *el = allElements.get(i);
                delete el;
        }
 
@@ -80,9 +80,9 @@ CSolver::~CSolver() {
        delete satEncoder;
 }
 
-void CSolver::resetSolver(){
-        //serialize();
-        uint size = allBooleans.getSize();
+void CSolver::resetSolver() {
+       //serialize();
+       uint size = allBooleans.getSize();
        for (uint i = 0; i < size; i++) {
                delete allBooleans.get(i);
        }
@@ -94,7 +94,7 @@ void CSolver::resetSolver(){
 
        size = allElements.getSize();
        for (uint i = 0; i < size; i++) {
-                Element* el = allElements.get(i);
+               Element *el = allElements.get(i);
                delete el;
        }
 
@@ -117,25 +117,25 @@ void CSolver::resetSolver(){
                delete allFunctions.get(i);
        }
        delete boolTrue.getBoolean();
-        allBooleans.clear();
-        allSets.clear();
-        allElements.clear();
-        allTables.clear();
-        allPredicates.clear();
-        allOrders.clear();
-        allFunctions.clear();
-        constraints.reset();
-        activeOrders.reset();
-        boolMap.reset();
+       allBooleans.clear();
+       allSets.clear();
+       allElements.clear();
+       allTables.clear();
+       allPredicates.clear();
+       allOrders.clear();
+       allFunctions.clear();
+       constraints.reset();
+       activeOrders.reset();
+       boolMap.reset();
        elemMap.reset();
-        
-        boolTrue = BooleanEdge(new BooleanConst(true));
+
+       boolTrue = BooleanEdge(new BooleanConst(true));
        boolFalse = boolTrue.negate();
-        unsat = false;
-        elapsedTime = 0;
-        tuner = NULL;
-        satEncoder->resetSATEncoder();
-        
+       unsat = false;
+       elapsedTime = 0;
+       tuner = NULL;
+       satEncoder->resetSATEncoder();
+
 }
 
 CSolver *CSolver::clone() {
@@ -150,7 +150,7 @@ CSolver *CSolver::clone() {
        return copy;
 }
 
-CSolver* CSolver::deserialize(const char * file){
+CSolver *CSolver::deserialize(const char *file) {
        model_print("deserializing ...\n");
        Deserializer deserializer(file);
        return deserializer.deserialize();
@@ -159,8 +159,8 @@ CSolver* CSolver::deserialize(const char * file){
 void CSolver::serialize() {
        model_print("serializing ...\n");
        char buffer[255];
-       long long nanotime=getTimeNano();
-       int numchars=sprintf(buffer, "DUMP%llu", nanotime);
+       long long nanotime = getTimeNano();
+       int numchars = sprintf(buffer, "DUMP%llu", nanotime);
        Serializer serializer(buffer);
        SetIteratorBooleanEdge *it = getConstraints();
        while (it->hasNext()) {
@@ -468,19 +468,19 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
                boolMap.put(constraint, constraint);
                constraint->updateParents();
                if (order->graph != NULL) {
-                       OrderGraph *graph=order->graph;
-                       OrderNode *from=graph->lookupOrderNodeFromOrderGraph(first);
+                       OrderGraph *graph = order->graph;
+                       OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
                        if (from != NULL) {
-                               OrderNode *to=graph->lookupOrderNodeFromOrderGraph(second);
+                               OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
                                if (to != NULL) {
-                                       OrderEdge *edge=graph->lookupOrderEdgeFromOrderGraph(from, to);
+                                       OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
                                        OrderEdge *invedge;
 
                                        if (edge != NULL && edge->mustPos) {
                                                replaceBooleanWithTrueNoRemove(constraint);
                                        } else if (edge != NULL && edge->mustNeg) {
                                                replaceBooleanWithFalseNoRemove(constraint);
-                                       } else if ((invedge=graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
+                                       } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
                                                                                 && invedge->mustPos) {
                                                replaceBooleanWithFalseNoRemove(constraint);
                                        }
@@ -539,7 +539,7 @@ Order *CSolver::createOrder(OrderType type, Set *set) {
 }
 
 /** Computes static ordering information to allow isTrue/isFalse
-               queries on newly created orders to work. */
+    queries on newly created orders to work. */
 
 void CSolver::inferFixedOrder(Order *order) {
        if (order->graph != NULL) {
@@ -548,7 +548,7 @@ void CSolver::inferFixedOrder(Order *order) {
        order->graph = buildMustOrderGraph(order);
        reachMustAnalysis(this, order->graph, true);
 }
-       
+
 void CSolver::inferFixedOrders() {
        SetIteratorOrder *orderit = activeOrders.iterator();
        while (orderit->hasNext()) {
@@ -559,7 +559,7 @@ void CSolver::inferFixedOrders() {
 
 #define NANOSEC 1000000000.0
 int CSolver::solve() {
-       long long starttime = getTimeNano();    
+       long long starttime = getTimeNano();
        bool deleteTuner = false;
        if (tuner == NULL) {
                tuner = new DefaultTuner();
@@ -581,16 +581,16 @@ int CSolver::solve() {
 
        computePolarities(this);
        long long time2 = getTimeNano();
-       model_print("Polarity time: %f\n", (time2-starttime)/NANOSEC);
+       model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
        Preprocess pp(this);
        pp.doTransform();
        long long time3 = getTimeNano();
-       model_print("Preprocess time: %f\n", (time3-time2)/NANOSEC);
-       
+       model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC);
+
        DecomposeOrderTransform dot(this);
        dot.doTransform();
        long long time4 = getTimeNano();
-       model_print("Decompose Order: %f\n", (time4-time3)/NANOSEC);
+       model_print("Decompose Order: %f\n", (time4 - time3) / NANOSEC);
 
        IntegerEncodingTransform iet(this);
        iet.doTransform();
@@ -601,19 +601,19 @@ int CSolver::solve() {
 
        naiveEncodingDecision(this);
        long long time5 = getTimeNano();
-       model_print("Encoding Graph Time: %f\n", (time5-time4)/NANOSEC);
-       
+       model_print("Encoding Graph Time: %f\n", (time5 - time4) / NANOSEC);
+
        long long startTime = getTimeNano();
        satEncoder->encodeAllSATEncoder(this);
        long long endTime = getTimeNano();
 
        elapsedTime = endTime - startTime;
-       model_print("Elapse Encode time: %f\n", elapsedTime/NANOSEC);
-       
+       model_print("Elapse Encode time: %f\n", elapsedTime / NANOSEC);
+
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
        int result = unsat ? IS_UNSAT : satEncoder->solve();
        model_print("Result Computed in CSolver: %d\n", result);
-       
+
        if (deleteTuner) {
                delete tuner;
                tuner = NULL;