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(); }
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(); }
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.";
// 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
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;
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;
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;
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;
}
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
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();
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
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(); }
// 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)
{
*/
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 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
*/
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
*/
// 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;
*/
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
*/
*/
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 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
*/
~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.
*/
~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.
*/
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
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
*/
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
*/
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
void testMkDatatypeSort();
+ void testDatatypeStructs();
+ void testDatatypeNames();
+
private:
Solver d_solver;
};
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<std::pair<std::string, Sort>> 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"));
+}
void tearDown() override;
void testGetDatatype();
+ void testDatatypeSorts();
void testInstantiate();
void testGetFunctionArity();
void testGetFunctionDomainSorts();
void testGetTupleLength();
void testGetTupleSorts();
+ void testSortCompare();
+ void testSortSubtyping();
+
private:
Solver d_solver;
};
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<Sort> 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
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));
+}
void testIteTerm();
void testTermAssignment();
+ void testTermCompare();
+ void testTermChildren();
+ void testSubstitute();
+ void testIsConst();
private:
Solver d_solver;
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<Term> es;
+ std::vector<Term> 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&);
+}
projects / cvc5.git / commitdiff