- long long startTime = getTimeNano();
- computePolarities(this);
-
- Preprocess pp(this);
- pp.doTransform();
-
- DecomposeOrderTransform dot(this);
- dot.doTransform();
-
- IntegerEncodingTransform iet(this);
- iet.doTransform();
-
- naiveEncodingDecision(this);
- satEncoder->encodeAllSATEncoder(this);
- int result = unsat ? IS_UNSAT : satEncoder->solve();
- long long finishTime = getTimeNano();
- elapsedTime = finishTime - startTime;
+ {
+ SetIteratorOrder *orderit = activeOrders.iterator();
+ while (orderit->hasNext()) {
+ Order *order = orderit->next();
+ if (order->graph != NULL) {
+ delete order->graph;
+ order->graph = NULL;
+ }
+ }
+ delete orderit;
+ }
+ computePolarities(this);
+ long long time1 = getTimeNano();
+ model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
+ Preprocess pp(this);
+ pp.doTransform();
+ long long time2 = getTimeNano();
+ model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
+
+ DecomposeOrderTransform dot(this);
+ dot.doTransform();
+ time1 = getTimeNano();
+ model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
+
+ IntegerEncodingTransform iet(this);
+ iet.doTransform();
+
+ ElementOpt eop(this);
+ eop.doTransform();
+
+ EncodingGraph eg(this);
+ eg.encode();
+
+ naiveEncodingDecision(this);
+ // eg.validate();
+
+ VarOrderingOpt bor(this, satEncoder);
+ bor.doTransform();
+
+ time2 = getTimeNano();
+ model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+
+ satEncoder->encodeAllSATEncoder(this);
+ time1 = getTimeNano();
+
+ model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
+
+ model_print("Is problem UNSAT after encoding: %d\n", unsat);
+
+
+ result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
+ model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
+ time2 = getTimeNano();
+ elapsedTime = time2 - startTime;
+ model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
+ }