Add default impl for AbstractProver#getStatistics to perform common checks and a delegate method that can be implemented by the solvers

Author: baierd

src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java

@@ -376,6 +376,19 @@ public final <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> impor
   protected abstract <R> R allSatImpl(AllSatCallback<R> callback, List<BooleanFormula> important)
       throws InterruptedException, SolverException;
 
+  @Override
+  public final ImmutableMap<String, String> getStatistics() {
+    Preconditions.checkState(!closed);
+    return getStatisticsImpl();
+  }
+
+  /**
+   * @implSpec override and implement for solvers that provide statistics.
+   */
+  protected ImmutableMap<String, String> getStatisticsImpl() {
+    return ImmutableMap.of();
+  }
+
   @Override
   public void close() {
     assertedFormulas.clear();

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

@@ -211,9 +211,8 @@ private List<BooleanFormula> encapsulate(long[] terms) {
   }
 
   @Override
-  public ImmutableMap<String, String> getStatistics() {
+  public ImmutableMap<String, String> getStatisticsImpl() {
     // Mathsat sigsevs if you try to get statistics for closed environments
-    Preconditions.checkState(!closed);
     final String stats = msat_get_search_stats(curEnv);
     return ImmutableMap.copyOf(
         Splitter.on("\n").trimResults().omitEmptyStrings().withKeyValueSeparator(" ").split(stats));

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java

@@ -201,7 +201,7 @@ protected Optional<List<BooleanFormula>> unsatCoreOverAssumptionsImpl(
   }
 
   @Override
-  public ImmutableMap<String, String> getStatistics() {
+  public ImmutableMap<String, String> getStatisticsImpl() {
     ImmutableMap.Builder<String, String> builder = ImmutableMap.builder();
     SmtInterpolSolverContext.flatten(builder, "", env.getInfo(":all-statistics"));
     return builder.buildOrThrow();

src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java

@@ -207,10 +207,7 @@ protected Optional<List<BooleanFormula>> unsatCoreOverAssumptionsImpl(
   protected abstract long getStatistics0();
 
   @Override
-  public ImmutableMap<String, String> getStatistics() {
-    // Z3 sigsevs if you try to get statistics for closed environments
-    Preconditions.checkState(!closed);
-
+  public ImmutableMap<String, String> getStatisticsImpl() {
     ImmutableMap.Builder<String, String> builder = ImmutableMap.builder();
     Set<String> seenKeys = new HashSet<>();
 

src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyAbstractProver.java

@@ -327,10 +327,7 @@ protected Optional<List<BooleanFormula>> unsatCoreOverAssumptionsImpl(
   }
 
   @Override
-  public ImmutableMap<String, String> getStatistics() {
-    // Z3 sigsevs if you try to get statistics for closed environments
-    Preconditions.checkState(!closed);
-
+  public ImmutableMap<String, String> getStatisticsImpl() {
     ImmutableMap.Builder<String, String> builder = ImmutableMap.builder();
     Set<String> seenKeys = new HashSet<>();