Add mkOp for a single Kind (#3522)

1 files changed, 12 insertions, 1 deletions

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 326a8fb70..8c9bdc10c 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1890,10 +1890,21 @@ class CVC4_PUBLIC Solver
                const std::vector<Term>& terms) const;
 
   /* .................................................................... */
-  /* Create Operator Terms                                                */
+  /* Create Operators                                                     */
   /* .................................................................... */
 
   /**
+   * Create an operator for a builtin Kind
+   * The Kind may not be the Kind for an indexed operator
+   *   (e.g. BITVECTOR_EXTRACT)
+   * Note: in this case, the Op simply wraps the Kind.
+   * The Kind can be used in mkTerm directly without
+   *   creating an op first.
+   * @param kind the kind to wrap
+   */
+  Op mkOp(Kind kind) const;
+
+  /**
    * Create operator of kind:
    *   - CHAIN
    * See enum Kind for a description of the parameters.