From a7352156510fc2d43ea764d75f8da511d2401ea7 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 1 Apr 2022 14:36:07 -0700 Subject: [PATCH] api: Remove Datatype::getConstructorTerm(). (#8529) --- examples/api/cpp/datatypes.cpp | 22 ++++++---- examples/api/java/Datatypes.java | 11 ++--- examples/api/python/datatypes.py | 14 +++--- src/api/cpp/cvc5.cpp | 10 ----- src/api/cpp/cvc5.h | 10 ----- src/api/cpp/cvc5_kind.h | 3 +- src/api/java/io/github/cvc5/Datatype.java | 16 ------- src/api/java/jni/datatype.cpp | 18 -------- src/api/python/cvc5.pxd | 1 - src/api/python/cvc5.pxi | 10 ----- test/unit/api/cpp/solver_black.cpp | 52 +++++++++++------------ test/unit/api/cpp/solver_white.cpp | 4 +- test/unit/api/cpp/term_black.cpp | 4 +- test/unit/api/cpp/term_white.cpp | 4 +- test/unit/api/java/SolverTest.java | 35 +++++++-------- test/unit/api/java/TermTest.java | 4 +- test/unit/api/python/test_solver.py | 45 ++++++++++---------- test/unit/api/python/test_term.py | 4 +- 18 files changed, 101 insertions(+), 166 deletions(-) diff --git a/examples/api/cpp/datatypes.cpp b/examples/api/cpp/datatypes.cpp index 08346568e..6d201cc3b 100644 --- a/examples/api/cpp/datatypes.cpp +++ b/examples/api/cpp/datatypes.cpp @@ -37,14 +37,17 @@ void test(Solver& slv, Sort& consListSort) // APPLY_CONSTRUCTOR, even though it has no arguments. Term t = slv.mkTerm( APPLY_CONSTRUCTOR, - {consList.getConstructorTerm("cons"), + {consList.getConstructor("cons").getConstructorTerm(), slv.mkInteger(0), - slv.mkTerm(APPLY_CONSTRUCTOR, {consList.getConstructorTerm("nil")})}); + slv.mkTerm(APPLY_CONSTRUCTOR, + {consList.getConstructor("nil").getConstructorTerm()})}); std::cout << "t is " << t << std::endl << "sort of cons is " - << consList.getConstructorTerm("cons").getSort() << std::endl - << "sort of nil is " << consList.getConstructorTerm("nil").getSort() + << consList.getConstructor("cons").getConstructorTerm().getSort() + << std::endl + << "sort of nil is " + << consList.getConstructor("nil").getConstructorTerm().getSort() << std::endl; // t2 = head(cons 0 nil), and of course this can be evaluated @@ -130,11 +133,12 @@ void test(Solver& slv, Sort& consListSort) Term head_a = slv.mkTerm(APPLY_SELECTOR, {paramConsList["cons"].getSelectorTerm("head"), a}); - std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() - << std::endl - << "sort of cons is " - << paramConsList.getConstructorTerm("cons").getSort() << std::endl - << std::endl; + std::cout + << "head_a is " << head_a << " of sort " << head_a.getSort() << std::endl + << "sort of cons is " + << paramConsList.getConstructor("cons").getConstructorTerm().getSort() + << std::endl + << std::endl; Term assertion = slv.mkTerm(GT, {head_a, slv.mkInteger(50)}); std::cout << "Assert " << assertion << std::endl; diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java index 35d6914f1..c60ca7908 100644 --- a/examples/api/java/Datatypes.java +++ b/examples/api/java/Datatypes.java @@ -35,13 +35,13 @@ public class Datatypes // "nil" is a constructor too, so it needs to be applied with // APPLY_CONSTRUCTOR, even though it has no arguments. Term t = slv.mkTerm(Kind.APPLY_CONSTRUCTOR, - consList.getConstructorTerm("cons"), + consList.getConstructor("cons").getConstructorTerm(), slv.mkInteger(0), - slv.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + slv.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructor("nil").getConstructorTerm())); System.out.println("t is " + t + "\n" - + "sort of cons is " + consList.getConstructorTerm("cons").getSort() + "\n" - + "sort of nil is " + consList.getConstructorTerm("nil").getSort()); + + "sort of cons is " + consList.getConstructor("cons").getConstructorTerm().getSort() + "\n" + + "sort of nil is " + consList.getConstructor("nil").getConstructorTerm().getSort()); // t2 = head(cons 0 nil), and of course this can be evaluated // @@ -126,7 +126,8 @@ public class Datatypes Term head_a = slv.mkTerm( Kind.APPLY_SELECTOR, paramConsList.getConstructor("cons").getSelectorTerm("head"), a); System.out.println("head_a is " + head_a + " of sort " + head_a.getSort() + "\n" - + "sort of cons is " + paramConsList.getConstructorTerm("cons").getSort() + "\n"); + + "sort of cons is " + paramConsList.getConstructor("cons").getConstructorTerm().getSort() + + "\n"); Term assertion = slv.mkTerm(Kind.GT, head_a, slv.mkInteger(50)); System.out.println("Assert " + assertion); slv.assertFormula(assertion); diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index 23704fa7c..85cecc9e4 100644 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -35,15 +35,16 @@ def test(slv, consListSort): # "nil" is a constructor too t = slv.mkTerm( - Kind.APPLY_CONSTRUCTOR, consList.getConstructorTerm("cons"), + Kind.APPLY_CONSTRUCTOR, + consList.getConstructor("cons").getConstructorTerm(), slv.mkInteger(0), - slv.mkTerm( - Kind.APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))) + slv.mkTerm(Kind.APPLY_CONSTRUCTOR, + consList.getConstructor("nil").getConstructorTerm())) print("t is {}\nsort of cons is {}\n sort of nil is {}".format( t, - consList.getConstructorTerm("cons").getSort(), - consList.getConstructorTerm("nil").getSort())) + consList.getConstructor("cons").getConstructorTerm().getSort(), + consList.getConstructor("nil").getConstructorTerm().getSort())) # t2 = head(cons 0 nil), and of course this can be evaluated # @@ -101,7 +102,8 @@ def test(slv, consListSort): paramConsList["cons"].getSelectorTerm("head"), a) print("head_a is {} of sort {}".format(head_a, head_a.getSort())) - print("sort of cons is", paramConsList.getConstructorTerm("cons").getSort()) + print("sort of cons is", + paramConsList.getConstructor("cons").getConstructorTerm().getSort()) assertion = slv.mkTerm(Kind.GT, head_a, slv.mkInteger(50)) print("Assert", assertion) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index beaa4887a..b4cc4cab2 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -3943,16 +3943,6 @@ DatatypeConstructor Datatype::getConstructor(const std::string& name) const CVC5_API_TRY_CATCH_END; } -Term Datatype::getConstructorTerm(const std::string& name) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - //////// all checks before this line - return getConstructorForName(name).getConstructorTerm(); - //////// - CVC5_API_TRY_CATCH_END; -} - DatatypeSelector Datatype::getSelector(const std::string& name) const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 147700fe5..65337fc51 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2283,16 +2283,6 @@ class CVC5_EXPORT Datatype DatatypeConstructor operator[](const std::string& name) const; DatatypeConstructor getConstructor(const std::string& name) const; - /** - * Get a term representing the datatype constructor with the given name. - * This is a linear search through the constructors, so in case of multiple, - * similarly-named constructors, the - * first is returned. - * @param name the name of the datatype constructor - * @return a Term representing the datatype constructor with the given name - */ - Term getConstructorTerm(const std::string& name) const; - /** * Get the datatype constructor with the given name. * This is a linear search through the constructors and their selectors, so diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 1506321b9..e8fe14a4b 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -2110,8 +2110,7 @@ enum Kind : int32_t * * - Arity: `n > 0` * - `1:` DatatypeConstructor Term - * (see DatatypeConstructor::getConstructorTerm() const, - * Datatype::getConstructorTerm(const std::string&) const) + * (see DatatypeConstructor::getConstructorTerm() const) * - `2..n:` Terms of the Sorts of the selectors of the constructor (the arguments to the constructor) * * - Create Term of this Kind with: diff --git a/src/api/java/io/github/cvc5/Datatype.java b/src/api/java/io/github/cvc5/Datatype.java index cfe0614ef..06ceaa67f 100644 --- a/src/api/java/io/github/cvc5/Datatype.java +++ b/src/api/java/io/github/cvc5/Datatype.java @@ -63,22 +63,6 @@ public class Datatype extends AbstractPointer implements IterableGetStringUTFChars(jName, nullptr); - std::string cName(s); - Term* retPointer = new Term(current->getConstructorTerm(cName)); - env->ReleaseStringUTFChars(jName, s); - return ((jlong)retPointer); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} - /* * Class: io_github_cvc5_Datatype * Method: getName diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index bfde85399..b823816ca 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -58,7 +58,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": DatatypeConstructor operator[](size_t idx) except + DatatypeConstructor operator[](const string& name) except + DatatypeConstructor getConstructor(const string& name) except + - Term getConstructorTerm(const string& name) except + DatatypeSelector getSelector(const string& name) except + string getName() except + size_t getNumConstructors() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 62b45de73..524f067ce 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -120,16 +120,6 @@ cdef class Datatype: dc.cdc = self.cd.getConstructor(name.encode()) return dc - def getConstructorTerm(self, str name): - """ - :param name: The name of the constructor. - :return: The term representing the datatype constructor with the - given name. - """ - cdef Term term = Term(self.solver) - term.cterm = self.cd.getConstructorTerm(name.encode()) - return term - def getSelector(self, str name): """ :param name: The name of the selector.. diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 204d270a0..3cec83f81 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -854,26 +854,23 @@ TEST_F(TestApiBlackSolver, mkTermFromOp) Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms - Term consTerm1 = list.getConstructorTerm("cons"); - Term consTerm2 = list.getConstructor("cons").getConstructorTerm(); - Term nilTerm1 = list.getConstructorTerm("nil"); - Term nilTerm2 = list.getConstructor("nil").getConstructorTerm(); + Term consTerm = list.getConstructor("cons").getConstructorTerm(); + Term nilTerm = list.getConstructor("nil").getConstructorTerm(); Term headTerm1 = list["cons"].getSelectorTerm("head"); Term headTerm2 = list["cons"].getSelector("head").getSelectorTerm(); Term tailTerm1 = list["cons"].getSelectorTerm("tail"); Term tailTerm2 = list["cons"]["tail"].getSelectorTerm(); // mkTerm(Op op, Term term) const - ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm1})); - ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm2})); - ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {nilTerm1}), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {consTerm1}), CVC5ApiException); - ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {consTerm2}), + ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm})); + ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {nilTerm}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {consTerm}), CVC5ApiException); + ASSERT_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {consTerm}), CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(APPLY_SELECTOR, {headTerm1}), CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException); - ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, {nilTerm1}), CVC5ApiException); + ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}), CVC5ApiException); // mkTerm(Op op, Term child) const ASSERT_NO_THROW(d_solver.mkTerm(opterm1, {a})); @@ -883,16 +880,16 @@ TEST_F(TestApiBlackSolver, mkTermFromOp) ASSERT_THROW(d_solver.mkTerm(opterm2, {a}), CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(opterm1, {Term()}), CVC5ApiException); ASSERT_THROW( - d_solver.mkTerm(APPLY_CONSTRUCTOR, {consTerm1, d_solver.mkInteger(0)}), + d_solver.mkTerm(APPLY_CONSTRUCTOR, {consTerm, d_solver.mkInteger(0)}), CVC5ApiException); ASSERT_THROW(slv.mkTerm(opterm1, {a}), CVC5ApiException); // mkTerm(Op op, Term child1, Term child2) const ASSERT_NO_THROW( d_solver.mkTerm(APPLY_CONSTRUCTOR, - {consTerm1, + {consTerm, d_solver.mkInteger(0), - d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm1})})); + d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm})})); ASSERT_THROW( d_solver.mkTerm(opterm2, {d_solver.mkInteger(1), d_solver.mkInteger(2)}), CVC5ApiException); @@ -902,9 +899,9 @@ TEST_F(TestApiBlackSolver, mkTermFromOp) ASSERT_THROW(d_solver.mkTerm(opterm2, {Term(), d_solver.mkInteger(1)}), CVC5ApiException); ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, - {consTerm1, + {consTerm, d_solver.mkInteger(0), - d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm1})}), + d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm})}), CVC5ApiException); // mkTerm(Op op, Term child1, Term child2, Term child3) const @@ -1505,8 +1502,8 @@ TEST_F(TestApiBlackSolver, getOp) Sort consListSort = d_solver.mkDatatypeSort(consListSpec); Datatype consList = consListSort.getDatatype(); - Term consTerm = consList.getConstructorTerm("cons"); - Term nilTerm = consList.getConstructorTerm("nil"); + Term consTerm = consList.getConstructor("cons").getConstructorTerm(); + Term nilTerm = consList.getConstructor("nil").getConstructorTerm(); Term headTerm = consList["cons"].getSelectorTerm("head"); Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}); @@ -2369,12 +2366,12 @@ TEST_F(TestApiBlackSolver, simplify) ASSERT_EQ(i1, d_solver.simplify(i3)); Datatype consList = consListSort.getDatatype(); - Term dt1 = - d_solver.mkTerm(APPLY_CONSTRUCTOR, - {consList.getConstructorTerm("cons"), - d_solver.mkInteger(0), - d_solver.mkTerm(APPLY_CONSTRUCTOR, - {consList.getConstructorTerm("nil")})}); + Term dt1 = d_solver.mkTerm( + APPLY_CONSTRUCTOR, + {consList.getConstructor("cons").getConstructorTerm(), + d_solver.mkInteger(0), + d_solver.mkTerm(APPLY_CONSTRUCTOR, + {consList.getConstructor("nil").getConstructorTerm()})}); ASSERT_NO_THROW(d_solver.simplify(dt1)); Term dt2 = d_solver.mkTerm(APPLY_SELECTOR, {consList["cons"].getSelectorTerm("head"), dt1}); @@ -2934,9 +2931,9 @@ TEST_F(TestApiBlackSolver, proj_issue373) Term t452 = d_solver.mkVar(s1, "_x281"); Term bvl = d_solver.mkTerm(d_solver.mkOp(VARIABLE_LIST), {t452}); - Term acons = - d_solver.mkTerm(d_solver.mkOp(APPLY_CONSTRUCTOR), - {s4.getDatatype().getConstructorTerm("_x115"), t452}); + Term acons = d_solver.mkTerm( + d_solver.mkOp(APPLY_CONSTRUCTOR), + {s4.getDatatype().getConstructor("_x115").getConstructorTerm(), t452}); // type exception ASSERT_THROW( d_solver.mkTerm(d_solver.mkOp(APPLY_CONSTRUCTOR), {bvl, acons, t452}), @@ -2977,7 +2974,8 @@ TEST_F(TestApiBlackSolver, proj_issue378) Sort s7 = d_solver.mkDatatypeSort(dtdecl); Sort s9 = s7.instantiate({s2}); Term t1507 = d_solver.mkTerm( - APPLY_CONSTRUCTOR, {s9.getDatatype().getConstructorTerm("_x184"), t7}); + APPLY_CONSTRUCTOR, + {s9.getDatatype().getConstructor("_x184").getConstructorTerm(), t7}); ASSERT_NO_THROW(d_solver.mkTerm( APPLY_UPDATER, {s9.getDatatype().getConstructor("_x186").getSelectorTerm("_x185"), diff --git a/test/unit/api/cpp/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp index 7699b9ae2..037f686b0 100644 --- a/test/unit/api/cpp/solver_white.cpp +++ b/test/unit/api/cpp/solver_white.cpp @@ -36,8 +36,8 @@ TEST_F(TestApiWhiteSolver, getOp) Sort consListSort = d_solver.mkDatatypeSort(consListSpec); Datatype consList = consListSort.getDatatype(); - Term nilTerm = consList.getConstructorTerm("nil"); - Term consTerm = consList.getConstructorTerm("cons"); + Term nilTerm = consList.getConstructor("nil").getConstructorTerm(); + Term consTerm = consList.getConstructor("cons").getConstructorTerm(); Term headTerm = consList["cons"].getSelectorTerm("head"); Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}); diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp index 45f53183b..82417abe4 100644 --- a/test/unit/api/cpp/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -188,8 +188,8 @@ TEST_F(TestApiBlackTerm, getOp) Term c = d_solver.mkConst(intListSort, "c"); Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms - Term consOpTerm = list.getConstructorTerm("cons"); - Term nilOpTerm = list.getConstructorTerm("nil"); + Term consOpTerm = list.getConstructor("cons").getConstructorTerm(); + Term nilOpTerm = list.getConstructor("nil").getConstructorTerm(); Term headOpTerm = list["cons"].getSelectorTerm("head"); Term tailOpTerm = list["cons"].getSelectorTerm("tail"); diff --git a/test/unit/api/cpp/term_white.cpp b/test/unit/api/cpp/term_white.cpp index 74f9baf1b..8f79e1bb6 100644 --- a/test/unit/api/cpp/term_white.cpp +++ b/test/unit/api/cpp/term_white.cpp @@ -63,8 +63,8 @@ TEST_F(TestApiWhiteTerm, getOp) Term c = d_solver.mkConst(intListSort, "c"); Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms - Term consOpTerm = list.getConstructorTerm("cons"); - Term nilOpTerm = list.getConstructorTerm("nil"); + Term consOpTerm = list.getConstructor("cons").getConstructorTerm(); + Term nilOpTerm = list.getConstructor("nil").getConstructorTerm(); Term headOpTerm = list["cons"].getSelectorTerm("head"); Term tailOpTerm = list["cons"].getSelectorTerm("tail"); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 33ebd2ddb..0f5f80e89 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -838,25 +838,22 @@ class SolverTest Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms - Term consTerm1 = list.getConstructorTerm("cons"); - Term consTerm2 = list.getConstructor("cons").getConstructorTerm(); - Term nilTerm1 = list.getConstructorTerm("nil"); - Term nilTerm2 = list.getConstructor("nil").getConstructorTerm(); + Term consTerm = list.getConstructor("cons").getConstructorTerm(); + Term nilTerm = list.getConstructor("nil").getConstructorTerm(); Term headTerm1 = list.getConstructor("cons").getSelectorTerm("head"); Term headTerm2 = list.getConstructor("cons").getSelector("head").getSelectorTerm(); Term tailTerm1 = list.getConstructor("cons").getSelectorTerm("tail"); Term tailTerm2 = list.getConstructor("cons").getSelector("tail").getSelectorTerm(); // mkTerm(Op op, Term term) const - assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)); - assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm2)); - assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, nilTerm1)); - assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, consTerm1)); - assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm2)); + assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm)); + assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, nilTerm)); + assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, consTerm)); + assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm)); assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1)); assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, headTerm1)); assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1)); - assertThrows(CVC5ApiException.class, () -> slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)); + assertThrows(CVC5ApiException.class, () -> slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm)); // mkTerm(Op op, Term child) const assertDoesNotThrow(() -> d_solver.mkTerm(opterm1, a)); @@ -866,16 +863,16 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, a)); assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1, d_solver.getNullTerm())); assertThrows(CVC5ApiException.class, - () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver.mkInteger(0))); + () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(0))); assertThrows(CVC5ApiException.class, () -> slv.mkTerm(opterm1, a)); // mkTerm(Op op, Term child1, Term child2) const assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, - consTerm1, + consTerm, d_solver.mkInteger(0), - d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1))); + d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm))); assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, d_solver.mkInteger(1), d_solver.mkInteger(2))); @@ -889,9 +886,9 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> slv.mkTerm(APPLY_CONSTRUCTOR, - consTerm1, + consTerm, d_solver.mkInteger(0), - d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1))); + d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm))); // mkTerm(Op op, Term child1, Term child2, Term child3) const assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1, a, b, a)); @@ -1550,8 +1547,8 @@ class SolverTest Sort consListSort = d_solver.mkDatatypeSort(consListSpec); Datatype consList = consListSort.getDatatype(); - Term consTerm = consList.getConstructorTerm("cons"); - Term nilTerm = consList.getConstructorTerm("nil"); + Term consTerm = consList.getConstructor("cons").getConstructorTerm(); + Term nilTerm = consList.getConstructor("nil").getConstructorTerm(); Term headTerm = consList.getConstructor("cons").getSelectorTerm("head"); Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm); @@ -2423,9 +2420,9 @@ class SolverTest Datatype consList = consListSort.getDatatype(); Term dt1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, - consList.getConstructorTerm("cons"), + consList.getConstructor("cons").getConstructorTerm(), d_solver.mkInteger(0), - d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructor("nil").getConstructorTerm())); assertDoesNotThrow(() -> d_solver.simplify(dt1)); Term dt2 = d_solver.mkTerm( APPLY_SELECTOR, consList.getConstructor("cons").getSelectorTerm("head"), dt1); diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index 3725a7be0..239e3262d 100644 --- a/test/unit/api/java/TermTest.java +++ b/test/unit/api/java/TermTest.java @@ -222,8 +222,8 @@ class TermTest Term c = d_solver.mkConst(intListSort, "c"); Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms - Term consOpTerm = list.getConstructorTerm("cons"); - Term nilOpTerm = list.getConstructorTerm("nil"); + Term consOpTerm = list.getConstructor("cons").getConstructorTerm(); + Term nilOpTerm = list.getConstructor("nil").getConstructorTerm(); } @Test diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index c27cef850..ac8c8b073 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -817,24 +817,22 @@ def test_mk_term_from_op(solver): lis = listSort.getDatatype() # list datatype constructor and selector operator terms - consTerm1 = lis.getConstructorTerm("cons") - consTerm2 = lis.getConstructor("cons").getConstructorTerm() - nilTerm1 = lis.getConstructorTerm("nil") - nilTerm2 = lis.getConstructor("nil").getConstructorTerm() + consTerm = lis.getConstructor("cons").getConstructorTerm() + nilTerm = lis.getConstructor("nil").getConstructorTerm() headTerm1 = lis["cons"].getSelectorTerm("head") headTerm2 = lis["cons"].getSelector("head").getSelectorTerm() tailTerm1 = lis["cons"].getSelectorTerm("tail") tailTerm2 = lis["cons"]["tail"].getSelectorTerm() # mkTerm(Op op, Term term) const - solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm1) - solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm2) + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm) + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.APPLY_SELECTOR, nilTerm1) + solver.mkTerm(Kind.APPLY_SELECTOR, nilTerm) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.APPLY_SELECTOR, consTerm1) + solver.mkTerm(Kind.APPLY_SELECTOR, consTerm) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm2) + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm) with pytest.raises(RuntimeError): solver.mkTerm(opterm1) with pytest.raises(RuntimeError): @@ -842,7 +840,7 @@ def test_mk_term_from_op(solver): with pytest.raises(RuntimeError): solver.mkTerm(opterm1) with pytest.raises(RuntimeError): - slv.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm1) + slv.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm) # mkTerm(Op op, Term child) const solver.mkTerm(opterm1, a) @@ -854,13 +852,13 @@ def test_mk_term_from_op(solver): with pytest.raises(RuntimeError): solver.mkTerm(opterm1, cvc5.Term(solver)) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm1, solver.mkInteger(0)) + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm, solver.mkInteger(0)) with pytest.raises(RuntimeError): slv.mkTerm(opterm1, a) # mkTerm(Op op, Term child1, Term child2) const - solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm1, solver.mkInteger(0), - solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm1)) + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm, solver.mkInteger(0), + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)) with pytest.raises(RuntimeError): solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2)) with pytest.raises(RuntimeError): @@ -871,9 +869,9 @@ def test_mk_term_from_op(solver): solver.mkTerm(opterm2, cvc5.Term(solver), solver.mkInteger(1)) with pytest.raises(RuntimeError): slv.mkTerm(Kind.APPLY_CONSTRUCTOR,\ - consTerm1,\ + consTerm,\ solver.mkInteger(0),\ - solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm1)) + solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm)) # mkTerm(Op op, Term child1, Term child2, Term child3) const with pytest.raises(RuntimeError): @@ -1151,8 +1149,8 @@ def test_get_op(solver): consListSort = solver.mkDatatypeSort(consListSpec) consList = consListSort.getDatatype() - consTerm = consList.getConstructorTerm("cons") - nilTerm = consList.getConstructorTerm("nil") + consTerm = consList.getConstructor("cons").getConstructorTerm() + nilTerm = consList.getConstructor("nil").getConstructorTerm() headTerm = consList["cons"].getSelectorTerm("head") listnil = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm) @@ -1716,14 +1714,15 @@ def test_simplify(solver): assert i1 == solver.simplify(i3) consList = consListSort.getDatatype() - dt1 = solver.mkTerm(\ - Kind.APPLY_CONSTRUCTOR,\ - consList.getConstructorTerm("cons"),\ - solver.mkInteger(0),\ + dt1 = solver.mkTerm( + Kind.APPLY_CONSTRUCTOR, + consList.getConstructor("cons").getConstructorTerm(), + solver.mkInteger(0), solver.mkTerm( - Kind.APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))) + Kind.APPLY_CONSTRUCTOR, + consList.getConstructor("nil").getConstructorTerm())) solver.simplify(dt1) - dt2 = solver.mkTerm(\ + dt2 = solver.mkTerm( Kind.APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1) solver.simplify(dt2) diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index 5cac4b89f..5af769267 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -187,8 +187,8 @@ def test_get_op(solver): c = solver.mkConst(intListSort, "c") list1 = listSort.getDatatype() # list datatype constructor and selector operator terms - consOpTerm = list1.getConstructorTerm("cons") - nilOpTerm = list1.getConstructorTerm("nil") + consOpTerm = list1.getConstructor("cons").getConstructorTerm() + nilOpTerm = list1.getConstructor("nil").getConstructorTerm() headOpTerm = list1["cons"].getSelectorTerm("head") tailOpTerm = list1["cons"].getSelectorTerm("tail") -- 2.30.2