summaryrefslogtreecommitdiff
path: root/src/api/cvc4cppkind.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/api/cvc4cppkind.h')
-rw-r--r--src/api/cvc4cppkind.h16
1 files changed, 16 insertions, 0 deletions
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 5910ef1c9..6f84a9959 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -2074,6 +2074,22 @@ enum CVC4_PUBLIC Kind : int32_t
* mkTerm(Kind kind, Term child)
*/
BAG_IS_SINGLETON,
+ /**
+ * Bag.from_set converts a set to a bag.
+ * Parameters: 1
+ * -[1]: Term of set sort
+ * Create with:
+ * mkTerm(Kind kind, Term child)
+ */
+ BAG_FROM_SET,
+ /**
+ * Bag.to_set converts a bag to a set.
+ * Parameters: 1
+ * -[1]: Term of bag sort
+ * Create with:
+ * mkTerm(Kind kind, Term child)
+ */
+ BAG_TO_SET,
/* Strings --------------------------------------------------------------- */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback