#381 improve interpolation behaviour

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

@@ -13,12 +13,12 @@
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Iterables;
+import com.google.common.collect.LinkedHashMultimap;
+import com.google.common.collect.Multimap;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import java.util.ArrayList;
-import java.util.LinkedHashMap;
 import java.util.LinkedHashSet;
 import java.util.List;
-import java.util.Map;
 import java.util.Set;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
@@ -37,8 +37,12 @@ public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
   private final Set<Evaluator> evaluators = new LinkedHashSet<>();
 
-  /** This data-structure tracks all formulas that were asserted on different levels. */
-  private final List<Map<BooleanFormula, T>> assertedFormulas = new ArrayList<>();
+  /**
+   * This data-structure tracks all formulas that were asserted on different levels. We can assert a
+   * formula multiple times on the same or also distinct levels and return a new ID for each
+   * assertion.
+   */
+  private final List<Multimap<BooleanFormula, T>> assertedFormulas = new ArrayList<>();
 
   private static final String TEMPLATE = "Please set the prover option %s.";
 
@@ -50,7 +54,7 @@ protected AbstractProver(Set<ProverOptions> pOptions) {
         pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS);
     enableSL = pOptions.contains(ProverOptions.ENABLE_SEPARATION_LOGIC);
 
-    assertedFormulas.add(new LinkedHashMap<>());
+    assertedFormulas.add(LinkedHashMultimap.create());
   }
 
   protected final void checkGenerateModels() {
@@ -86,7 +90,7 @@ public int size() {
   public final void push() throws InterruptedException {
     checkState(!closed);
     pushImpl();
-    assertedFormulas.add(new LinkedHashMap<>());
+    assertedFormulas.add(LinkedHashMultimap.create());
   }
 
   protected abstract void pushImpl() throws InterruptedException;
@@ -115,15 +119,15 @@ public final void pop() {
 
   protected ImmutableSet<BooleanFormula> getAssertedFormulas() {
     ImmutableSet.Builder<BooleanFormula> builder = ImmutableSet.builder();
-    for (Map<BooleanFormula, T> level : assertedFormulas) {
+    for (Multimap<BooleanFormula, T> level : assertedFormulas) {
       builder.addAll(level.keySet());
     }
     return builder.build();
   }
 
   protected ImmutableSet<T> getAssertedConstraintIds() {
     ImmutableSet.Builder<T> builder = ImmutableSet.builder();
-    for (Map<BooleanFormula, T> level : assertedFormulas) {
+    for (Multimap<BooleanFormula, T> level : assertedFormulas) {
       builder.addAll(level.values());
     }
     return builder.build();

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2022 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -11,18 +11,23 @@
 import com.google.common.base.Preconditions;
 import com.google.common.collect.Collections2;
 import com.google.common.collect.ImmutableList;
+import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import io.github.cvc5.CVC5ApiException;
 import io.github.cvc5.Result;
 import io.github.cvc5.Solver;
 import io.github.cvc5.Term;
 import io.github.cvc5.UnknownExplanation;
+import java.util.ArrayDeque;
 import java.util.ArrayList;
 import java.util.Collection;
+import java.util.Deque;
 import java.util.List;
 import java.util.Optional;
 import java.util.Set;
-import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.ShutdownNotifier;
+import org.sosy_lab.common.UniqueIdGenerator;
+import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap;
+import org.sosy_lab.common.collect.PersistentMap;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Evaluator;
 import org.sosy_lab.java_smt.api.FormulaManager;
@@ -31,12 +36,15 @@
 import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat;
 
-public class CVC5AbstractProver<T> extends AbstractProverWithAllSat<T> {
+abstract class CVC5AbstractProver<T> extends AbstractProverWithAllSat<T> {
+
+  private static final UniqueIdGenerator ID_GENERATOR = new UniqueIdGenerator();
 
   private final FormulaManager mgr;
   protected final CVC5FormulaCreator creator;
   protected final Solver solver;
   private boolean changedSinceLastSatQuery = false;
+  protected final Deque<PersistentMap<String, Term>> assertedTerms = new ArrayDeque<>();
 
   // TODO: does CVC5 support separation logic in incremental mode?
   protected final boolean incremental;
@@ -53,6 +61,7 @@ protected CVC5AbstractProver(
     creator = pFormulaCreator;
     incremental = !enableSL;
     solver = new Solver();
+    assertedTerms.add(PathCopyingPersistentTreeMap.of());
 
     setSolverOptions(randomSeed, pOptions, solver);
   }
@@ -82,6 +91,7 @@ protected void setSolverOptions(int randomSeed, Set<ProverOptions> pOptions, Sol
   @Override
   protected void pushImpl() throws InterruptedException {
     setChanged();
+    assertedTerms.push(assertedTerms.peek()); // add copy of top-level
     if (incremental) {
       try {
         solver.push();
@@ -103,17 +113,20 @@ protected void popImpl() {
             "You tried to use pop() on an CVC5 assertion stack illegally.", e);
       }
     }
+    assertedTerms.pop();
   }
 
-  @Override
-  protected @Nullable T addConstraintImpl(BooleanFormula pF) throws InterruptedException {
+  @CanIgnoreReturnValue
+  protected String addConstraint0(BooleanFormula pF) {
     Preconditions.checkState(!closed);
     setChanged();
     Term exp = creator.extractInfo(pF);
     if (incremental) {
       solver.assertFormula(exp);
     }
-    return null;
+    String id = "ID_" + ID_GENERATOR.getFreshId();
+    assertedTerms.push(assertedTerms.pop().putAndCopy(id, exp));
+    return id;
   }
 
   @SuppressWarnings("resource")
@@ -214,6 +227,7 @@ public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
   @Override
   public void close() {
     if (!closed) {
+      assertedTerms.clear();
       solver.deletePointer();
     }
     super.close();

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2023 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -30,8 +30,8 @@
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
 
-public class CVC5InterpolatingProver extends CVC5AbstractProver<Term>
-    implements InterpolatingProverEnvironment<Term> {
+public class CVC5InterpolatingProver extends CVC5AbstractProver<String>
+    implements InterpolatingProverEnvironment<String> {
 
   private final FormulaManager mgr;
   private final Set<ProverOptions> solverOptions;
@@ -65,16 +65,12 @@ protected void setSolverOptions(int randomSeed, Set<ProverOptions> pOptions, Sol
   }
 
   @Override
-  protected Term addConstraintImpl(BooleanFormula pConstraint) throws InterruptedException {
-    checkState(!closed);
-    Term t = creator.extractInfo(pConstraint);
-
-    super.addConstraintImpl(pConstraint);
-    return t; // t is not wrapped in the Abstract Class
+  protected String addConstraintImpl(BooleanFormula constraint) throws InterruptedException {
+    return super.addConstraint0(constraint);
   }
 
   @Override
-  public BooleanFormula getInterpolant(Collection<Term> pFormulasOfA)
+  public BooleanFormula getInterpolant(Collection<String> pFormulasOfA)
       throws SolverException, InterruptedException {
     checkState(!closed);
     checkArgument(
@@ -83,18 +79,19 @@ public BooleanFormula getInterpolant(Collection<Term> pFormulasOfA)
 
     final Set<Term> assertedFormulas =
         transformedImmutableSetCopy(getAssertedFormulas(), creator::extractInfo);
-    final Set<Term> formulasOfA = ImmutableSet.copyOf(pFormulasOfA);
+    final Set<Term> formulasOfA =
+        transformedImmutableSetCopy(pFormulasOfA, assertedTerms.peek()::get);
     final Set<Term> formulasOfB = Sets.difference(assertedFormulas, formulasOfA);
 
     Term itp = getCVC5Interpolation(formulasOfA, formulasOfB);
     return creator.encapsulateBoolean(itp);
   }
 
   @Override
-  public List<BooleanFormula> getSeqInterpolants(List<? extends Collection<Term>> partitions)
+  public List<BooleanFormula> getSeqInterpolants(List<? extends Collection<String>> partitions)
       throws SolverException, InterruptedException {
     checkArgument(!partitions.isEmpty(), "at least one partition should be available.");
-    final ImmutableSet<Term> assertedConstraintIds = getAssertedConstraintIds();
+    final ImmutableSet<String> assertedConstraintIds = getAssertedConstraintIds();
     checkArgument(
         partitions.stream().allMatch(assertedConstraintIds::containsAll),
         "interpolation can only be done over previously asserted formulas.");
@@ -104,8 +101,14 @@ public List<BooleanFormula> getSeqInterpolants(List<? extends Collection<Term>>
     Term previousItp = solver.mkTrue();
     for (int i = 1; i < n; i++) {
       Collection<Term> formulasA =
-          ImmutableSet.<Term>builder().addAll(partitions.get(i - 1)).add(previousItp).build();
-      Collection<Term> formulasB = FluentIterable.concat(partitions.subList(i, n)).toSet();
+          FluentIterable.from(partitions.get(i - 1))
+              .transform(assertedTerms.peek()::get)
+              .append(previousItp)
+              .toSet();
+      Collection<Term> formulasB =
+          FluentIterable.concat(partitions.subList(i, n))
+              .transform(assertedTerms.peek()::get)
+              .toSet();
       Term itp = getCVC5Interpolation(formulasA, formulasB);
       itps.add(creator.encapsulateBoolean(itp));
       previousItp = itp;
@@ -115,7 +118,7 @@ public List<BooleanFormula> getSeqInterpolants(List<? extends Collection<Term>>
 
   @Override
   public List<BooleanFormula> getTreeInterpolants(
-      List<? extends Collection<Term>> partitionedFormulas, int[] startOfSubTree) {
+      List<? extends Collection<String>> partitionedFormulas, int[] startOfSubTree) {
     throw new UnsupportedOperationException(
         "directly receiving tree interpolants is not supported."
             + "Use another solver or another strategy for interpolants.");

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5TheoremProver.java

@@ -2,15 +2,17 @@
 // 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: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
 package org.sosy_lab.java_smt.solvers.cvc5;
 
 import java.util.Set;
+import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
+import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.FormulaManager;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
@@ -26,4 +28,11 @@ protected CVC5TheoremProver(
       FormulaManager pMgr) {
     super(pFormulaCreator, pShutdownNotifier, randomSeed, pOptions, pMgr);
   }
+
+  @Override
+  @Nullable
+  protected Void addConstraintImpl(BooleanFormula constraint) throws InterruptedException {
+    addConstraint0(constraint);
+    return null;
+  }
 }

src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java

@@ -255,7 +255,7 @@ private void requireTreeItp() {
     assume()
         .withMessage("Solver does not support tree-interpolation.")
         .that(solver)
-        .isAnyOf(Solvers.Z3, Solvers.SMTINTERPOL, Solvers.PRINCESS);
+        .isAnyOf(Solvers.SMTINTERPOL, Solvers.PRINCESS);
   }
 
   @Test
@@ -1179,4 +1179,82 @@ public <T> void testInvalidToken() throws InterruptedException, SolverException
     assertThrows(
         IllegalArgumentException.class, () -> stack.getInterpolant(ImmutableList.of((T) p3)));
   }
+
+  /*
+   * This tests that 2 formulas that are equal but not the same are treated that way by the
+   * interpolation procedure. (Asserting the 2 formulas on the stack should return 2 distinct itp
+   *  points, that are then treated as distinct itp points by the interpolation.)
+   */
+  @Test
+  public <T> void issue381InterpolationTest1() throws InterruptedException, SolverException {
+    try (InterpolatingProverEnvironment<T> prover = newEnvironmentForTest()) {
+      var x = imgr.makeVariable("x");
+      var one = imgr.makeNumber(1);
+      var eq = imgr.equal(one, x);
+      var lt1 = imgr.lessThan(one, x);
+      var lt2 = imgr.lessThan(one, x);
+      assertThat(lt1).isEqualTo(lt2);
+
+      var eqT = prover.addConstraint(eq);
+      var ltT1 = prover.addConstraint(lt1);
+      var ltT2 = prover.addConstraint(lt2);
+      assertThat(ltT1).isNotEqualTo(ltT2);
+      assertThat(prover.isUnsat()).isTrue();
+
+      var itps = prover.getSeqInterpolants0(ImmutableList.of(eqT, ltT1));
+      assertThat(itps).isNotNull();
+    }
+  }
+
+  /*
+   * This tests that 2 formulas that are equal but not the same are treated that way by the
+   * interpolation procedure. (Asserting the 2 formulas on the stack should return 2 distinct itp
+   *  points, that are then treated as distinct itp points by the interpolation.)
+   */
+  @Test
+  public <T> void issue381InterpolationTest2() throws InterruptedException, SolverException {
+    try (InterpolatingProverEnvironment<T> prover = newEnvironmentForTest()) {
+      var x = imgr.makeVariable("x");
+      var one = imgr.makeNumber(1);
+      var eq = imgr.equal(one, x);
+      var lt1 = imgr.lessThan(one, x);
+      var lt2 = imgr.lessThan(one, x);
+      assertThat(lt1).isEqualTo(lt2);
+
+      var eqT = prover.addConstraint(eq);
+      var ltT1 = prover.addConstraint(lt1);
+      var ltT2 = prover.addConstraint(lt2);
+      assertThat(ltT1).isNotEqualTo(ltT2);
+      assertThat(prover.isUnsat()).isTrue();
+
+      var itps = prover.getSeqInterpolants0(ImmutableList.of(eqT, ltT2));
+      assertThat(itps).isNotNull();
+    }
+  }
+
+  /*
+   * This tests that 2 formulas that are equal but not the same are treated that way by the
+   * interpolation procedure. (Asserting the 2 formulas on the stack should return 2 distinct itp
+   *  points, that are then treated as distinct itp points by the interpolation.)
+   */
+  @Test
+  public <T> void issue381InterpolationTest3() throws InterruptedException, SolverException {
+    try (InterpolatingProverEnvironment<T> prover = newEnvironmentForTest()) {
+      var x = imgr.makeVariable("x");
+      var one = imgr.makeNumber(1);
+      var eq = imgr.equal(one, x);
+      var lt1 = imgr.lessThan(one, x);
+      var lt2 = imgr.lessThan(one, x);
+      assertThat(lt1).isEqualTo(lt2);
+
+      var eqT = prover.addConstraint(eq);
+      var ltT1 = prover.addConstraint(lt1);
+      var ltT2 = prover.addConstraint(lt2);
+      assertThat(ltT1).isNotEqualTo(ltT2);
+      assertThat(prover.isUnsat()).isTrue();
+
+      var itps = prover.getInterpolant(ImmutableList.of(eqT));
+      assertThat(itps).isNotNull();
+    }
+  }
 }