From ffe428bb7f9c87557b0a5c742171f8224d9f186f Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Fri, 1 Apr 2022 19:40:47 -0500 Subject: [PATCH] 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. --- src/api/java/io/github/cvc5/Solver.java | 38 ------------------ src/api/java/io/github/cvc5/Sort.java | 14 ------- src/api/java/io/github/cvc5/Term.java | 16 -------- test/unit/api/java/DatatypeTest.java | 53 +++++++++++++++---------- test/unit/api/java/SolverTest.java | 4 +- test/unit/api/java/TermTest.java | 19 +++++---- 6 files changed, 45 insertions(+), 99 deletions(-) diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java index 9fcb261d3..908e90dc5 100644 --- 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 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 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 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 65ff8e49d..a5d4a539a 100644 --- 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 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 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 a0a0620ac..a60b11427 100644 --- 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, 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 terms, List 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 354d8662f..bc13ab634 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -97,7 +97,8 @@ class DatatypeTest dtdecls.add(list); AtomicReference 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 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 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 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 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 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 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 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 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 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 iargs = new ArrayList<>(); iargs.add(isort); - Sort listInt = dtsorts[0].instantiate(iargs); + Sort listInt = dtsorts[0].instantiate(iargs.toArray(new Sort[0])); AtomicReference 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 5515fa649..4d5c35472 100644 --- 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 239e3262d..3ecddb82c 100644 --- 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 -- 2.30.2