Add support for UNSAT core to the OpenSMT backend

lib/ivy.xml

@@ -160,7 +160,7 @@ SPDX-License-Identifier: Apache-2.0
         <!-- Solver Binaries -->
         <dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.10" conf="runtime-mathsat->solver-mathsat" />
         <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.12.5" conf="runtime-z3->solver-z3; contrib->sources,javadoc" />
-        <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.5.2-g7f502169" conf="runtime-opensmt->solver-opensmt; contrib->sources,javadoc" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.6.0-g48b72153" conf="runtime-opensmt->solver-opensmt; contrib->sources,javadoc" />
         <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.1-sosy0" conf="runtime-optimathsat->solver-optimathsat" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="1.0.5-g4cb2ab9eb" conf="runtime-cvc5->solver-cvc5" />

lib/native/source/opensmt/api.patch

@@ -131,15 +131,15 @@ diff --git a/src/common/FastRational.h b/src/common/FastRational.h
 index a3f4bb1c..9fc7ac3d 100644
 --- a/src/common/FastRational.h
 +++ b/src/common/FastRational.h
-@@ -13,6 +13,7 @@ Copyright (c) 2008, 2009 Centre national de la recherche scientifique (CNRS)
- #include "Vec.h"
+@@ -14,6 +14,7 @@ Copyright (c) 2008, 2009 Centre national de la recherche scientifique (CNRS)
  #include <stack>
  #include <vector>
+ #include <optional>
 +#include <mutex>
 
  typedef int32_t  word;
  typedef uint32_t uword;
-@@ -71,6 +72,7 @@ class FastRational
+@@ -72,6 +73,7 @@ class FastRational
  {
      class mpqPool
      {
@@ -195,16 +195,15 @@ index b90430c2..c4b34fc4 100644
      return mkUninterpFun(sym, std::move(terms));
  }
 
-@@ -1455,6 +1466,9 @@ Logic::collectStats(PTRef root, int& n_of_conn, int& n_of_eq, int& n_of_uf, int&
-
- PTRef Logic::conjoinExtras(PTRef root) { return root; }
+@@ -1445,6 +1456,8 @@ Logic::collectStats(PTRef root, int& n_of_conn, int& n_of_eq, int& n_of_uf, int&
+     }
+ }
 
 +Sort const&       Logic::getSortDefinition (SRef s)     const { return sort_store[s]; }
 +SortSymbol const& Logic::getSortSymbol     (SSymRef ss) const { return sort_store[ss]; }
-+
+ 
  // Fetching sorts
  SRef        Logic::getSortRef    (const PTRef tr)        const { return getSortRef(getPterm(tr).symb()); }
- SRef        Logic::getSortRef    (const SymRef sr)       const { return getSym(sr).rsort(); }
 diff --git a/src/logics/Logic.h b/src/logics/Logic.h
 index 73513cd1..888f970c 100644
 --- a/src/logics/Logic.h

lib/native/source/opensmt/swig/opensmt/InterpolationContext.i

@@ -6,7 +6,7 @@
 //
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-%ignore InterpolationContext::InterpolationContext (SMTConfig &c, Theory &th, TermMapper &termMapper, Proof const &t, PartitionManager &pmanager);
+%ignore InterpolationContext::InterpolationContext (SMTConfig &c, Theory &th, TermMapper &termMapper, ResolutionProof const &t, PartitionManager &pmanager);
 %ignore InterpolationContext::printProofDotty ();
 %ignore InterpolationContext::getInterpolants (const std::vector< vec< int > > &partitions, vec< PTRef > &interpolants);
 %ignore InterpolationContext::getSingleInterpolant (vec< PTRef > &interpolants, const ipartitions_t &A_mask);
@@ -37,7 +37,7 @@
     for (int i = 0; i < interpolants.size(); i++)
       result.emplace_back(interpolants[i]);
     return result;
-  }
  }
+}
 
 %include "include/opensmt/InterpolationContext.h"

lib/native/source/opensmt/swig/opensmt/MainSolver.i

