Skip to content

Yices: Use "MCSat+dpllt" for interpolation #705

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.

Sign up for GitHub

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

Open
daniel-raffler wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Yices: Use "MCSat+dpllt" for interpolation #705

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2ce68cc
Yices: Allow interpolation to be interrupted
daniel-raffler Aug 10, 2026
54558f2
Yices: Use dpllt as solver for "B" partitions during interpolation
daniel-raffler Aug 10, 2026
6f053bf
Checkstyle + Errorprone
daniel-raffler Aug 12, 2026
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
116 changes: 80 additions & 36 deletions src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,15 +12,15 @@

import static org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy;

import com.google.common.collect.FluentIterable;
import com.google.common.collect.ImmutableList;
import com.google.common.collect.ImmutableSet;
import com.google.common.collect.Sets;
import com.google.common.primitives.Ints;
import com.sri.yices.Context;
import com.sri.yices.InterpolationContext;
import com.sri.yices.Status;
import com.sri.yices.Terms;
import com.sri.yices.YicesException;
import java.util.ArrayList;
import java.util.Collection;
import java.util.List;
import java.util.Set;
Expand All @@ -31,6 +31,7 @@
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;
import org.sosy_lab.java_smt.basicimpl.ShutdownHook;

class Yices2InterpolatingProver extends Yices2AbstractProver<Integer>
implements InterpolatingProverEnvironment<Integer> {
Expand Down Expand Up @@ -61,25 +62,34 @@ public BooleanFormula getInterpolant(Collection<Integer> formulasOfA)
var setA = ImmutableSet.copyOf(formulasOfA);
var setB = Sets.difference(getAssertedConstraintIds(), setA);

return creator.encapsulateBoolean(
interpolate(
transformedImmutableSetCopy(setA, stack.peekLast()::get),
transformedImmutableSetCopy(setB, stack.peekLast()::get)));
}

private int interpolate(Collection<Integer> setA, Collection<Integer> setB)
throws InterruptedException, SolverException {
try (var ctxA = newContext("mcsat");
var ctxB = newContext("mcsat")) {
var ctxB = newContext("dpllt")) {

ctxA.assertFormulas(Ints.toArray(transformedImmutableSetCopy(setA, stack.peekLast()::get)));
try {
ctxB.assertFormulas(Ints.toArray(transformedImmutableSetCopy(setB, stack.peekLast()::get)));
ctxB.push(); // Will trigger an exception if B is already unsat by itself

} catch (YicesException e) {
return creator.encapsulateBoolean(Terms.mkTrue());
}
return creator.encapsulateBoolean(interpolate(ctxA, ctxB));
}
}

ctxA.assertFormulas(Ints.toArray(setA));
ctxB.assertFormulas(Ints.toArray(setB));
var context = new InterpolationContext(ctxA, ctxB);
@SuppressWarnings("try")
private int interpolate(Context ctxA, Context ctxB) throws InterruptedException, SolverException {
var context = new InterpolationContext(ctxA, ctxB);

// TODO How to abort this?
// For now, let's just check before and after the call:
Status status;
try (ShutdownHook hook =
new ShutdownHook(
shutdownNotifier,
() -> {
ctxA.stopSearch();
ctxB.stopSearch();
})) {
shutdownNotifier.shutdownIfNecessary();
Status status;
try {
status = context.check(DEFAULT_PARAMS, false);
} catch (YicesException e) {
Expand All @@ -89,34 +99,68 @@ private int interpolate(Collection<Integer> setA, Collection<Integer> setB)
throw e;
}
}
shutdownNotifier.shutdownIfNecessary();
if (status == Status.UNSAT) {
}

switch (status) {
case INTERRUPTED -> throw new InterruptedException();
case UNSAT -> {
return context.getInterpolant();
} else {
throw new IllegalStateException("Solver state must be unsat");
}
case UNKNOWN -> throw new SolverException("Could not interpolate");
default -> throw new RuntimeException("Inconsistent SAT result during interpolation");
}
}

