Resolving conflicts after merging with altgen

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 160e6867f854c7abb42a646521782cd576a69d0f..5d4f56d2e1897b6311e629835e533b54f07891b6 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -40,6 +40,7 @@ CSolver::CSolver() :
 /** This function tears down the solver and the entire AST */
 
 CSolver::~CSolver() {
+       //serialize();
        uint size = allBooleans.getSize();
        for (uint i = 0; i < size; i++) {
                delete allBooleans.get(i);
@@ -52,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;
        }
 
@@ -79,6 +80,64 @@ CSolver::~CSolver() {
        delete satEncoder;
 }
 
+void CSolver::resetSolver() {
+       //serialize();
+       uint size = allBooleans.getSize();
+       for (uint i = 0; i < size; i++) {
+               delete allBooleans.get(i);
+       }
+
+       size = allSets.getSize();
+       for (uint i = 0; i < size; i++) {
+               delete allSets.get(i);
+       }
+
+       size = allElements.getSize();
+       for (uint i = 0; i < size; i++) {
+               Element *el = allElements.get(i);
+               delete el;
+       }
+
+       size = allTables.getSize();
+       for (uint i = 0; i < size; i++) {
+               delete allTables.get(i);
+       }
+
+       size = allPredicates.getSize();
+       for (uint i = 0; i < size; i++) {
+               delete allPredicates.get(i);
+       }
+
+       size = allOrders.getSize();
+       for (uint i = 0; i < size; i++) {
+               delete allOrders.get(i);
+       }
+       size = allFunctions.getSize();
+       for (uint i = 0; i < size; i++) {
+               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();
+       elemMap.reset();
+
+       boolTrue = BooleanEdge(new BooleanConst(true));
+       boolFalse = boolTrue.negate();
+       unsat = false;
+       elapsedTime = 0;
+       tuner = NULL;
+       satEncoder->resetSATEncoder();
+
+}
+
 CSolver *CSolver::clone() {
        CSolver *copy = new CSolver();
        CloneMap map;
@@ -91,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();
@@ -100,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()) {
@@ -123,6 +182,10 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange
        return set;
 }
 
+bool CSolver::itemExistInSet(Set *set, uint64_t item){
+        return set->exists(item);
+}
+
 VarType CSolver::getSetVarType(Set *set) {
        return set->getType();
 }
@@ -409,19 +472,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);
                                        }
@@ -480,7 +543,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) {
@@ -489,7 +552,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()) {
@@ -500,7 +563,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();
@@ -522,16 +585,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();
@@ -542,19 +605,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;