diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-26 02:58:45 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-28 18:36:12 -0400 |
| commit | 4de6452284ff546d67d7e483bd4cb9a9bc64d8e3 (patch) | |
| tree | 9074c555658428471605c444e99b9c296bee5631 /src/theory/sets/kinds | |
| parent | efe23f3a0b6b9e42927420a27198d06dd02766ba (diff) | |
add construles, type_rules rm redundant, kinds cleanup
Diffstat (limited to 'src/theory/sets/kinds')
| -rw-r--r-- | src/theory/sets/kinds | 56 |
1 files changed, 29 insertions, 27 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index e46f3a4f8..12f114fc0 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -4,24 +4,25 @@ # src/theory/builtin/kinds. # -theory THEORY_SETS ::CVC4::theory::sets::TheorySets "theory/sets/theory_sets.h" +theory THEORY_SETS \ + ::CVC4::theory::sets::TheorySets \ + "theory/sets/theory_sets.h" typechecker "theory/sets/theory_sets_type_rules.h" -rewriter ::CVC4::theory::sets::TheorySetsRewriter "theory/sets/theory_sets_rewriter.h" +rewriter ::CVC4::theory::sets::TheorySetsRewriter \ + "theory/sets/theory_sets_rewriter.h" properties parametric -properties check propagate #presolve postsolve +properties check propagate -# Theory content goes here. - -# constants... +# constants constant EMPTYSET \ ::CVC4::EmptySet \ ::CVC4::EmptySetHashFunction \ "util/emptyset.h" \ "empty set" -# types... -operator SET_TYPE 1 "set type" # the type +# the type +operator SET_TYPE 1 "set type" cardinality SET_TYPE \ "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \ "theory/sets/theory_sets_type_rules.h" @@ -33,24 +34,25 @@ enumerator SET_TYPE \ "::CVC4::theory::sets::SetEnumerator" \ "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" -operator MEMBER 2 "set membership" - -operator SET_SINGLETON 1 "singleton set" - -typerule UNION ::CVC4::theory::sets::SetUnionTypeRule -typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule -typerule SETMINUS ::CVC4::theory::sets::SetSetminusTypeRule -typerule SUBSET ::CVC4::theory::sets::SetSubsetTypeRule -typerule MEMBER ::CVC4::theory::sets::SetMemberTypeRule -typerule SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule -typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule - -construle SET_SINGLETON ::CVC4::theory::sets::SetConstTypeRule -construle UNION ::CVC4::theory::sets::SetConstTypeRule +# operators +operator UNION 2 "set union" +operator INTERSECTION 2 "set intersection" +operator SETMINUS 2 "set subtraction" +operator SUBSET 2 "subset" +operator MEMBER 2 "set membership" +operator SET_SINGLETON 1 "singleton set" + +typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule +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 SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule +typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule + +construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule +construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule +construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule +construle SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule endtheory |