@@ -61,17 +61,29 @@
 %ignore MainSolver::getSMTSolver();
 %ignore MainSolver::getSMTSolver() const;
 %ignore MainSolver::getTHandler();
+%ignore MainSolver::getTHandler () const;
 %ignore MainSolver::getLogic();
 %ignore MainSolver::getTheory();
 %ignore MainSolver::getTheory() const;
 %ignore MainSolver::getPartitionManager();
 %ignore MainSolver::insertFormula(PTRef, char**);
 %ignore MainSolver::initialize();
 %ignore MainSolver::simplifyFormulas();
+%ignore MainSolver::getUnsatCore() const;
 %ignore MainSolver::printFramesAsQuery() const;
 %ignore MainSolver::solverEmpty() const;
 %ignore MainSolver::writeSolverState_smtlib2(const char*, char**) const;
 %ignore MainSolver::getTermValue(PTRef) const;
 %ignore MainSolver::createTheory(Logic&, SMTConfig&);
+%extend MainSolver {
+  %newobject getUnsatCore();
+  std::vector<PTRef> getUnsatCore() {
+    std::vector<PTRef> result;
+    for (PTRef r : $self->getUnsatCore()) {
+      result.emplace_back(r);
+    }
+    return result;
+  }
+}
 
 %include "include/opensmt/MainSolver.h"

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java

@@ -65,9 +65,17 @@ protected OpenSmtAbstractProver(
   }
 
   protected static SMTConfig getConfigInstance(
-      OpenSMTOptions pSolverOptions, boolean interpolation) {
+      Set<ProverOptions> pOptions, OpenSMTOptions pSolverOptions, boolean interpolation) {
     SMTConfig config = new SMTConfig();
     config.setOption(":random-seed", new SMTOption(pSolverOptions.randomSeed));
+    config.setOption(
+        ":produce-models",
+        new SMTOption(
+            pOptions.contains(ProverOptions.GENERATE_MODELS)
+                || pOptions.contains(ProverOptions.GENERATE_ALL_SAT)));
+    config.setOption(
+        ":produce-unsat-cores",
+        new SMTOption(pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE)));
     config.setOption(":produce-interpolants", new SMTOption(interpolation));
     if (interpolation) {
       config.setOption(":interpolation-bool-algorithm", new SMTOption(pSolverOptions.algBool));
@@ -255,19 +263,27 @@ public boolean isUnsat() throws InterruptedException, SolverException {
 
   @Override
   public List<BooleanFormula> getUnsatCore() {
-    throw new UnsupportedOperationException("OpenSMT does not support unsat core.");
+    Preconditions.checkState(!closed);
+    checkGenerateUnsatCores();
+    Preconditions.checkState(!changedSinceLastSatQuery);
+
+    ImmutableList.Builder<BooleanFormula> result = ImmutableList.builder();
+    for (PTRef r : osmtSolver.getUnsatCore()) {
+      result.add(creator.encapsulateBoolean(r));
+    }
+    return result.build();
   }
 
   @Override
   public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
       throws SolverException, InterruptedException {
-    throw new UnsupportedOperationException("OpenSMT does not support unsat core.");
+    throw new UnsupportedOperationException("OpenSMT does not support solving with assumptions.");
   }
 
   @Override
   public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
       Collection<BooleanFormula> pAssumptions) throws SolverException, InterruptedException {
-    throw new UnsupportedOperationException("OpenSMT does not support unsat core.");
+    throw new UnsupportedOperationException("OpenSMT does not support solving with assumptions.");
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtInterpolatingProver.java

@@ -47,7 +47,7 @@ class OpenSmtInterpolatingProver extends OpenSmtAbstractProver<Integer>
         pFormulaCreator,
         pMgr,
         pShutdownNotifier,
-        getConfigInstance(pSolverOptions, true),
+        getConfigInstance(pOptions, pSolverOptions, true),
         pOptions);
     trackedConstraints.push(0); // initialize first level
   }

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtNativeAPITest.java

@@ -423,4 +423,29 @@ public void testAbort() {
     sstat r = mainSolver.check();
     assertThat(r).isEqualTo(sstat.Undef());
   }
