diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 862d2d116c..72c894c56f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/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 implements BasicProverEnvironment { private final Set evaluators = new LinkedHashSet<>(); - /** This data-structure tracks all formulas that were asserted on different levels. */ - private final List> 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> assertedFormulas = new ArrayList<>(); private static final String TEMPLATE = "Please set the prover option %s."; @@ -50,7 +54,7 @@ protected AbstractProver(Set 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,7 +119,7 @@ public final void pop() { protected ImmutableSet getAssertedFormulas() { ImmutableSet.Builder builder = ImmutableSet.builder(); - for (Map level : assertedFormulas) { + for (Multimap level : assertedFormulas) { builder.addAll(level.keySet()); } return builder.build(); @@ -123,7 +127,7 @@ protected ImmutableSet getAssertedFormulas() { protected ImmutableSet getAssertedConstraintIds() { ImmutableSet.Builder builder = ImmutableSet.builder(); - for (Map level : assertedFormulas) { + for (Multimap level : assertedFormulas) { builder.addAll(level.values()); } return builder.build(); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java index 99b750925a..32e83314b1 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/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 +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // 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 extends AbstractProverWithAllSat { +abstract class CVC5AbstractProver extends AbstractProverWithAllSat { + + 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> 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 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> unsatCoreOverAssumptions( @Override public void close() { if (!closed) { + assertedTerms.clear(); solver.deletePointer(); } super.close(); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java index af1bee3186..dfcc5ca857 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java +++ b/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 +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // 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 - implements InterpolatingProverEnvironment { +public class CVC5InterpolatingProver extends CVC5AbstractProver + implements InterpolatingProverEnvironment { private final FormulaManager mgr; private final Set solverOptions; @@ -65,16 +65,12 @@ protected void setSolverOptions(int randomSeed, Set 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 pFormulasOfA) + public BooleanFormula getInterpolant(Collection pFormulasOfA) throws SolverException, InterruptedException { checkState(!closed); checkArgument( @@ -83,7 +79,8 @@ public BooleanFormula getInterpolant(Collection pFormulasOfA) final Set assertedFormulas = transformedImmutableSetCopy(getAssertedFormulas(), creator::extractInfo); - final Set formulasOfA = ImmutableSet.copyOf(pFormulasOfA); + final Set formulasOfA = + transformedImmutableSetCopy(pFormulasOfA, assertedTerms.peek()::get); final Set formulasOfB = Sets.difference(assertedFormulas, formulasOfA); Term itp = getCVC5Interpolation(formulasOfA, formulasOfB); @@ -91,10 +88,10 @@ public BooleanFormula getInterpolant(Collection pFormulasOfA) } @Override - public List getSeqInterpolants(List> partitions) + public List getSeqInterpolants(List> partitions) throws SolverException, InterruptedException { checkArgument(!partitions.isEmpty(), "at least one partition should be available."); - final ImmutableSet assertedConstraintIds = getAssertedConstraintIds(); + final ImmutableSet assertedConstraintIds = getAssertedConstraintIds(); checkArgument( partitions.stream().allMatch(assertedConstraintIds::containsAll), "interpolation can only be done over previously asserted formulas."); @@ -104,8 +101,14 @@ public List getSeqInterpolants(List> Term previousItp = solver.mkTrue(); for (int i = 1; i < n; i++) { Collection formulasA = - ImmutableSet.builder().addAll(partitions.get(i - 1)).add(previousItp).build(); - Collection formulasB = FluentIterable.concat(partitions.subList(i, n)).toSet(); + FluentIterable.from(partitions.get(i - 1)) + .transform(assertedTerms.peek()::get) + .append(previousItp) + .toSet(); + Collection 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 getSeqInterpolants(List> @Override public List getTreeInterpolants( - List> partitionedFormulas, int[] startOfSubTree) { + List> partitionedFormulas, int[] startOfSubTree) { throw new UnsupportedOperationException( "directly receiving tree interpolants is not supported." + "Use another solver or another strategy for interpolants."); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5TheoremProver.java index f19222988a..55f875cbce 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5TheoremProver.java +++ b/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 +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // 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; + } } diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java index 601913bcf4..8b4b26b1e5 100644 --- a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java +++ b/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 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 void issue381InterpolationTest1() throws InterruptedException, SolverException { + try (InterpolatingProverEnvironment 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 void issue381InterpolationTest2() throws InterruptedException, SolverException { + try (InterpolatingProverEnvironment 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 void issue381InterpolationTest3() throws InterruptedException, SolverException { + try (InterpolatingProverEnvironment 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(); + } + } }