diff options
Diffstat (limited to 'src/api/cvc4cpp.cpp')
-rw-r--r-- | src/api/cvc4cpp.cpp | 223 |
1 files changed, 198 insertions, 25 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) { |