summaryrefslogtreecommitdiff
path: root/src/theory/uf/kinds
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf/kinds')
-rw-r--r--src/theory/uf/kinds2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 888fa140f..e2d740e20 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -15,6 +15,8 @@ parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; fi
typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule
+variable BOOLEAN_TERM_VARIABLE "Boolean term variable"
+
operator CARDINALITY_CONSTRAINT 2 "cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S"
typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback