From 603a6b2c417dc7943a109faccad6b499f5e324ef Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 30 Sep 2026 18:25:28 +0200 Subject: [PATCH 1/3] Add a test for issue #709 --- .../test/InterpolatingProverTest.java | 38 +++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java index 96f4c34301..1eca5ba34b 100644 --- a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java +++ b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java @@ -23,6 +23,7 @@ import java.util.Set; import org.junit.Test; import org.sosy_lab.common.UniqueIdGenerator; +import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -1284,4 +1285,41 @@ public void issue381InterpolationTest3() throws InterruptedException, Solver assertThat(itps).isNotNull(); } } + + // Check that Princess does not leak abbreviation symbols in its interpolants + @Test + public void princessAbbreviationsTest() + throws SolverException, InterruptedException, InvalidConfigurationException { + assume().that(solver).isEqualTo(Solvers.PRINCESS); + + // Lower the threshold for introducing abbreviations + setAdditionalConfigOptionForSolver("solver.princess.minAtomsForAbbreviation", "0"); + + var a = makeVariable("a"); + var b = makeVariable("b"); + var c = makeVariable("c"); + var f = bmgr.makeVariable("f"); + var g = bmgr.makeVariable("g"); + var h = bmgr.not(f); + var i = bmgr.not(g); + + var s = mgr.makeDistinct(a, b, c); + var p = bmgr.and(bmgr.implication(s, f), bmgr.implication(s, g)); + var q = bmgr.and(bmgr.implication(s, h), bmgr.implication(s, i)); + + try (var prover = newEnvironmentForTest()) { + var p1 = prover.addConstraint(s); + var p2 = prover.addConstraint(p); + var p3 = prover.addConstraint(q); + + assertThat(prover.isUnsat()).isTrue(); + + var itps = prover.getSeqInterpolants0(ImmutableList.of(p1, p2, p3)); + for (var itp : itps) { + // Check that there are no abbreviation symbols in the interpolants + assertThat(mgr.extractVariables(p).keySet()) + .containsAtLeastElementsIn(mgr.extractVariables(itp).keySet()); + } + } + } } From e6dfa47549a22d6fc8a23ebbe029d8731d885c81 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 30 Sep 2026 18:31:33 +0200 Subject: [PATCH 2/3] Princess: Eliminate abbreviation symbols from interpolants --- .../solvers/princess/PrincessAbstractProver.java | 12 +++++++++++- .../princess/PrincessInterpolatingProver.java | 13 +++++++------ 2 files changed, 18 insertions(+), 7 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java index 582ca0e388..1e8077f2c4 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -15,6 +15,7 @@ import ap.api.PartialModel; import ap.api.SimpleAPI; import ap.api.SimpleAPI.SimpleAPIException; +import ap.parser.IExpression; import ap.parser.IFormula; import ap.parser.IFunction; import ap.parser.ITerm; @@ -24,7 +25,9 @@ import java.util.ArrayList; import java.util.Collection; import java.util.Deque; +import java.util.HashMap; import java.util.List; +import java.util.Map; import java.util.Optional; import java.util.Set; import java.util.concurrent.Callable; @@ -53,6 +56,8 @@ abstract class PrincessAbstractProver extends AbstractProverWithAllSat { private final PrincessFormulaCreator creator; + protected final Map abbreviations = new HashMap<>(); + PrincessAbstractProver( PrincessFormulaManager pMgr, PrincessFormulaCreator creator, @@ -101,8 +106,13 @@ protected int addConstraint0(BooleanFormula constraint) { api.setPartitionNumber(formulaId); final IFormula t = (IFormula) mgr.extractInfo(constraint); - api.addAssertion(api.abbrevSharedExpressions(t, creator.getEnv().getMinAtomsForAbbreviation())); + // Introduce abbreviation symbols for shared subterms before pushing the formula + var abbreviated = + api.abbrevSharedExpressionsWithMap(t, creator.getEnv().getMinAtomsForAbbreviation()); + abbreviated._2.foreachEntry(abbreviations::put); + + api.addAssertion((IFormula) abbreviated._1); return formulaId; } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java index 4a4bf36ac3..c65719363c 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessInterpolatingProver.java @@ -15,6 +15,7 @@ import ap.basetypes.Tree; import ap.parser.IBoolLit; import ap.parser.IFormula; +import ap.parser.Rewriter; import com.google.common.base.Preconditions; import com.google.common.collect.FluentIterable; import com.google.common.collect.ImmutableList; @@ -23,7 +24,6 @@ import com.google.common.collect.Sets; import com.google.common.graph.Traverser; import java.util.ArrayDeque; -import java.util.ArrayList; import java.util.Collection; import java.util.Deque; import java.util.List; @@ -91,13 +91,14 @@ public List getSeqInterpolants( assert itps.length() == pPartitions.size() - 1 : "There should be (n-1) interpolants for n partitions"; - // convert data-structure back - // TODO check that interpolants do not contain abbreviations we did not introduce ourselves - final List result = new ArrayList<>(); + // Substitute abbreviations and convert the data-structure back to Java + ImmutableList.Builder builder = ImmutableList.builder(); for (final IFormula itp : asJava(itps)) { - result.add(mgr.encapsulateBooleanFormula(itp)); + builder.add( + mgr.encapsulateBooleanFormula( + Rewriter.rewrite(itp, expr -> abbreviations.getOrDefault(expr, expr)))); } - return result; + return builder.build(); } @Override From a90fa86cd93df84ffc263d7a7b50ec72732aca0d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 30 Sep 2026 18:41:06 +0200 Subject: [PATCH 3/3] Fix ecj issue --- .../java_smt/solvers/princess/PrincessAbstractProver.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java index 1e8077f2c4..3dee61f8e7 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -110,7 +110,7 @@ protected int addConstraint0(BooleanFormula constraint) { // Introduce abbreviation symbols for shared subterms before pushing the formula var abbreviated = api.abbrevSharedExpressionsWithMap(t, creator.getEnv().getMinAtomsForAbbreviation()); - abbreviated._2.foreachEntry(abbreviations::put); + abbreviations.putAll(asJava(abbreviated._2)); api.addAssertion((IFormula) abbreviated._1); return formulaId;