diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-24 11:35:37 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-24 11:35:37 -0600 |
commit | 90fe2a057cdcdaea34f0a03f837159d9adb45914 (patch) | |
tree | d8054e7cff139891f49bb1205c739afbbeeae7f0 /src | |
parent | a431edc5eba8b04812768b475b240725fb07d8c6 (diff) |
Add missing functions to new C++ API (#3769)
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 223 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 208 |
2 files changed, 395 insertions, 36 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> Sort::getConstructorDomainSorts() const +{ + CVC4_API_CHECK(isConstructor()) << "Not a function sort."; + std::vector<CVC4::Type> 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<Term> es, + const std::vector<Term>& 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 @@ -230,6 +230,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. */ bool isNull() const; @@ -295,6 +323,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 */ @@ -373,6 +418,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 */ Datatype getDatatype() const; @@ -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<Sort> 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; @@ -722,6 +797,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 */ uint64_t getId() const; @@ -737,6 +854,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<Term> es, + const std::vector<Term>& replacements) const; + + /** * @return true iff this term has an operator */ bool hasOp() const; @@ -753,6 +882,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. @@ -1274,6 +1406,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 * multiple, similarly-named selectors, the first is returned. @@ -1387,6 +1537,12 @@ class CVC4_PUBLIC DatatypeConstructor 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 * not ref counted. @@ -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 */ @@ -1545,6 +1725,12 @@ class CVC4_PUBLIC Datatype 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 * not ref counted. |