New C++ API: Fix checks for mkTerm. (#2820)

This required fixing the OpTerm handling for mkTerm functions in the API.

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(). */