@Override
public List<BooleanFormula> getSeqInterpolants(List<? extends Collection<Integer>> partitions)
throws SolverException, InterruptedException {
final int n = partitions.size();
final List<BooleanFormula> itps = new ArrayList<>();
var previousItp = Terms.mkTrue();
for (int i = 1; i < n; i++) {
Collection<Integer> formulasA =
FluentIterable.from(partitions.get(i - 1))
.transform(stack.peekLast()::get)
.append(new Integer[] {previousItp})
.toSet();
Collection<Integer> formulasB =
FluentIterable.concat(partitions.subList(i, n)).transform(stack.peekLast()::get).toSet();
var itp = interpolate(formulasA, formulasB);
itps.add(creator.encapsulateBoolean(itp));
previousItp = itp;

var groups =
partitions.stream()
.map(partition -> partition.stream().map(stack.peekLast()::get).toList())
.toList();

try (var ctxA = newContext("mcsat");
var ctxB = newContext("dpllt")) {

ctxB.push();
int skipped = 0;
for (int i = groups.size() - 1; i > 0; i--) {
try {
ctxB.assertFormulas(groups.get(i));
ctxB.push();
} catch (YicesException e) {
// Yices will throw this exception once the Bs have become unsat
skipped = i;
break;
}
}
ctxB.pop();

ImmutableList.Builder<BooleanFormula> builder = ImmutableList.builder();

var lastItp = Terms.mkTrue();
for (int i = 0; i < groups.size() - 1; i++) {
if (i < skipped) {
// Interpolants are 'true' until B is no longer unsat by itself
builder.add(creator.encapsulateBoolean(lastItp));

} else {
ctxA.push();

ctxA.assertFormula(lastItp);
ctxA.assertFormulas(groups.get(i));

lastItp = interpolate(ctxA, ctxB);
builder.add(creator.encapsulateBoolean(lastItp));

ctxA.pop();
ctxB.pop();
}
}

return builder.build();
}
return itps;
}

@Override
Expand Down
10 changes: 8 additions & 2 deletions src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -497,7 +497,11 @@ public <T> void sequentialBVInterpolation() throws SolverException, InterruptedE

List<BooleanFormula> itps1 = stack.getSeqInterpolants0(ImmutableList.of(TA, TB, TC, TD));
List<BooleanFormula> itps2 = stack.getSeqInterpolants0(ImmutableList.of(TD, TC, TB, TA));
List<BooleanFormula> itps3 = stack.getSeqInterpolants0(ImmutableList.of(TA, TC, TB, TD));
List<BooleanFormula> itps3 = ImmutableList.of();
if (solver != Solvers.YICES2) {
// FIXME Yices fails to terminate for this example
itps3 = stack.getSeqInterpolants0(ImmutableList.of(TA, TC, TB, TD));
}
List<BooleanFormula> itps4 =
stack.getSeqInterpolants0(ImmutableList.of(TA, TA, TA, TB, TC, TD, TD));
List<BooleanFormula> itps5 =
Expand All @@ -509,7 +513,9 @@ public <T> void sequentialBVInterpolation() throws SolverException, InterruptedE

checkItpSequence(ImmutableList.of(A, B, C, D), itps1);
checkItpSequence(ImmutableList.of(D, C, B, A), itps2);
checkItpSequence(ImmutableList.of(A, C, B, D), itps3);
if (solver != Solvers.YICES2) {
checkItpSequence(ImmutableList.of(A, C, B, D), itps3);
}
checkItpSequence(ImmutableList.of(A, A, A, B, C, D, D), itps4);
checkItpSequence(ImmutableList.of(A, A, B, C, D, A, D), itps5);
checkItpSequence(ImmutableList.of(B, C, D, A, A, A, D), itps6);
Expand Down
Loading