Add test coverage for almost everything from the Python API (#8720)

This PR adds tests for almost everything that is not yet covered by the python API tests.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 0c6167963c621c0454ec1854d305dc12a3f70315..d7e85c4d36a2f73b5bb35a135ed1640bc637a868 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -3429,6 +3429,7 @@ bool DatatypeConstructorDecl::isNull() const
 std::string DatatypeConstructorDecl::toString() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
   //////// all checks before this line
   std::stringstream ss;
   ss << *d_ctor;

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 2e6dfa49339cf4589a4b35526c79be771ac5c695..8f6bd3b24bb316aef6074f67a2289ec3151ee6b8 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -360,6 +360,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         void addAnyConstant(Term ntSymbol) except +
         void addAnyVariable(Term ntSymbol) except +
         void addRules(Term ntSymbol, vector[Term] rules) except +
+        string toString() except +
 
     cdef cppclass Sort:
         Sort() except +
@@ -400,6 +401,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         Datatype getDatatype() except +
         Sort instantiate(const vector[Sort]& params) except +
         vector[Sort] getInstantiatedParameters() except +
+        Sort substitute(const Sort & es, const Sort & reps) except +
         Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except +
         size_t getDatatypeConstructorArity() except +
         vector[Sort] getDatatypeConstructorDomainSorts() except +
@@ -465,6 +467,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         uint64_t getId() except +
         Kind getKind() except +
         Sort getSort() except +
+        Term substitute(const Term & es, const Term & reps) except +
         Term substitute(const vector[Term] & es, const vector[Term] & reps) except +
         bint hasOp() except +
         Op getOp() except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 5af31b074f3a2b35761bc61fe12798d7b3a3b32e..b46b5f98f76b3728dc2d5c2da0cf1a08e7b409ee 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -653,6 +653,9 @@ cdef class Grammar:
         self.solver = solver
         self.cgrammar = c_Grammar()
 
+    def __str__(self):
+        return self.cgrammar.toString().decode()
+
     def addRule(self, Term ntSymbol, Term rule):
         """
             Add ``rule`` to the set of rules corresponding to ``ntSymbol``.
@@ -3241,8 +3244,8 @@ cdef class Sort:
         cdef vector[c_Sort] ces
         cdef vector[c_Sort] creplacements
 
-        # normalize the input parameters to be lists
         if isinstance(sort_or_list_1, list):
+            # call the API substitute method with lists
             assert isinstance(sort_or_list_2, list)
             es = sort_or_list_1
             replacements = sort_or_list_2
@@ -3255,14 +3258,11 @@ cdef class Sort:
             for e, r in zip(es, replacements):
                 ces.push_back((<Sort?> e).csort)
                 creplacements.push_back((<Sort?> r).csort)
-
+            sort.csort = self.csort.substitute(ces, creplacements)
         else:
-            # add the single elements to the vectors
-            ces.push_back((<Sort?> sort_or_list_1).csort)
-            creplacements.push_back((<Sort?> sort_or_list_2).csort)
+            # call the API substitute method with single sorts
+            sort.csort = self.csort.substitute((<Sort?> sort_or_list_1).csort, (<Sort?> sort_or_list_2).csort)
 
-        # call the API substitute method with lists
-        sort.csort = self.csort.substitute(ces, creplacements)
         return sort
 
 
@@ -3599,8 +3599,8 @@ cdef class Term:
         cdef vector[c_Term] ces
         cdef vector[c_Term] creplacements
 
-        # normalize the input parameters to be lists
         if isinstance(term_or_list_1, list):
+            # call the API substitute method with lists
             assert isinstance(term_or_list_2, list)
             es = term_or_list_1
             replacements = term_or_list_2
@@ -3612,14 +3612,11 @@ cdef class Term:
             for e, r in zip(es, replacements):
                 ces.push_back((<Term?> e).cterm)
                 creplacements.push_back((<Term?> r).cterm)
-
+            term.cterm = self.cterm.substitute(ces, creplacements)
         else:
-            # add the single elements to the vectors
-            ces.push_back((<Term?> term_or_list_1).cterm)
-            creplacements.push_back((<Term?> term_or_list_2).cterm)
+            # call the API substitute method with single terms
+            term.cterm = self.cterm.substitute((<Term?> term_or_list_1).cterm, (<Term?> term_or_list_2).cterm)
 
-        # call the API substitute method with lists
-        term.cterm = self.cterm.substitute(ces, creplacements)
         return term
 
     def hasOp(self):

diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py
index 9caedd3f82ec7b7ce2436eccee905d4b747a7c92..1b6c20bdbe5f2ef5ecd4b11e4b524f05eb3813ea 100644 (file)
--- a/test/unit/api/python/test_datatype_api.py
+++ b/test/unit/api/python/test_datatype_api.py
@@ -58,14 +58,16 @@ def test_is_null(solver):
   assert sel.isNull()
 
   # changing the objects to be non-null
-  dtypeSpec = solver.mkDatatypeDecl("list");
-  cons = solver.mkDatatypeConstructorDecl("cons");
-  cons.addSelector("head", solver.getIntegerSort());
-  dtypeSpec.addConstructor(cons);
+  dtypeSpec = solver.mkDatatypeDecl("list")
+  cons = solver.mkDatatypeConstructorDecl("cons")
+  cons.addSelector("head", solver.getIntegerSort())
+  dtypeSpec.addConstructor(cons)
+  assert dtypeSpec.getNumConstructors() == 1
+  assert not dtypeSpec.isParametric()
   listSort = solver.mkDatatypeSort(dtypeSpec)
-  d = listSort.getDatatype();
-  consConstr = d[0];
-  sel = consConstr[0];
+  d = listSort.getDatatype()
+  consConstr = d[0]
+  sel = consConstr[0]
 
   # verifying that the new objects are non-null
   assert not dtypeSpec.isNull()

diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py
index 464f5164857eca0c7e745b831d021108e923b74a..53f3f55fcb02853185d3c9db63d8197a26164e4d 100644 (file)
--- a/test/unit/api/python/test_grammar.py
+++ b/test/unit/api/python/test_grammar.py
@@ -24,6 +24,16 @@ def solver():
     return cvc5.Solver()
 
 
+def test_to_string(solver):
+    solver.setOption("sygus", "true")
+    boolean = solver.getBooleanSort()
+    start = solver.mkVar(boolean)
+    nts = solver.mkVar(boolean)
+    g = solver.mkGrammar([nts], [start])
+    g.addRule(start, solver.mkBoolean(False))
+    str(g)
+
+
 def test_add_rule(solver):
     solver.setOption("sygus", "true")
     boolean = solver.getBooleanSort()

diff --git a/test/unit/api/python/test_uncovered.cpp b/test/unit/api/python/test_uncovered.cpp
index eaea0a5e2ca2968a90aa7f528427ba3f7311fb7c..fe53cf4edc6397b09901959f26c2188908c66385 100644 (file)
--- a/test/unit/api/python/test_uncovered.cpp
+++ b/test/unit/api/python/test_uncovered.cpp
@@ -44,9 +44,11 @@ TEST_F(TestApiBlackUncovered, streaming_operators)
 {
   std::stringstream ss;
   ss << cvc5::modes::LearnedLitType::PREPROCESS;
+  ss << cvc5::UnknownExplanation::UNKNOWN_REASON;
   ss << cvc5::Result();
   ss << cvc5::Op();
   ss << cvc5::SynthResult();
+  ss << cvc5::Grammar();
 
   Sort intsort = d_solver.getIntegerSort();
   Term x = d_solver.mkConst(intsort, "x");
@@ -56,6 +58,92 @@ TEST_F(TestApiBlackUncovered, streaming_operators)
   ss << std::unordered_set<Term>{x, x};
 }
 
+TEST_F(TestApiBlackUncovered, datatypeApi)
+{
+  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+  cons.addSelector("head", d_solver.getIntegerSort());
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort listSort = d_solver.mkDatatypeSort(dtypeSpec);
+  Datatype d = listSort.getDatatype();
+
+  std::stringstream ss;
+  ss << cons;
+  ss << d.getConstructor("cons");
+  ss << d.getSelector("head");
+  ss << std::vector<DatatypeConstructorDecl>{cons, nil};
+  ss << d;
+
+  {
+    DatatypeConstructor c = d.getConstructor("cons");
+    DatatypeConstructor::const_iterator it;
+    it = c.begin();
+    ASSERT_NE(it, c.end());
+    ASSERT_EQ(it, c.begin());
+    *it;
+    ASSERT_NO_THROW(it->getName());
+    ++it;
+    it++;
+  }
+  {
+    Datatype::const_iterator it;
+    it = d.begin();
+    ASSERT_NE(it, d.end());
+    ASSERT_EQ(it, d.begin());
+    it->getName();
+    *it;
+    ++it;
+    it++;
+  }
+}
+
+TEST_F(TestApiBlackUncovered, termNativeTypes)
+{
+  Term t = d_solver.mkInteger(0);
+  d_solver.mkReal(0);
+  d_solver.mkReal(0, 1);
+  t.isInt32Value();
+  t.getInt32Value();
+  t.isInt64Value();
+  t.getInt64Value();
+  t.isUInt32Value();
+  t.getUInt32Value();
+  t.isUInt64Value();
+  t.getUInt64Value();
+  t.isReal32Value();
+  t.getReal32Value();
+  t.isReal64Value();
+  t.getReal64Value();
+}
+
+TEST_F(TestApiBlackUncovered, termIterators)
+{
+  Term t = d_solver.mkInteger(0);
+  auto it = t.begin();
+  auto it2(it);
+  it++;
+}
+
+TEST_F(TestApiBlackUncovered, checkSatAssumingSingle)
+{
+  Sort boolsort = d_solver.getBooleanSort();
+  Term b = d_solver.mkConst(boolsort, "b");
+  d_solver.checkSatAssuming(b);
+}
+
+TEST_F(TestApiBlackUncovered, mkOpInitializerList)
+{
+  d_solver.mkOp(Kind::BITVECTOR_EXTRACT, {1, 1});
+}
+
+TEST_F(TestApiBlackUncovered, mkTermKind)
+{
+  Term b = d_solver.mkConst(d_solver.getRealSort(), "b");
+  d_solver.mkTerm(Kind::GT, {b, b});
+}
+
 TEST_F(TestApiBlackUncovered, getValue)
 {
   d_solver.setOption("produce-models", "true");