From: Gereon Kremer Date: Mon, 2 May 2022 21:08:58 +0000 (-0700) Subject: Add missing tests for some corners of the API (#8688) X-Git-Tag: cvc5-1.0.1~190 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=79cf93488f06d8e141463146afc8fcad0cb905f1;p=cvc5.git Add missing tests for some corners of the API (#8688) This PR adds a bunch of unit tests for some not yet covered corners of the API. --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index e6e068661..b5f0d463a 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1915,6 +1915,9 @@ size_t Op::getNumIndicesHelper() const case TUPLE_PROJECT: size = d_node->getConst().getIndices().size(); break; + case TABLE_PROJECT: + size = d_node->getConst().getIndices().size(); + break; default: CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k); } return size; @@ -4208,6 +4211,11 @@ bool Datatype::const_iterator::operator!=( bool Datatype::isNullHelper() const { return d_dtype == nullptr; } +std::ostream& operator<<(std::ostream& out, const Datatype& dtype) +{ + return out << dtype.toString(); +} + /* -------------------------------------------------------------------------- */ /* Grammar */ /* -------------------------------------------------------------------------- */ diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 0743bc219..5af31b074 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2377,21 +2377,26 @@ cdef class Solver: diffi[termk] = termv return diffi - def getValue(self, Term t): + def getValue(self, term_or_list): """ - Get the value of the given term in the current model. + Get the value of the given term or list of terms in the current + model. SMT-LIB: .. code-block:: smtlib - ( get-value ( ) ) + ( get-value ( * ) ) - :param term: The term for which the value is queried. - :return: The value of the given term. + :param term_or_list: The term or list of terms for which the value + is queried. + :return: The value or list of values of the given term or list of + terms. """ + if isinstance(term_or_list, list): + return [self.getValue(t) for t in term_or_list] cdef Term term = Term(self) - term.cterm = self.csolver.getValue(t.cterm) + term.cterm = self.csolver.getValue(( term_or_list).cterm) return term def getModelDomainElements(self, Sort s): diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index 2a66a3b55..f810037f3 100644 --- a/test/unit/api/cpp/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp @@ -61,6 +61,8 @@ TEST_F(TestApiBlackDatatype, isNull) cons = d_solver.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", d_solver.getIntegerSort()); dtypeSpec.addConstructor(cons); + ASSERT_EQ(dtypeSpec.getNumConstructors(), 1); + ASSERT_FALSE(dtypeSpec.isParametric()); Sort listSort = d_solver.mkDatatypeSort(dtypeSpec); d = listSort.getDatatype(); consConstr = d[0]; @@ -72,6 +74,55 @@ TEST_F(TestApiBlackDatatype, isNull) ASSERT_FALSE(d.isNull()); ASSERT_FALSE(consConstr.isNull()); ASSERT_FALSE(sel.isNull()); + + { + std::stringstream ss; + ss << cons; + ASSERT_EQ(ss.str(), cons.toString()); + } + { + std::stringstream ss; + ss << sel; + ASSERT_EQ(ss.str(), sel.toString()); + } + { + std::stringstream ss; + ss << consConstr; + ASSERT_EQ(ss.str(), consConstr.toString()); + } + { + std::stringstream ss; + ss << d; + ASSERT_EQ(ss.str(), d.toString()); + } + + { + Datatype::const_iterator it; + it = d.begin(); + ASSERT_TRUE(it != d.end()); + ASSERT_FALSE(it->isNull()); + ASSERT_FALSE((*it).isNull()); + auto tmp = it; + tmp++; + ASSERT_EQ(tmp, d.end()); + tmp = it; + ++tmp; + ASSERT_EQ(tmp, d.end()); + } + + { + DatatypeConstructor::const_iterator it; + it = consConstr.begin(); + ASSERT_TRUE(it != consConstr.end()); + ASSERT_FALSE(it->isNull()); + ASSERT_FALSE((*it).isNull()); + auto tmp = it; + tmp++; + ASSERT_EQ(tmp, consConstr.end()); + tmp = it; + ++tmp; + ASSERT_EQ(tmp, consConstr.end()); + } } TEST_F(TestApiBlackDatatype, mkDatatypeSorts) diff --git a/test/unit/api/cpp/grammar_black.cpp b/test/unit/api/cpp/grammar_black.cpp index 5340f0f7a..810f301f0 100644 --- a/test/unit/api/cpp/grammar_black.cpp +++ b/test/unit/api/cpp/grammar_black.cpp @@ -23,6 +23,22 @@ class TestApiBlackGrammar : public TestApi { }; +TEST_F(TestApiBlackGrammar, toString) +{ + d_solver.setOption("sygus", "true"); + Sort boolean = d_solver.getBooleanSort(); + Term start = d_solver.mkVar(boolean); + Grammar g; + g = d_solver.mkGrammar({}, {start}); + g.addRule(start, d_solver.mkBoolean(false)); + + { + std::stringstream ss; + ss << g; + ASSERT_EQ(ss.str(), g.toString()); + } +} + TEST_F(TestApiBlackGrammar, addRule) { d_solver.setOption("sygus", "true"); diff --git a/test/unit/api/cpp/op_black.cpp b/test/unit/api/cpp/op_black.cpp index b9c059602..498c18c00 100644 --- a/test/unit/api/cpp/op_black.cpp +++ b/test/unit/api/cpp/op_black.cpp @@ -102,6 +102,9 @@ TEST_F(TestApiBlackOp, getNumIndices) std::vector indices = {0, 3, 2, 0, 1, 2}; Op tupleProject = d_solver.mkOp(TUPLE_PROJECT, indices); ASSERT_EQ(indices.size(), tupleProject.getNumIndices()); + + Op tableProject = d_solver.mkOp(TABLE_PROJECT, indices); + ASSERT_EQ(indices.size(), tableProject.getNumIndices()); } TEST_F(TestApiBlackOp, subscriptOperator) @@ -122,6 +125,7 @@ TEST_F(TestApiBlackOp, subscriptOperator) Op iand = d_solver.mkOp(IAND, {11}); Op fpToUbv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, {12}); Op fpToSbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, {13}); + Op regexpRepeat = d_solver.mkOp(REGEXP_REPEAT, {14}); ASSERT_EQ(4, divisible[0].getUInt32Value()); ASSERT_EQ(5, bvRepeat[0].getUInt32Value()); @@ -133,6 +137,7 @@ TEST_F(TestApiBlackOp, subscriptOperator) ASSERT_EQ(11, iand[0].getUInt32Value()); ASSERT_EQ(12, fpToUbv[0].getUInt32Value()); ASSERT_EQ(13, fpToSbv[0].getUInt32Value()); + ASSERT_EQ(14, regexpRepeat[0].getUInt32Value()); // Operators with 2 indices Op bvExtract = d_solver.mkOp(BITVECTOR_EXTRACT, {1, 0}); diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 6fbc2f46f..a25669474 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -91,6 +91,15 @@ TEST_F(TestApiBlackSolver, recoverableException) Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x).notTerm()); ASSERT_THROW(d_solver.getValue(x), CVC5ApiRecoverableException); + + try { + d_solver.getValue(x); + } + catch (const CVC5ApiRecoverableException& e) + { + ASSERT_NO_THROW(e.what()); + ASSERT_NO_THROW(e.getMessage()); + } } TEST_F(TestApiBlackSolver, supportsFloatingPoint) @@ -720,6 +729,8 @@ TEST_F(TestApiBlackSolver, mkString) "\"asdf\\u{5c}nasdf\""); ASSERT_EQ(d_solver.mkString("asdf\\u{005c}nasdf", true).toString(), "\"asdf\\u{5c}nasdf\""); + std::wstring s; + ASSERT_EQ(d_solver.mkString(s).getStringValue(), s); } TEST_F(TestApiBlackSolver, mkTerm) @@ -1339,6 +1350,16 @@ TEST_F(TestApiBlackSolver, uFIteration) } } +TEST_F(TestApiBlackSolver, getAssertions) +{ + Term a = d_solver.mkConst(d_solver.getBooleanSort(), "a"); + Term b = d_solver.mkConst(d_solver.getBooleanSort(), "b"); + d_solver.assertFormula(a); + d_solver.assertFormula(b); + std::vector asserts{a, b}; + ASSERT_EQ(d_solver.getAssertions(), asserts); +} + TEST_F(TestApiBlackSolver, getInfo) { ASSERT_NO_THROW(d_solver.getInfo("name")); @@ -1665,7 +1686,7 @@ TEST_F(TestApiBlackSolver, getDriverOptions) ASSERT_EQ(dopts.in().rdbuf(), std::cin.rdbuf()); ASSERT_EQ(dopts.out().rdbuf(), std::cout.rdbuf()); } - + TEST_F(TestApiBlackSolver, getStatistics) { ASSERT_NO_THROW(cvc5::Stat()); @@ -1943,6 +1964,14 @@ TEST_F(TestApiBlackSolver, getValue3) ASSERT_NO_THROW(d_solver.getValue(sum)); ASSERT_NO_THROW(d_solver.getValue(p_f_y)); + std::vector a; + ASSERT_NO_THROW(a.emplace_back(d_solver.getValue(x))); + ASSERT_NO_THROW(a.emplace_back(d_solver.getValue(y))); + ASSERT_NO_THROW(a.emplace_back(d_solver.getValue(z))); + std::vector b; + ASSERT_NO_THROW(b = d_solver.getValue({x,y,z})); + ASSERT_EQ(a,b); + Solver slv; ASSERT_THROW(slv.getValue(x), CVC5ApiException); } diff --git a/test/unit/api/cpp/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp index 35911b4e8..93f229f17 100644 --- a/test/unit/api/cpp/solver_white.cpp +++ b/test/unit/api/cpp/solver_white.cpp @@ -50,5 +50,12 @@ TEST_F(TestApiWhiteSolver, getOp) ASSERT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR)); } +TEST_F(TestApiWhiteSolver, printStatisticsSafe) +{ + testing::internal::CaptureStdout(); + d_solver.printStatisticsSafe(STDOUT_FILENO); + testing::internal::GetCapturedStdout(); +} + } // namespace test } // namespace cvc5::internal diff --git a/test/unit/api/cpp/synth_result_black.cpp b/test/unit/api/cpp/synth_result_black.cpp index 025e62772..c902fbbc9 100644 --- a/test/unit/api/cpp/synth_result_black.cpp +++ b/test/unit/api/cpp/synth_result_black.cpp @@ -44,6 +44,11 @@ TEST_F(TestApiBlackSynthResult, hasSolution) ASSERT_FALSE(res.hasNoSolution()); ASSERT_FALSE(res.isUnknown()); ASSERT_EQ(res.toString(), "(SOLUTION)"); + { + std::stringstream ss; + ss << res; + ASSERT_EQ(res.toString(), ss.str()); + } } TEST_F(TestApiBlackSynthResult, hasNoSolution) diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp index 93a5b73f6..defcc935e 100644 --- a/test/unit/api/cpp/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -667,6 +667,14 @@ TEST_F(TestApiBlackTerm, termChildren) Term tnull; ASSERT_THROW(tnull.getNumChildren(), CVC5ApiException); + Term::const_iterator it; + it = t1.begin(); + ASSERT_TRUE((*it).isIntegerValue()); + it++; + ASSERT_TRUE((*it).isIntegerValue()); + ++it; + ASSERT_EQ(it, t1.end()); + // apply term f(2) Sort intSort = d_solver.getIntegerSort(); Sort fsort = d_solver.mkFunctionSort({intSort}, intSort); @@ -1159,6 +1167,16 @@ TEST_F(TestApiBlackTerm, termScopedToString) ASSERT_EQ(x.toString(), "x"); } -TEST_F(TestApiBlackTerm, toString) { ASSERT_NO_THROW(Term().toString()); } +TEST_F(TestApiBlackTerm, toString) { + ASSERT_NO_THROW(Term().toString()); + + Sort intsort = d_solver.getIntegerSort(); + Term x = d_solver.mkConst(intsort, "x"); + std::stringstream ss; + + ss << std::vector{x, x}; + ss << std::set{x, x}; + ss << std::unordered_set{x, x}; +} } // namespace test } // namespace cvc5::internal diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java index 7113e9db6..224b051c4 100644 --- a/test/unit/api/java/OpTest.java +++ b/test/unit/api/java/OpTest.java @@ -140,6 +140,7 @@ class OpTest Op iand = d_solver.mkOp(IAND, 11); Op fpToUbv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 12); Op fpToSbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13); + Op regexpRepeat = d_solver.mkOp(REGEXP_REPEAT, 14); assertEquals(4, divisible.get(0).getIntegerValue().intValue()); assertEquals(5, bvRepeat.get(0).getIntegerValue().intValue()); @@ -151,6 +152,7 @@ class OpTest assertEquals(11, iand.get(0).getIntegerValue().intValue()); assertEquals(12, fpToUbv.get(0).getIntegerValue().intValue()); assertEquals(13, fpToSbv.get(0).getIntegerValue().intValue()); + assertEquals(14, regexpRepeat.get(0).getIntegerValue().intValue()); // Operators with 2 indices Op bvExtract = d_solver.mkOp(BITVECTOR_EXTRACT, 1, 0); diff --git a/test/unit/api/java/UncoveredTest.cpp b/test/unit/api/java/UncoveredTest.cpp index 1c2cb89ce..a041db700 100644 --- a/test/unit/api/java/UncoveredTest.cpp +++ b/test/unit/api/java/UncoveredTest.cpp @@ -23,11 +23,49 @@ class TestApiBlackUncovered : public TestApi { }; +TEST_F(TestApiBlackUncovered, exception_getmessage) +{ + d_solver.setOption("produce-models", "true"); + Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); + d_solver.assertFormula(x.eqTerm(x).notTerm()); + + ASSERT_THROW(d_solver.getValue(x), CVC5ApiRecoverableException); + + try { + d_solver.getValue(x); + } + catch (const CVC5ApiRecoverableException& e) + { + ASSERT_NO_THROW(e.getMessage()); + } +} + TEST_F(TestApiBlackUncovered, streaming_operators) { - std::stringstream ss; - ss << cvc5::modes::LearnedLitType::PREPROCESS; - ss << cvc5::SynthResult(); + std::stringstream ss; + ss << cvc5::modes::LearnedLitType::PREPROCESS; + ss << cvc5::Result(); + ss << cvc5::Op(); + ss << cvc5::SynthResult(); + + Sort intsort = d_solver.getIntegerSort(); + Term x = d_solver.mkConst(intsort, "x"); + + ss << std::vector{x, x}; + ss << std::set{x, x}; + ss << std::unordered_set{x, x}; +} + +TEST_F(TestApiBlackUncovered, hash) +{ + std::hash()(Op()); + std::hash()(Sort()); +} + +TEST_F(TestApiBlackUncovered, isOutputOn) +{ + d_solver.isOutputOn("inst"); + d_solver.getOutput("inst"); } TEST_F(TestApiBlackUncovered, Options) diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py index 00af24c4f..4ba607926 100644 --- a/test/unit/api/python/test_op.py +++ b/test/unit/api/python/test_op.py @@ -105,6 +105,9 @@ def test_get_num_indices(solver): tuple_project_op = solver.mkOp(Kind.TUPLE_PROJECT, *indices) assert len(indices) == tuple_project_op.getNumIndices() + table_project_op = solver.mkOp(Kind.TABLE_PROJECT, *indices) + assert len(indices) == table_project_op.getNumIndices() + def test_subscript_operator(solver): # Operators with 0 indices @@ -124,6 +127,7 @@ def test_subscript_operator(solver): iand = solver.mkOp(Kind.IAND, 11) floatingpoint_to_ubv = solver.mkOp(Kind.FLOATINGPOINT_TO_UBV, 12) floatingopint_to_sbv = solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, 13) + regexp_repeat = solver.mkOp(Kind.REGEXP_REPEAT, 14) assert 4 == divisible[0].getIntegerValue() assert 5 == bitvector_repeat[0].getIntegerValue() @@ -135,6 +139,7 @@ def test_subscript_operator(solver): assert 11 == iand[0].getIntegerValue() assert 12 == floatingpoint_to_ubv[0].getIntegerValue() assert 13 == floatingopint_to_sbv[0].getIntegerValue() + assert 14 == regexp_repeat[0].getIntegerValue() # Operators with 2 indices bitvector_extract = solver.mkOp(Kind.BITVECTOR_EXTRACT, 1, 0) diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 736111d96..3939f2d09 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -703,6 +703,8 @@ def test_mk_string(solver): str(solver.mkString("asdf\\nasdf")) == "\"asdf\\u{5c}nasdf\"" str(solver.mkString("asdf\\u{005c}nasdf", True)) ==\ "\"asdf\\u{5c}nasdf\"" + s = "" + assert solver.mkString(s).getStringValue() == s def test_mk_term(solver): @@ -1127,6 +1129,15 @@ def test_uf_iteration(solver): idx = idx + 1 +def test_get_assertions(solver): + a = solver.mkConst(solver.getBooleanSort(), 'a') + b = solver.mkConst(solver.getBooleanSort(), 'b') + solver.assertFormula(a) + solver.assertFormula(b) + asserts = [a,b] + assert solver.getAssertions() == asserts + + def test_get_info(solver): solver.getInfo("name") with pytest.raises(RuntimeError): @@ -1403,6 +1414,10 @@ def test_get_value3(solver): solver.getValue(summ) solver.getValue(p_f_y) + a = [solver.getValue(x), solver.getValue(y), solver.getValue(z)] + b = solver.getValue([x,y,z]) + assert a == b + slv = cvc5.Solver() with pytest.raises(RuntimeError): slv.getValue(x) diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index f166ecd0a..c9db1cb9a 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -1313,7 +1313,6 @@ def test_get_cardinality_constraint(solver): nullt.isCardinalityConstraint() - def test_term_scoped_to_string(solver): intsort = solver.getIntegerSort() x = solver.mkConst(intsort, "x") diff --git a/test/unit/api/python/test_uncovered.cpp b/test/unit/api/python/test_uncovered.cpp index c64887b0f..fbeef181e 100644 --- a/test/unit/api/python/test_uncovered.cpp +++ b/test/unit/api/python/test_uncovered.cpp @@ -23,11 +23,53 @@ class TestApiBlackUncovered : public TestApi { }; +TEST_F(TestApiBlackUncovered, exception_getmessage) +{ + d_solver.setOption("produce-models", "true"); + Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); + d_solver.assertFormula(x.eqTerm(x).notTerm()); + + ASSERT_THROW(d_solver.getValue(x), CVC5ApiRecoverableException); + + try { + d_solver.getValue(x); + } + catch (const CVC5ApiRecoverableException& e) + { + ASSERT_NO_THROW(e.getMessage()); + } +} + TEST_F(TestApiBlackUncovered, streaming_operators) { - std::stringstream ss; - ss << cvc5::modes::LearnedLitType::PREPROCESS; - ss << cvc5::SynthResult(); + std::stringstream ss; + ss << cvc5::modes::LearnedLitType::PREPROCESS; + ss << cvc5::Result(); + ss << cvc5::Op(); + ss << cvc5::SynthResult(); + + Sort intsort = d_solver.getIntegerSort(); + Term x = d_solver.mkConst(intsort, "x"); + + ss << std::vector{x, x}; + ss << std::set{x, x}; + ss << std::unordered_set{x, x}; +} + +TEST_F(TestApiBlackUncovered, getValue) +{ + d_solver.setOption("produce-models", "true"); + Sort boolsort = d_solver.getBooleanSort(); + Term b = d_solver.mkConst(boolsort, "b"); + d_solver.assertFormula(b); + d_solver.checkSat(); + d_solver.getValue({b, b, b}); +} + +TEST_F(TestApiBlackUncovered, isOutputOn) +{ + d_solver.isOutputOn("inst"); + d_solver.getOutput("inst"); } TEST_F(TestApiBlackUncovered, Options)