+ 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);
+
+ if (deleteTuner) {
+ delete tuner;
+ tuner = NULL;
+ }
+ return result;
+}
+
+int CSolver::solve() {
+ if (isUnSAT()) {
+ return IS_UNSAT;
+ }
+ long long startTime = getTimeNano();
+ bool deleteTuner = false;
+ if (tuner == NULL) {
+ tuner = new DefaultTuner();
+ deleteTuner = true;
+ }
+ int result = IS_INDETER;
+ if (useInterpreter()) {
+ interpreter->encode();
+ model_print("Problem encoded in Interpreter\n");
+ result = interpreter->solve();
+ model_print("Problem solved by Interpreter\n");
+ } else {
+
+ {
+ SetIteratorOrder *orderit = activeOrders.iterator();
+ while (orderit->hasNext()) {
+ Order *order = orderit->next();
+ if (order->graph != NULL) {
+ delete order->graph;
+ order->graph = NULL;
+ }
+ }
+ delete orderit;
+ }
+ long long time1, time2;
+
+ computePolarities(this);
+ time1 = getTimeNano();
+ model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
+ if(!optimizationsOff){
+ Preprocess pp(this);
+ pp.doTransform();
+ 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();
+ if(!optimizationsOff){
+ 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);
+ }