Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

293 cvc5 interpolation #320

Merged
merged 62 commits into from
Oct 2, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
62 commits
Select commit Hold shift + click to select a range
773c760
Added CVC5 Interpolation Test in NativeAPITest
RSoegtrop May 11, 2023
dbf09ec
Working CVC5 Interpolation Example
RSoegtrop Jun 2, 2023
010b8a9
first prototype of cvc5 interpolation
RSoegtrop Jun 22, 2023
57c9eb8
added tree interpolation for cvc5. currently to slow to use
RSoegtrop Jun 27, 2023
937c3d6
finalizing sequential interpolation for cvc5
RSoegtrop Jun 28, 2023
ac7e609
fixed bug with unhandled cases
RSoegtrop Jul 10, 2023
26fdd27
test: added non terminating nativ cvc5 interpolation test
RSoegtrop Jul 11, 2023
ab8abc9
cleanup cvc5 interpolation and tests
RSoegtrop Jul 13, 2023
c5e096b
added documentation for cvc5 interpolation
RSoegtrop Jul 17, 2023
e368fcb
formatting
RSoegtrop Jul 18, 2023
99ace6d
fixed build issues
RSoegtrop Jul 18, 2023
750cecd
cvc5-interpolation: added separate solver instance for interpolation
RSoegtrop Jul 19, 2023
47f7b0a
removed separate assertion stack in CVC5 Interpolation
RSoegtrop Jul 24, 2023
747ec8f
fixed nullpointer exception
RSoegtrop Jul 24, 2023
b675a34
moved separate solver instance to exist only during interpolation
RSoegtrop Jul 27, 2023
5df8bd5
detailed cvc5 interpolation description
RSoegtrop Jul 27, 2023
953977b
cleanup. comment refinment.
RSoegtrop Aug 1, 2023
7cef68b
removed arrayLists
RSoegtrop Aug 2, 2023
6d244e6
fixed comments, buildissues, formatting
RSoegtrop Aug 2, 2023
46f7dfe
checkstyle suggestions
RSoegtrop Aug 2, 2023
9fc1499
refaster suggestions
RSoegtrop Aug 2, 2023
c2bfff8
removed recursion in formula building
RSoegtrop Aug 3, 2023
a85e32a
Merge branch 'master' into 293-cvc5-interpolation
RSoegtrop Aug 3, 2023
d021d30
debugging sequential Interpolation
RSoegtrop Aug 6, 2023
aee76aa
fixed conjunction building to be less expensive. fixed setting solver…
RSoegtrop Aug 6, 2023
5bd6c70
swapped most immutablelists with sets
RSoegtrop Aug 7, 2023
1438874
inserted Print
RSoegtrop Aug 7, 2023
7334751
changed implementation of CVC5 sequential Interpolation
RSoegtrop Aug 9, 2023
0164727
editorial
RSoegtrop Aug 10, 2023
27440c4
sequential interpolation working
RSoegtrop Aug 14, 2023
a2f30b1
refaster and checkstyle
RSoegtrop Aug 14, 2023
3a10f5a
format
RSoegtrop Aug 14, 2023
c57d776
added symbol check for interpolant
RSoegtrop Aug 15, 2023
49f1683
Ignored not terminating Tests
RSoegtrop Aug 15, 2023
7b14114
removed tree interpolation
RSoegtrop Aug 17, 2023
9b171fc
fixed build and checkstyle
RSoegtrop Aug 22, 2023
3240030
fixing build issue
RSoegtrop Aug 22, 2023
ce588fc
still fixing build issues
RSoegtrop Aug 22, 2023
eaf14d7
added interpolation check
RSoegtrop Aug 23, 2023
73d49a4
removed formula getter
RSoegtrop Aug 23, 2023
548e824
Merge branch 'master' into 293-cvc5-interpolation
RSoegtrop Aug 23, 2023
3b5f322
added test for trivial interpolation. updates access to assertedFormulas
RSoegtrop Aug 23, 2023
d4b2275
fix interpolation test
RSoegtrop Aug 28, 2023
cc09345
changed cvc5 to craig interpolation validation test to assertion
RSoegtrop Aug 31, 2023
8dddb6c
added documentation for interpolationCheck
RSoegtrop Aug 31, 2023
ef7e635
checkstyle
RSoegtrop Aug 31, 2023
b0f2d4c
Delete src/org/sosy_lab/java_smt/example/Interpolation2.java
RSoegtrop Sep 1, 2023
b7b345e
Fix CVC5 interpolation assertion for interpolants
Sep 1, 2023
afb52d6
Disable an internal assertion for interpolants for CVC5 interpolation…
Sep 1, 2023
a23e85e
do not ignore tests for all solvers, but only for CVC5.
kfriedberger Sep 2, 2023
470c192
some cleanup and simplification.
kfriedberger Sep 2, 2023
167b20c
rename for readability.
kfriedberger Sep 2, 2023
8e8f3ec
simplify and shorted some code.
kfriedberger Sep 2, 2023
c29bd55
simplify and shorten some code.
kfriedberger Sep 2, 2023
826a695
change code to satisfy the Eclipse-compiler and Refaster.
kfriedberger Sep 2, 2023
55a279d
disable slow test for CVC5 and interpolation.
kfriedberger Sep 2, 2023
6a56e82
Merge remote-tracking branch 'origin/master' into 293-cvc5-interpolation
kfriedberger Sep 3, 2023
7a1676e
adding test for counterexample with sequential interpolation vs repea…
kfriedberger Sep 10, 2023
fba562e
bugfix: FluentIterable::append does unwrap Iterables, including Terms…
kfriedberger Sep 10, 2023
acca076
add ConfigurationOption for validating interpolants from CVC5.
kfriedberger Oct 1, 2023
e9e9997
update documentation.
kfriedberger Oct 1, 2023
5e02942
fix JavaDoc format
kfriedberger Oct 1, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/org/sosy_lab/java_smt/SolverContextFactory.java
Original file line number Diff line number Diff line change
Expand Up @@ -240,6 +240,7 @@ private SolverContext generateContext0(Solvers solverToCreate)
case CVC5:
return CVC5SolverContext.create(
logger,
config,
shutdownNotifier,
(int) randomSeed,
nonLinearArithmetic,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
22 changes: 11 additions & 11 deletions src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
234 changes: 234 additions & 0 deletions src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java
Original file line number Diff line number Diff line change
@@ -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();
}
}
}
90 changes: 90 additions & 0 deletions src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
}
Loading