From 5dcb75066729d24fe17805049cd0df4ce8767302 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Sat, 2 Apr 2022 11:57:50 -0700 Subject: [PATCH] api: Rename get(Selector|Constructor)Term() to getTerm(). (#8537) --- docs/theories/datatypes.rst | 10 ++-- examples/api/cpp/datatypes.cpp | 37 ++++++-------- examples/api/java/Datatypes.java | 21 ++++---- examples/api/java/Statistics.java | 2 +- examples/api/python/datatypes.py | 14 +++--- src/api/cpp/cvc5.cpp | 6 +-- src/api/cpp/cvc5.h | 4 +- src/api/cpp/cvc5_kind.h | 4 +- .../io/github/cvc5/DatatypeConstructor.java | 6 +-- .../java/io/github/cvc5/DatatypeSelector.java | 6 +-- src/api/java/jni/datatype_constructor.cpp | 10 ++-- src/api/java/jni/datatype_selector.cpp | 10 ++-- src/api/python/cvc5.pxd | 4 +- src/api/python/cvc5.pxi | 8 +-- src/parser/parser.cpp | 4 +- src/parser/smt2/smt2.cpp | 4 +- test/unit/api/cpp/datatype_api_black.cpp | 8 +-- test/unit/api/cpp/solver_black.cpp | 49 +++++++++---------- test/unit/api/cpp/solver_white.cpp | 6 +-- test/unit/api/cpp/sort_black.cpp | 8 +-- test/unit/api/cpp/term_black.cpp | 8 +-- test/unit/api/cpp/term_white.cpp | 8 +-- test/unit/api/java/DatatypeTest.java | 8 +-- test/unit/api/java/SolverTest.java | 24 ++++----- test/unit/api/java/SortTest.java | 8 +-- test/unit/api/java/TermTest.java | 4 +- test/unit/api/python/test_datatype_api.py | 8 +-- test/unit/api/python/test_solver.py | 24 ++++----- test/unit/api/python/test_sort.py | 8 +-- test/unit/api/python/test_term.py | 8 +-- 30 files changed, 157 insertions(+), 172 deletions(-) diff --git a/docs/theories/datatypes.rst b/docs/theories/datatypes.rst index d78c13e0a..4106e31fe 100644 --- a/docs/theories/datatypes.rst +++ b/docs/theories/datatypes.rst @@ -207,7 +207,7 @@ a `cvc5::Solver solver` object. | | | | | | | ``Datatype dt = s.getDatatype();`` | | | | | -| | | ``Term ci = dt[i].getConstructorTerm();`` | +| | | ``Term ci = dt[i].getTerm();`` | | | | | | | | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {ci, , ..., });`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ @@ -215,7 +215,7 @@ a `cvc5::Solver solver` object. | | | | | | | ``Datatype dt = s.getDatatype();`` | | | | | -| | | ``Term sij = dt[i].getSelector(j).getSelectorTerm();`` | +| | | ``Term sij = dt[i].getSelector(j).getTerm();`` | | | | | | | | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sij, t});`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ @@ -249,7 +249,7 @@ a `cvc5::Solver solver` object. | | | | | | | ``Datatype dt = s.getDatatype();`` | | | | | -| | | ``Term c = dt[0].getConstructorTerm();`` | +| | | ``Term c = dt[0].getTerm();`` | | | | | | | | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, , ..., });`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ @@ -257,7 +257,7 @@ a `cvc5::Solver solver` object. | | | | | | | ``Datatype dt = s.getDatatype();`` | | | | | -| | | ``Term sel = dt[0].getSelector(i).getSelectorTerm();`` | +| | | ``Term sel = dt[0].getSelector(i).getTerm();`` | | | | | | | | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sel, t});`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ @@ -291,7 +291,7 @@ a `cvc5::Solver solver` object. | | | | | | | ``Datatype dt = s.getDatatype();`` | | | | | -| | | ``Term c = dt[0].getConstructorTerm();`` | +| | | ``Term c = dt[0].getTerm();`` | | | | | | | | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, , ..., });`` | +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+ diff --git a/examples/api/cpp/datatypes.cpp b/examples/api/cpp/datatypes.cpp index 75e4a97d1..bbdaa7e0f 100644 --- a/examples/api/cpp/datatypes.cpp +++ b/examples/api/cpp/datatypes.cpp @@ -35,29 +35,25 @@ void test(Solver& slv, Sort& consListSort) // which is equivalent to consList["cons"].getConstructor(). Note that // "nil" is a constructor too, so it needs to be applied with // APPLY_CONSTRUCTOR, even though it has no arguments. - Term t = slv.mkTerm( - APPLY_CONSTRUCTOR, - {consList.getConstructor("cons").getConstructorTerm(), - slv.mkInteger(0), - slv.mkTerm(APPLY_CONSTRUCTOR, - {consList.getConstructor("nil").getConstructorTerm()})}); + Term t = slv.mkTerm(APPLY_CONSTRUCTOR, + {consList.getConstructor("cons").getTerm(), + slv.mkInteger(0), + slv.mkTerm(APPLY_CONSTRUCTOR, + {consList.getConstructor("nil").getTerm()})}); std::cout << "t is " << t << std::endl << "sort of cons is " - << consList.getConstructor("cons").getConstructorTerm().getSort() - << std::endl + << consList.getConstructor("cons").getTerm().getSort() << std::endl << "sort of nil is " - << consList.getConstructor("nil").getConstructorTerm().getSort() - << std::endl; + << consList.getConstructor("nil").getTerm().getSort() << std::endl; // t2 = head(cons 0 nil), and of course this can be evaluated // // 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(APPLY_SELECTOR, - {consList["cons"].getSelector("head").getSelectorTerm(), t}); + Term t2 = slv.mkTerm(APPLY_SELECTOR, + {consList["cons"].getSelector("head").getTerm(), t}); std::cout << "t2 is " << t2 << std::endl << "simplify(t2) is " << slv.simplify(t2) << std::endl @@ -133,14 +129,13 @@ void test(Solver& slv, Sort& consListSort) std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; 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 " - << paramConsList.getConstructor("cons").getConstructorTerm().getSort() - << std::endl - << std::endl; + APPLY_SELECTOR, {paramConsList["cons"].getSelector("head").getTerm(), a}); + std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() + << std::endl + << "sort of cons is " + << paramConsList.getConstructor("cons").getTerm().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 0f70ce0dc..03c80c0a0 100644 --- a/examples/api/java/Datatypes.java +++ b/examples/api/java/Datatypes.java @@ -35,22 +35,21 @@ 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.getConstructor("cons").getConstructorTerm(), + consList.getConstructor("cons").getTerm(), slv.mkInteger(0), - slv.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructor("nil").getConstructorTerm())); + slv.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructor("nil").getTerm())); System.out.println("t is " + t + "\n" - + "sort of cons is " + consList.getConstructor("cons").getConstructorTerm().getSort() + "\n" - + "sort of nil is " + consList.getConstructor("nil").getConstructorTerm().getSort()); + + "sort of cons is " + consList.getConstructor("cons").getTerm().getSort() + "\n" + + "sort of nil is " + consList.getConstructor("nil").getTerm().getSort()); // t2 = head(cons 0 nil), and of course this can be evaluated // // 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").getSelector("head").getSelectorTerm(), - t); + Term t2 = slv.mkTerm( + Kind.APPLY_SELECTOR, consList.getConstructor("cons").getSelector("head").getTerm(), t); System.out.println("t2 is " + t2 + "\n" + "simplify(t2) is " + slv.simplify(t2) + "\n"); @@ -124,12 +123,10 @@ 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").getSelector("head").getSelectorTerm(), - a); + Term head_a = slv.mkTerm( + Kind.APPLY_SELECTOR, paramConsList.getConstructor("cons").getSelector("head").getTerm(), 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"); + + "sort of cons is " + paramConsList.getConstructor("cons").getTerm().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/java/Statistics.java b/examples/api/java/Statistics.java index da1bbeb8c..fc7015e04 100644 --- a/examples/api/java/Statistics.java +++ b/examples/api/java/Statistics.java @@ -202,7 +202,7 @@ public class Statistics // (assert (forall ((x Person)) (not (set.member (mkTuple x x) ancestor)))) Term var = solver.mkVar(personSort, "x"); DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0); - Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), var, var); + Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getTerm(), var, var); Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor); Term notMember = solver.mkTerm(NOT, member); diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index 39642297c..24226d443 100644 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -36,16 +36,16 @@ def test(slv, consListSort): t = slv.mkTerm( Kind.APPLY_CONSTRUCTOR, - consList.getConstructor("cons").getConstructorTerm(), + consList.getConstructor("cons").getTerm(), slv.mkInteger(0), slv.mkTerm( Kind.APPLY_CONSTRUCTOR, - consList.getConstructor("nil").getConstructorTerm())) + consList.getConstructor("nil").getTerm())) print("t is {}\nsort of cons is {}\n sort of nil is {}".format( t, - consList.getConstructor("cons").getConstructorTerm().getSort(), - consList.getConstructor("nil").getConstructorTerm().getSort())) + consList.getConstructor("cons").getTerm().getSort(), + consList.getConstructor("nil").getTerm().getSort())) # t2 = head(cons 0 nil), and of course this can be evaluated # @@ -55,7 +55,7 @@ def test(slv, consListSort): t2 = slv.mkTerm( Kind.APPLY_SELECTOR, - consList["cons"].getSelector("head").getSelectorTerm(), + consList["cons"].getSelector("head").getTerm(), t) print("t2 is {}\nsimplify(t2) is {}\n\n".format(t2, slv.simplify(t2))) @@ -102,11 +102,11 @@ def test(slv, consListSort): head_a = slv.mkTerm( Kind.APPLY_SELECTOR, - paramConsList["cons"].getSelector("head").getSelectorTerm(), + paramConsList["cons"].getSelector("head").getTerm(), a) print("head_a is {} of sort {}".format(head_a, head_a.getSort())) print("sort of cons is", - paramConsList.getConstructor("cons").getConstructorTerm().getSort()) + paramConsList.getConstructor("cons").getTerm().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 26da68abc..2da46514e 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -3593,7 +3593,7 @@ std::string DatatypeSelector::getName() const CVC5_API_TRY_CATCH_END; } -Term DatatypeSelector::getSelectorTerm() const +Term DatatypeSelector::getTerm() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -3682,7 +3682,7 @@ std::string DatatypeConstructor::getName() const CVC5_API_TRY_CATCH_END; } -Term DatatypeConstructor::getConstructorTerm() const +Term DatatypeConstructor::getTerm() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -6124,7 +6124,7 @@ Term Solver::mkTuple(const std::vector& sorts, Sort s = mkTupleSortHelper(sorts); Datatype dt = s.getDatatype(); internal::NodeBuilder nb(extToIntKind(APPLY_CONSTRUCTOR)); - nb << *dt[0].getConstructorTerm().d_node; + nb << *dt[0].getTerm().d_node; nb.append(args); internal::Node res = nb.constructNode(); (void)res.getType(true); /* kick off type checking */ diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 7bf71accd..78bad1eee 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2017,7 +2017,7 @@ class CVC5_EXPORT DatatypeSelector * Get the selector operator of this datatype selector. * @return the selector term */ - Term getSelectorTerm() const; + Term getTerm() const; /** * Get the updater operator of this datatype selector. @@ -2092,7 +2092,7 @@ class CVC5_EXPORT DatatypeConstructor * Get the constructor operator of this datatype constructor. * @return the constructor term */ - Term getConstructorTerm() const; + Term getTerm() const; /** * Get the constructor operator of this datatype constructor whose return diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 1d5c2da90..7d405891a 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -2533,7 +2533,7 @@ enum Kind : int32_t * * - Arity: ``n > 0`` * - * - ``1:`` DatatypeConstructor Term (see DatatypeConstructor::getConstructorTerm() const) + * - ``1:`` DatatypeConstructor Term (see DatatypeConstructor::getTerm() const) * - ``2..n:`` Terms of the Sorts of the selectors of the constructor (the arguments to the constructor) * * - Create Term of this Kind with: @@ -2555,7 +2555,7 @@ enum Kind : int32_t * * - Arity: ``2`` * - * - ``1:`` DatatypeSelector Term (see DatatypeSelector::getSelectorTerm() const) + * - ``1:`` DatatypeSelector Term (see DatatypeSelector::getTerm() 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 e3e482fee..94a838d95 100644 --- a/src/api/java/io/github/cvc5/DatatypeConstructor.java +++ b/src/api/java/io/github/cvc5/DatatypeConstructor.java @@ -50,13 +50,13 @@ public class DatatypeConstructor extends AbstractPointer implements IterablegetConstructorTerm()); + Term* retPointer = new Term(current->getTerm()); return (jlong)retPointer; CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/java/jni/datatype_selector.cpp b/src/api/java/jni/datatype_selector.cpp index d75263b50..a5f20cb1a 100644 --- a/src/api/java/jni/datatype_selector.cpp +++ b/src/api/java/jni/datatype_selector.cpp @@ -46,17 +46,15 @@ JNIEXPORT jstring JNICALL Java_io_github_cvc5_DatatypeSelector_getName( /* * Class: io_github_cvc5_DatatypeSelector - * Method: getSelectorTerm + * Method: getTerm * Signature: (J)J */ -JNIEXPORT jlong JNICALL -Java_io_github_cvc5_DatatypeSelector_getSelectorTerm(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jlong JNICALL Java_io_github_cvc5_DatatypeSelector_getTerm( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeSelector* current = (DatatypeSelector*)pointer; - Term* retPointer = new Term(current->getSelectorTerm()); + Term* retPointer = new Term(current->getTerm()); return (jlong)retPointer; CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 65bb821f9..c4fb71c5c 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -85,7 +85,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": DatatypeSelector operator[](size_t idx) except + DatatypeSelector operator[](const string& name) except + string getName() except + - Term getConstructorTerm() except + + Term getTerm() except + Term getInstantiatedConstructorTerm(const Sort& retSort) except + Term getTesterTerm() except + size_t getNumSelectors() except + @@ -122,7 +122,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": cdef cppclass DatatypeSelector: DatatypeSelector() except + string getName() except + - Term getSelectorTerm() except + + Term getTerm() except + Term getUpdaterTerm() except + Sort getCodomainSort() except + bint isNull() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 8fc4904e7..f43888edd 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -256,12 +256,12 @@ cdef class DatatypeConstructor: """ return self.cdc.getName().decode() - def getConstructorTerm(self): + def getTerm(self): """ :return: The constructor operator as a term. """ cdef Term term = Term(self.solver) - term.cterm = self.cdc.getConstructorTerm() + term.cterm = self.cdc.getTerm() return term def getInstantiatedConstructorTerm(self, Sort retSort): @@ -491,12 +491,12 @@ cdef class DatatypeSelector: """ return self.cds.getName().decode() - def getSelectorTerm(self): + def getTerm(self): """ :return: The selector opeartor of this datatype selector as a term. """ cdef Term term = Term(self.solver) - term.cterm = self.cds.getSelectorTerm() + term.cterm = self.cds.getTerm() return term def getUpdaterTerm(self): diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 59bc68090..5e82012dd 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -388,7 +388,7 @@ std::vector Parser::bindMutualDatatypeTypes( for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) { const cvc5::DatatypeConstructor& ctor = dt[j]; - cvc5::Term constructor = ctor.getConstructorTerm(); + cvc5::Term constructor = ctor.getTerm(); Trace("parser-idt") << "+ define " << constructor << std::endl; string constructorName = ctor.getName(); if(consNames.find(constructorName)==consNames.end()) { @@ -414,7 +414,7 @@ std::vector Parser::bindMutualDatatypeTypes( for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++) { const cvc5::DatatypeSelector& sel = ctor[k]; - cvc5::Term selector = sel.getSelectorTerm(); + cvc5::Term selector = sel.getTerm(); Trace("parser-idt") << "+++ define " << selector << std::endl; string selectorName = sel.getName(); if(selNames.find(selectorName)==selNames.end()) { diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index bf610ae86..63cc3af4e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1101,8 +1101,8 @@ cvc5::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) cvc5::Term ret; if (p.d_kind == cvc5::APPLY_SELECTOR) { - ret = d_solver->mkTerm(cvc5::APPLY_SELECTOR, - {dt[0][n].getSelectorTerm(), args[0]}); + ret = + d_solver->mkTerm(cvc5::APPLY_SELECTOR, {dt[0][n].getTerm(), args[0]}); } else { diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index f4831b9a0..ad0c56701 100644 --- a/test/unit/api/cpp/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp @@ -36,8 +36,8 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSort) DatatypeConstructor consConstr = d[0]; DatatypeConstructor nilConstr = d[1]; ASSERT_THROW(d[2], CVC5ApiException); - ASSERT_NO_THROW(consConstr.getConstructorTerm()); - ASSERT_NO_THROW(nilConstr.getConstructorTerm()); + ASSERT_NO_THROW(consConstr.getTerm()); + ASSERT_NO_THROW(nilConstr.getTerm()); } TEST_F(TestApiBlackDatatype, isNull) @@ -206,7 +206,7 @@ TEST_F(TestApiBlackDatatype, datatypeStructs) ASSERT_TRUE(dt.isWellFounded()); // get constructor DatatypeConstructor dcons = dt[0]; - Term consTerm = dcons.getConstructorTerm(); + Term consTerm = dcons.getTerm(); ASSERT_EQ(dcons.getNumSelectors(), 2); // create datatype sort to test @@ -588,7 +588,7 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons) Term testConsTerm; // get the specialized constructor term for list[Int] ASSERT_NO_THROW(testConsTerm = nilc.getInstantiatedConstructorTerm(listInt)); - ASSERT_NE(testConsTerm, nilc.getConstructorTerm()); + ASSERT_NE(testConsTerm, nilc.getTerm()); // error to get the specialized constructor term for Int ASSERT_THROW(nilc.getInstantiatedConstructorTerm(isort), CVC5ApiException); } diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 7461a879e..17812748b 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -227,7 +227,7 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts) Term t1 = d_solver.mkConst(isort1, "t"); Term t0 = d_solver.mkTerm( APPLY_SELECTOR, - {t1.getSort().getDatatype().getSelector("s1").getSelectorTerm(), t1}); + {t1.getSort().getDatatype().getSelector("s1").getTerm(), t1}); ASSERT_EQ(dt_sorts[0].instantiate({d_solver.getBooleanSort()}), t0.getSort()); /* Note: More tests are in datatype_api_black. */ @@ -852,10 +852,10 @@ TEST_F(TestApiBlackSolver, mkTermFromOp) Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms - Term consTerm = list.getConstructor("cons").getConstructorTerm(); - Term nilTerm = list.getConstructor("nil").getConstructorTerm(); - Term headTerm = list["cons"].getSelector("head").getSelectorTerm(); - Term tailTerm = list["cons"]["tail"].getSelectorTerm(); + Term consTerm = list.getConstructor("cons").getTerm(); + Term nilTerm = list.getConstructor("nil").getTerm(); + Term headTerm = list["cons"].getSelector("head").getTerm(); + Term tailTerm = list["cons"]["tail"].getTerm(); // mkTerm(Op op, Term term) const ASSERT_NO_THROW(d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm})); @@ -1498,9 +1498,9 @@ TEST_F(TestApiBlackSolver, getOp) Sort consListSort = d_solver.mkDatatypeSort(consListSpec); Datatype consList = consListSort.getDatatype(); - Term consTerm = consList.getConstructor("cons").getConstructorTerm(); - Term nilTerm = consList.getConstructor("nil").getConstructorTerm(); - Term headTerm = consList["cons"].getSelector("head").getSelectorTerm(); + Term consTerm = consList.getConstructor("cons").getTerm(); + Term nilTerm = consList.getConstructor("nil").getTerm(); + Term headTerm = consList["cons"].getSelector("head").getTerm(); Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}); Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, @@ -2364,14 +2364,13 @@ TEST_F(TestApiBlackSolver, simplify) Datatype consList = consListSort.getDatatype(); Term dt1 = d_solver.mkTerm( APPLY_CONSTRUCTOR, - {consList.getConstructor("cons").getConstructorTerm(), + {consList.getConstructor("cons").getTerm(), d_solver.mkInteger(0), d_solver.mkTerm(APPLY_CONSTRUCTOR, - {consList.getConstructor("nil").getConstructorTerm()})}); + {consList.getConstructor("nil").getTerm()})}); ASSERT_NO_THROW(d_solver.simplify(dt1)); Term dt2 = d_solver.mkTerm( - APPLY_SELECTOR, - {consList["cons"].getSelector("head").getSelectorTerm(), dt1}); + APPLY_SELECTOR, {consList["cons"].getSelector("head").getTerm(), dt1}); ASSERT_NO_THROW(d_solver.simplify(dt2)); Term b1 = d_solver.mkVar(bvSort, "b1"); @@ -2853,7 +2852,7 @@ TEST_F(TestApiBlackSolver, tupleProject) for (size_t i = 0; i < indices.size(); i++) { - Term selectorTerm = constructor[indices[i]].getSelectorTerm(); + Term selectorTerm = constructor[indices[i]].getTerm(); Term selectedTerm = d_solver.mkTerm(APPLY_SELECTOR, {selectorTerm, tuple}); Term simplifiedTerm = d_solver.simplify(selectedTerm); ASSERT_EQ(elements[indices[i]], simplifiedTerm); @@ -2930,7 +2929,7 @@ TEST_F(TestApiBlackSolver, proj_issue373) Term bvl = d_solver.mkTerm(d_solver.mkOp(VARIABLE_LIST), {t452}); Term acons = d_solver.mkTerm( d_solver.mkOp(APPLY_CONSTRUCTOR), - {s4.getDatatype().getConstructor("_x115").getConstructorTerm(), t452}); + {s4.getDatatype().getConstructor("_x115").getTerm(), t452}); // type exception ASSERT_THROW( d_solver.mkTerm(d_solver.mkOp(APPLY_CONSTRUCTOR), {bvl, acons, t452}), @@ -2970,16 +2969,14 @@ TEST_F(TestApiBlackSolver, proj_issue378) dtdecl.addConstructor(cdecl); Sort s7 = d_solver.mkDatatypeSort(dtdecl); Sort s9 = s7.instantiate({s2}); - 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") - .getSelector("_x185") - .getSelectorTerm(), - t1507, - t7})); + Term t1507 = + d_solver.mkTerm(APPLY_CONSTRUCTOR, + {s9.getDatatype().getConstructor("_x184").getTerm(), t7}); + ASSERT_NO_THROW(d_solver.mkTerm( + APPLY_UPDATER, + {s9.getDatatype().getConstructor("_x186").getSelector("_x185").getTerm(), + t1507, + t7})); } TEST_F(TestApiBlackSolver, proj_issue379) @@ -3072,7 +3069,7 @@ TEST_F(TestApiBlackSolver, proj_issue382) Term t82 = d_solver.mkTerm(MATCH, {t13, t53, t53, t53, t81}); Term t325 = d_solver.mkTerm( APPLY_SELECTOR, - {t82.getSort().getDatatype().getSelector("_x19").getSelectorTerm(), t82}); + {t82.getSort().getDatatype().getSelector("_x19").getTerm(), t82}); ASSERT_NO_THROW(d_solver.simplify(t325)); } @@ -3347,7 +3344,7 @@ TEST_F(TestApiBlackSolver, projIssue431) .getDatatype() .getConstructor("_cons64") .getSelector("_sel62") - .getSelectorTerm(); + .getTerm(); 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 ab2b87831..3cc89434b 100644 --- a/test/unit/api/cpp/solver_white.cpp +++ b/test/unit/api/cpp/solver_white.cpp @@ -36,9 +36,9 @@ TEST_F(TestApiWhiteSolver, getOp) Sort consListSort = d_solver.mkDatatypeSort(consListSpec); Datatype consList = consListSort.getDatatype(); - Term nilTerm = consList.getConstructor("nil").getConstructorTerm(); - Term consTerm = consList.getConstructor("cons").getConstructorTerm(); - Term headTerm = consList["cons"].getSelector("head").getSelectorTerm(); + Term nilTerm = consList.getConstructor("nil").getTerm(); + Term consTerm = consList.getConstructor("cons").getTerm(); + Term headTerm = consList["cons"].getSelector("head").getTerm(); Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilTerm}); Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index ccbe23f9b..8a716faec 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -146,7 +146,7 @@ TEST_F(TestApiBlackSort, isConstructor) { Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); - Sort cons_sort = dt[0].getConstructorTerm().getSort(); + Sort cons_sort = dt[0].getTerm().getSort(); ASSERT_TRUE(cons_sort.isDatatypeConstructor()); ASSERT_NO_THROW(Sort().isDatatypeConstructor()); } @@ -155,7 +155,7 @@ TEST_F(TestApiBlackSort, isSelector) { Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); - Sort cons_sort = dt[0][1].getSelectorTerm().getSort(); + Sort cons_sort = dt[0][1].getTerm().getSort(); ASSERT_TRUE(cons_sort.isDatatypeSelector()); ASSERT_NO_THROW(Sort().isDatatypeSelector()); } @@ -277,7 +277,7 @@ TEST_F(TestApiBlackSort, datatypeSorts) // get constructor DatatypeConstructor dcons = dt[0]; - Term consTerm = dcons.getConstructorTerm(); + Term consTerm = dcons.getTerm(); Sort consSort = consTerm.getSort(); ASSERT_TRUE(consSort.isDatatypeConstructor()); ASSERT_FALSE(consSort.isDatatypeTester()); @@ -299,7 +299,7 @@ TEST_F(TestApiBlackSort, datatypeSorts) // get selector DatatypeSelector dselTail = dcons[1]; - Term tailTerm = dselTail.getSelectorTerm(); + Term tailTerm = dselTail.getTerm(); ASSERT_TRUE(tailTerm.getSort().isDatatypeSelector()); ASSERT_EQ(tailTerm.getSort().getDatatypeSelectorDomainSort(), dtypeSort); ASSERT_EQ(tailTerm.getSort().getDatatypeSelectorCodomainSort(), dtypeSort); diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp index c1034cf1d..ec4743037 100644 --- a/test/unit/api/cpp/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -188,10 +188,10 @@ 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.getConstructor("cons").getConstructorTerm(); - Term nilOpTerm = list.getConstructor("nil").getConstructorTerm(); - Term headOpTerm = list["cons"].getSelector("head").getSelectorTerm(); - Term tailOpTerm = list["cons"].getSelector("tail").getSelectorTerm(); + Term consOpTerm = list.getConstructor("cons").getTerm(); + Term nilOpTerm = list.getConstructor("nil").getTerm(); + Term headOpTerm = list["cons"].getSelector("head").getTerm(); + Term tailOpTerm = list["cons"].getSelector("tail").getTerm(); 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 470dd4db8..86d6b976e 100644 --- a/test/unit/api/cpp/term_white.cpp +++ b/test/unit/api/cpp/term_white.cpp @@ -63,10 +63,10 @@ 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.getConstructor("cons").getConstructorTerm(); - Term nilOpTerm = list.getConstructor("nil").getConstructorTerm(); - Term headOpTerm = list["cons"].getSelector("head").getSelectorTerm(); - Term tailOpTerm = list["cons"].getSelector("tail").getSelectorTerm(); + Term consOpTerm = list.getConstructor("cons").getTerm(); + Term nilOpTerm = list.getConstructor("nil").getTerm(); + Term headOpTerm = list["cons"].getSelector("head").getTerm(); + Term tailOpTerm = list["cons"].getSelector("tail").getTerm(); Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, {nilOpTerm}); Term consTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index bc13ab634..557db2f9b 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -54,8 +54,8 @@ class DatatypeTest DatatypeConstructor consConstr = d.getConstructor(0); DatatypeConstructor nilConstr = d.getConstructor(1); assertThrows(CVC5ApiException.class, () -> d.getConstructor(2)); - assertDoesNotThrow(() -> consConstr.getConstructorTerm()); - assertDoesNotThrow(() -> nilConstr.getConstructorTerm()); + assertDoesNotThrow(() -> consConstr.getTerm()); + assertDoesNotThrow(() -> nilConstr.getTerm()); } @Test @@ -200,7 +200,7 @@ class DatatypeTest assertTrue(dt.isWellFounded()); // get constructor DatatypeConstructor dcons = dt.getConstructor(0); - Term consTerm = dcons.getConstructorTerm(); + Term consTerm = dcons.getTerm(); assertEquals(dcons.getNumSelectors(), 2); // create datatype sort to test @@ -592,7 +592,7 @@ class DatatypeTest // get the specialized constructor term for list[Int] assertDoesNotThrow(() -> atomicTerm.set(nilc.getInstantiatedConstructorTerm(listInt))); Term testConsTerm = atomicTerm.get(); - assertNotEquals(testConsTerm, nilc.getConstructorTerm()); + assertNotEquals(testConsTerm, nilc.getTerm()); // error to get the specialized constructor term for Int assertThrows(CVC5ApiException.class, () -> nilc.getInstantiatedConstructorTerm(isort)); } diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 0865d6045..bd21caeb9 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -215,7 +215,7 @@ class SolverTest Sort isort1 = dt_sorts[1].instantiate(new Sort[] {d_solver.getBooleanSort()}); Term t1 = d_solver.mkConst(isort1, "t"); Term t0 = d_solver.mkTerm(APPLY_SELECTOR, - t1.getSort().getDatatype().getConstructor("c1").getSelector("s1").getSelectorTerm(), + t1.getSort().getDatatype().getConstructor("c1").getSelector("s1").getTerm(), t1); assertEquals(dt_sorts[0].instantiate(new Sort[] {d_solver.getBooleanSort()}), t0.getSort()); @@ -834,10 +834,10 @@ class SolverTest Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms - Term consTerm = list.getConstructor("cons").getConstructorTerm(); - Term nilTerm = list.getConstructor("nil").getConstructorTerm(); - Term headTerm = list.getConstructor("cons").getSelector("head").getSelectorTerm(); - Term tailTerm = list.getConstructor("cons").getSelector("tail").getSelectorTerm(); + Term consTerm = list.getConstructor("cons").getTerm(); + Term nilTerm = list.getConstructor("nil").getTerm(); + Term headTerm = list.getConstructor("cons").getSelector("head").getTerm(); + Term tailTerm = list.getConstructor("cons").getSelector("tail").getTerm(); // mkTerm(Op op, Term term) const assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm)); @@ -1541,9 +1541,9 @@ class SolverTest Sort consListSort = d_solver.mkDatatypeSort(consListSpec); Datatype consList = consListSort.getDatatype(); - Term consTerm = consList.getConstructor("cons").getConstructorTerm(); - Term nilTerm = consList.getConstructor("nil").getConstructorTerm(); - Term headTerm = consList.getConstructor("cons").getSelector("head").getSelectorTerm(); + Term consTerm = consList.getConstructor("cons").getTerm(); + Term nilTerm = consList.getConstructor("nil").getTerm(); + Term headTerm = consList.getConstructor("cons").getSelector("head").getTerm(); Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm); Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil); @@ -2414,12 +2414,12 @@ class SolverTest Datatype consList = consListSort.getDatatype(); Term dt1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, - consList.getConstructor("cons").getConstructorTerm(), + consList.getConstructor("cons").getTerm(), d_solver.mkInteger(0), - d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructor("nil").getConstructorTerm())); + d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructor("nil").getTerm())); assertDoesNotThrow(() -> d_solver.simplify(dt1)); Term dt2 = d_solver.mkTerm( - APPLY_SELECTOR, consList.getConstructor("cons").getSelector("head").getSelectorTerm(), dt1); + APPLY_SELECTOR, consList.getConstructor("cons").getSelector("head").getTerm(), dt1); assertDoesNotThrow(() -> d_solver.simplify(dt2)); Term b1 = d_solver.mkVar(bvSort, "b1"); @@ -2939,7 +2939,7 @@ class SolverTest for (int i = 0; i < indices.length; i++) { - Term selectorTerm = constructor.getSelector(indices[i]).getSelectorTerm(); + Term selectorTerm = constructor.getSelector(indices[i]).getTerm(); Term selectedTerm = d_solver.mkTerm(APPLY_SELECTOR, selectorTerm, tuple); Term simplifiedTerm = d_solver.simplify(selectedTerm); assertEquals(elements[indices[i]], simplifiedTerm); diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index bc3376ab7..1396b27c7 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -165,7 +165,7 @@ class SortTest { Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); - Sort cons_sort = dt.getConstructor(0).getConstructorTerm().getSort(); + Sort cons_sort = dt.getConstructor(0).getTerm().getSort(); assertTrue(cons_sort.isDatatypeConstructor()); assertDoesNotThrow(() -> d_solver.getNullSort().isDatatypeConstructor()); } @@ -175,7 +175,7 @@ class SortTest { Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); - Sort cons_sort = dt.getConstructor(0).getSelector(1).getSelectorTerm().getSort(); + Sort cons_sort = dt.getConstructor(0).getSelector(1).getTerm().getSort(); assertTrue(cons_sort.isDatatypeSelector()); assertDoesNotThrow(() -> d_solver.getNullSort().isDatatypeSelector()); } @@ -294,7 +294,7 @@ class SortTest // get constructor DatatypeConstructor dcons = dt.getConstructor(0); - Term consTerm = dcons.getConstructorTerm(); + Term consTerm = dcons.getTerm(); Sort consSort = consTerm.getSort(); assertTrue(consSort.isDatatypeConstructor()); assertFalse(consSort.isDatatypeTester()); @@ -316,7 +316,7 @@ class SortTest // get selector DatatypeSelector dselTail = dcons.getSelector(1); - Term tailTerm = dselTail.getSelectorTerm(); + Term tailTerm = dselTail.getTerm(); assertTrue(tailTerm.getSort().isDatatypeSelector()); assertEquals(tailTerm.getSort().getDatatypeSelectorDomainSort(), dtypeSort); assertEquals(tailTerm.getSort().getDatatypeSelectorCodomainSort(), dtypeSort); diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index 3ecddb82c..c8ee81f0a 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.getConstructor("cons").getConstructorTerm(); - Term nilOpTerm = list.getConstructor("nil").getConstructorTerm(); + Term consOpTerm = list.getConstructor("cons").getTerm(); + Term nilOpTerm = list.getConstructor("nil").getTerm(); } @Test diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index df4485741..09d5ce05e 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -39,8 +39,8 @@ def test_mk_datatype_sort(solver): nilConstr = d[1] with pytest.raises(RuntimeError): d[2] - consConstr.getConstructorTerm() - nilConstr.getConstructorTerm() + consConstr.getTerm() + nilConstr.getTerm() def test_is_null(solver): # creating empty (null) objects. @@ -203,7 +203,7 @@ def test_datatype_structs(solver): assert dt.isWellFounded() # get constructor dcons = dt[0] - consTerm = dcons.getConstructorTerm() + consTerm = dcons.getTerm() assert dcons.getNumSelectors() == 2 # create datatype sort to test @@ -558,7 +558,7 @@ def test_datatype_specialized_cons(solver): testConsTerm = Term(solver) # get the specialized constructor term for list[Int] testConsTerm = nilc.getInstantiatedConstructorTerm(listInt) - assert testConsTerm != nilc.getConstructorTerm() + assert testConsTerm != nilc.getTerm() # error to get the specialized constructor term for Int with pytest.raises(RuntimeError): nilc.getInstantiatedConstructorTerm(isort) diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index fb09cdee2..53821e174 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -177,7 +177,7 @@ def test_mk_datatype_sorts(solver): t1 = solver.mkConst(isort1, "t") t0 = solver.mkTerm( Kind.APPLY_SELECTOR, - t1.getSort().getDatatype().getSelector("s1").getSelectorTerm(), + t1.getSort().getDatatype().getSelector("s1").getTerm(), t1) assert dt_sorts[0].instantiate({solver.getBooleanSort()}) == t0.getSort() @@ -827,10 +827,10 @@ def test_mk_term_from_op(solver): lis = listSort.getDatatype() # list datatype constructor and selector operator terms - consTerm = lis.getConstructor("cons").getConstructorTerm() - nilTerm = lis.getConstructor("nil").getConstructorTerm() - headTerm = lis["cons"].getSelector("head").getSelectorTerm() - tailTerm = lis["cons"]["tail"].getSelectorTerm() + consTerm = lis.getConstructor("cons").getTerm() + nilTerm = lis.getConstructor("nil").getTerm() + headTerm = lis["cons"].getSelector("head").getTerm() + tailTerm = lis["cons"]["tail"].getTerm() # mkTerm(Op op, Term term) const solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm) @@ -1157,9 +1157,9 @@ def test_get_op(solver): consListSort = solver.mkDatatypeSort(consListSpec) consList = consListSort.getDatatype() - consTerm = consList.getConstructor("cons").getConstructorTerm() - nilTerm = consList.getConstructor("nil").getConstructorTerm() - headTerm = consList["cons"].getSelector("head").getSelectorTerm() + consTerm = consList.getConstructor("cons").getTerm() + nilTerm = consList.getConstructor("nil").getTerm() + headTerm = consList["cons"].getSelector("head").getTerm() listnil = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilTerm) listcons1 = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consTerm, @@ -1724,15 +1724,15 @@ def test_simplify(solver): consList = consListSort.getDatatype() dt1 = solver.mkTerm( Kind.APPLY_CONSTRUCTOR, - consList.getConstructor("cons").getConstructorTerm(), + consList.getConstructor("cons").getTerm(), solver.mkInteger(0), solver.mkTerm( Kind.APPLY_CONSTRUCTOR, - consList.getConstructor("nil").getConstructorTerm())) + consList.getConstructor("nil").getTerm())) solver.simplify(dt1) dt2 = solver.mkTerm( Kind.APPLY_SELECTOR, - consList["cons"].getSelector("head").getSelectorTerm(), + consList["cons"].getSelector("head").getTerm(), dt1) solver.simplify(dt2) @@ -2589,7 +2589,7 @@ def test_tuple_project(solver): for i in indices: - selectorTerm = constructor[i].getSelectorTerm() + selectorTerm = constructor[i].getTerm() selectedTerm = solver.mkTerm(Kind.APPLY_SELECTOR, selectorTerm, tuple) simplifiedTerm = solver.simplify(selectedTerm) assert elements[i] == simplifiedTerm diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index c6168d17f..77800d69e 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -136,7 +136,7 @@ def test_is_datatype(solver): def test_is_constructor(solver): dt_sort = create_datatype_sort(solver) dt = dt_sort.getDatatype() - cons_sort = dt[0].getConstructorTerm().getSort() + cons_sort = dt[0].getTerm().getSort() assert cons_sort.isDatatypeConstructor() Sort(solver).isDatatypeConstructor() @@ -146,7 +146,7 @@ def test_is_selector(solver): dt = dt_sort.getDatatype() dt0 = dt[0] dt01 = dt0[1] - cons_sort = dt01.getSelectorTerm().getSort() + cons_sort = dt01.getTerm().getSort() assert cons_sort.isDatatypeSelector() Sort(solver).isDatatypeSelector() @@ -250,7 +250,7 @@ def test_datatype_sorts(solver): # get constructor dcons = dt[0] - consTerm = dcons.getConstructorTerm() + consTerm = dcons.getTerm() consSort = consTerm.getSort() assert consSort.isDatatypeConstructor() assert not consSort.isDatatypeTester() @@ -275,7 +275,7 @@ def test_datatype_sorts(solver): # get selector dselTail = dcons[1] - tailTerm = dselTail.getSelectorTerm() + tailTerm = dselTail.getTerm() assert tailTerm.getSort().isDatatypeSelector() assert tailTerm.getSort().getDatatypeSelectorDomainSort() == dtypeSort assert tailTerm.getSort().getDatatypeSelectorCodomainSort() == dtypeSort diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index c070b00ec..b9fc1e46a 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -187,10 +187,10 @@ def test_get_op(solver): c = solver.mkConst(intListSort, "c") list1 = listSort.getDatatype() # list datatype constructor and selector operator terms - consOpTerm = list1.getConstructor("cons").getConstructorTerm() - nilOpTerm = list1.getConstructor("nil").getConstructorTerm() - headOpTerm = list1["cons"].getSelector("head").getSelectorTerm() - tailOpTerm = list1["cons"].getSelector("tail").getSelectorTerm() + consOpTerm = list1.getConstructor("cons").getTerm() + nilOpTerm = list1.getConstructor("nil").getTerm() + headOpTerm = list1["cons"].getSelector("head").getTerm() + tailOpTerm = list1["cons"].getSelector("tail").getTerm() nilTerm = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, nilOpTerm) consTerm = solver.mkTerm(Kind.APPLY_CONSTRUCTOR, consOpTerm, -- 2.30.2