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/kinds3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index fa24df717..e99c3366c 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -18,4 +18,7 @@ typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule
operator CARDINALITY_CONSTRAINT 2 "cardinality constraint"
typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule
+operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint"
+typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule
+
endtheory
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback