Merge pull request #325 from sosy-lab/322-unify-constraint-tracking

Unify constraints tracking across all solvers

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

@@ -2,16 +2,27 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2023 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
 package org.sosy_lab.java_smt.basicimpl;
 
+import static com.google.common.base.Preconditions.checkState;
+
 import com.google.common.base.Preconditions;
+import com.google.common.collect.FluentIterable;
+import com.google.common.collect.ImmutableSet;
+import com.google.common.collect.Iterables;
+import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import java.util.ArrayList;
+import java.util.Collection;
 import java.util.LinkedHashSet;
+import java.util.List;
 import java.util.Set;
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
+import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Evaluator;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 
@@ -22,9 +33,13 @@ public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
   protected final boolean generateUnsatCores;
   private final boolean generateUnsatCoresOverAssumptions;
   protected final boolean enableSL;
+  protected boolean closed = false;
 
   private final Set<Evaluator> evaluators = new LinkedHashSet<>();
 
+  /** This data-structure tracks all formulas that were asserted on different levels. */
+  private final List<Collection<BooleanFormula>> assertedFormulas = new ArrayList<>();
+
   private static final String TEMPLATE = "Please set the prover option %s.";
 
   protected AbstractProver(Set<ProverOptions> pOptions) {
@@ -34,6 +49,8 @@ protected AbstractProver(Set<ProverOptions> pOptions) {
     generateUnsatCoresOverAssumptions =
         pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS);
     enableSL = pOptions.contains(ProverOptions.ENABLE_SEPARATION_LOGIC);
+
+    assertedFormulas.add(new LinkedHashSet<>());
   }
 
   protected final void checkGenerateModels() {
@@ -59,6 +76,37 @@ protected final void checkEnableSeparationLogic() {
     Preconditions.checkState(enableSL, TEMPLATE, ProverOptions.ENABLE_SEPARATION_LOGIC);
   }
 
+  @Override
+  public int size() {
+    checkState(!closed);
+    return assertedFormulas.size() - 1;
+  }
+
+  @Override
+  public void push() throws InterruptedException {
+    checkState(!closed);
+    assertedFormulas.add(new LinkedHashSet<>());
+  }
+
+  @Override
+  public void pop() {
+    checkState(!closed);
+    checkState(assertedFormulas.size() > 1, "initial level must remain until close");
+    assertedFormulas.remove(assertedFormulas.size() - 1); // remove last
+  }
+
+  @Override
+  @CanIgnoreReturnValue
+  public @Nullable T addConstraint(BooleanFormula constraint) throws InterruptedException {
+    checkState(!closed);
+    Iterables.getLast(assertedFormulas).add(constraint);
+    return null;
+  }
+
+  protected ImmutableSet<BooleanFormula> getAssertedFormulas() {
+    return FluentIterable.concat(assertedFormulas).toSet();
+  }
+
   /**
    * This method registers the Evaluator to be cleaned up before the next change on the prover
    * stack.
@@ -79,6 +127,8 @@ protected void closeAllEvaluators() {
 
   @Override
   public void close() {
+    assertedFormulas.clear();
     closeAllEvaluators();
+    closed = true;
   }
 }

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

@@ -31,8 +31,6 @@ public abstract class AbstractProverWithAllSat<T> extends AbstractProver<T> {
   protected final ShutdownNotifier shutdownNotifier;
   private final BooleanFormulaManager bmgr;
 
-  protected boolean closed;
-
   protected AbstractProverWithAllSat(
       Set<ProverOptions> pOptions,
       BooleanFormulaManager pBmgr,

src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java

@@ -117,6 +117,11 @@ public void close() {
     delegate.close();
   }
 
+  @Override
+  public String toString() {
+    return delegate.toString();
+  }
+
   @Override
   public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant)
       throws InterruptedException, SolverException {

src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java

@@ -125,6 +125,11 @@ public void close() {
     logger.log(Level.FINER, "closed");
   }
 
+  @Override
+  public String toString() {
+    return wrapped.toString();
+  }
+
   @Override
   public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> important)
       throws InterruptedException, SolverException {

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java

@@ -104,6 +104,11 @@ public void close() {
     delegate.close();
   }
 
+  @Override
+  public String toString() {
+    return delegate.toString();
+  }
+
   @Override
   public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant)
       throws InterruptedException, SolverException {

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java

@@ -111,6 +111,13 @@ public void close() {
     }
   }
 
+  @Override
+  public String toString() {
+    synchronized (sync) {
+      return delegate.toString();
+    }
+  }
+
   @Override
   public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant)
       throws InterruptedException, SolverException {

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java

@@ -128,6 +128,13 @@ public void close() {
     }
   }
 
+  @Override
+  public String toString() {
+    synchronized (sync) {
+      return delegate.toString();
+    }
+  }
+
   @Override
   public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant)
       throws InterruptedException, SolverException {

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java

@@ -9,10 +9,8 @@
 package org.sosy_lab.java_smt.solvers.boolector;
 
 import com.google.common.base.Preconditions;
-import java.util.ArrayDeque;
-import java.util.ArrayList;
+import com.google.common.collect.Collections2;
 import java.util.Collection;
-import java.util.Deque;
 import java.util.List;
 import java.util.Optional;
 import java.util.Set;
@@ -28,16 +26,13 @@
 import org.sosy_lab.java_smt.solvers.boolector.BtorJNI.TerminationCallback;
 
 abstract class BoolectorAbstractProver<T> extends AbstractProverWithAllSat<T> {
-  // BoolectorAbstractProver<E, AF> extends AbstractProverWithAllSat<E>
-  // AF = assertedFormulas; E = ?
 
   /** Boolector does not support multiple solver stacks. */
   private final AtomicBoolean isAnyStackAlive;
 
   private final long btor;
   private final BoolectorFormulaManager manager;
   private final BoolectorFormulaCreator creator;
-  protected final Deque<List<Long>> assertedFormulas = new ArrayDeque<>();
   protected boolean wasLastSatCheckSat = false; // and stack is not changed
   private final TerminationCallback terminationCallback;
   private final long terminationCallbackHelper;
@@ -64,7 +59,7 @@ protected BoolectorAbstractProver(
         "Boolector does not support the usage of multiple "
             + "solver stacks at the same time. Please close any existing solver stack.");
     // push an initial level, required for cleaning up later (see #close), for reusage of Boolector.
-    push();
+    BtorJNI.boolector_push(manager.getEnvironment(), 1);
   }
 
   @Override
