summaryrefslogtreecommitdiff
path: root/test/unit/theory/logic_info_white.h
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2013-09-09 14:47:53 -0400
committerKshitij Bansal <kshitij@cs.nyu.edu>2014-02-21 07:25:13 -0500
commit50c26544c83a71e87efa487e4af063b1b5647c0f (patch)
tree82d4f3b2632a2cf06aff70550f37f80dc80d9543 /test/unit/theory/logic_info_white.h
parent53b8499f48a00dc876d56c76fbc79aafe5803529 (diff)
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
Diffstat (limited to 'test/unit/theory/logic_info_white.h')
-rw-r--r--test/unit/theory/logic_info_white.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 5f6a93ae7..f569d6389 100644
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -512,6 +512,7 @@ public:
info = info.getUnlockedCopy();
TS_ASSERT( !info.isLocked() );
info.disableTheory(THEORY_STRINGS);
+ info.disableTheory(THEORY_SETS);
info.arithOnlyLinear();
info.disableIntegers();
info.lock();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback