From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 20 Oct 2021 19:48:11 +0000 (-0500)
Subject: Check whether abduct option is enabled (#7418)
X-Git-Tag: cvc5-1.0.0~1038
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=221f8b49844a0d65739393df9327de0338154ff2;p=cvc5.git

Check whether abduct option is enabled (#7418)

This addresses one of the issues related to #6605.
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index f6a1eed17..2bc101bec 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7205,7 +7205,7 @@ std::string Solver::getProof(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(d_slv->getOptions().smt.produceProofs)
-      << "Cannot get proof explicitly enabled (try --produce-proofs)";
+      << "Cannot get proof unless proofs are enabled (try --produce-proofs)";
   CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT)
       << "Cannot get proof unless in unsat mode.";
   return d_slv->getProof();
@@ -7456,6 +7456,8 @@ bool Solver::getAbduct(const Term& conj, Term& output) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
+  CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts)
+      << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
   //////// all checks before this line
   Node result;
   bool success = d_slv->getAbduct(*conj.d_node, result);
@@ -7472,6 +7474,8 @@ bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
+  CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts)
+      << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
   //////// all checks before this line
   Node result;
   bool success =
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index f90018101..d5137393e 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1225,6 +1225,23 @@ TEST_F(TestApiBlackSolver, getAbduct)
   ASSERT_EQ(output2, truen);
 }
 
+TEST_F(TestApiBlackSolver, getAbduct2)
+{
+  d_solver.setLogic("QF_LIA");
+  d_solver.setOption("incremental", "false");
+  Sort intSort = d_solver.getIntegerSort();
+  Term zero = d_solver.mkInteger(0);
+  Term x = d_solver.mkConst(intSort, "x");
+  Term y = d_solver.mkConst(intSort, "y");
+  // Assumptions for abduction: x > 0
+  d_solver.assertFormula(d_solver.mkTerm(GT, x, zero));
+  // Conjecture for abduction: y > 0
+  Term conj = d_solver.mkTerm(GT, y, zero);
+  Term output;
+  // Fails due to option not set
+  ASSERT_THROW(d_solver.getAbduct(conj, output), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackSolver, getInterpolant)
 {
   d_solver.setLogic("QF_LIA");