diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaInterpolatingProver.java index 65099084ec..77c3ac2c07 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaInterpolatingProver.java @@ -13,6 +13,7 @@ import static com.google.common.base.Preconditions.checkState; import com.google.common.collect.FluentIterable; +import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; import java.util.Collection; import java.util.List; @@ -25,12 +26,18 @@ import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Option; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Options; +import org.sosy_lab.java_smt.solvers.bitwuzla.api.Term; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Vector_Term; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Vector_Vector_Term; class BitwuzlaInterpolatingProver extends BitwuzlaAbstractProver implements InterpolatingProverEnvironment { + private static final ImmutableSet ACCEPTED_INTERPOLATION_ERROR_MESSAGES = + ImmutableSet.of( + "interpolation queries with lemmas that use fresh variables not supported", + "interpolation queries with mixed lemmas not supported"); + BitwuzlaInterpolatingProver( BitwuzlaFormulaManager pManager, BitwuzlaFormulaCreator pCreator, @@ -55,11 +62,25 @@ private static Options enableInterpolation(Options pSolverOptions) { @Override public BooleanFormula getInterpolant(Collection formulasOfA) throws SolverException, InterruptedException { - return creator.encapsulateBoolean( - formulasOfA.isEmpty() - ? creator.getEnv().mk_true() - : env.get_interpolant( - new Vector_Term(FluentIterable.from(formulasOfA).transform(stack.peek()::get)))); + Term interpolant; + if (formulasOfA.isEmpty()) { + interpolant = creator.getEnv().mk_true(); + } else { + Vector_Term itpVector = + new Vector_Term(FluentIterable.from(formulasOfA).transform(stack.peek()::get)); + try { + interpolant = env.get_interpolant(itpVector); + + } catch (IllegalArgumentException e) { + // TODO Starting with Bitwuzla 0.9.2 we could catch the Unsupported exception in C++ + if (ACCEPTED_INTERPOLATION_ERROR_MESSAGES.contains(e.getMessage())) { + throw new SolverException(e.getMessage()); + } else { + throw e; + } + } + } + return creator.encapsulateBoolean(interpolant); } @Override @@ -72,7 +93,16 @@ public List getSeqInterpolants( FluentIterable.from(partitionedFormulas) .transform( p -> new Vector_Term(FluentIterable.from(p).transform(stack.peek()::get)))); - Vector_Term itps = env.get_interpolants(partitions); + Vector_Term itps; + try { + itps = env.get_interpolants(partitions); + } catch (IllegalArgumentException e) { + if (ACCEPTED_INTERPOLATION_ERROR_MESSAGES.contains(e.getMessage())) { + throw new SolverException(e.getMessage()); + } else { + throw e; + } + } checkState( creator.getEnv().mk_false().equals(Iterables.getLast(itps)), "the last interpolant should be false"); diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java index 16b33bb5ec..cfa0eeebcb 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -117,7 +117,7 @@ protected T addConstraintImpl(BooleanFormula pF) throws InterruptedException { @SuppressWarnings("resource") @Override - protected Model getModelImpl() { + protected Model getModelImpl() throws SolverException { return registerEvaluator( new OpenSmtModel( this, creator, Collections2.transform(getAssertedFormulas(), creator::extractInfo))); diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtInterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtInterpolatingProver.java index 98ed23d185..96d66cc0a2 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtInterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtInterpolatingProver.java @@ -19,6 +19,7 @@ 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; import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtSolverContext.OpenSMTOptions; import org.sosy_lab.java_smt.solvers.opensmt.api.PTRef; import org.sosy_lab.java_smt.solvers.opensmt.api.VectorInt; @@ -68,15 +69,29 @@ protected void popImpl() { super.popImpl(); } + /** + * Check if OpenSMT supports interpolation for the current logic, and throw an {@link + * SolverException} otherwise. + */ + private void checkLogicSupportInterpolation() throws SolverException { + if (!creator.getLogic().doesLogicSupportInterpolation()) { + throw new SolverException( + "OpenSMT does not support interpolation for the specified logic %s." + .formatted(creator.getLogic())); + } + } + @Override - public BooleanFormula getInterpolant(Collection formulasOfA) { + public BooleanFormula getInterpolant(Collection formulasOfA) throws SolverException { + checkLogicSupportInterpolation(); return creator.encapsulateBoolean( osmtSolver.getInterpolationContext().getSingleInterpolant(new VectorInt(formulasOfA))); } @Override public List getSeqInterpolants( - List> partitionedFormulas) { + List> partitionedFormulas) throws SolverException { + checkLogicSupportInterpolation(); VectorVectorInt partitions = new VectorVectorInt(); for (int i = 1; i < partitionedFormulas.size(); i++) { VectorInt prefix = new VectorInt(); diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtModel.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtModel.java index 890637d847..d5f316c27a 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtModel.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtModel.java @@ -18,6 +18,7 @@ import java.util.LinkedHashMap; import java.util.List; import java.util.Map; +import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.basicimpl.AbstractModel; import org.sosy_lab.java_smt.solvers.opensmt.api.Logic; import org.sosy_lab.java_smt.solvers.opensmt.api.Model; @@ -38,7 +39,8 @@ class OpenSmtModel extends AbstractModel { OpenSmtModel( OpenSmtAbstractProver pProver, OpenSmtFormulaCreator pCreator, - Collection pAssertedTerms) { + Collection pAssertedTerms) + throws SolverException { super(pProver, pCreator); osmtLogic = pCreator.getEnv(); @@ -51,7 +53,7 @@ class OpenSmtModel extends AbstractModel { } private ImmutableList generateModel( - OpenSmtFormulaCreator pCreator, Collection pAssertedTerms) { + OpenSmtFormulaCreator pCreator, Collection pAssertedTerms) throws SolverException { Map userDeclarations = new LinkedHashMap<>(); for (PTRef asserted : pAssertedTerms) { userDeclarations.putAll(creator.extractVariablesAndUFs(asserted, true)); @@ -69,8 +71,9 @@ private ImmutableList generateModel( if (osmtLogic.isArraySort(sort)) { // INFO: Disable model generation if arrays are used // https://github.com/usi-verification-and-security/opensmt/issues/630 - throw new UnsupportedOperationException( - "OpenSMT does not support model generation when arrays are used"); + throw new SolverException( + "OpenSMT2 can not return satisfiable assignments for arrays. To avoid wrong" + + "interpretation, we disallow model export for queries including arrays."); } if (numArgs == 0) { diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java index 89b2a895f3..1774e5f4a6 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java @@ -19,6 +19,7 @@ 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; @@ -33,6 +34,12 @@ class Yices2InterpolatingProver extends Yices2AbstractProver implements InterpolatingProverEnvironment { + + private static final ImmutableSet ACCEPTED_INTERPOLATION_ERROR_MESSAGES = + ImmutableSet.of( + "mcsat: unsupported theory\n", + "mcsat: assumption variable has a type that mcsat cannot decide on\n"); + Yices2InterpolatingProver( Yices2FormulaCreator creator, Set pOptions, @@ -61,7 +68,7 @@ public BooleanFormula getInterpolant(Collection formulasOfA) } private int interpolate(Collection setA, Collection setB) - throws InterruptedException { + throws InterruptedException, SolverException { try (var ctxA = newContext("mcsat"); var ctxB = newContext("mcsat")) { @@ -72,12 +79,21 @@ private int interpolate(Collection setA, Collection setB) // TODO How to abort this? // For now, let's just check before and after the call: shutdownNotifier.shutdownIfNecessary(); - var status = context.check(DEFAULT_PARAMS, false); + Status status; + try { + status = context.check(DEFAULT_PARAMS, false); + } catch (YicesException e) { + if (ACCEPTED_INTERPOLATION_ERROR_MESSAGES.contains(e.getMessage())) { + throw new SolverException(e.getMessage().stripTrailing()); + } else { + throw e; + } + } shutdownNotifier.shutdownIfNecessary(); if (status == Status.UNSAT) { return context.getInterpolant(); } else { - throw new IllegalArgumentException("Solver state must be unsat"); + throw new IllegalStateException("Solver state must be unsat"); } } }