SMT Refactoring

key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java

@@ -35,6 +35,7 @@
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.settings.TestGenerationSettings;
 import de.uka.ilkd.key.smt.*;
+import de.uka.ilkd.key.smt.communication.AbstractCESolverSocket;
 import de.uka.ilkd.key.smt.model.Model;
 import de.uka.ilkd.key.smt.solvertypes.SolverType;
 import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
@@ -392,16 +393,18 @@ public Collection<SMTSolver> filterSolverResultsAndShowSolverStatistics(
         final List<SMTSolver> output = new ArrayList<>();
         for (final SMTSolver solver : problemSolvers) {
             try {
-                final SMTSolverResult.ThreeValuedTruth res = solver.getFinalResult().isValid();
+                final SMTSolverResult.ThreeValuedTruth res =
+                    solver.getFinalResult().isValid();
                 if (res == SMTSolverResult.ThreeValuedTruth.UNKNOWN) {
                     unknown++;
                     if (solver.getException() != null) {
                         LOGGER.warn("Solver returned exception", solver.getException());
                     }
                 } else if (res == SMTSolverResult.ThreeValuedTruth.FALSIFIABLE) {
                     solvedPaths++;
-                    if (solver.getSocket().getQuery() != null) {
-                        final Model m = solver.getSocket().getQuery().getModel();
+                    if (solver.getSocket() instanceof AbstractCESolverSocket) {
+                        final Model m =
+                            ((AbstractCESolverSocket) solver.getSocket()).getQuery().getModel();
                         if (TestCaseGenerator.modelIsOK(m)) {
                             output.add(solver);
                         } else {

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java

@@ -23,6 +23,7 @@
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.settings.TestGenerationSettings;
 import de.uka.ilkd.key.smt.*;
+import de.uka.ilkd.key.smt.communication.AbstractCESolverSocket;
 import de.uka.ilkd.key.smt.lang.SMTSort;
 import de.uka.ilkd.key.smt.model.Model;
 import de.uka.ilkd.key.smt.solvertypes.SolverType;
@@ -99,7 +100,7 @@ public void launcherStopped(SolverLauncher launcher, Collection<SMTSolver> finis
             SMTSolverResult result = solver.getFinalResult();
             if (result.isValid().equals(SMTSolverResult.ThreeValuedTruth.FALSIFIABLE)
                     && models.size() < target) {
-                Model model = solver.getSocket().getQuery().getModel();
+                Model model = ((AbstractCESolverSocket) solver.getSocket()).getQuery().getModel();
                 models.add(model);
                 addModelToTerm(model);
 

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java

@@ -22,6 +22,7 @@
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.settings.TestGenerationSettings;
 import de.uka.ilkd.key.smt.SMTSolver;
+import de.uka.ilkd.key.smt.communication.AbstractCESolverSocket;
 import de.uka.ilkd.key.smt.model.Heap;
 import de.uka.ilkd.key.smt.model.Model;
 import de.uka.ilkd.key.smt.model.ObjectVal;
@@ -521,8 +522,9 @@ public StringBuilder createTestCaseCotent(Collection<SMTSolver> problemSolvers)
                          */
                         .proof().name().toString();
                 boolean success = false;
-                if (solver.getSocket().getQuery() != null) {
-                    final Model m = solver.getSocket().getQuery().getModel();
+                if (solver.getSocket() instanceof AbstractCESolverSocket) {
+                    final Model m =
+                        ((AbstractCESolverSocket) solver.getSocket()).getQuery().getModel();
                     if (TestCaseGenerator.modelIsOK(m)) {
                         logger.writeln("Generate: " + originalNodeName);
                         Map<String, Sort> typeInfMap =

key.core/src/main/java/de/uka/ilkd/key/smt/SMTProblem.java

@@ -101,7 +101,8 @@ public Sequent getSequent() {
      * thrown.
      */
     public SMTSolverResult getFinalResult() {
-        SMTSolverResult unknown = SMTSolverResult.NO_IDEA;
+        SMTSolverResult unknown = SMTSolverResult
+                .getUnknownResult(solvers.stream().findFirst().orElseThrow(), this, -1L, null);
         SMTSolverResult valid = null;
         SMTSolverResult invalid = null;
         for (SMTSolver solver : solvers) {

key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolver.java

@@ -4,6 +4,7 @@
 package de.uka.ilkd.key.smt;
 
 import java.util.Collection;
+import java.util.concurrent.Callable;
 
 import de.uka.ilkd.key.smt.communication.AbstractSolverSocket;
 import de.uka.ilkd.key.smt.solvertypes.SolverType;
@@ -21,7 +22,7 @@
  *
  * @author ?
  */
-public interface SMTSolver {
+public interface SMTSolver extends Runnable, Callable<SMTSolverResult> {
 
     /**
      * Possible reasons for why a solver process was interrupted/stopped.
@@ -102,9 +103,6 @@ enum SolverState {
      */
     long getTimeout();
 
-    void setTimeout(long timeout);
-
-
     /**
      * Returns the current state of the solver. Possible values are<br>
      * <code>Waiting</code>: The solver process is waiting for the start signal<br>
@@ -130,16 +128,6 @@ enum SolverState {
      */
     boolean isRunning();
 
-    /**
-     * Starts a solver process. This method should be accessed only by an instance of
-     * <code>SolverLauncher</code>. If you want to start a solver please have a look at
-     * <code>SolverLauncher</code>.
-     *
-     * @param timeout
-     * @param settings
-     */
-    void start(SolverTimeout timeout, SMTSettings settings);
-
     /**
      * @return the reason of the interruption: see <code>ReasonOfInterruption</code>.
      */