From a3e8a80434c85d85530c5ec6d064581782c35737 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 5 May 2022 13:54:48 -0700 Subject: [PATCH] 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. --- src/api/cpp/cvc5.cpp | 1 + src/api/python/cvc5.pxd | 3 + src/api/python/cvc5.pxi | 25 +++---- test/unit/api/python/test_datatype_api.py | 16 +++-- test/unit/api/python/test_grammar.py | 10 +++ test/unit/api/python/test_uncovered.cpp | 88 +++++++++++++++++++++++ 6 files changed, 122 insertions(+), 21 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 0c6167963..d7e85c4d3 100644 --- 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 2e6dfa493..8f6bd3b24 100644 --- 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 5af31b074..b46b5f98f 100644 --- 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(( e).csort) creplacements.push_back(( r).csort) - + sort.csort = self.csort.substitute(ces, creplacements) else: - # add the single elements to the vectors - ces.push_back(( sort_or_list_1).csort) - creplacements.push_back(( sort_or_list_2).csort) + # call the API substitute method with single sorts + sort.csort = self.csort.substitute(( sort_or_list_1).csort, ( 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(( e).cterm) creplacements.push_back(( r).cterm) - + term.cterm = self.cterm.substitute(ces, creplacements) else: - # add the single elements to the vectors - ces.push_back(( term_or_list_1).cterm) - creplacements.push_back(( term_or_list_2).cterm) + # call the API substitute method with single terms + term.cterm = self.cterm.substitute(( term_or_list_1).cterm, ( 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 9caedd3f8..1b6c20bdb 100644 --- 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 464f51648..53f3f55fc 100644 --- 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 eaea0a5e2..fe53cf4ed 100644 --- 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{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{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"); -- 2.30.2