diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-13 22:17:02 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-20 17:18:58 -0400 |
| commit | b5914204bd29c3bc3480fdec234882cedaad2c2a (patch) | |
| tree | 2ae5c1b1fc438c9e62ec67ccb41afd8fed77ccb0 /src/theory/sets/kinds | |
| parent | ac4a85a1682dd7e59d9ecc23ac7f3cd5e1716e4f (diff) | |
constant normal form and rewrite
Diffstat (limited to 'src/theory/sets/kinds')
| -rw-r--r-- | src/theory/sets/kinds | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index e46f3a4f8..a56601b98 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -41,6 +41,7 @@ operator SUBSET 2 "subset" operator MEMBER 2 "set membership" operator SET_SINGLETON 1 "singleton set" +operator FINITE_SET 1: "finite set" typerule UNION ::CVC4::theory::sets::SetUnionTypeRule typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule |