From a7352156510fc2d43ea764d75f8da511d2401ea7 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
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 Iterable<DatatypeConstr
private native long getConstructor(long pointer, String name);
- /**
- * 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
- */
- public Term getConstructorTerm(String name)
- {
- long termPointer = getConstructorTerm(pointer, name);
- return new Term(solver, termPointer);
- }
-
- private native long getConstructorTerm(long pointer, String name);
-
/**
* 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/java/jni/datatype.cpp b/src/api/java/jni/datatype.cpp
index e6ba593f6..4af77bb4a 100644
--- a/src/api/java/jni/datatype.cpp
+++ b/src/api/java/jni/datatype.cpp
@@ -66,24 +66,6 @@ Java_io_github_cvc5_Datatype_getConstructor__JLjava_lang_String_2(
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
-/*
- * Class: io_github_cvc5_Datatype
- * Method: getConstructorTerm
- * Signature: (JLjava/lang/String;)J
- */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_Datatype_getConstructorTerm(
- JNIEnv* env, jobject, jlong pointer, jstring jName)
-{
- CVC5_JAVA_API_TRY_CATCH_BEGIN;
- Datatype* current = (Datatype*)pointer;
- const char* s = env->GetStringUTFChars(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