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.

diff --git a/src/api/java/io/github/cvc5/DatatypeDecl.java b/src/api/java/io/github/cvc5/DatatypeDecl.java
index c44fcf6f335854d0b5e56f850244dc7c092135b0..7cb631e2beb76106caff4ad1404f3edaf973e9dc 100644 (file)
--- 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 2409981087c234c4fcb9d690e2849b694cde66a4..e13090beadffdbbf9117c4eecda2894c047fab55 100644 (file)
--- 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<Solver*>(pointer);
+  const char* s = env->GetStringUTFChars(jsymbol, nullptr);
+  std::string symbol(s);
+  Sort* sortptr = reinterpret_cast<Sort*>(sort);
+  std::vector<Term> initValue = getObjectsFromPointers<Term>(env, initValuePointers);
+  Term* retPointer = new Term(solver->declarePool(symbol, *sortptr, initValue));
+  return reinterpret_cast<jlong>(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 4a60ccbce519f874adf53389793d4c2131fe8668..4b87682e7baeb7d87a3a4c5d94781bf67fc42772 100644 (file)
--- 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 0ed846778220d29530baa8dab9ec2fcad5e8b9d7..60d3a2e4645cdd0c4a367323c3403d82ff936471 100644 (file)
--- 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 41b3c989b62df6c6e53997377ab50fa179d9b781..70d36dd759f46272f42c3c6cf618e893b1d52da1 100644 (file)
--- 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 224b051c437e851ac027854f63cba7c5b4d84876..c14518a2f68c4a4b7a3c8901125cf551d28dfcbf 100644 (file)
--- 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 0bcf3078147180fd0e6396d15a2e887e1df7b807..7b2de58f4ccbd98ff854c2ad451e0033cc459716 100644 (file)
--- 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 beb30135752b192c2fb8548c5e1a261245a29e6b..eca76590bd7fff8c49a5a96499a626f53a78498d 100644 (file)
--- 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 076eb1b4e925b9643efa84997f1e08e03ecdccad..97b693cd0d4fc43e36b779759a87211ef0daa06a 100644 (file)
--- 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<Term>{x, x};
 }
 
+TEST_F(TestApiBlackUncovered, mkString)
+{
+  std::wstring s;
+  ASSERT_EQ(d_solver.mkString(s).getStringValue(), s);
+}
+
 TEST_F(TestApiBlackUncovered, hash)
 {
     std::hash<Op>()(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