+
+  @Test
+  public void testUnsatCore() {
+    // Adapted from test_UnsatCore.cc
+    Logic logic = LogicFactory.getInstance(Logic_t.QF_UF);
+
+    PTRef b1 = logic.mkBoolVar("b1");
+    PTRef b2 = logic.mkBoolVar("b2");
+    PTRef nb1 = logic.mkNot(b1);
+
+    SMTConfig config = new SMTConfig();
+    config.setOption(":produce-unsat-cores", new SMTOption(true));
+
+    MainSolver mainSolver = new MainSolver(logic, config, "opensmt-test");
+
+    mainSolver.insertFormula(b1);
+    mainSolver.insertFormula(b2);
+    mainSolver.insertFormula(nb1);
+
+    sstat r = mainSolver.check();
+    assertThat(r).isEqualTo(sstat.False());
+
+    VectorPTRef core = mainSolver.getUnsatCore();
+    assertThat(core).containsExactly(b1, nb1);
+  }
 }

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtTheoremProver.java

@@ -28,7 +28,7 @@ class OpenSmtTheoremProver extends OpenSmtAbstractProver<Void> implements Prover
         pFormulaCreator,
         pMgr,
         pShutdownNotifier,
-        getConfigInstance(pSolverOptions, false),
+        getConfigInstance(pOptions, pSolverOptions, false),
         pOptions);
   }
 

src/org/sosy_lab/java_smt/test/BooleanFormulaSubjectTest.java

@@ -66,12 +66,7 @@ public void testIsSatisfiableYes() throws SolverException, InterruptedException
 
   @Test
   public void testIsSatisfiableNo() {
-    // INFO: OpenSMT does not support unsat core
-    assume()
-        .withMessage("Solver does not support unsat core generation in a usable way")
-        .that(solverToUse())
-        .isNoneOf(Solvers.BOOLECTOR, Solvers.OPENSMT);
-
+    requireUnsatCore();
     AssertionError failure =
         expectFailure(whenTesting -> whenTesting.that(contradiction).isSatisfiable());
     assertThat(failure).factValue("which has unsat core").isNotEmpty();

src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java

@@ -15,6 +15,7 @@
 import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.CVC4;
 import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.CVC5;
 import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.MATHSAT5;
+import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.OPENSMT;
 import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.PRINCESS;
 import static org.sosy_lab.java_smt.api.SolverContext.ProverOptions.GENERATE_UNSAT_CORE;
 import static org.sosy_lab.java_smt.api.SolverContext.ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS;
@@ -119,7 +120,7 @@ public void unsatCoreWithAssumptionsNullTest() {
         .withMessage(
             "Solver %s does not support unsat core generation over assumptions", solverToUse())
         .that(solverToUse())
-        .isNoneOf(PRINCESS, CVC4, CVC5);
+        .isNoneOf(PRINCESS, CVC4, CVC5, OPENSMT);
 
     try (ProverEnvironment pe =
         context.newProverEnvironment(GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) {
@@ -134,7 +135,7 @@ public void unsatCoreWithAssumptionsTest() throws SolverException, InterruptedEx
         .withMessage(
             "Solver %s does not support unsat core generation over assumptions", solverToUse())
         .that(solverToUse())
-        .isNoneOf(PRINCESS, CVC4, CVC5);
+        .isNoneOf(PRINCESS, CVC4, CVC5, OPENSMT);
     try (ProverEnvironment pe =
         context.newProverEnvironment(GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)) {
       pe.push();

src/org/sosy_lab/java_smt/test/SolverBasedTest0.java

@@ -332,7 +332,7 @@ protected void requireUnsatCore() {
     assume()
         .withMessage("Solver %s does not support unsat core generation", solverToUse())
         .that(solverToUse())
-        .isNoneOf(Solvers.BOOLECTOR, Solvers.OPENSMT);
+        .isNotEqualTo(Solvers.BOOLECTOR);
   }
 
   protected void requireUnsatCoreOverAssumptions() {