diff options
Diffstat (limited to 'src/api/cvc4cpp.h')
-rw-r--r-- | src/api/cvc4cpp.h | 51 |
1 files changed, 39 insertions, 12 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index a06f2e415..b8da070fc 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1100,6 +1100,17 @@ class CVC4_PUBLIC DatatypeSelector ~DatatypeSelector(); /** + * @return true if this datatype selector has been resolved. + */ + bool isResolved() const; + + /** + * Get the selector operator of this datatype selector. + * @return the selector operator + */ + OpTerm getSelectorTerm() const; + + /** * @return a string representation of this datatype selector */ std::string toString() const; @@ -1154,7 +1165,7 @@ class CVC4_PUBLIC DatatypeConstructor * Get the constructor operator of this datatype constructor. * @return the constructor operator */ - Term getConstructorTerm() const; + OpTerm getConstructorTerm() const; /** * Get the datatype selector with the given name. @@ -1173,7 +1184,7 @@ class CVC4_PUBLIC DatatypeConstructor * @param name the name of the datatype selector * @return a term representing the datatype selector with the given name */ - Term getSelectorTerm(const std::string& name) const; + OpTerm getSelectorTerm(const std::string& name) const; /** * @return a string representation of this datatype constructor @@ -1320,7 +1331,7 @@ class CVC4_PUBLIC Datatype * similarly-named constructors, the * first is returned. */ - Term getConstructorTerm(const std::string& name) const; + OpTerm getConstructorTerm(const std::string& name) const; /** Get the number of constructors for this Datatype. */ size_t getNumConstructors() const; @@ -1725,43 +1736,59 @@ class CVC4_PUBLIC Solver Term mkTerm(Kind kind, const std::vector<Term>& children) const; /** - * Create unary term from a given operator term. + * Create nullary term of given kind from a given operator term. + * Create operator terms with mkOpTerm(). + * @param kind the kind of the term + * @param the operator term + * @return the Term + */ + Term mkTerm(Kind kind, OpTerm opTerm) const; + + /** + * Create unary term of given kind from a given operator term. * Create operator terms with mkOpTerm(). + * @param kind the kind of the term * @param the operator term * @child the child of the term * @return the Term */ - Term mkTerm(OpTerm opTerm, Term child) const; + Term mkTerm(Kind kind, OpTerm opTerm, Term child) const; /** - * Create binary term from a given operator term. + * Create binary term of given kind from a given operator term. + * @param kind the kind of the term * Create operator terms with mkOpTerm(). * @param the operator term * @child1 the first child of the term * @child2 the second child of the term * @return the Term */ - Term mkTerm(OpTerm opTerm, Term child1, Term child2) const; + Term mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const; /** - * Create ternary term from a given operator term. + * Create ternary term of given kind from a given operator term. * Create operator terms with mkOpTerm(). + * @param kind the kind of the term * @param the operator term * @child1 the first child of the term * @child2 the second child of the term * @child3 the third child of the term * @return the Term */ - Term mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const; + Term mkTerm( + Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const; /** - * Create n-ary term from a given operator term. + * Create n-ary term of given kind from a given operator term. * Create operator terms with mkOpTerm(). + * @param kind the kind of the term * @param the operator term * @children the children of the term * @return the Term */ - Term mkTerm(OpTerm opTerm, const std::vector<Term>& children) const; + Term mkTerm(Kind kind, + OpTerm opTerm, + const std::vector<Term>& children) const; /** * Create a tuple term. Terms are automatically converted if sorts are @@ -2485,7 +2512,7 @@ class CVC4_PUBLIC Solver /* Helper to convert a vector of sorts to internal types. */ std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const; /* Helper to check for API misuse in mkTerm functions. */ - void checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const; + void checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const; /* Helper to check for API misuse in mkOpTerm functions. */ void checkMkTerm(Kind kind, uint32_t nchildren) const; /* Helper for mk-functions that call d_exprMgr->mkConst(). */ |