MathSAT: shorten some code and refactor callback-providing method.

This commit unifies the level of abstraction
for registering a shutdown-callback and removing the callback afterwards.

Author: kfriedberger

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java

@@ -24,6 +24,7 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_pop_backtrack_point;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_push_backtrack_point;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_option_checked;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_termination_callback;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_get_arg;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_boolean_constant;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_not;
@@ -99,14 +100,12 @@ private long buildConfig(Set<ProverOptions> opts) {
   public boolean isUnsat() throws InterruptedException, SolverException {
     Preconditions.checkState(!closed);
 
-    long hook = context.addTerminationTest(curEnv);
-    boolean result;
+    final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest());
     try {
-      result = !msat_check_sat(curEnv);
+      return !msat_check_sat(curEnv);
     } finally {
       msat_free_termination_callback(hook);
     }
-    return result;
   }
 
   @Override
@@ -115,14 +114,12 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
     Preconditions.checkState(!closed);
     checkForLiterals(pAssumptions);
 
-    long hook = context.addTerminationTest(curEnv);
-    boolean result;
+    final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest());
     try {
-      result = !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions));
+      return !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions));
     } finally {
       msat_free_termination_callback(hook);
     }
-    return result;
   }
 
   private void checkForLiterals(Collection<BooleanFormula> formulas) {

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java

@@ -17,7 +17,6 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_env;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_version;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_option_checked;
-import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_termination_callback;
 
 import com.google.common.annotations.VisibleForTesting;
 import com.google.common.base.Preconditions;
@@ -300,9 +299,13 @@ public void close() {
     }
   }
 
-  long addTerminationTest(long env) {
+  /**
+   * Get a termination callback for the current context. The callback can be registered upfront,
+   * i.e., before calling a possibly expensive computation in the solver to allow a proper shutdown.
+   */
+  TerminationCallback getTerminationTest() {
     Preconditions.checkState(!closed, "solver context is already closed");
-    return msat_set_termination_callback(env, terminationTest);
+    return terminationTest;
   }
 
   @Override