Remove java API methods that accepts lists as arguments (#8541)

This PR removes some unnecessary methods in the Java API that were added to simplify several unit tests that use dynamic arrays. The goal is to make the java API consistent and as small as possible.
Users could use asList, toArray methods to use generic lists if they wish.

diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java
index 9fcb261d3972127ef19d4c8e54409118a649ae61..908e90dc5584f841eef89c48108569ae8496c80b 100644 (file)
--- a/src/api/java/io/github/cvc5/Solver.java
+++ b/src/api/java/io/github/cvc5/Solver.java
@@ -214,20 +214,6 @@ public class Solver implements IPointer, AutoCloseable
   private native long mkDatatypeSort(long pointer, long datatypeDeclPointer)
       throws CVC5ApiException;
 
-  /**
-   * Create a vector of datatype sorts. The names of the datatype
-   * declarations must be distinct.
-   *
-   * @param dtypedecls the datatype declarations from which the sort is
-   *     created
-   * @return the datatype sorts
-   * @throws CVC5ApiException
-   */
-  public Sort[] mkDatatypeSorts(List<DatatypeDecl> dtypedecls) throws CVC5ApiException
-  {
-    return mkDatatypeSorts(dtypedecls.toArray(new DatatypeDecl[0]));
-  }
-
   /**
    * Create a vector of datatype sorts. The names of the datatype
    * declarations must be distinct.
@@ -623,18 +609,6 @@ public class Solver implements IPointer, AutoCloseable
   private native long mkTerm(
       long pointer, long opPointer, long child1Pointer, long child2Pointer, long child3Pointer);
 
-  /**
-   * Create n-ary term of given kind from a given operator.
-   * Create operators with mkOp().
-   * @param op the operator
-   * @param children the children of the term
-   * @return the Term
-   */
-  public Term mkTerm(Op op, List<Term> children)
-  {
-    return mkTerm(op, children.toArray(new Term[0]));
-  }
-
   /**
    * Create n-ary term of given kind from a given operator.
    * Create operators with mkOp().
@@ -1389,18 +1363,6 @@ public class Solver implements IPointer, AutoCloseable
   private native long mkDatatypeDecl(
       long pointer, String name, long paramPointer, boolean isCoDatatype);
 
-  /**
-   * Create a datatype declaration.
-   * Create sorts parameter with Solver::mkParamSort().
-   * @param name the name of the datatype
-   * @param params a list of sort parameters
-   * @return the DatatypeDecl
-   */
-  public DatatypeDecl mkDatatypeDecl(String name, List<Sort> params)
-  {
-    return mkDatatypeDecl(name, params.toArray(new Sort[0]));
-  }
-
   /**
    * Create a datatype declaration.
    * Create sorts parameter with Solver::mkParamSort().

diff --git a/src/api/java/io/github/cvc5/Sort.java b/src/api/java/io/github/cvc5/Sort.java
index 65ff8e49d9227913d428c13080546d6b78d185a9..a5d4a539ac9045c25b2f322cf250cb3f24543cec 100644 (file)
--- a/src/api/java/io/github/cvc5/Sort.java
+++ b/src/api/java/io/github/cvc5/Sort.java
@@ -406,20 +406,6 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
 
   private native long getDatatype(long pointer);
 
-  /**
-   * Instantiate a parameterized datatype sort or uninterpreted sort
-   * constructor sort.
-   *
-   * Create sorts parameter with Solver.mkParamSort().
-   *
-   * @param params the list of sort parameters to instantiate with
-   * @return the instantiated sort
-   */
-  public Sort instantiate(List<Sort> params)
-  {
-    return instantiate(params.toArray(new Sort[0]));
-  }
-
   /**
    * Instantiate a parameterized datatype sort or uninterpreted sort
    * constructor sort.

diff --git a/src/api/java/io/github/cvc5/Term.java b/src/api/java/io/github/cvc5/Term.java
index a0a0620ace5b8d6e80db099480742733ad3e5c08..a60b11427cb61159a35b5ff82694fc7a18f2b264 100644 (file)
--- a/src/api/java/io/github/cvc5/Term.java
+++ b/src/api/java/io/github/cvc5/Term.java
@@ -151,22 +151,6 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable<
 
   private native long substitute(long pointer, long termPointer, long replacementPointer);
 
-  /**
-   * @return the result of simultaneously replacing 'terms' by 'replacements'
-   * in this term
-   *
-   * Note that this replacement is applied during a pre-order traversal and
-   * only once to the term. It is not run until fix point. In the case that
-   * terms contains duplicates, the replacement earliest in the vector takes
-   * priority. For example, calling substitute on f(x,y) with
-   *   terms = { x, z }, replacements = { g(z), w }
-   * results in the term f(g(z),y).
-   */
-  public Term substitute(List<Term> terms, List<Term> replacements)
-  {
-    return substitute(terms.toArray(new Term[0]), replacements.toArray(new Term[0]));
-  }
-
   /**
    * @return the result of simultaneously replacing 'terms' by 'replacements'
    * in this term

diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java
index 354d8662f947831b9211b050bcbd536e20bb9370..bc13ab634b7cdd8f730d7c1702424fe12805307c 100644 (file)
--- a/test/unit/api/java/DatatypeTest.java
+++ b/test/unit/api/java/DatatypeTest.java
@@ -97,7 +97,8 @@ class DatatypeTest
     dtdecls.add(list);
 
     AtomicReference<Sort[]> atomic = new AtomicReference<>();
-    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
+    assertDoesNotThrow(
+        () -> atomic.set(d_solver.mkDatatypeSorts(dtdecls.toArray(new DatatypeDecl[0]))));
     Sort[] dtsorts = atomic.get();
     assertEquals(dtsorts.length, dtdecls.size());
     for (int i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
@@ -120,7 +121,8 @@ class DatatypeTest
     List<DatatypeDecl> dtdeclsBad = new ArrayList<>();
     DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD");
     dtdeclsBad.add(emptyD);
-    assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSorts(dtdeclsBad));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkDatatypeSorts(dtdeclsBad.toArray(new DatatypeDecl[0])));
   }
 
   @Test
@@ -152,7 +154,8 @@ class DatatypeTest
     dtdecls.add(list);
 
     AtomicReference<Sort[]> atomic = new AtomicReference<>();
-    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
+    assertDoesNotThrow(
+        () -> atomic.set(d_solver.mkDatatypeSorts(dtdecls.toArray(new DatatypeDecl[0]))));
     Sort[] dtsorts = atomic.get();
     assertEquals(dtsorts.length, dtdecls.size());
     for (int i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
@@ -291,7 +294,7 @@ class DatatypeTest
     Sort t2 = d_solver.mkParamSort("T2");
     v.add(t1);
     v.add(t2);
-    DatatypeDecl pairSpec = d_solver.mkDatatypeDecl("pair", v);
+    DatatypeDecl pairSpec = d_solver.mkDatatypeDecl("pair", v.toArray(new Sort[0]));
 
     DatatypeConstructorDecl mkpair = d_solver.mkDatatypeConstructorDecl("mk-pair");
     mkpair.addSelector("first", t1);
@@ -307,19 +310,19 @@ class DatatypeTest
     v.clear();
     v.add(d_solver.getIntegerSort());
     v.add(d_solver.getIntegerSort());
-    Sort pairIntInt = pairType.instantiate(v);
+    Sort pairIntInt = pairType.instantiate(v.toArray(new Sort[0]));
     v.clear();
     v.add(d_solver.getRealSort());
     v.add(d_solver.getRealSort());
-    Sort pairRealReal = pairType.instantiate(v);
+    Sort pairRealReal = pairType.instantiate(v.toArray(new Sort[0]));
     v.clear();
     v.add(d_solver.getRealSort());
     v.add(d_solver.getIntegerSort());
-    Sort pairRealInt = pairType.instantiate(v);
+    Sort pairRealInt = pairType.instantiate(v.toArray(new Sort[0]));
     v.clear();
     v.add(d_solver.getIntegerSort());
     v.add(d_solver.getRealSort());
-    Sort pairIntReal = pairType.instantiate(v);
+    Sort pairIntReal = pairType.instantiate(v.toArray(new Sort[0]));
 
     assertNotEquals(pairIntInt, pairRealReal);
     assertNotEquals(pairIntReal, pairRealReal);
@@ -333,7 +336,7 @@ class DatatypeTest
   void datatypeIsFinite() throws CVC5ApiException
   {
     List<Sort> v = new ArrayList<>();
-    DatatypeDecl dtypedecl = d_solver.mkDatatypeDecl("dt", v);
+    DatatypeDecl dtypedecl = d_solver.mkDatatypeDecl("dt", v.toArray(new Sort[0]));
     DatatypeConstructorDecl ctordecl = d_solver.mkDatatypeConstructorDecl("cons");
     ctordecl.addSelector("sel", d_solver.getBooleanSort());
     dtypedecl.addConstructor(ctordecl);
@@ -342,7 +345,7 @@ class DatatypeTest
 
     Sort p = d_solver.mkParamSort("p1");
     v.add(p);
-    DatatypeDecl pdtypedecl = d_solver.mkDatatypeDecl("dt", v);
+    DatatypeDecl pdtypedecl = d_solver.mkDatatypeDecl("dt", v.toArray(new Sort[0]));
     DatatypeConstructorDecl pctordecl = d_solver.mkDatatypeConstructorDecl("cons");
     pctordecl.addSelector("sel", p);
     pdtypedecl.addConstructor(pctordecl);
@@ -393,7 +396,8 @@ class DatatypeTest
     dtdecls.add(ns);
     // this is well-founded and has no nested recursion
     AtomicReference<Sort[]> atomic = new AtomicReference<>();
-    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
+    assertDoesNotThrow(
+        () -> atomic.set(d_solver.mkDatatypeSorts(dtdecls.toArray(new DatatypeDecl[0]))));
     Sort[] dtsorts = atomic.get();
     assertEquals(dtsorts.length, 3);
     assertTrue(dtsorts[0].getDatatype().isWellFounded());
@@ -419,7 +423,8 @@ class DatatypeTest
 
     // dtsorts.clear();
     // this is not well-founded due to non-simple recursion
-    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
+    assertDoesNotThrow(
+        () -> atomic.set(d_solver.mkDatatypeSorts(dtdecls.toArray(new DatatypeDecl[0]))));
     dtsorts = atomic.get();
     assertEquals(dtsorts.length, 1);
     assertTrue(
@@ -461,7 +466,8 @@ class DatatypeTest
 
     // dtsorts.clear();
     // both are well-founded and have nested recursion
-    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
+    assertDoesNotThrow(
+        () -> atomic.set(d_solver.mkDatatypeSorts(dtdecls.toArray(new DatatypeDecl[0]))));
     dtsorts = atomic.get();
     assertEquals(dtsorts.length, 2);
     assertTrue(dtsorts[0].getDatatype().isWellFounded());
@@ -495,7 +501,8 @@ class DatatypeTest
 
     // dtsorts.clear();
     // both are well-founded and have nested recursion
-    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
+    assertDoesNotThrow(
+        () -> atomic.set(d_solver.mkDatatypeSorts(dtdecls.toArray(new DatatypeDecl[0]))));
     dtsorts = atomic.get();
     assertEquals(dtsorts.length, 2);
     assertTrue(dtsorts[0].getDatatype().isWellFounded());
@@ -511,13 +518,13 @@ class DatatypeTest
     List<Sort> v = new ArrayList<>();
     Sort x = d_solver.mkParamSort("X");
     v.add(x);
-    DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v);
+    DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v.toArray(new Sort[0]));
 
     List<Sort> args = new ArrayList<>();
     args.add(x);
-    Sort urListX = unresList5.instantiate(args);
+    Sort urListX = unresList5.instantiate(args.toArray(new Sort[0]));
     args.set(0, urListX);
-    Sort urListListX = unresList5.instantiate(args);
+    Sort urListListX = unresList5.instantiate(args.toArray(new Sort[0]));
 
     DatatypeConstructorDecl cons5 = d_solver.mkDatatypeConstructorDecl("cons5");
     cons5.addSelector("car", x);
@@ -530,7 +537,8 @@ class DatatypeTest
     dtdecls.add(list5);
 
     // well-founded and has nested recursion
-    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
+    assertDoesNotThrow(
+        () -> atomic.set(d_solver.mkDatatypeSorts(dtdecls.toArray(new DatatypeDecl[0]))));
     dtsorts = atomic.get();
     assertEquals(dtsorts.length, 1);
     assertTrue(dtsorts[0].getDatatype().isWellFounded());
@@ -550,11 +558,11 @@ class DatatypeTest
     List<Sort> v = new ArrayList<>();
     Sort x = d_solver.mkParamSort("X");
     v.add(x);
-    DatatypeDecl plist = d_solver.mkDatatypeDecl("plist", v);
+    DatatypeDecl plist = d_solver.mkDatatypeDecl("plist", v.toArray(new Sort[0]));
 
     List<Sort> args = new ArrayList<>();
     args.add(x);
-    Sort urListX = unresList.instantiate(args);
+    Sort urListX = unresList.instantiate(args.toArray(new Sort[0]));
 
     DatatypeConstructorDecl pcons = d_solver.mkDatatypeConstructorDecl("pcons");
     pcons.addSelector("car", x);
@@ -568,7 +576,8 @@ class DatatypeTest
 
     // make the datatype sorts
     AtomicReference<Sort[]> atomic = new AtomicReference<>();
-    assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls)));
+    assertDoesNotThrow(
+        () -> atomic.set(d_solver.mkDatatypeSorts(dtdecls.toArray(new DatatypeDecl[0]))));
     Sort[] dtsorts = atomic.get();
     assertEquals(dtsorts.length, 1);
     Datatype d = dtsorts[0].getDatatype();
@@ -577,7 +586,7 @@ class DatatypeTest
     Sort isort = d_solver.getIntegerSort();
     List<Sort> iargs = new ArrayList<>();
     iargs.add(isort);
-    Sort listInt = dtsorts[0].instantiate(iargs);
+    Sort listInt = dtsorts[0].instantiate(iargs.toArray(new Sort[0]));
 
     AtomicReference<Term> atomicTerm = new AtomicReference<>();
     // get the specialized constructor term for list[Int]

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 5515fa64927119c1979aa87c12bb3ba249f1b815..4d5c35472327c442e58672ab249724c3c555b93c 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -193,9 +193,9 @@ class SolverTest
     DatatypeConstructorDecl unil = d_solver.mkDatatypeConstructorDecl("unil");
     ulist.addConstructor(unil);
     DatatypeDecl[] udecls = new DatatypeDecl[] {ulist};
-    assertDoesNotThrow(() -> d_solver.mkDatatypeSorts(Arrays.asList(udecls)));
+    assertDoesNotThrow(() -> d_solver.mkDatatypeSorts(udecls));
 
-    assertThrows(CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls)));
+    assertThrows(CVC5ApiException.class, () -> slv.mkDatatypeSorts(udecls));
     slv.close();
 
     /* mutually recursive with unresolved parameterized sorts */

diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java
index 239e3262d48dc5c41eb3b2d1ee07bd4f6b34f2a0..3ecddb82c35869a2c8fb8ef5058ab7702c6b6c6f 100644 (file)
--- a/test/unit/api/java/TermTest.java
+++ b/test/unit/api/java/TermTest.java
@@ -206,7 +206,7 @@ class TermTest
     }
 
     // testing rebuild from op and children
