diff options
Diffstat (limited to 'src/theory/uf/kinds')
| -rw-r--r-- | src/theory/uf/kinds | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 2de3715e1..ec353dc59 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -6,6 +6,7 @@ theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" typechecker "theory/uf/theory_uf_type_rules.h" +instantiator ::CVC4::theory::uf::InstantiatorTheoryUf "theory/uf/theory_uf_instantiator.h" properties stable-infinite parametric properties check propagate staticLearning presolve @@ -15,4 +16,8 @@ parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule +operator CARDINALITY_CONSTRAINT 2 "cardinality constraint" + +typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule + endtheory |