From 4d338e4c45caefee34f08c4294127a20f96e7ff6 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 7 Mar 2022 14:11:55 -0800 Subject: [PATCH] Update documentation of `Solver::getUnsatCore()` (#8239) Fixes https://github.com/cvc5/cvc5-projects/issues/308. This commit adds documentation for the differences between `Solver::getUnsatCore()` and SMT-LIB's `(get-unsat-core)`. --- src/api/cpp/cvc5.h | 7 +++++++ src/api/java/io/github/cvc5/api/Solver.java | 7 ++++++- src/api/python/cvc5.pxi | 9 ++++++++- test/unit/api/cpp/solver_black.cpp | 19 ++++++++++++++++--- 4 files changed, 37 insertions(+), 5 deletions(-) diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index fa8552458..6b614f49a 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4149,6 +4149,13 @@ class CVC5_EXPORT Solver * * Requires to enable option * :ref:`produce-unsat-cores `. + * + * .. note:: + * In contrast to SMT-LIB, the API does not distinguish between named and + * unnamed assertions when producing an unsatisfiable core. Additionally, + * the API allows this option to be called after a check with assumptions. + * A subset of those assumptions may be included in the unsatisfiable core + * returned by this method. * \endverbatim * * @return a set of terms representing the unsatisfiable core diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index f1ad0cea6..762eb4c79 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -1865,9 +1865,14 @@ public class Solver implements IPointer, AutoCloseable * Get the unsatisfiable core. * SMT-LIB: * {@code - * ( get-unsat-core ) + * (get-unsat-core) * } * Requires to enable option 'produce-unsat-cores'. + * @apiNote In contrast to SMT-LIB, the API does not distinguish between + * named and unnamed assertions when producing an unsatisfiable + * core. Additionally, the API allows this option to be called after + * a check with assumptions. A subset of those assumptions may be + * included in the unsatisfiable core returned by this method. * @return a set of terms representing the unsatisfiable core */ public Term[] getUnsatCore() diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 12eec9b1a..f0a2d3617 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2035,10 +2035,17 @@ cdef class Solver: .. code-block:: smtlib - ( get-unsat-core ) + (get-unsat-core) Requires to enable option :ref:`produce-unsat-cores `. + .. note:: + In contrast to SMT-LIB, the API does not distinguish between named and + unnamed assertions when producing an unsatisfiable core. Additionally, + the API allows this option to be called after a check with assumptions. + A subset of those assumptions may be included in the unsatisfiable core + returned by this method. + :return: a set of terms representing the unsatisfiable core """ core = [] diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 0d92b3b54..70ea31883 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -1635,7 +1635,7 @@ TEST_F(TestApiBlackSolver, getUnsatCoreAndProof) Sort boolSort = d_solver.getBooleanSort(); Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort); Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort); - std::vector unsat_core; + std::vector uc; Term x = d_solver.mkConst(uSort, "x"); Term y = d_solver.mkConst(uSort, "y"); @@ -1655,12 +1655,13 @@ TEST_F(TestApiBlackSolver, getUnsatCoreAndProof) d_solver.assertFormula(p_f_y.notTerm()); ASSERT_TRUE(d_solver.checkSat().isUnsat()); - ASSERT_NO_THROW(unsat_core = d_solver.getUnsatCore()); + ASSERT_NO_THROW(uc = d_solver.getUnsatCore()); + ASSERT_FALSE(uc.empty()); ASSERT_NO_THROW(d_solver.getProof()); d_solver.resetAssertions(); - for (const auto& t : unsat_core) + for (const auto& t : uc) { d_solver.assertFormula(t); } @@ -2826,6 +2827,18 @@ TEST_F(TestApiBlackSolver, issue5893) ASSERT_NO_FATAL_FAILURE(distinct.getOp()); } +TEST_F(TestApiBlackSolver, proj_issue308) +{ + Solver slv; + slv.setOption("check-proofs", "true"); + Sort s1 = slv.getBooleanSort(); + Term t1 = slv.mkConst(s1, "_x0"); + Term t2 = slv.mkTerm(Kind::XOR, t1, t1); + slv.checkSatAssuming({t2}); + auto unsat_core = slv.getUnsatCore(); + ASSERT_FALSE(unsat_core.empty()); +} + TEST_F(TestApiBlackSolver, proj_issue373) { Sort s1 = d_solver.getRealSort(); -- 2.30.2