Princess: Eliminate abbreviation symbols from interpolants

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<E> extends AbstractProverWithAllSat<E> {
 
   private final PrincessFormulaCreator creator;
 
+  protected final Map<IExpression, IExpression> 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());
+    abbreviations.putAll(asJava(abbreviated._2));
+
+    api.addAssertion((IFormula) abbreviated._1);
     return formulaId;
   }
 

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<BooleanFormula> 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<BooleanFormula> result = new ArrayList<>();
+    // Substitute abbreviations and convert the data-structure back to Java
+    ImmutableList.Builder<BooleanFormula> 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

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 <T> 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());
+      }
+    }
+  }
 }