-    assertEquals(fx, d_solver.mkTerm(fx.getOp(), children));
+    assertEquals(fx, d_solver.mkTerm(fx.getOp(), children.toArray(new Term[0])));
 
     // Test Datatypes Ops
     Sort sort = d_solver.mkParamSort("T");
@@ -1069,15 +1069,17 @@ class TermTest
     rs.add(y);
     es.add(y);
     rs.add(one);
-    assertEquals(xpy.substitute(es, rs), xpone);
+    assertEquals(xpy.substitute(es.toArray(new Term[0]), rs.toArray(new Term[0])), xpone);
 
     // incorrect substitution due to arity
     rs.remove(rs.size() - 1);
-    assertThrows(CVC5ApiException.class, () -> xpy.substitute(es, rs));
+    assertThrows(CVC5ApiException.class,
+        () -> xpy.substitute(es.toArray(new Term[0]), rs.toArray(new Term[0])));
 
     // incorrect substitution due to types
     rs.add(ttrue);
-    assertThrows(CVC5ApiException.class, () -> xpy.substitute(es, rs));
+    assertThrows(CVC5ApiException.class,
+        () -> xpy.substitute(es.toArray(new Term[0]), rs.toArray(new Term[0])));
 
     // null cannot substitute
     Term tnull = d_solver.getNullTerm();
@@ -1086,15 +1088,18 @@ class TermTest
     assertThrows(CVC5ApiException.class, () -> xpx.substitute(x, tnull));
     rs.remove(rs.size() - 1);
     rs.add(tnull);
-    assertThrows(CVC5ApiException.class, () -> xpy.substitute(es, rs));
+    assertThrows(CVC5ApiException.class,
+        () -> xpy.substitute(es.toArray(new Term[0]), rs.toArray(new Term[0])));
     es.clear();
     rs.clear();
     es.add(x);
     rs.add(y);
-    assertThrows(CVC5ApiException.class, () -> tnull.substitute(es, rs));
+    assertThrows(CVC5ApiException.class,
+        () -> tnull.substitute(es.toArray(new Term[0]), rs.toArray(new Term[0])));
     es.add(tnull);
     rs.add(one);
-    assertThrows(CVC5ApiException.class, () -> xpx.substitute(es, rs));
+    assertThrows(CVC5ApiException.class,
+        () -> xpx.substitute(es.toArray(new Term[0]), rs.toArray(new Term[0])));
   }
 
   @Test