diff options
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 29 |
1 files changed, 6 insertions, 23 deletions
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 @@ -753,23 +753,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; |