From 93247764b867d5b02ecc0c9d150b184d4c997a2a Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 1 Apr 2022 18:53:15 -0700 Subject: [PATCH] api: Remove DatatypeConstructor::getSelectorTerm(). (#8535) --- examples/api/cpp/datatypes.cpp | 8 ++-- examples/api/java/Datatypes.java | 10 +++-- examples/api/python/datatypes.py | 11 ++++-- src/api/cpp/cvc5.cpp | 10 ----- src/api/cpp/cvc5.h | 12 +++--- src/api/cpp/cvc5_kind.h | 2 +- .../io/github/cvc5/DatatypeConstructor.java | 14 ------- src/api/java/jni/datatype_constructor.cpp | 21 ---------- src/api/python/cvc5.pxd | 1 - src/api/python/cvc5.pxi | 10 ----- test/unit/api/cpp/solver_black.cpp | 39 ++++++++++--------- test/unit/api/cpp/solver_white.cpp | 2 +- test/unit/api/cpp/term_black.cpp | 4 +- test/unit/api/cpp/term_white.cpp | 4 +- test/unit/api/java/SolverTest.java | 16 ++++---- test/unit/api/python/test_solver.py | 18 ++++----- test/unit/api/python/test_term.py | 4 +- 17 files changed, 68 insertions(+), 118 deletions(-) diff --git a/examples/api/cpp/datatypes.cpp b/examples/api/cpp/datatypes.cpp index 6d201cc3b..75e4a97d1 100644 --- a/examples/api/cpp/datatypes.cpp +++ b/examples/api/cpp/datatypes.cpp @@ -56,7 +56,8 @@ void test(Solver& slv, Sort& consListSort) // consList["cons"]) in order to get the "head" selector symbol // to apply. Term t2 = - slv.mkTerm(APPLY_SELECTOR, {consList["cons"].getSelectorTerm("head"), t}); + slv.mkTerm(APPLY_SELECTOR, + {consList["cons"].getSelector("head").getSelectorTerm(), t}); std::cout << "t2 is " << t2 << std::endl << "simplify(t2) is " << slv.simplify(t2) << std::endl @@ -131,8 +132,9 @@ void test(Solver& slv, Sort& consListSort) Term a = slv.mkConst(paramConsIntListSort, "a"); std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; - Term head_a = slv.mkTerm(APPLY_SELECTOR, - {paramConsList["cons"].getSelectorTerm("head"), a}); + Term head_a = slv.mkTerm( + APPLY_SELECTOR, + {paramConsList["cons"].getSelector("head").getSelectorTerm(), a}); std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() << std::endl << "sort of cons is " diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java index c60ca7908..0f70ce0dc 100644 --- a/examples/api/java/Datatypes.java +++ b/examples/api/java/Datatypes.java @@ -48,8 +48,9 @@ public class Datatypes // Here we first get the DatatypeConstructor for cons (with // consList["cons"]) in order to get the "head" selector symbol // to apply. - Term t2 = - slv.mkTerm(Kind.APPLY_SELECTOR, consList.getConstructor("cons").getSelectorTerm("head"), t); + Term t2 = slv.mkTerm(Kind.APPLY_SELECTOR, + consList.getConstructor("cons").getSelector("head").getSelectorTerm(), + t); System.out.println("t2 is " + t2 + "\n" + "simplify(t2) is " + slv.simplify(t2) + "\n"); @@ -123,8 +124,9 @@ public class Datatypes Term a = slv.mkConst(paramConsIntListSort, "a"); System.out.println("term " + a + " is of sort " + a.getSort()); - Term head_a = slv.mkTerm( - Kind.APPLY_SELECTOR, paramConsList.getConstructor("cons").getSelectorTerm("head"), a); + Term head_a = slv.mkTerm(Kind.APPLY_SELECTOR, + paramConsList.getConstructor("cons").getSelector("head").getSelectorTerm(), + a); System.out.println("head_a is " + head_a + " of sort " + head_a.getSort() + "\n" + "sort of cons is " + paramConsList.getConstructor("cons").getConstructorTerm().getSort() + "\n"); diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index 85cecc9e4..39642297c 100644 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -38,8 +38,9 @@ def test(slv, consListSort): Kind.APPLY_CONSTRUCTOR, consList.getConstructor("cons").getConstructorTerm(), slv.mkInteger(0), - slv.mkTerm(Kind.APPLY_CONSTRUCTOR, - consList.getConstructor("nil").getConstructorTerm())) + slv.mkTerm( + Kind.APPLY_CONSTRUCTOR, + consList.getConstructor("nil").getConstructorTerm())) print("t is {}\nsort of cons is {}\n sort of nil is {}".format( t, @@ -53,7 +54,9 @@ def test(slv, consListSort): # to apply. t2 = slv.mkTerm( - Kind.APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t) + Kind.APPLY_SELECTOR, + consList["cons"].getSelector("head").getSelectorTerm(), + t) print("t2 is {}\nsimplify(t2) is {}\n\n".format(t2, slv.simplify(t2))) @@ -99,7 +102,7 @@ def test(slv, consListSort): head_a = slv.mkTerm( Kind.APPLY_SELECTOR, - paramConsList["cons"].getSelectorTerm("head"), + paramConsList["cons"].getSelector("head").getSelectorTerm(), a) print("head_a is {} of sort {}".format(head_a, head_a.getSort())) print("sort of cons is", diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 89cd72f3f..26da68abc 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -3762,16 +3762,6 @@ DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const CVC5_API_TRY_CATCH_END; } -Term DatatypeConstructor::getSelectorTerm(const std::string& name) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - //////// all checks before this line - return getSelector(name).getSelectorTerm(); - //////// - CVC5_API_TRY_CATCH_END; -} - DatatypeConstructor::const_iterator DatatypeConstructor::begin() const { return DatatypeConstructor::const_iterator(d_solver, *d_ctor, true); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3470884e1..7bf71accd 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2155,16 +2155,14 @@ class CVC5_EXPORT DatatypeConstructor * @return the first datatype selector with the given name */ DatatypeSelector operator[](const std::string& name) const; - DatatypeSelector getSelector(const std::string& name) const; - /** - * Get the term representation of the datatype selector with the given name. - * This is a linear search through the arguments, so in case of multiple, - * similarly-named arguments, the selector for the first is returned. + * Get the datatype selector with the given name. + * This is a linear search through the selectors, so in case of + * multiple, similarly-named selectors, the first is returned. * @param name the name of the datatype selector - * @return a term representing the datatype selector with the given name + * @return the first datatype selector with the given name */ - Term getSelectorTerm(const std::string& name) const; + DatatypeSelector getSelector(const std::string& name) const; /** * @return true if this DatatypeConstructor is a null object diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 464415372..1d5c2da90 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -2555,7 +2555,7 @@ enum Kind : int32_t * * - Arity: ``2`` * - * - ``1:`` DatatypeSelector Term (see DatatypeSelector::getSelectorTerm() const, DatatypeConstructor::getSelectorTerm(const std::string&) const) + * - ``1:`` DatatypeSelector Term (see DatatypeSelector::getSelectorTerm() const) * - ``2:`` Term of the codomain Sort of the selector * * - Create Term of this Kind with: diff --git a/src/api/java/io/github/cvc5/DatatypeConstructor.java b/src/api/java/io/github/cvc5/DatatypeConstructor.java index 808328946..e3e482fee 100644 --- a/src/api/java/io/github/cvc5/DatatypeConstructor.java +++ b/src/api/java/io/github/cvc5/DatatypeConstructor.java @@ -137,20 +137,6 @@ public class DatatypeConstructor extends AbstractPointer implements IterableGetStringUTFChars(jName, nullptr); - std::string cName(s); - Term* retPointer = new Term(current->getSelectorTerm(cName)); - env->ReleaseStringUTFChars(jName, s); - return (jlong)retPointer; - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} - /* * Class: io_github_cvc5_DatatypeConstructor * Method: isNull diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 7f5bf10ef..65bb821f9 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -90,7 +90,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": Term getTesterTerm() except + size_t getNumSelectors() except + DatatypeSelector getSelector(const string& name) except + - Term getSelectorTerm(const string& name) except + bint isNull() except + string toString() except + cppclass const_iterator: diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index f39b9cf04..8fc4904e7 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -333,16 +333,6 @@ cdef class DatatypeConstructor: ds.cds = self.cdc.getSelector(name.encode()) return ds - def getSelectorTerm(self, str name): - """ - :param name: The name of the datatype selector. - :return: A term representing the firstdatatype selector with the - given name. - """ - cdef Term term = Term(self.solver) - term.cterm = self.cdc.getSelectorTerm(name.encode()) - return term - def isNull(self): """ :return: True if this DatatypeConstructor is a null object. diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index cf048ce4f..7461a879e 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -854,10 +854,8 @@ TEST_F(TestApiBlackSolver, mkTermFromOp) // list datatype constructor and selector operator terms 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(); + Term headTerm = list["cons"].getSelector("head").getSelectorTerm(); + Term tailTerm = list["cons"]["tail"].getSelectorTerm(); // mkTerm(Op op, Term term) const ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm})); @@ -866,15 +864,15 @@ TEST_F(TestApiBlackSolver, mkTermFromOp) 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(APPLY_SELECTOR, {headTerm}), CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(opterm1), CVC5ApiException); ASSERT_THROW(slv.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}), CVC5ApiException); // mkTerm(Op op, Term child) const ASSERT_NO_THROW(d_solver.mkTerm(opterm1, {a})); ASSERT_NO_THROW(d_solver.mkTerm(opterm2, {d_solver.mkInteger(1)})); - ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, {headTerm1, c})); - ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, {tailTerm2, c})); + ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, {headTerm, c})); + ASSERT_NO_THROW(d_solver.mkTerm(APPLY_SELECTOR, {tailTerm, c})); ASSERT_THROW(d_solver.mkTerm(opterm2, {a}), CVC5ApiException); ASSERT_THROW(d_solver.mkTerm(opterm1, {Term()}), CVC5ApiException); ASSERT_THROW( @@ -1502,7 +1500,7 @@ TEST_F(TestApiBlackSolver, getOp) Term consTerm = consList.getConstructor("cons").getConstructorTerm(); Term nilTerm = consList.getConstructor("nil").getConstructorTerm(); - Term headTerm = consList["cons"].getSelectorTerm("head"); + Term headTerm = consList["cons"].getSelector("head").getSelectorTerm(); Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}); Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, @@ -2371,8 +2369,9 @@ TEST_F(TestApiBlackSolver, simplify) 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}); + Term dt2 = d_solver.mkTerm( + APPLY_SELECTOR, + {consList["cons"].getSelector("head").getSelectorTerm(), dt1}); ASSERT_NO_THROW(d_solver.simplify(dt2)); Term b1 = d_solver.mkVar(bvSort, "b1"); @@ -2974,11 +2973,13 @@ TEST_F(TestApiBlackSolver, proj_issue378) Term t1507 = d_solver.mkTerm( APPLY_CONSTRUCTOR, {s9.getDatatype().getConstructor("_x184").getConstructorTerm(), t7}); - ASSERT_NO_THROW(d_solver.mkTerm( - APPLY_UPDATER, - {s9.getDatatype().getConstructor("_x186").getSelectorTerm("_x185"), - t1507, - t7})); + ASSERT_NO_THROW(d_solver.mkTerm(APPLY_UPDATER, + {s9.getDatatype() + .getConstructor("_x186") + .getSelector("_x185") + .getSelectorTerm(), + t1507, + t7})); } TEST_F(TestApiBlackSolver, proj_issue379) @@ -3342,9 +3343,11 @@ TEST_F(TestApiBlackSolver, projIssue431) Sort s14 = slv.mkDatatypeSorts({_dt46})[0]; Term t31 = slv.mkConst(s7, "_x100"); Term t47 = slv.mkConst(s14, "_x112"); - Term sel = - t47.getSort().getDatatype().getConstructor("_cons64").getSelectorTerm( - "_sel62"); + Term sel = t47.getSort() + .getDatatype() + .getConstructor("_cons64") + .getSelector("_sel62") + .getSelectorTerm(); Term t274 = slv.mkTerm(APPLY_SELECTOR, {sel, t47}); Term t488 = slv.mkTerm(Kind::APPLY_UF, {t31, t274}); slv.assertFormula({t488}); diff --git a/test/unit/api/cpp/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp index 037f686b0..ab2b87831 100644 --- a/test/unit/api/cpp/solver_white.cpp +++ b/test/unit/api/cpp/solver_white.cpp @@ -38,7 +38,7 @@ TEST_F(TestApiWhiteSolver, getOp) Term nilTerm = consList.getConstructor("nil").getConstructorTerm(); Term consTerm = consList.getConstructor("cons").getConstructorTerm(); - Term headTerm = consList["cons"].getSelectorTerm("head"); + Term headTerm = consList["cons"].getSelector("head").getSelectorTerm(); Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}); Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp index 82417abe4..c1034cf1d 100644 --- a/test/unit/api/cpp/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -190,8 +190,8 @@ TEST_F(TestApiBlackTerm, getOp) // list datatype constructor and selector operator terms Term consOpTerm = list.getConstructor("cons").getConstructorTerm(); Term nilOpTerm = list.getConstructor("nil").getConstructorTerm(); - Term headOpTerm = list["cons"].getSelectorTerm("head"); - Term tailOpTerm = list["cons"].getSelectorTerm("tail"); + Term headOpTerm = list["cons"].getSelector("head").getSelectorTerm(); + Term tailOpTerm = list["cons"].getSelector("tail").getSelectorTerm(); Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilOpTerm}); Term consTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, diff --git a/test/unit/api/cpp/term_white.cpp b/test/unit/api/cpp/term_white.cpp index 8f79e1bb6..470dd4db8 100644 --- a/test/unit/api/cpp/term_white.cpp +++ b/test/unit/api/cpp/term_white.cpp @@ -65,8 +65,8 @@ TEST_F(TestApiWhiteTerm, getOp) // list datatype constructor and selector operator terms Term consOpTerm = list.getConstructor("cons").getConstructorTerm(); Term nilOpTerm = list.getConstructor("nil").getConstructorTerm(); - Term headOpTerm = list["cons"].getSelectorTerm("head"); - Term tailOpTerm = list["cons"].getSelectorTerm("tail"); + Term headOpTerm = list["cons"].getSelector("head").getSelectorTerm(); + Term tailOpTerm = list["cons"].getSelector("tail").getSelectorTerm(); Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilOpTerm}); Term consTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 4d5c35472..0865d6045 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -836,10 +836,8 @@ class SolverTest // list datatype constructor and selector operator terms 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(); + Term headTerm = list.getConstructor("cons").getSelector("head").getSelectorTerm(); + Term tailTerm = list.getConstructor("cons").getSelector("tail").getSelectorTerm(); // mkTerm(Op op, Term term) const assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm)); @@ -847,15 +845,15 @@ class SolverTest 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(APPLY_SELECTOR, headTerm)); assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1)); assertThrows(CVC5ApiException.class, () -> slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm)); // mkTerm(Op op, Term child) const assertDoesNotThrow(() -> d_solver.mkTerm(opterm1, a)); assertDoesNotThrow(() -> d_solver.mkTerm(opterm2, d_solver.mkInteger(1))); - assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_SELECTOR, headTerm1, c)); - assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_SELECTOR, tailTerm2, c)); + assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_SELECTOR, headTerm, c)); + assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_SELECTOR, tailTerm, c)); assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, a)); assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1, d_solver.getNullTerm())); assertThrows(CVC5ApiException.class, @@ -1545,7 +1543,7 @@ class SolverTest Term consTerm = consList.getConstructor("cons").getConstructorTerm(); Term nilTerm = consList.getConstructor("nil").getConstructorTerm(); - Term headTerm = consList.getConstructor("cons").getSelectorTerm("head"); + Term headTerm = consList.getConstructor("cons").getSelector("head").getSelectorTerm(); Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm); Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil); @@ -2421,7 +2419,7 @@ class SolverTest 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); + APPLY_SELECTOR, consList.getConstructor("cons").getSelector("head").getSelectorTerm(), dt1); assertDoesNotThrow(() -> d_solver.simplify(dt2)); Term b1 = d_solver.mkVar(bvSort, "b1"); diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 4520701c5..fb09cdee2 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -829,10 +829,8 @@ def test_mk_term_from_op(solver): # list datatype constructor and selector operator terms 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() + headTerm = lis["cons"].getSelector("head").getSelectorTerm() + tailTerm = lis["cons"]["tail"].getSelectorTerm() # mkTerm(Op op, Term term) const solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm) @@ -846,7 +844,7 @@ def test_mk_term_from_op(solver): with pytest.raises(RuntimeError): solver.mkTerm(opterm1) with pytest.raises(RuntimeError): - solver.mkTerm(Kind.APPLY_SELECTOR, headTerm1) + solver.mkTerm(Kind.APPLY_SELECTOR, headTerm) with pytest.raises(RuntimeError): solver.mkTerm(opterm1) with pytest.raises(RuntimeError): @@ -855,8 +853,8 @@ def test_mk_term_from_op(solver): # mkTerm(Op op, Term child) const solver.mkTerm(opterm1, a) solver.mkTerm(opterm2, solver.mkInteger(1)) - solver.mkTerm(Kind.APPLY_SELECTOR, headTerm1, c) - solver.mkTerm(Kind.APPLY_SELECTOR, tailTerm2, c) + solver.mkTerm(Kind.APPLY_SELECTOR, headTerm, c) + solver.mkTerm(Kind.APPLY_SELECTOR, tailTerm, c) with pytest.raises(RuntimeError): solver.mkTerm(opterm2, a) with pytest.raises(RuntimeError): @@ -1161,7 +1159,7 @@ def test_get_op(solver): consTerm = consList.getConstructor("cons").getConstructorTerm() nilTerm = consList.getConstructor("nil").getConstructorTerm() - headTerm = consList["cons"].getSelectorTerm("head") + headTerm = consList["cons"].getSelector("head").getSelectorTerm() listnil = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm) listcons1 = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm, @@ -1733,7 +1731,9 @@ def test_simplify(solver): consList.getConstructor("nil").getConstructorTerm())) solver.simplify(dt1) dt2 = solver.mkTerm( - Kind.APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1) + Kind.APPLY_SELECTOR, + consList["cons"].getSelector("head").getSelectorTerm(), + dt1) solver.simplify(dt2) b1 = solver.mkVar(bvSort, "b1") diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index 5af769267..c070b00ec 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -189,8 +189,8 @@ def test_get_op(solver): # list datatype constructor and selector operator terms consOpTerm = list1.getConstructor("cons").getConstructorTerm() nilOpTerm = list1.getConstructor("nil").getConstructorTerm() - headOpTerm = list1["cons"].getSelectorTerm("head") - tailOpTerm = list1["cons"].getSelectorTerm("tail") + headOpTerm = list1["cons"].getSelector("head").getSelectorTerm() + tailOpTerm = list1["cons"].getSelector("tail").getSelectorTerm() nilTerm = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilOpTerm) consTerm = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consOpTerm, -- 2.30.2