summaryrefslogtreecommitdiff
path: root/src/api/cpp/cvc5_kind.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/api/cpp/cvc5_kind.h')
-rw-r--r--src/api/cpp/cvc5_kind.h16
1 files changed, 16 insertions, 0 deletions
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 2ec190360..2c5d2873e 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -412,6 +412,22 @@ enum CVC5_EXPORT Kind : int32_t
* - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
*/
IAND,
+ /**
+ * Operator for raising 2 to a non-negative integer power
+ *
+ * Create with:
+ * - `Solver::mkOp(Kind kind) const`
+ *
+
+ * Parameters:
+ * - 1: Op of kind IAND
+ * - 2: Integer term
+ *
+ * Create with:
+ * - `Solver::mkTerm(const Op& op, const Term& child) const`
+ * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
+ */
+ POW2,
#if 0
/* Synonym for MULT. */
NONLINEAR_MULT,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback