From 50c26544c83a71e87efa487e4af063b1b5647c0f Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 9 Sep 2013 14:47:53 -0400
Subject: add new theory (sets)

Specification (smt2) -- as per this commit, subject to change

- Parameterized sort Set, e.g. (Set Int)

- Empty set constant (typed), use with "as" to specify the type, e.g.
    (as emptyset (Set Int))

- Create a singleton set
    (setenum X (Set X)) : creates singleton set

- Functions/operators
    (union (Set X) (Set X) (Set X))
    (intersection (Set X) (Set X) (Set X))
    (setminus (Set X) (Set X) (Set X))

- Predicates
    (in X (Set X) Bool) : membership
    (subseteq (Set X) (Set X) Bool) : set containment
---
 test/regress/regress0/sets/Makefile | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test/regress/regress0/sets/Makefile

(limited to 'test/regress/regress0/sets/Makefile')

diff --git a/test/regress/regress0/sets/Makefile b/test/regress/regress0/sets/Makefile
new file mode 100644
index 000000000..67ae35206
--- /dev/null
+++ b/test/regress/regress0/sets/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/sets
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
-- 
cgit v1.2.3