@@ -73,14 +68,13 @@ public void close() {
       // Free resources of callback
       BtorJNI.boolector_free_termination(terminationCallbackHelper);
       // remove the whole stack, including the initial level from the constructor call.
-      BtorJNI.boolector_pop(manager.getEnvironment(), assertedFormulas.size());
-      assertedFormulas.clear();
+      BtorJNI.boolector_pop(manager.getEnvironment(), size() + 1);
       // You can't use delete here because you wouldn't be able to access model
       // Wait till we have visitor/toList, after that we can delete here
       // BtorJNI.boolector_delete(btor);
-      closed = true;
       Preconditions.checkState(isAnyStackAlive.getAndSet(false));
     }
+    super.close();
   }
 
   /*
@@ -113,23 +107,17 @@ public boolean isUnsat() throws SolverException, InterruptedException {
   public void pop() {
     Preconditions.checkState(!closed);
     Preconditions.checkState(size() > 0);
-    assertedFormulas.pop();
     BtorJNI.boolector_pop(manager.getEnvironment(), 1);
+    super.pop();
   }
 
   @Override
-  public void push() {
+  public void push() throws InterruptedException {
     Preconditions.checkState(!closed);
-    assertedFormulas.push(new ArrayList<>());
+    super.push();
     BtorJNI.boolector_push(manager.getEnvironment(), 1);
   }
 
-  @Override
-  public int size() {
-    Preconditions.checkState(!closed);
-    return assertedFormulas.size() - 1;
-  }
-
   @Override
   public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
       throws SolverException, InterruptedException {
@@ -151,7 +139,8 @@ public Model getModel() throws SolverException {
 
   @Override
   protected BoolectorModel getEvaluatorWithoutChecks() {
-    return new BoolectorModel(btor, creator, this, getAssertedTerms());
+    return new BoolectorModel(
+        btor, creator, this, Collections2.transform(getAssertedFormulas(), creator::extractInfo));
   }
 
   @Override
@@ -168,19 +157,13 @@ public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
 
   @Override
   @Nullable
-  public T addConstraint(BooleanFormula constraint) {
+  public T addConstraint(BooleanFormula constraint) throws InterruptedException {
+    super.addConstraint(constraint);
     BtorJNI.boolector_assert(
         manager.getEnvironment(), BoolectorFormulaManager.getBtorTerm(constraint));
-    assertedFormulas.peek().add(BoolectorFormulaManager.getBtorTerm(constraint));
     return null;
   }
 
-  protected Collection<Long> getAssertedTerms() {
-    List<Long> result = new ArrayList<>();
-    assertedFormulas.forEach(result::addAll);
-    return result;
-  }
-
   /**
    * Simply returns true if the prover is closed. False otherwise.
    *