From 90fe2a057cdcdaea34f0a03f837159d9adb45914 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 24 Feb 2020 11:35:37 -0600 Subject: Add missing functions to new C++ API (#3769) --- src/api/cvc4cpp.cpp | 223 ++++++++++++++++++++++++++++++++----- src/api/cvc4cpp.h | 208 ++++++++++++++++++++++++++++++++-- test/unit/api/datatype_api_black.h | 116 ++++++++++++++++++- test/unit/api/sort_black.h | 81 ++++++++++++++ test/unit/api/term_black.h | 102 +++++++++++++++++ 5 files changed, 692 insertions(+), 38 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index b16e5afc5..41a374283 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -827,6 +827,14 @@ bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; } bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; } +bool Sort::operator<(const Sort& s) const { return *d_type < *s.d_type; } + +bool Sort::operator>(const Sort& s) const { return *d_type > *s.d_type; } + +bool Sort::operator<=(const Sort& s) const { return *d_type <= *s.d_type; } + +bool Sort::operator>=(const Sort& s) const { return *d_type >= *s.d_type; } + bool Sort::isNull() const { return isNullHelper(); } bool Sort::isBoolean() const { return d_type->isBoolean(); } @@ -853,6 +861,10 @@ bool Sort::isParametricDatatype() const return DatatypeType(*d_type).isParametric(); } +bool Sort::isConstructor() const { return d_type->isConstructor(); } +bool Sort::isSelector() const { return d_type->isSelector(); } +bool Sort::isTester() const { return d_type->isTester(); } + bool Sort::isFunction() const { return d_type->isFunction(); } bool Sort::isPredicate() const { return d_type->isPredicate(); } @@ -873,6 +885,13 @@ bool Sort::isFirstClass() const { return d_type->isFirstClass(); } bool Sort::isFunctionLike() const { return d_type->isFunctionLike(); } +bool Sort::isSubsortOf(Sort s) const { return d_type->isSubtypeOf(*s.d_type); } + +bool Sort::isComparableTo(Sort s) const +{ + return d_type->isComparableTo(*s.d_type); +} + Datatype Sort::getDatatype() const { CVC4_API_CHECK(isDatatype()) << "Expected datatype sort."; @@ -902,6 +921,27 @@ std::string Sort::toString() const { return d_type->toString(); } // to the new API. !!! CVC4::Type Sort::getType(void) const { return *d_type; } +/* Constructor sort ------------------------------------------------------- */ + +size_t Sort::getConstructorArity() const +{ + CVC4_API_CHECK(isConstructor()) << "Not a function sort."; + return ConstructorType(*d_type).getArity(); +} + +std::vector Sort::getConstructorDomainSorts() const +{ + CVC4_API_CHECK(isConstructor()) << "Not a function sort."; + std::vector types = ConstructorType(*d_type).getArgTypes(); + return typeVectorToSorts(types); +} + +Sort Sort::getConstructorCodomainSort() const +{ + CVC4_API_CHECK(isConstructor()) << "Not a function sort."; + return ConstructorType(*d_type).getRangeType(); +} + /* Function sort ------------------------------------------------------- */ size_t Sort::getFunctionArity() const @@ -1290,6 +1330,44 @@ bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; } bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; } +bool Term::operator<(const Term& t) const { return *d_expr < *t.d_expr; } + +bool Term::operator>(const Term& t) const { return *d_expr > *t.d_expr; } + +bool Term::operator<=(const Term& t) const { return *d_expr <= *t.d_expr; } + +bool Term::operator>=(const Term& t) const { return *d_expr >= *t.d_expr; } + +size_t Term::getNumChildren() const +{ + CVC4_API_CHECK_NOT_NULL; + // special case for apply kinds + if (isApplyKind(d_expr->getKind())) + { + return d_expr->getNumChildren() + 1; + } + return d_expr->getNumChildren(); +} + +Term Term::operator[](size_t index) const +{ + CVC4_API_CHECK_NOT_NULL; + // special cases for apply kinds + if (isApplyKind(d_expr->getKind())) + { + CVC4_API_CHECK(d_expr->hasOperator()) + << "Expected apply kind to have operator when accessing child of Term"; + if (index == 0) + { + // return the operator + return api::Term(d_expr->getOperator()); + } + // otherwise we are looking up child at (index-1) + index--; + } + return api::Term((*d_expr)[index]); +} + uint64_t Term::getId() const { CVC4_API_CHECK_NOT_NULL; @@ -1308,6 +1386,37 @@ Sort Term::getSort() const return Sort(d_expr->getType()); } +Term Term::substitute(Term e, Term replacement) const +{ + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK(!e.isNull()) + << "Expected non-null term to replace in substitute"; + CVC4_API_CHECK(!replacement.isNull()) + << "Expected non-null term as replacement in substitute"; + CVC4_API_CHECK(e.getSort().isComparableTo(replacement.getSort())) + << "Expecting terms of comparable sort in substitute"; + return api::Term(d_expr->substitute(e.getExpr(), replacement.getExpr())); +} + +Term Term::substitute(const std::vector es, + const std::vector& replacements) const +{ + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK(es.size() == replacements.size()) + << "Expecting vectors of the same arity in substitute"; + for (unsigned i = 0, nterms = es.size(); i < nterms; i++) + { + CVC4_API_CHECK(!es[i].isNull()) + << "Expected non-null term to replace in substitute"; + CVC4_API_CHECK(!replacements[i].isNull()) + << "Expected non-null term as replacement in substitute"; + CVC4_API_CHECK(es[i].getSort().isComparableTo(replacements[i].getSort())) + << "Expecting terms of comparable sort in substitute"; + } + return api::Term(d_expr->substitute(termVectorToExprs(es), + termVectorToExprs(replacements))); +} + bool Term::hasOp() const { CVC4_API_CHECK_NOT_NULL; @@ -1344,6 +1453,12 @@ Op Term::getOp() const bool Term::isNull() const { return isNullHelper(); } +bool Term::isConst() const +{ + CVC4_API_CHECK_NOT_NULL; + return d_expr->isConst(); +} + Term Term::notTerm() const { CVC4_API_CHECK_NOT_NULL; @@ -1775,15 +1890,15 @@ DatatypeSelector::DatatypeSelector() { d_stor = nullptr; } DatatypeSelector::DatatypeSelector(const CVC4::DatatypeConstructorArg& stor) : d_stor(new CVC4::DatatypeConstructorArg(stor)) { + CVC4_API_CHECK(d_stor->isResolved()) << "Expected resolved datatype selector"; } DatatypeSelector::~DatatypeSelector() {} -bool DatatypeSelector::isResolved() const { return d_stor->isResolved(); } +std::string DatatypeSelector::getName() const { return d_stor->getName(); } Term DatatypeSelector::getSelectorTerm() const { - CVC4_API_CHECK(isResolved()) << "Expected resolved datatype selector."; Term sel = d_stor->getSelector(); return sel; } @@ -1816,39 +1931,55 @@ DatatypeConstructor::DatatypeConstructor() { d_ctor = nullptr; } DatatypeConstructor::DatatypeConstructor(const CVC4::DatatypeConstructor& ctor) : d_ctor(new CVC4::DatatypeConstructor(ctor)) { + CVC4_API_CHECK(d_ctor->isResolved()) + << "Expected resolved datatype constructor"; } DatatypeConstructor::~DatatypeConstructor() {} -bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); } +std::string DatatypeConstructor::getName() const { return d_ctor->getName(); } Term DatatypeConstructor::getConstructorTerm() const { - CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor."; Term ctor = d_ctor->getConstructor(); return ctor; } +Term DatatypeConstructor::getTesterTerm() const +{ + Term tst = d_ctor->getTester(); + return tst; +} + +std::string DatatypeConstructor::getTesterName() const +{ + return d_ctor->getTesterName(); +} + +size_t DatatypeConstructor::getNumSelectors() const +{ + return d_ctor->getNumArgs(); +} + +DatatypeSelector DatatypeConstructor::operator[](size_t index) const +{ + return (*d_ctor)[index]; +} + DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const { - // CHECK: selector with name exists? - // CHECK: is resolved? - return (*d_ctor)[name]; + return getSelectorForName(name); } DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const { - // CHECK: cons with name exists? - // CHECK: is resolved? - return (*d_ctor)[name]; + return getSelectorForName(name); } Term DatatypeConstructor::getSelectorTerm(const std::string& name) const { - // CHECK: cons with name exists? - // CHECK: is resolved? - Term sel = d_ctor->getSelector(name); - return sel; + DatatypeSelector sel = getSelector(name); + return sel.getSelectorTerm(); } DatatypeConstructor::const_iterator DatatypeConstructor::begin() const @@ -1940,6 +2071,25 @@ const CVC4::DatatypeConstructor& DatatypeConstructor::getDatatypeConstructor( return *d_ctor; } +DatatypeSelector DatatypeConstructor::getSelectorForName( + const std::string& name) const +{ + bool foundSel = false; + size_t index = 0; + for (size_t i = 0, nsels = getNumSelectors(); i < nsels; i++) + { + if ((*d_ctor)[i].getName() == name) + { + index = i; + foundSel = true; + break; + } + } + CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor " + << getName() << " exists"; + return (*d_ctor)[index]; +} + std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor) { out << ctor.toString(); @@ -1951,6 +2101,7 @@ std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor) Datatype::Datatype(const CVC4::Datatype& dtype) : d_dtype(new CVC4::Datatype(dtype)) { + CVC4_API_CHECK(d_dtype->isResolved()) << "Expected resolved datatype"; } // Nullary constructor for Cython @@ -1960,39 +2111,42 @@ Datatype::~Datatype() {} DatatypeConstructor Datatype::operator[](size_t idx) const { - // CHECK (maybe): is resolved? CVC4_API_CHECK(idx < getNumConstructors()) << "Index out of bounds."; return (*d_dtype)[idx]; } DatatypeConstructor Datatype::operator[](const std::string& name) const { - // CHECK: cons with name exists? - // CHECK: is resolved? - return (*d_dtype)[name]; + return getConstructorForName(name); } DatatypeConstructor Datatype::getConstructor(const std::string& name) const { - // CHECK: cons with name exists? - // CHECK: is resolved? - return (*d_dtype)[name]; + return getConstructorForName(name); } Term Datatype::getConstructorTerm(const std::string& name) const { - // CHECK: cons with name exists? - // CHECK: is resolved? - Term ctor = d_dtype->getConstructor(name); - return ctor; + DatatypeConstructor ctor = getConstructor(name); + return ctor.getConstructorTerm(); } +std::string Datatype::getName() const { return d_dtype->getName(); } + size_t Datatype::getNumConstructors() const { return d_dtype->getNumConstructors(); } bool Datatype::isParametric() const { return d_dtype->isParametric(); } +bool Datatype::isCodatatype() const { return d_dtype->isCodatatype(); } + +bool Datatype::isTuple() const { return d_dtype->isTuple(); } + +bool Datatype::isRecord() const { return d_dtype->isRecord(); } + +bool Datatype::isFinite() const { return d_dtype->isFinite(); } +bool Datatype::isWellFounded() const { return d_dtype->isWellFounded(); } std::string Datatype::toString() const { return d_dtype->getName(); } @@ -2010,6 +2164,25 @@ Datatype::const_iterator Datatype::end() const // to the new API. !!! const CVC4::Datatype& Datatype::getDatatype(void) const { return *d_dtype; } +DatatypeConstructor Datatype::getConstructorForName( + const std::string& name) const +{ + bool foundCons = false; + size_t index = 0; + for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++) + { + if ((*d_dtype)[i].getName() == name) + { + index = i; + foundCons = true; + break; + } + } + CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype " + << getName() << " exists"; + return (*d_dtype)[index]; +} + Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype, bool begin) { diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 9820aeb19..103637a7d 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -229,6 +229,34 @@ class CVC4_PUBLIC Sort */ bool operator!=(const Sort& s) const; + /** + * Comparison for ordering on sorts. + * @param s the sort to compare to + * @return true if this sort is less than s + */ + bool operator<(const Sort& s) const; + + /** + * Comparison for ordering on sorts. + * @param s the sort to compare to + * @return true if this sort is greater than s + */ + bool operator>(const Sort& s) const; + + /** + * Comparison for ordering on sorts. + * @param s the sort to compare to + * @return true if this sort is less than or equal to s + */ + bool operator<=(const Sort& s) const; + + /** + * Comparison for ordering on sorts. + * @param s the sort to compare to + * @return true if this sort is greater than or equal to s + */ + bool operator>=(const Sort& s) const; + /** * @return true if this Sort is a null sort. */ @@ -294,6 +322,23 @@ class CVC4_PUBLIC Sort */ bool isParametricDatatype() const; + /** + * Is this a constructor sort? + * @return true if the sort is a constructor sort + */ + bool isConstructor() const; + + /** + * Is this a selector sort? + * @return true if the sort is a selector sort + */ + bool isSelector() const; + + /** + * Is this a tester sort? + * @return true if the sort is a tester sort + */ + bool isTester() const; /** * Is this a function sort? * @return true if the sort is a function sort @@ -372,6 +417,19 @@ class CVC4_PUBLIC Sort */ bool isFunctionLike() const; + /** + * Is this sort a subsort of the given sort? + * @return true if this sort is a subsort of s + */ + bool isSubsortOf(Sort s) const; + + /** + * Is this sort comparable to the given sort (i.e., do they share + * a common ancestor in the subsort tree)? + * @return true if this sort is comparable to s + */ + bool isComparableTo(Sort s) const; + /** * @return the underlying datatype of a datatype sort */ @@ -399,10 +457,27 @@ class CVC4_PUBLIC Sort // to the new API. !!! CVC4::Type getType(void) const; + /* Constructor sort ------------------------------------------------------- */ + + /** + * @return the arity of a constructor sort + */ + size_t getConstructorArity() const; + + /** + * @return the domain sorts of a constructor sort + */ + std::vector getConstructorDomainSorts() const; + + /** + * @return the codomain sort of a constructor sort + */ + Sort getConstructorCodomainSort() const; + /* Function sort ------------------------------------------------------- */ /** - * @return the arity of a function sort + * @return the arity of a function sort */ size_t getFunctionArity() const; @@ -721,6 +796,48 @@ class CVC4_PUBLIC Term */ bool operator!=(const Term& t) const; + /** + * Comparison for ordering on terms. + * @param t the term to compare to + * @return true if this term is less than t + */ + bool operator<(const Term& t) const; + + /** + * Comparison for ordering on terms. + * @param t the term to compare to + * @return true if this term is greater than t + */ + bool operator>(const Term& t) const; + + /** + * Comparison for ordering on terms. + * @param t the term to compare to + * @return true if this term is less than or equal to t + */ + bool operator<=(const Term& t) const; + + /** + * Comparison for ordering on terms. + * @param t the term to compare to + * @return true if this term is greater than or equal to t + */ + bool operator>=(const Term& t) const; + + /** + * Returns the number of children of this term. + * + * @return the number of term + */ + size_t getNumChildren() const; + + /** + * Get the child term at a given index. + * @param index the index of the child term to return + * @return the child term with the given index + */ + Term operator[](size_t index) const; + /** * @return the id of this term */ @@ -736,6 +853,18 @@ class CVC4_PUBLIC Term */ Sort getSort() const; + /** + * @return the result of replacing "e" by "replacement" in this term + */ + Term substitute(Term e, Term replacement) const; + + /** + * @return the result of simulatenously replacing "es" by "replacements" in + * this term + */ + Term substitute(const std::vector es, + const std::vector& replacements) const; + /** * @return true iff this term has an operator */ @@ -752,6 +881,13 @@ class CVC4_PUBLIC Term */ bool isNull() const; + /** + * Check if this is a Term representing a constant. + * + * @return true if a constant Term + */ + bool isConst() const; + /** * Boolean negation. * @return the Boolean negation of this term @@ -1205,10 +1341,8 @@ class CVC4_PUBLIC DatatypeSelector */ ~DatatypeSelector(); - /** - * @return true if this datatype selector has been resolved. - */ - bool isResolved() const; + /** @return the name of this Datatype selector. */ + std::string getName() const; /** * Get the selector operator of this datatype selector. @@ -1262,10 +1396,8 @@ class CVC4_PUBLIC DatatypeConstructor */ ~DatatypeConstructor(); - /** - * @return true if this datatype constructor has been resolved. - */ - bool isResolved() const; + /** @return the name of this Datatype constructor. */ + std::string getName() const; /** * Get the constructor operator of this datatype constructor. @@ -1273,6 +1405,24 @@ class CVC4_PUBLIC DatatypeConstructor */ Term getConstructorTerm() const; + /** + * Get the tester operator of this datatype constructor. + * @return the tester operator + */ + Term getTesterTerm() const; + + /** + * @return the tester name for this Datatype constructor. + */ + std::string getTesterName() const; + + /** + * @return the number of selectors (so far) of this Datatype constructor. + */ + size_t getNumSelectors() const; + + /** @return the i^th DatatypeSelector. */ + DatatypeSelector operator[](size_t index) const; /** * Get the datatype selector with the given name. * This is a linear search through the selectors, so in case of @@ -1386,6 +1536,12 @@ class CVC4_PUBLIC DatatypeConstructor const CVC4::DatatypeConstructor& getDatatypeConstructor(void) const; private: + /** + * Return selector for name. + * @param name The name of selector to find + * @return the selector object for the name + */ + DatatypeSelector getSelectorForName(const std::string& name) const; /** * The internal datatype constructor wrapped by this datatype constructor. * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is @@ -1445,12 +1601,36 @@ class CVC4_PUBLIC Datatype */ Term getConstructorTerm(const std::string& name) const; - /** Get the number of constructors for this Datatype. */ + /** @return the name of this Datatype. */ + std::string getName() const; + + /** @return the number of constructors for this Datatype. */ size_t getNumConstructors() const; - /** Is this Datatype parametric? */ + /** @return true if this datatype is parametric */ bool isParametric() const; + /** @return true if this datatype corresponds to a co-datatype */ + bool isCodatatype() const; + + /** @return true if this datatype corresponds to a tuple */ + bool isTuple() const; + + /** @return true if this datatype corresponds to a record */ + bool isRecord() const; + + /** @return true if this datatype is finite */ + bool isFinite() const; + + /** + * Is this datatype well-founded? If this datatype is not a codatatype, + * this returns false if there are no values of this datatype that are of + * finite size. + * + * @return true if this datatype is well-founded + */ + bool isWellFounded() const; + /** * @return a string representation of this datatype */ @@ -1544,6 +1724,12 @@ class CVC4_PUBLIC Datatype const CVC4::Datatype& getDatatype(void) const; private: + /** + * Return constructor for name. + * @param name The name of constructor to find + * @return the constructor object for the name + */ + DatatypeConstructor getConstructorForName(const std::string& name) const; /** * The internal datatype wrapped by this datatype. * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h index b9c671a30..2d7a9c12b 100644 --- a/test/unit/api/datatype_api_black.h +++ b/test/unit/api/datatype_api_black.h @@ -28,6 +28,9 @@ class DatatypeBlack : public CxxTest::TestSuite void testMkDatatypeSort(); + void testDatatypeStructs(); + void testDatatypeNames(); + private: Solver d_solver; }; @@ -50,8 +53,117 @@ void DatatypeBlack::testMkDatatypeSort() DatatypeConstructor consConstr = d[0]; DatatypeConstructor nilConstr = d[1]; TS_ASSERT_THROWS(d[2], CVC4ApiException&); - TS_ASSERT(consConstr.isResolved()); - TS_ASSERT(nilConstr.isResolved()); TS_ASSERT_THROWS_NOTHING(consConstr.getConstructorTerm()); TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm()); } + +void DatatypeBlack::testDatatypeStructs() +{ + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + + // create datatype sort to test + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", intSort); + cons.addSelector(head); + DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); + cons.addSelector(tail); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype dt = dtypeSort.getDatatype(); + TS_ASSERT(!dt.isCodatatype()); + TS_ASSERT(!dt.isTuple()); + TS_ASSERT(!dt.isRecord()); + TS_ASSERT(!dt.isFinite()); + TS_ASSERT(dt.isWellFounded()); + // get constructor + DatatypeConstructor dcons = dt[0]; + Term consTerm = dcons.getConstructorTerm(); + TS_ASSERT(dcons.getNumSelectors() == 2); + // get tester name: notice this is only to support the Z3-style datatypes + // prior to SMT-LIB 2.6 where testers where changed to indexed symbols. + TS_ASSERT_THROWS_NOTHING(dcons.getTesterName()); + + // create datatype sort to test + DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum"); + DatatypeConstructorDecl ca("A"); + dtypeSpecEnum.addConstructor(ca); + DatatypeConstructorDecl cb("B"); + dtypeSpecEnum.addConstructor(cb); + DatatypeConstructorDecl cc("C"); + dtypeSpecEnum.addConstructor(cc); + Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum); + Datatype dtEnum = dtypeSortEnum.getDatatype(); + TS_ASSERT(!dtEnum.isTuple()); + TS_ASSERT(dtEnum.isFinite()); + + // create codatatype + DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true); + DatatypeConstructorDecl consStream("cons"); + DatatypeSelectorDecl headStream("head", intSort); + consStream.addSelector(headStream); + DatatypeSelectorDecl tailStream("tail", DatatypeDeclSelfSort()); + consStream.addSelector(tailStream); + dtypeSpecStream.addConstructor(consStream); + Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream); + Datatype dtStream = dtypeSortStream.getDatatype(); + TS_ASSERT(dtStream.isCodatatype()); + TS_ASSERT(!dtStream.isFinite()); + // codatatypes may be well-founded + TS_ASSERT(dtStream.isWellFounded()); + + // create tuple + Sort tupSort = d_solver.mkTupleSort({boolSort}); + Datatype dtTuple = tupSort.getDatatype(); + TS_ASSERT(dtTuple.isTuple()); + TS_ASSERT(!dtTuple.isRecord()); + TS_ASSERT(dtTuple.isFinite()); + TS_ASSERT(dtTuple.isWellFounded()); + + // create record + std::vector> fields = { + std::make_pair("b", boolSort), std::make_pair("i", intSort)}; + Sort recSort = d_solver.mkRecordSort(fields); + TS_ASSERT(recSort.isDatatype()); + Datatype dtRecord = recSort.getDatatype(); + TS_ASSERT(!dtRecord.isTuple()); + TS_ASSERT(dtRecord.isRecord()); + TS_ASSERT(!dtRecord.isFinite()); + TS_ASSERT(dtRecord.isWellFounded()); +} + +void DatatypeBlack::testDatatypeNames() +{ + Sort intSort = d_solver.getIntegerSort(); + + // create datatype sort to test + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", intSort); + cons.addSelector(head); + DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); + cons.addSelector(tail); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype dt = dtypeSort.getDatatype(); + TS_ASSERT(dt.getName() == std::string("list")); + TS_ASSERT_THROWS_NOTHING(dt.getConstructor("nil")); + TS_ASSERT_THROWS_NOTHING(dt["cons"]); + TS_ASSERT_THROWS(dt.getConstructor("head"), CVC4ApiException&); + TS_ASSERT_THROWS(dt.getConstructor(""), CVC4ApiException&); + + DatatypeConstructor dcons = dt[0]; + TS_ASSERT(dcons.getName() == std::string("cons")); + TS_ASSERT_THROWS_NOTHING(dcons.getSelector("head")); + TS_ASSERT_THROWS_NOTHING(dcons["tail"]); + TS_ASSERT_THROWS(dcons.getSelector("cons"), CVC4ApiException&); + + // get selector + DatatypeSelector dselTail = dcons[1]; + TS_ASSERT(dselTail.getName() == std::string("tail")); +} diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h index 4ea29b8d7..1bac8a283 100644 --- a/test/unit/api/sort_black.h +++ b/test/unit/api/sort_black.h @@ -27,6 +27,7 @@ class SortBlack : public CxxTest::TestSuite void tearDown() override; void testGetDatatype(); + void testDatatypeSorts(); void testInstantiate(); void testGetFunctionArity(); void testGetFunctionDomainSorts(); @@ -47,6 +48,9 @@ class SortBlack : public CxxTest::TestSuite void testGetTupleLength(); void testGetTupleSorts(); + void testSortCompare(); + void testSortSubtyping(); + private: Solver d_solver; }; @@ -72,6 +76,49 @@ void SortBlack::testGetDatatype() TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&); } +void SortBlack::testDatatypeSorts() +{ + Sort intSort = d_solver.getIntegerSort(); + // create datatype sort to test + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", intSort); + cons.addSelector(head); + DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); + cons.addSelector(tail); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype dt = dtypeSort.getDatatype(); + TS_ASSERT(!dtypeSort.isConstructor()); + TS_ASSERT_THROWS(dtypeSort.getConstructorCodomainSort(), CVC4ApiException&); + TS_ASSERT_THROWS(dtypeSort.getConstructorDomainSorts(), CVC4ApiException&); + TS_ASSERT_THROWS(dtypeSort.getConstructorArity(), CVC4ApiException&); + + // get constructor + DatatypeConstructor dcons = dt[0]; + Term consTerm = dcons.getConstructorTerm(); + Sort consSort = consTerm.getSort(); + TS_ASSERT(consSort.isConstructor()); + TS_ASSERT(!consSort.isTester()); + TS_ASSERT(!consSort.isSelector()); + TS_ASSERT(consSort.getConstructorArity() == 2); + std::vector consDomSorts = consSort.getConstructorDomainSorts(); + TS_ASSERT(consDomSorts[0] == intSort); + TS_ASSERT(consDomSorts[1] == dtypeSort); + TS_ASSERT(consSort.getConstructorCodomainSort() == dtypeSort); + + // get tester + Term isConsTerm = dcons.getTesterTerm(); + TS_ASSERT(isConsTerm.getSort().isTester()); + + // get selector + DatatypeSelector dselTail = dcons[1]; + Term tailTerm = dselTail.getSelectorTerm(); + TS_ASSERT(tailTerm.getSort().isSelector()); +} + void SortBlack::testInstantiate() { // instantiate parametric datatype, check should not fail @@ -277,3 +324,37 @@ void SortBlack::testGetTupleSorts() Sort bvSort = d_solver.mkBitVectorSort(32); TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&); } + +void SortBlack::testSortCompare() +{ + Sort boolSort = d_solver.getBooleanSort(); + Sort intSort = d_solver.getIntegerSort(); + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort bvSort2 = d_solver.mkBitVectorSort(32); + TS_ASSERT(bvSort >= bvSort2); + TS_ASSERT(bvSort <= bvSort2); + TS_ASSERT((intSort > boolSort) != (intSort < boolSort)); + TS_ASSERT((intSort > bvSort || intSort == bvSort) == (intSort >= bvSort)); +} + +void SortBlack::testSortSubtyping() +{ + Sort intSort = d_solver.getIntegerSort(); + Sort realSort = d_solver.getRealSort(); + TS_ASSERT(intSort.isSubsortOf(realSort)); + TS_ASSERT(!realSort.isSubsortOf(intSort)); + TS_ASSERT(intSort.isComparableTo(realSort)); + TS_ASSERT(realSort.isComparableTo(intSort)); + + Sort arraySortII = d_solver.mkArraySort(intSort, intSort); + Sort arraySortIR = d_solver.mkArraySort(intSort, realSort); + TS_ASSERT(!arraySortII.isComparableTo(intSort)); + // we do not support subtyping for arrays + TS_ASSERT(!arraySortII.isComparableTo(arraySortIR)); + + Sort setSortI = d_solver.mkSetSort(intSort); + Sort setSortR = d_solver.mkSetSort(realSort); + // we support subtyping for sets + TS_ASSERT(setSortI.isSubsortOf(setSortR)); + TS_ASSERT(setSortR.isComparableTo(setSortI)); +} diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index ea619db7c..8f63c55ec 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -39,6 +39,10 @@ class TermBlack : public CxxTest::TestSuite void testIteTerm(); void testTermAssignment(); + void testTermCompare(); + void testTermChildren(); + void testSubstitute(); + void testIsConst(); private: Solver d_solver; @@ -652,3 +656,101 @@ void TermBlack::testTermAssignment() t2 = d_solver.mkReal(2); TS_ASSERT_EQUALS(t1, d_solver.mkReal(1)); } + +void TermBlack::testTermCompare() +{ + Term t1 = d_solver.mkReal(1); + Term t2 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2)); + Term t3 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2)); + TS_ASSERT(t2 >= t3); + TS_ASSERT(t2 <= t3); + TS_ASSERT((t1 > t2) != (t1 < t2)); + TS_ASSERT((t1 > t2 || t1 == t2) == (t1 >= t2)); +} + +void TermBlack::testTermChildren() +{ + // simple term 2+3 + Term two = d_solver.mkReal(2); + Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkReal(3)); + TS_ASSERT(t1[0] == two); + TS_ASSERT(t1.getNumChildren() == 2); + Term tnull; + TS_ASSERT_THROWS(tnull.getNumChildren(), CVC4ApiException&); + + // apply term f(2) + Sort intSort = d_solver.getIntegerSort(); + Sort fsort = d_solver.mkFunctionSort(intSort, intSort); + Term f = d_solver.mkConst(fsort, "f"); + Term t2 = d_solver.mkTerm(APPLY_UF, f, two); + // due to our higher-order view of terms, we treat f as a child of APPLY_UF + TS_ASSERT(t2.getNumChildren() == 2); + TS_ASSERT_EQUALS(t2[0], f); + TS_ASSERT_EQUALS(t2[1], two); + TS_ASSERT_THROWS(tnull[0], CVC4ApiException&); +} + +void TermBlack::testSubstitute() +{ + Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); + Term one = d_solver.mkReal(1); + Term ttrue = d_solver.mkTrue(); + Term xpx = d_solver.mkTerm(PLUS, x, x); + Term onepone = d_solver.mkTerm(PLUS, one, one); + + TS_ASSERT_EQUALS(xpx.substitute(x, one), onepone); + TS_ASSERT_EQUALS(onepone.substitute(one, x), xpx); + // incorrect due to type + TS_ASSERT_THROWS(xpx.substitute(one, ttrue), CVC4ApiException&); + + // simultaneous substitution + Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y"); + Term xpy = d_solver.mkTerm(PLUS, x, y); + Term xpone = d_solver.mkTerm(PLUS, y, one); + std::vector es; + std::vector rs; + es.push_back(x); + rs.push_back(y); + es.push_back(y); + rs.push_back(one); + TS_ASSERT_EQUALS(xpy.substitute(es, rs), xpone); + + // incorrect substitution due to arity + rs.pop_back(); + TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&); + + // incorrect substitution due to types + rs.push_back(ttrue); + TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&); + + // null cannot substitute + Term tnull; + TS_ASSERT_THROWS(tnull.substitute(one, x), CVC4ApiException&); + TS_ASSERT_THROWS(xpx.substitute(tnull, x), CVC4ApiException&); + TS_ASSERT_THROWS(xpx.substitute(x, tnull), CVC4ApiException&); + rs.pop_back(); + rs.push_back(tnull); + TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&); + es.clear(); + rs.clear(); + es.push_back(x); + rs.push_back(y); + TS_ASSERT_THROWS(tnull.substitute(es, rs), CVC4ApiException&); + es.push_back(tnull); + rs.push_back(one); + TS_ASSERT_THROWS(xpx.substitute(es, rs), CVC4ApiException&); +} + +void TermBlack::testIsConst() +{ + Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); + Term one = d_solver.mkReal(1); + Term xpone = d_solver.mkTerm(PLUS, x, one); + Term onepone = d_solver.mkTerm(PLUS, one, one); + TS_ASSERT(!x.isConst()); + TS_ASSERT(one.isConst()); + TS_ASSERT(!xpone.isConst()); + TS_ASSERT(!onepone.isConst()); + Term tnull; + TS_ASSERT_THROWS(tnull.isConst(), CVC4ApiException&); +} -- cgit v1.2.3