From 6007962d5e173477ba8850141e519b49c0659c57 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 10 May 2022 07:55:44 -0700 Subject: [PATCH] Add test coverage for almost everything from the Java API (#8723) This PR adds tests for almost everything that is not yet covered by the java API tests. --- src/api/java/io/github/cvc5/DatatypeDecl.java | 2 +- src/api/java/jni/solver.cpp | 19 ++++ test/unit/api/java/CMakeLists.txt | 1 + test/unit/api/java/DatatypeTest.java | 42 +++++++ test/unit/api/java/GrammarTest.java | 11 ++ test/unit/api/java/OpTest.java | 3 + test/unit/api/java/SolverTest.java | 28 +++++ test/unit/api/java/SortTest.java | 10 ++ test/unit/api/java/UncoveredTest.cpp | 106 ++++++++++++++++++ 9 files changed, 221 insertions(+), 1 deletion(-) diff --git a/src/api/java/io/github/cvc5/DatatypeDecl.java b/src/api/java/io/github/cvc5/DatatypeDecl.java index c44fcf6f3..7cb631e2b 100644 --- a/src/api/java/io/github/cvc5/DatatypeDecl.java +++ b/src/api/java/io/github/cvc5/DatatypeDecl.java @@ -55,7 +55,7 @@ public class DatatypeDecl extends AbstractPointer private native void addConstructor(long pointer, long declPointer); /** Get the number of constructors (so far) for this Datatype declaration. */ - int getNumConstructors() + public int getNumConstructors() { return getNumConstructors(pointer); } diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 240998108..e13090bea 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -2116,6 +2116,25 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getValueSepNil( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } +/* + * Class: io_github_cvc5_Solver + * Method: declarePool + * Signature: (Ljava/lang/String;J[J])J + */ +JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_declarePool( + JNIEnv* env, jobject, jlong pointer, jstring jsymbol, jlong sort, jlongArray initValuePointers) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast(pointer); + const char* s = env->GetStringUTFChars(jsymbol, nullptr); + std::string symbol(s); + Sort* sortptr = reinterpret_cast(sort); + std::vector initValue = getObjectsFromPointers(env, initValuePointers); + Term* retPointer = new Term(solver->declarePool(symbol, *sortptr, initValue)); + return reinterpret_cast(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_Solver * Method: pop diff --git a/test/unit/api/java/CMakeLists.txt b/test/unit/api/java/CMakeLists.txt index 4a60ccbce..4b87682e7 100644 --- a/test/unit/api/java/CMakeLists.txt +++ b/test/unit/api/java/CMakeLists.txt @@ -67,6 +67,7 @@ cvc5_add_java_api_test(OpTest) cvc5_add_java_api_test(ResultTest) cvc5_add_java_api_test(SolverTest) cvc5_add_java_api_test(SortTest) +cvc5_add_java_api_test(SynthResultTest) cvc5_add_java_api_test(TermTest) cvc5_add_unit_test_white(UncoveredTest api/java) diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index 0ed846778..60d3a2e46 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -58,6 +58,48 @@ class DatatypeTest assertDoesNotThrow(() -> nilConstr.getTerm()); } + @Test + void isNull() throws CVC5ApiException + { + // creating empty (null) objects. + DatatypeDecl dtypeSpec = null; + DatatypeConstructorDecl cons = null; + Datatype d = null; + DatatypeConstructor consConstr = null; + DatatypeSelector sel = null; + + // verifying that the objects are considered null. + assertNull(dtypeSpec); + assertNull(cons); + assertNull(d); + assertNull(consConstr); + assertNull(sel); + + // changing the objects to be non-null + dtypeSpec = d_solver.mkDatatypeDecl("list"); + cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", d_solver.getIntegerSort()); + dtypeSpec.addConstructor(cons); + assertEquals(dtypeSpec.getNumConstructors(), 1); + assertFalse(dtypeSpec.isParametric()); + Sort listSort = d_solver.mkDatatypeSort(dtypeSpec); + d = listSort.getDatatype(); + consConstr = d.getConstructor(0); + sel = consConstr.getSelector(0); + + // verifying that the new objects are non-null + assertFalse(dtypeSpec.isNull()); + assertFalse(cons.isNull()); + assertFalse(d.isNull()); + assertFalse(consConstr.isNull()); + assertFalse(sel.isNull()); + + cons.toString(); + sel.toString(); + consConstr.toString(); + d.toString(); + } + @Test void mkDatatypeSorts() throws CVC5ApiException { diff --git a/test/unit/api/java/GrammarTest.java b/test/unit/api/java/GrammarTest.java index 41b3c989b..70d36dd75 100644 --- a/test/unit/api/java/GrammarTest.java +++ b/test/unit/api/java/GrammarTest.java @@ -39,6 +39,17 @@ class GrammarTest d_solver.close(); } + @Test + void testToString() + { + d_solver.setOption("sygus", "true"); + Sort bool = d_solver.getBooleanSort(); + Term start = d_solver.mkVar(bool); + Grammar g = d_solver.mkGrammar(new Term[] {}, new Term[] {start}); + g.addRule(start, d_solver.mkBoolean(false)); + g.toString(); + } + @Test void addRule() { diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java index 224b051c4..c14518a2f 100644 --- a/test/unit/api/java/OpTest.java +++ b/test/unit/api/java/OpTest.java @@ -119,6 +119,9 @@ class OpTest int[] indices = {0, 3, 2, 0, 1, 2}; Op tupleProject = d_solver.mkOp(TUPLE_PROJECT, indices); assertEquals(6, tupleProject.getNumIndices()); + + Op tableProject = d_solver.mkOp(TABLE_PROJECT, indices); + assertEquals(6, tableProject.getNumIndices()); } @Test diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 0bcf30781..7b2de58f4 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1383,6 +1383,18 @@ class SolverTest } } + @Test + void 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); + Term[] asserts = d_solver.getAssertions(); + assertEquals(asserts[0], a); + assertEquals(asserts[1], b); + } + @Test void getInfo() { @@ -1517,6 +1529,20 @@ class SolverTest assertNotEquals(output, output2); } + @Test + void declarePool() throws CVC5ApiException + { + Sort intSort = d_solver.getIntegerSort(); + Sort setSort = d_solver.mkSetSort(intSort); + Term zero = d_solver.mkInteger(0); + Term x = d_solver.mkConst(intSort, "x"); + Term y = d_solver.mkConst(intSort, "y"); + // declare a pool with initial value { 0, x, y } + Term p = d_solver.declarePool("p", intSort, new Term[]{zero, x, y}); + // pool should have the same sort + assertEquals(p.getSort(), setSort); + } + @Test void getOp() throws CVC5ApiException { @@ -1946,6 +1972,8 @@ class SolverTest assertDoesNotThrow(() -> d_solver.getValue(sum)); assertDoesNotThrow(() -> d_solver.getValue(p_f_y)); + Term[] b = d_solver.getValue(new Term[]{x, y, z}); + Solver slv = new Solver(); assertThrows(CVC5ApiException.class, () -> slv.getValue(x)); slv.close(); diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index beb301357..eca76590b 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -191,6 +191,16 @@ class SortTest assertDoesNotThrow(() -> d_solver.getNullSort().isDatatypeTester()); } + @Test + void isDatatypeUpdater() throws CVC5ApiException + { + Sort dt_sort = create_datatype_sort(); + Datatype dt = dt_sort.getDatatype(); + Sort updater_sort = dt.getConstructor(0).getSelector(0).getUpdaterTerm().getSort(); + assertTrue(updater_sort.isDatatypeUpdater()); + assertDoesNotThrow(() -> d_solver.getNullSort().isDatatypeUpdater()); + } + @Test void isFunction() { diff --git a/test/unit/api/java/UncoveredTest.cpp b/test/unit/api/java/UncoveredTest.cpp index 076eb1b4e..97b693cd0 100644 --- a/test/unit/api/java/UncoveredTest.cpp +++ b/test/unit/api/java/UncoveredTest.cpp @@ -23,6 +23,24 @@ class TestApiBlackUncovered : public TestApi { }; +TEST_F(TestApiBlackUncovered, comparison_operators) +{ + cvc5::Result res; + res != res; + cvc5::Sort sort; + sort != sort; + sort <= sort; + sort >= sort; + sort > sort; + cvc5::Op op; + op != op; + cvc5::Term term; + term != term; + term <= term; + term >= term; + term > term; +} + TEST_F(TestApiBlackUncovered, exception_getmessage) { d_solver.setOption("produce-models", "true"); @@ -40,13 +58,46 @@ TEST_F(TestApiBlackUncovered, exception_getmessage) } } +TEST_F(TestApiBlackUncovered, term_native_types) +{ + Term t = d_solver.mkInteger(0); + 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, term_iterators) +{ + Term t = d_solver.mkInteger(0); + t = d_solver.mkTerm(Kind::GT, {t, t}); + Term::const_iterator it; + it = t.begin(); + auto it2(it); + it == t.end(); + it != it2; + *it2; + ++it; + it++; +} + 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 +107,12 @@ TEST_F(TestApiBlackUncovered, streaming_operators) ss << std::unordered_set{x, x}; } +TEST_F(TestApiBlackUncovered, mkString) +{ + std::wstring s; + ASSERT_EQ(d_solver.mkString(s).getStringValue(), s); +} + TEST_F(TestApiBlackUncovered, hash) { std::hash()(Op()); @@ -91,5 +148,54 @@ TEST_F(TestApiBlackUncovered, Statistics) testing::internal::GetCapturedStdout(); } +TEST_F(TestApiBlackUncovered, Datatypes) +{ + // default constructors + DatatypeConstructorDecl dtcd; + DatatypeSelector dts; + DatatypeConstructor dc; + DatatypeDecl dtd; + Datatype d; + + dtd = d_solver.mkDatatypeDecl("list"); + dtcd = d_solver.mkDatatypeConstructorDecl("cons"); + dtcd.addSelector("head", d_solver.getIntegerSort()); + dtd.addConstructor(dtcd); + Sort s = d_solver.mkDatatypeSort(dtd); + d = s.getDatatype(); + dc = d.getConstructor("cons"); + dc.getSelector("head"); + + { + Datatype::const_iterator it; + it = d.begin(); + it != d.end(); + *it; + it->getName(); + ++it; + it == d.end(); + it++; + } + { + DatatypeConstructor::const_iterator it; + it = dc.begin(); + it != dc.end(); + *it; + it->getName(); + ++it; + it = dc.begin(); + it++; + it == dc.end(); + } + + { + std::stringstream ss; + ss << d; + ss << dtcd; + ss << dc; + ss << d.getSelector("head"); + } +} + } // namespace test } // namespace cvc5::internal -- 2.30.2