From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 9 May 2022 17:05:28 +0000 (-0500)
Subject: Add unit tests for getInstantiations (#8741)
X-Git-Tag: cvc5-1.0.1~154
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9058998bfeb00200bf32c74d23efa60ee08a50ac;p=cvc5.git

Add unit tests for getInstantiations (#8741)
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d7e85c4d3..a69d1f641 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7288,6 +7288,12 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
 std::string Solver::getInstantiations() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == internal::SmtMode::UNSAT
+                             || d_slv->getSmtMode() == internal::SmtMode::SAT
+                             || d_slv->getSmtMode()
+                                    == internal::SmtMode::SAT_UNKNOWN)
+      << "Cannot get instantiations unless after a UNSAT, SAT or UNKNOWN "
+         "response.";
   //////// all checks before this line
   std::stringstream ss;
   d_slv->printInstantiations(ss);
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 577c8ad4c..b8d05446d 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -2340,6 +2340,24 @@ TEST_F(TestApiBlackSolver, blockModelValues5)
   ASSERT_NO_THROW(d_solver.blockModelValues({x}));
 }
 
+TEST_F(TestApiBlackSolver, getInstantiations)
+{
+  Sort iSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Term p = d_solver.declareFun("p", {iSort}, boolSort);
+  Term x = d_solver.mkVar(iSort, "x");
+  Term bvl = d_solver.mkTerm(VARIABLE_LIST, {x});
+  Term app = d_solver.mkTerm(APPLY_UF, {p, x});
+  Term q = d_solver.mkTerm(FORALL, {bvl, app});
+  d_solver.assertFormula(q);
+  Term five = d_solver.mkInteger(5);
+  Term app2 = d_solver.mkTerm(NOT, {d_solver.mkTerm(APPLY_UF, {p, five})});
+  d_solver.assertFormula(app2);
+  ASSERT_THROW(d_solver.getInstantiations(), CVC5ApiException);
+  d_solver.checkSat();
+  ASSERT_NO_THROW(d_solver.getInstantiations());
+}
+
 TEST_F(TestApiBlackSolver, setInfo)
 {
   ASSERT_THROW(d_solver.setInfo("cvc5-lagic", "QF_BV"), CVC5ApiException);
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index f967efe30..0bcf30781 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -2340,6 +2340,25 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.blockModelValues(new Term[] {x}));
   }
 
+  @Test
+  void getInstantiations() throws CVC5ApiException
+  {
+    Sort iSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Term p = d_solver.declareFun("p", new Sort[] {iSort}, boolSort);
+    Term x = d_solver.mkVar(iSort, "x");
+    Term bvl = d_solver.mkTerm(VARIABLE_LIST, new Term[] {x});
+    Term app = d_solver.mkTerm(APPLY_UF, new Term[] {p, x});
+    Term q = d_solver.mkTerm(FORALL, new Term[] {bvl, app});
+    d_solver.assertFormula(q);
+    Term five = d_solver.mkInteger(5);
+    Term app2 = d_solver.mkTerm(NOT, new Term[] {d_solver.mkTerm(APPLY_UF, new Term[] {p, five})});
+    d_solver.assertFormula(app2);
+    assertThrows(CVC5ApiException.class, () -> d_solver.getInstantiations());
+    d_solver.checkSat();
+    assertDoesNotThrow(() -> d_solver.getInstantiations());
+  }
+
   @Test
   void setInfo() throws CVC5ApiException
   {
diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 3939f2d09..6705a940f 100644
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -1641,6 +1641,23 @@ def test_block_model_values5(solver):
     solver.checkSat()
     solver.blockModelValues([x])
 
+def getInstantiations():
+    iSort = solver.getIntegerSort()
+    boolSort = solver.getBooleanSort()
+    p = solver.declareFun("p", [iSort], boolSort)
+    x = solver.mkVar(iSort, "x")
+    bvl = solver.mkTerm(Kind.VARIABLE_LIST, [x])
+    app = solver.mkTerm(Kind.APPLY_UF, [p, x])
+    q = solver.mkTerm(Kind.FORALL, [bvl, app]);
+    solver.assertFormula(q)
+    five = solver.mkInteger(5)
+    app2 = solver.mkTerm(Kind.NOT, [solver.mkTerm(Kind.APPLY_UF, [p, five])])
+    solver.assertFormula(app2)
+    with pytest.raises(RuntimeError):
+        solver.getInstantiations()
+    solver.checkSat()
+    solver.getInstantiations()
+
 def test_get_statistics(solver):
     intSort = solver.getIntegerSort()
     x = solver.mkConst(intSort, "x")