+int CSolver::solveIncremental() {
+ if (isUnSAT()) {
+ return IS_UNSAT;
+ }
+
+
+ long long startTime = getTimeNano();
+ bool deleteTuner = false;
+ if (tuner == NULL) {
+ tuner = new DefaultTuner();
+ deleteTuner = true;
+ }
+ int result = IS_INDETER;
+ ASSERT (!useInterpreter());
+
+ 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();
+
+ //Doing element optimization on new constraints
+// ElementOpt eop(this);
+// eop.doTransform();
+
+ //Since no new element is added, we assuming adding new constraint
+ //has no impact on previous encoding decisions
+// EncodingGraph eg(this);
+// eg.encode();
+
+ naiveEncodingDecision(this);
+ // eg.validate();
+ //Order of sat solver variables don't change!
+// VarOrderingOpt bor(this, satEncoder);
+// bor.doTransform();
+
+ long long time2 = getTimeNano();
+ //Encoding newly added constraints
+ satEncoder->encodeAllSATEncoder(this);
+ long long 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);
+
+ if (deleteTuner) {
+ delete tuner;
+ tuner = NULL;
+ }
+ return result;
+}
+