diff options
Diffstat (limited to 'src/theory/sets/kinds')
| -rw-r--r-- | src/theory/sets/kinds | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index efd00093a..3fb73749d 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -12,7 +12,7 @@ rewriter ::CVC4::theory::sets::TheorySetsRewriter \ "theory/sets/theory_sets_rewriter.h" properties parametric -properties check propagate +properties check propagate presolve # constants constant EMPTYSET \ @@ -42,6 +42,7 @@ operator SUBSET 2 "subset predicate; first parameter a subset of second" operator MEMBER 2 "set membership predicate; first parameter a member of second" operator SINGLETON 1 "the set of the single element given as a parameter" operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)" +operator CARD 1 "set cardinality operator" operator JOIN 2 "set join" operator PRODUCT 2 "set cartesian product" @@ -56,6 +57,7 @@ typerule MEMBER ::CVC4::theory::sets::MemberTypeRule typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule typerule INSERT ::CVC4::theory::sets::InsertTypeRule +typerule CARD ::CVC4::theory::sets::CardTypeRule typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule @@ -67,6 +69,7 @@ construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule construle INSERT ::CVC4::theory::sets::InsertTypeRule +construle CARD ::CVC4::theory::sets::CardTypeRule construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule |