diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-10-04 15:10:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-04 15:10:24 -0500 |
| commit | 13cf41801f8f2bac538cb45d53ae7427916041a7 (patch) | |
| tree | 78e82b56e92004991890943ba5da863e6af3538f /src/theory/sets/kinds | |
| parent | d662d3321a46aac61973f7a90341ea870c0b1171 (diff) | |
Remove subtyping for sets theory (#5179)
This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:
Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON
Diffstat (limited to 'src/theory/sets/kinds')
| -rw-r--r-- | src/theory/sets/kinds | 27 |
1 files changed, 18 insertions, 9 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index fd941ab29..57120e42e 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -35,15 +35,23 @@ enumerator SET_TYPE \ "theory/sets/theory_sets_type_enumerator.h" # operators -operator UNION 2 "set union" -operator INTERSECTION 2 "set intersection" -operator SETMINUS 2 "set subtraction" -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 COMPLEMENT 1 "set COMPLEMENT (with respect to finite universe)" +operator UNION 2 "set union" +operator INTERSECTION 2 "set intersection" +operator SETMINUS 2 "set subtraction" +operator SUBSET 2 "subset predicate; first parameter a subset of second" +operator MEMBER 2 "set membership predicate; first parameter a member of second" + +constant SINGLETON_OP \ + ::CVC4::SingletonOp \ + ::CVC4::SingletonOpHashFunction \ + "theory/sets/singleton_op.h" \ + "operator for singletons; payload is an instance of the CVC4::SingletonOp class" +parameterized SINGLETON SINGLETON_OP 1 \ +"constructs a set of a single element. First parameter is a SingletonOp. Second is a term" + +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 COMPLEMENT 1 "set COMPLEMENT (with respect to finite universe)" nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it." # A set comprehension is specified by: @@ -82,6 +90,7 @@ typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule typerule SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule typerule SUBSET ::CVC4::theory::sets::SubsetTypeRule typerule MEMBER ::CVC4::theory::sets::MemberTypeRule +typerule SINGLETON_OP "SimpleTypeRule<RBuiltinOperator>" typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule typerule INSERT ::CVC4::theory::sets::InsertTypeRule |