Merge pull request #320 from sosy-lab/293-cvc5-interpolation

[CVC5]: Add support for Craig interpolation based on the interpolation of CVC5.

Author: kfriedberger

src/org/sosy_lab/java_smt/SolverContextFactory.java

@@ -240,6 +240,7 @@ private SolverContext generateContext0(Solvers solverToCreate)
       case CVC5:
         return CVC5SolverContext.create(
             logger,
+            config,
             shutdownNotifier,
             (int) randomSeed,
             nonLinearArithmetic,

src/org/sosy_lab/java_smt/api/InterpolatingProverEnvironment.java

@@ -30,8 +30,11 @@ public interface InterpolatingProverEnvironment<T> extends BasicProverEnvironmen
    * {@link #isUnsat()} call that returned <code>true</code>.
    *
    * <p>There is no direct guarantee that the interpolants returned are part of an inductive
-   * sequence', however this seems to work for most (all?) solvers as long as the same proof is
-   * used, i.e. all interpolants are computed after the same SAT-check.
+   * sequence', however this seems to work for most solvers as long as the same proof is used, i.e.
+   * all interpolants are computed after the same SAT-check. If a solver does not use the same
+   * internal proof for several interpolation queries (such as CVC5), then the returned interpolants
+   * might not satisfy the sequence-criteria. We suggest the proper method {@link
+   * #getSeqInterpolants} for that case.
    *
    * @param formulasOfA A collection of values returned by {@link #push(BooleanFormula)}. All the
    *     corresponding formulas from group A, the remaining formulas form group B.

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

@@ -54,29 +54,29 @@ protected CVC5AbstractProver(
     incremental = !enableSL;
     solver = new Solver();
 
-    setSolverOptions(randomSeed, pOptions);
+    setSolverOptions(randomSeed, pOptions, solver);
   }
 
-  private void setSolverOptions(int randomSeed, Set<ProverOptions> pOptions) {
+  protected void setSolverOptions(int randomSeed, Set<ProverOptions> pOptions, Solver pSolver) {
     if (incremental) {
-      solver.setOption("incremental", "true");
+      pSolver.setOption("incremental", "true");
     }
     if (pOptions.contains(ProverOptions.GENERATE_MODELS)) {
-      solver.setOption("produce-models", "true");
+      pSolver.setOption("produce-models", "true");
     }
     if (pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE)) {
-      solver.setOption("produce-unsat-cores", "true");
+      pSolver.setOption("produce-unsat-cores", "true");
     }
-    solver.setOption("produce-assertions", "true");
-    solver.setOption("dump-models", "true");
-    solver.setOption("output-language", "smt2");
-    solver.setOption("seed", String.valueOf(randomSeed));
+    pSolver.setOption("produce-assertions", "true");
+    pSolver.setOption("dump-models", "true");
+    pSolver.setOption("output-language", "smt2");
+    pSolver.setOption("seed", String.valueOf(randomSeed));
 
     // Set Strings option to enable all String features (such as lessOrEquals)
-    solver.setOption("strings-exp", "true");
+    pSolver.setOption("strings-exp", "true");
 
     // Enable more complete quantifier solving (for more info see CVC5QuantifiedFormulaManager)
-    solver.setOption("full-saturate-quant", "true");
+    pSolver.setOption("full-saturate-quant", "true");
   }
 
   @Override

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

@@ -0,0 +1,234 @@
+// This file is part of JavaSMT,
+// 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-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.solvers.cvc5;
+
+import static com.google.common.base.Preconditions.checkState;
+import static org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy;
+
+import com.google.common.base.Preconditions;
+import com.google.common.collect.FluentIterable;
+import com.google.common.collect.ImmutableSet;
+import com.google.common.collect.Sets;
+import io.github.cvc5.CVC5ApiException;
+import io.github.cvc5.Kind;
+import io.github.cvc5.Solver;
+import io.github.cvc5.Term;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.List;
+import java.util.Set;
+import org.sosy_lab.common.ShutdownNotifier;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.FormulaManager;
+import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
+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> {
+
+  private final FormulaManager mgr;
+  private final Set<ProverOptions> solverOptions;
+  private final int seed;
+  private final CVC5BooleanFormulaManager bmgr;
+  private final boolean validateInterpolants;
+
+  CVC5InterpolatingProver(
+      CVC5FormulaCreator pFormulaCreator,
+      ShutdownNotifier pShutdownNotifier,
+      int randomSeed,
+      Set<ProverOptions> pOptions,
+      FormulaManager pMgr,
+      boolean pValidateInterpolants) {
+    super(pFormulaCreator, pShutdownNotifier, randomSeed, pOptions, pMgr);
+    mgr = pMgr;
+    solverOptions = pOptions;
+    seed = randomSeed;
+    bmgr = (CVC5BooleanFormulaManager) mgr.getBooleanFormulaManager();
+    validateInterpolants = pValidateInterpolants;
+  }
+
+  /**
+   * Sets the same solver Options of the Original Solver to the separate solvertoSet, except for
+   * produce-interpolants which is set here. From CVC5AbstractProver Line 66
+   */
+  @Override
+  protected void setSolverOptions(int randomSeed, Set<ProverOptions> pOptions, Solver pSolver) {
+    super.setSolverOptions(randomSeed, pOptions, pSolver);
+    pSolver.setOption("produce-interpolants", "true");
+  }
+
+  @Override
+  public Term addConstraint(BooleanFormula pConstraint) throws InterruptedException {
+    checkState(!closed);
+    Term t = creator.extractInfo(pConstraint);
+
+    super.addConstraint(pConstraint);
+    return t; // t is not wrapped in the Abstract Class
+  }
+
+  @Override
+  public BooleanFormula getInterpolant(Collection<Term> pFormulasOfA)
+      throws SolverException, InterruptedException {
+    checkState(!closed);
+
+    final Set<Term> assertedFormulas =
+        transformedImmutableSetCopy(getAssertedFormulas(), creator::extractInfo);
+    final Set<Term> formulasOfA = ImmutableSet.copyOf(pFormulasOfA);
+    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)
+      throws SolverException, InterruptedException {
+    Preconditions.checkArgument(
+        !partitions.isEmpty(), "at least one partition should be available.");
+
+    final int n = partitions.size();
+    final List<BooleanFormula> itps = new ArrayList<>();
+    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();
+      Term itp = getCVC5Interpolation(formulasA, formulasB);
+      itps.add(creator.encapsulateBoolean(itp));
+      previousItp = itp;
+    }
+    return itps;
+  }
+
+  @Override
+  public List<BooleanFormula> getTreeInterpolants(
+      List<? extends Collection<Term>> partitionedFormulas, int[] startOfSubTree) {
+    throw new UnsupportedOperationException(
+        "directly receiving tree interpolants is not supported."
+            + "Use another solver or another strategy for interpolants.");
+  }
+
+  /**
+   * This method computes Craig interpolants for a pair of formulas using CVC5-Interpolation.
+   *
+   * <p>CVC5's interpolation returns an interpolant I for two input formulas A and B, such that the
+   * following holds:
+   *
+   * <ol>
+   *   <li>(A -> I) is valid (1CVC5),
+   *   <li>(I -> B) is valid (2CVC5), and
+   *   <li>I only contains symbols from A and B (3CVC5).
+   * </ol>
+   *
+   * <p>Craig interpolation returns an interpolant psi for two input formulas phi- and phi+, such
+   * that the following holds:
+   *
+   * <ol>
+   *   <li>(phi- -> psi) is valid (1Craig),
+   *   <li>(psi && phi+) is unsatisfiable (2Craig), and
+   *   <li>psi only contains symbols from phi- and phi+ (3Craig).
+   * </ol>
+   *
+   * <p>We can transform CVC5 interpolation to Craig interpolation by negating the formula B, i.e.,
+   * the CVC5 interpolant for input (A, B) represents a Craig interpolant for input (A, not B). Here
+   * is a proof for this:
+   *
+   * <ol>
+   *   <li>(1CVC5) <=> (1Craig): holds, due to substitution of A with phi- and I with psi.
+   *   <li>(2CVC5) <=> (I -> B) is valid <=> ((not I) || B) is valid <=> (not (I && (not B))) is
+   *       valid <=> (I && (not B)) is unsatisfiable <=> (2Craig) holds, due to substitution of I
+   *       with psi and (not B) with phi+.
+   *   <li>(3CVC5) <=> (3Craig): holds, negation does not change symbols.
+   * </ol>
+   *
+   * <p>Hence, CVC5's interpolation produces an equivalent interpolation result to Craig
+   * interpolation, if the input B is negated.
+   *
+   * <p>Please note, that this method will use a different proof for each call, and thus, a sequence
+   * of interpolation queries will most likely not produce sequential Craig interpolants on its own.
+   * Therefore, the caller has to use constraints based on previously computed interpolants.
+   *
+   * @param formulasA formulas for psi- of the interpolation query
+   * @param formulasB formulas for psi+ of the interpolation (will be negated internally)
+   * @return interpolation result following the definition of Craig interpolation.
+   */
+  private Term getCVC5Interpolation(Collection<Term> formulasA, Collection<Term> formulasB) {
+    Term phiPlus = bmgr.andImpl(formulasA);
+    Term phiMinus = bmgr.andImpl(formulasB);
+
+    // Uses a separate Solver instance to leave the original solver-context unmodified
+    Solver itpSolver = new Solver();
+    setSolverOptions(seed, solverOptions, itpSolver);
+
+    Term interpolant;
+    try {
+      itpSolver.assertFormula(phiPlus);
+      interpolant = itpSolver.getInterpolant(itpSolver.mkTerm(Kind.NOT, phiMinus));
+    } finally {
+      itpSolver.deletePointer();
+    }
+
+    if (validateInterpolants) {
+      checkInterpolationCriteria(interpolant, phiPlus, phiMinus);
+    }
+
+    return interpolant;
+  }
+
+  /**
+   * Checks, whether the returned interpolant indeed satisfies Craig-Interpolation and Symbol Usage.
+   *
+   * @param interpolant the given Interpolant for aTerm and bTerm after Craig Interpolation
+   * @param phiPlus the phi+ Term in Craig Interpolation
+   * @param phiMinus the phi- Term in Craig Interpolation (before negation for CVC5-Interpolation)
+   */
+  private void checkInterpolationCriteria(Term interpolant, Term phiPlus, Term phiMinus) {
+
+    // checks that every Symbol of the interpolant appears either in term A or term B
+    Set<String> interpolantSymbols =
+        mgr.extractVariablesAndUFs(creator.encapsulateBoolean(interpolant)).keySet();
+    Set<String> interpolASymbols =
+        mgr.extractVariablesAndUFs(creator.encapsulateBoolean(phiPlus)).keySet();
+    Set<String> interpolBSymbols =
+        mgr.extractVariablesAndUFs(creator.encapsulateBoolean(phiMinus)).keySet();
+    Set<String> intersection = Sets.intersection(interpolASymbols, interpolBSymbols);
+    checkState(
+        intersection.containsAll(interpolantSymbols),
+        "Interpolant contains symbols %s that are not part of both input formulas.",
+        Sets.difference(interpolantSymbols, intersection));
+
+    // build and check both Craig interpolation formulas with the generated interpolant.
+    Solver validationSolver = new Solver();
+    // interpolation option is not required for validation
+    super.setSolverOptions(seed, solverOptions, validationSolver);
+    try {
+      validationSolver.push();
+      validationSolver.assertFormula(validationSolver.mkTerm(Kind.IMPLIES, phiPlus, interpolant));
+      checkState(
+          validationSolver.checkSat().isSat(),
+          "Invalid Craig interpolation: phi+ does not imply the interpolant.");
+      validationSolver.pop();
+
+      validationSolver.push();
+      validationSolver.assertFormula(validationSolver.mkTerm(Kind.AND, interpolant, phiMinus));
+      checkState(
+          validationSolver.checkSat().isUnsat(),
+          "Invalid Craig interpolation: interpolant does not contradict phi-.");
+      validationSolver.pop();
+
+    } catch (CVC5ApiException e) {
+      throw new IllegalArgumentException(
+          "Failure when validating interpolant '" + interpolant + "'.", e);
+
+    } finally {
+      validationSolver.deletePointer();
+    }
+  }
+}

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

@@ -1232,4 +1232,94 @@ public void termAccessAfterModelClosed() throws CVC5ApiException {
 
     System.out.println(valueV);
   }
+
+  @Test
+  public void checkCVC5InterpolationMethod() {
+    solver.setOption("produce-interpolants", "true");
+    Term xp = solver.mkConst(solver.getIntegerSort(), "xp");
+    Term y = solver.mkConst(solver.getIntegerSort(), "y");
+
+    Term ip0 = solver.mkTerm(Kind.GT, xp, y);
+    Term ip1 = solver.mkTerm(Kind.EQUAL, xp, solver.mkInteger(0));
+    Term ip2 = solver.mkTerm(Kind.GT, y, solver.mkInteger(0));
+
+    Term a = ip0;
+    Term b = solver.mkTerm(Kind.AND, ip1, ip2);
+
+    assertThat(!interpolateAndCheck(solver, a, b).isNull()).isTrue();
+  }
+
+  /**
+   * Interpolates Terms after CVC5 and checks the Definition of Craig-Interpolation for the
+   * interpolation.
+   *
+   * @return Interpolantion of interpolantA and interpolantB after CVC5 Interpolation Definition
+   */
+  private Term interpolateAndCheck(Solver solverP, Term interpolantA, Term interpolantB) {
+    // solver.setOption("produce-interpolants", "true");
+    solverP.assertFormula(interpolantA);
+    System.out.println(
+        "Interpolation Pair:\n" + interpolantA + "\n" + solverP.mkTerm(Kind.NOT, interpolantB));
+    Term interpolation = solverP.getInterpolant(solverP.mkTerm(Kind.NOT, interpolantB));
+    System.out.println("Interpolation: " + interpolation);
+    solverP.resetAssertions();
+    Term cvc51 = solverP.mkTerm(Kind.IMPLIES, interpolantA, interpolation);
+    Term cvc52 =
+        solverP.mkTerm(Kind.IMPLIES, interpolation, solverP.mkTerm(Kind.NOT, interpolantB));
+
+    solverP.assertFormula(cvc51);
+    solverP.assertFormula(cvc52);
+    if (solverP.checkSat().isUnsat()) {
+      System.out.println("Does not satisfy CVC5 Interpolation Definition");
+      return null;
+    }
+
+    solverP.resetAssertions();
+    solverP.assertFormula(solverP.mkTerm(Kind.NOT, solverP.mkTerm(Kind.AND, cvc51, cvc52)));
+    if (solverP.checkSat().isSat()) {
+      System.out.println("Does not satisfy generally CVC5 Interpolation Definition");
+      return null;
+    }
+
+    solverP.resetAssertions();
+    Term craig1 = solverP.mkTerm(Kind.IMPLIES, interpolantA, interpolation);
+    Term craig2 =
+        solverP.mkTerm(
+            Kind.EQUAL,
+            solverP.mkTerm(Kind.AND, interpolation, interpolantB),
+            solverP.mkBoolean(false));
+    solverP.assertFormula(craig1);
+    solverP.assertFormula(craig2);
+    if (solverP.checkSat().isUnsat()) {
+      System.out.println("Does not satisfy Craig Interpolation Definition");
+      return null;
+    }
+    solverP.resetAssertions();
+    solverP.assertFormula(solverP.mkTerm(Kind.NOT, solverP.mkTerm(Kind.AND, craig1, craig2)));
+    if (solverP.checkSat().isSat()) {
+      System.out.println("Does not satisfy generally Craig Interpolation Definition");
+      return null;
+    }
+    System.out.println("------------");
+    return interpolation;
+  }
+
+  @Test
+  @Ignore // Does not terminate
+  public void testSimpleInterpolation() {
+    // Out of InterpolatingProverTest.java
+    // Line: 65
+    solver.setOption("produce-interpolants", "true");
+    Term xprime = solver.mkConst(solver.getIntegerSort(), "x");
+    Term y = solver.mkConst(solver.getIntegerSort(), "y");
+    Term z = solver.mkConst(solver.getIntegerSort(), "z");
+    Term f1 = solver.mkTerm(Kind.EQUAL, y, solver.mkTerm(Kind.MULT, solver.mkInteger(2), xprime));
+    Term f2 =
+        solver.mkTerm(
+            Kind.EQUAL,
+            y,
+            solver.mkTerm(
+                Kind.ADD, solver.mkInteger(1), solver.mkTerm(Kind.MULT, z, solver.mkInteger(2))));
+    interpolateAndCheck(solver, f1, f2);
+  }
 }