From 0398c53a582a3242ef89dceae59d00137f17df79 Mon Sep 17 00:00:00 2001 From: makaimann Date: Tue, 18 Feb 2020 20:11:52 -0800 Subject: [PATCH] Change datatype selector/constructor/tester to terms (#3773) --- examples/api/datatypes-new.cpp | 14 +++-- src/api/cvc4cpp.cpp | 97 ++++++++++++++++++++++------------ src/api/cvc4cpp.h | 29 +++------- test/unit/api/solver_black.h | 93 +++++++++++++++++--------------- test/unit/api/term_black.h | 92 ++++++++++++++++++++++++++++---- 5 files changed, 211 insertions(+), 114 deletions(-) diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index 43f97796e..c5773fa72 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -36,9 +36,11 @@ 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(consList.getConstructorTerm("cons"), - slv.mkReal(0), - slv.mkTerm(consList.getConstructorTerm("nil"))); + Term t = slv.mkTerm( + APPLY_CONSTRUCTOR, + consList.getConstructorTerm("cons"), + slv.mkReal(0), + slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); std::cout << "t is " << t << std::endl << "sort of cons is " @@ -51,7 +53,8 @@ void test(Solver& slv, Sort& consListSort) // 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(consList["cons"].getSelectorTerm("head"), t); + Term t2 = + slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); std::cout << "t2 is " << t2 << std::endl << "simplify(t2) is " << slv.simplify(t2) << std::endl @@ -116,7 +119,8 @@ 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(paramConsList["cons"].getSelectorTerm("head"), a); + 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 " diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index ef7296089..f4ca1147f 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -593,6 +593,18 @@ namespace { bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; } +/** Returns true if the internal kind is one where the API term structure + * differs from internal structure. This happens for APPLY_* kinds. + * The API takes a "higher-order" perspective and treats functions as well + * as datatype constructors/selectors/testers as terms + * but interally they are not + */ +bool isApplyKind(CVC4::Kind k) +{ + return (k == CVC4::Kind::APPLY_UF || k == CVC4::Kind::APPLY_CONSTRUCTOR + || k == CVC4::Kind::APPLY_SELECTOR || k == CVC4::Kind::APPLY_TESTER); +} + #ifdef CVC4_ASSERTIONS bool isDefinedIntKind(CVC4::Kind k) { @@ -611,8 +623,20 @@ uint32_t maxArity(Kind k) { Assert(isDefinedKind(k)); Assert(isDefinedIntKind(extToIntKind(k))); - return CVC4::ExprManager::maxArity(extToIntKind(k)); + uint32_t max = CVC4::ExprManager::maxArity(extToIntKind(k)); + + // special cases for API level + // higher-order logic perspective at API + // functions/constructors/selectors/testers are terms + if (isApplyKind(extToIntKind(k)) + && max != std::numeric_limits::max()) // be careful not to + // overflow + { + max++; + } + return max; } + } // namespace std::string kindToString(Kind k) @@ -1327,36 +1351,31 @@ Op Term::getOp() const CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(d_expr->hasOperator()) << "Expecting Term to have an Op when calling getOp()"; - CVC4::Expr op = d_expr->getOperator(); - CVC4::Type t = op.getType(); - // special cases for Datatype operators - if (t.isSelector()) + // special cases for parameterized operators that are not indexed operators + // the API level differs from the internal structure + // indexed operators are stored in Ops + // whereas functions and datatype operators are terms, and the Op + // is one of the APPLY_* kinds + if (isApplyKind(d_expr->getKind())) { - return Op(APPLY_SELECTOR, op); + return Op(intToExtKind(d_expr->getKind())); } - else if (t.isConstructor()) + else if (d_expr->isParameterized()) { - return Op(APPLY_CONSTRUCTOR, op); - } - else if (t.isTester()) - { - return Op(APPLY_TESTER, op); + // it's an indexed operator + // so we should return the indexed op + CVC4::Expr op = d_expr->getOperator(); + return Op(intToExtKind(d_expr->getKind()), op); } else { - return Op(intToExtKind(op.getKind()), op); + return Op(intToExtKind(d_expr->getKind())); } } bool Term::isNull() const { return isNullHelper(); } -bool Term::isParameterized() const -{ - CVC4_API_CHECK_NOT_NULL; - return d_expr->isParameterized(); -} - Term Term::notTerm() const { CVC4_API_CHECK_NOT_NULL; @@ -1528,14 +1547,18 @@ Term::const_iterator Term::const_iterator::operator++(int) Term Term::const_iterator::operator*() const { Assert(d_orig_expr != nullptr); - if (!d_pos && (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF)) + // this term has an extra child (mismatch between API and internal structure) + // the extra child will be the first child + bool extra_child = isApplyKind(d_orig_expr->getKind()); + + if (!d_pos && extra_child) { return Term(d_orig_expr->getOperator()); } else { uint32_t idx = d_pos; - if (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF) + if (extra_child) { Assert(idx > 0); --idx; @@ -1553,7 +1576,13 @@ Term::const_iterator Term::begin() const Term::const_iterator Term::end() const { int endpos = d_expr->getNumChildren(); - if (d_expr->getKind() == CVC4::Kind::APPLY_UF) + // special cases for APPLY_* + // the API differs from the internal structure + // the API takes a "higher-order" perspective and the applied + // function or datatype constructor/selector/tester is a Term + // which means it needs to be one of the children, even though + // internally it is not + if (isApplyKind(d_expr->getKind())) { // one more child if this is a UF application (count the UF as a child) ++endpos; @@ -1771,11 +1800,11 @@ DatatypeSelector::~DatatypeSelector() {} bool DatatypeSelector::isResolved() const { return d_stor->isResolved(); } -Op DatatypeSelector::getSelectorTerm() const +Term DatatypeSelector::getSelectorTerm() const { CVC4_API_CHECK(isResolved()) << "Expected resolved datatype selector."; - CVC4::Expr sel = d_stor->getSelector(); - return Op(APPLY_SELECTOR, sel); + Term sel = d_stor->getSelector(); + return sel; } std::string DatatypeSelector::toString() const @@ -1812,11 +1841,11 @@ DatatypeConstructor::~DatatypeConstructor() {} bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); } -Op DatatypeConstructor::getConstructorTerm() const +Term DatatypeConstructor::getConstructorTerm() const { CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor."; - CVC4::Expr ctor = d_ctor->getConstructor(); - return Op(APPLY_CONSTRUCTOR, ctor); + Term ctor = d_ctor->getConstructor(); + return ctor; } DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const @@ -1833,12 +1862,12 @@ DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const return (*d_ctor)[name]; } -Op DatatypeConstructor::getSelectorTerm(const std::string& name) const +Term DatatypeConstructor::getSelectorTerm(const std::string& name) const { // CHECK: cons with name exists? // CHECK: is resolved? - CVC4::Expr sel = d_ctor->getSelector(name); - return Op(APPLY_SELECTOR, sel); + Term sel = d_ctor->getSelector(name); + return sel; } DatatypeConstructor::const_iterator DatatypeConstructor::begin() const @@ -1963,12 +1992,12 @@ DatatypeConstructor Datatype::getConstructor(const std::string& name) const return (*d_dtype)[name]; } -Op Datatype::getConstructorTerm(const std::string& name) const +Term Datatype::getConstructorTerm(const std::string& name) const { // CHECK: cons with name exists? // CHECK: is resolved? - CVC4::Expr ctor = d_dtype->getConstructor(name); - return Op(APPLY_CONSTRUCTOR, ctor); + Term ctor = d_dtype->getConstructor(name); + return ctor; } size_t Datatype::getNumConstructors() const diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 84615afc0..f7f16832a 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -752,23 +752,6 @@ class CVC4_PUBLIC Term */ bool isNull() const; - /** - * @return true if this expression is parameterized. - * - * !!! The below documentation is not accurate until we have a way of getting - * operators from terms. - * - * In detail, a term that is parameterized is one that has an operator that - * must be provided in addition to its kind to construct it. For example, - * say we want to re-construct a Term t where its children a1, ..., an are - * replaced by b1 ... bn. Then there are two cases: - * (1) If t is parametric, call: - * mkTerm(t.getKind(), t.getOperator(), b1, ..., bn ) - * (2) If t is not parametric, call: - * mkTerm(t.getKind(), b1, ..., bn ) - */ - bool isParameterized() const; - /** * Boolean negation. * @return the Boolean negation of this term @@ -1218,9 +1201,9 @@ class CVC4_PUBLIC DatatypeSelector /** * Get the selector operator of this datatype selector. - * @return the selector operator + * @return the selector term */ - Op getSelectorTerm() const; + Term getSelectorTerm() const; /** * @return a string representation of this datatype selector @@ -1275,9 +1258,9 @@ class CVC4_PUBLIC DatatypeConstructor /** * Get the constructor operator of this datatype constructor. - * @return the constructor operator + * @return the constructor term */ - Op getConstructorTerm() const; + Term getConstructorTerm() const; /** * Get the datatype selector with the given name. @@ -1296,7 +1279,7 @@ class CVC4_PUBLIC DatatypeConstructor * @param name the name of the datatype selector * @return a term representing the datatype selector with the given name */ - Op getSelectorTerm(const std::string& name) const; + Term getSelectorTerm(const std::string& name) const; /** * @return a string representation of this datatype constructor @@ -1443,7 +1426,7 @@ class CVC4_PUBLIC Datatype * similarly-named constructors, the * first is returned. */ - Op getConstructorTerm(const std::string& name) const; + Term getConstructorTerm(const std::string& name) const; /** Get the number of constructors for this Datatype. */ size_t getNumConstructors() const; diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 2831b840d..e53b989f0 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -642,47 +642,55 @@ void SolverBlack::testMkTermFromOp() Term c = d_solver->mkConst(intListSort, "c"); Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms - Op consTerm1 = list.getConstructorTerm("cons"); - Op consTerm2 = list.getConstructor("cons").getConstructorTerm(); - Op nilTerm1 = list.getConstructorTerm("nil"); - Op nilTerm2 = list.getConstructor("nil").getConstructorTerm(); - Op headTerm1 = list["cons"].getSelectorTerm("head"); - Op headTerm2 = list["cons"].getSelector("head").getSelectorTerm(); - Op tailTerm1 = list["cons"].getSelectorTerm("tail"); - Op tailTerm2 = list["cons"]["tail"].getSelectorTerm(); - - // mkTerm(Kind kind, Op op) const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm1)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm2)); - TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(consTerm2), CVC4ApiException&); + Term consTerm1 = list.getConstructorTerm("cons"); + Term consTerm2 = list.getConstructor("cons").getConstructorTerm(); + Term nilTerm1 = list.getConstructorTerm("nil"); + Term nilTerm2 = 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 + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm2)); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, nilTerm1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, consTerm1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm2), + CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(headTerm1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(tailTerm2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1), + CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&); - // mkTerm(Kind kind, Op op, Term child) const + // mkTerm(Op op, Term child) const TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a)); TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkReal(1))); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(headTerm1, c)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(tailTerm2, c)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c)); TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1, d_solver->mkReal(0)), - CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)), + CVC4ApiException&); - // mkTerm(Kind kind, Op op, Term child1, Term child2) const + // mkTerm(Op op, Term child1, Term child2) const TS_ASSERT_THROWS_NOTHING( d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2))); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( - consTerm1, d_solver->mkReal(0), d_solver->mkTerm(nilTerm1))); + TS_ASSERT_THROWS_NOTHING( + d_solver->mkTerm(APPLY_CONSTRUCTOR, + consTerm1, + d_solver->mkReal(0), + d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1))); TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, d_solver->mkReal(1), Term()), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, Term(), d_solver->mkReal(1)), CVC4ApiException&); - // mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3) + // mkTerm(Op op, Term child1, Term child2, Term child3) // const TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2))); @@ -942,26 +950,23 @@ void SolverBlack::testGetOp() Sort consListSort = d_solver->mkDatatypeSort(consListSpec); Datatype consList = consListSort.getDatatype(); - Op consTerm = consList.getConstructorTerm("cons"); - Op nilTerm = consList.getConstructorTerm("nil"); - Op headTerm = consList["cons"].getSelectorTerm("head"); - - TS_ASSERT(consTerm.getKind() == APPLY_CONSTRUCTOR); - TS_ASSERT(nilTerm.getKind() == APPLY_CONSTRUCTOR); - TS_ASSERT(headTerm.getKind() == APPLY_SELECTOR); + Term consTerm = consList.getConstructorTerm("cons"); + Term nilTerm = consList.getConstructorTerm("nil"); + Term headTerm = consList["cons"].getSelectorTerm("head"); - Term listnil = d_solver->mkTerm(nilTerm); - Term listcons1 = d_solver->mkTerm(consTerm, d_solver->mkReal(1), listnil); - Term listhead = d_solver->mkTerm(headTerm, listcons1); + Term listnil = d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm); + Term listcons1 = d_solver->mkTerm( + APPLY_CONSTRUCTOR, consTerm, d_solver->mkReal(1), listnil); + Term listhead = d_solver->mkTerm(APPLY_SELECTOR, headTerm, listcons1); TS_ASSERT(listnil.hasOp()); - TS_ASSERT_EQUALS(listnil.getOp(), nilTerm); + TS_ASSERT_EQUALS(listnil.getOp(), APPLY_CONSTRUCTOR); TS_ASSERT(listcons1.hasOp()); - TS_ASSERT_EQUALS(listcons1.getOp(), consTerm); + TS_ASSERT_EQUALS(listcons1.getOp(), APPLY_CONSTRUCTOR); TS_ASSERT(listhead.hasOp()); - TS_ASSERT_EQUALS(listhead.getOp(), headTerm); + TS_ASSERT_EQUALS(listhead.getOp(), APPLY_SELECTOR); } void SolverBlack::testPush1() @@ -1074,12 +1079,14 @@ void SolverBlack::testSimplify() TS_ASSERT(i1 == d_solver->simplify(i3)); Datatype consList = consListSort.getDatatype(); - Term dt1 = - d_solver->mkTerm(consList.getConstructorTerm("cons"), - d_solver->mkReal(0), - d_solver->mkTerm(consList.getConstructorTerm("nil"))); + Term dt1 = d_solver->mkTerm( + APPLY_CONSTRUCTOR, + consList.getConstructorTerm("cons"), + d_solver->mkReal(0), + d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1)); - Term dt2 = d_solver->mkTerm(consList["cons"].getSelectorTerm("head"), dt1); + Term dt2 = d_solver->mkTerm( + APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt2)); Term b1 = d_solver->mkVar(bvSort, "b1"); diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index 0d5400f5f..ea619db7c 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -28,8 +28,8 @@ class TermBlack : public CxxTest::TestSuite void testGetId(); void testGetKind(); void testGetSort(); + void testGetOp(); void testIsNull(); - void testIsParameterized(); void testNotTerm(); void testAndTerm(); void testOrTerm(); @@ -152,6 +152,88 @@ void TermBlack::testGetSort() TS_ASSERT(p_f_y.getSort() == boolSort); } +void TermBlack::testGetOp() +{ + Sort intsort = d_solver.getIntegerSort(); + Sort bvsort = d_solver.mkBitVectorSort(8); + Sort arrsort = d_solver.mkArraySort(bvsort, intsort); + Sort funsort = d_solver.mkFunctionSort(intsort, bvsort); + + Term x = d_solver.mkConst(intsort, "x"); + Term a = d_solver.mkConst(arrsort, "a"); + Term b = d_solver.mkConst(bvsort, "b"); + + TS_ASSERT(!x.hasOp()); + TS_ASSERT_THROWS(x.getOp(), CVC4ApiException&); + + Term ab = d_solver.mkTerm(SELECT, a, b); + Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); + Term extb = d_solver.mkTerm(ext, b); + + TS_ASSERT(ab.hasOp()); + TS_ASSERT_EQUALS(ab.getOp(), Op(SELECT)); + TS_ASSERT(!ab.getOp().isIndexed()); + // can compare directly to a Kind (will invoke Op constructor) + TS_ASSERT_EQUALS(ab.getOp(), SELECT); + TS_ASSERT(extb.hasOp()); + TS_ASSERT(extb.getOp().isIndexed()); + TS_ASSERT_EQUALS(extb.getOp(), ext); + + Term f = d_solver.mkConst(funsort, "f"); + Term fx = d_solver.mkTerm(APPLY_UF, f, x); + + TS_ASSERT(!f.hasOp()); + TS_ASSERT_THROWS(f.getOp(), CVC4ApiException&); + TS_ASSERT(fx.hasOp()); + TS_ASSERT_EQUALS(fx.getOp(), APPLY_UF); + std::vector children(fx.begin(), fx.end()); + // testing rebuild from op and children + TS_ASSERT_EQUALS(fx, d_solver.mkTerm(fx.getOp(), children)); + + // Test Datatypes Ops + Sort sort = d_solver.mkParamSort("T"); + DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort); + DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl nil("nil"); + DatatypeSelectorDecl head("head", sort); + DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); + cons.addSelector(head); + cons.addSelector(tail); + listDecl.addConstructor(cons); + listDecl.addConstructor(nil); + Sort listSort = d_solver.mkDatatypeSort(listDecl); + Sort intListSort = + listSort.instantiate(std::vector{d_solver.getIntegerSort()}); + 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 headOpTerm = list["cons"].getSelectorTerm("head"); + Term tailOpTerm = list["cons"].getSelectorTerm("tail"); + + Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm); + Term consTerm = d_solver.mkTerm( + APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkReal(0), nilTerm); + Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm); + Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm); + + TS_ASSERT(nilTerm.hasOp()); + TS_ASSERT(consTerm.hasOp()); + TS_ASSERT(headTerm.hasOp()); + TS_ASSERT(tailTerm.hasOp()); + + TS_ASSERT_EQUALS(nilTerm.getOp(), APPLY_CONSTRUCTOR); + TS_ASSERT_EQUALS(consTerm.getOp(), APPLY_CONSTRUCTOR); + TS_ASSERT_EQUALS(headTerm.getOp(), APPLY_SELECTOR); + TS_ASSERT_EQUALS(tailTerm.getOp(), APPLY_SELECTOR); + + // Test rebuilding + children.clear(); + children.insert(children.begin(), headTerm.begin(), headTerm.end()); + TS_ASSERT_EQUALS(headTerm, d_solver.mkTerm(headTerm.getOp(), children)); +} + void TermBlack::testIsNull() { Term x; @@ -189,14 +271,6 @@ void TermBlack::testNotTerm() TS_ASSERT_THROWS_NOTHING(p_f_x.notTerm()); } -void TermBlack::testIsParameterized() -{ - Term n; - TS_ASSERT_THROWS(n.isParameterized(), CVC4ApiException&); - Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x"); - TS_ASSERT_THROWS_NOTHING(x.isParameterized()); -} - void TermBlack::testAndTerm() { Sort bvSort = d_solver.mkBitVectorSort(8); -- 2.30.2