add new theory (sets)
authorKshitij Bansal <kshitij@cs.nyu.edu>
Mon, 9 Sep 2013 18:47:53 +0000 (14:47 -0400)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Fri, 21 Feb 2014 12:25:13 +0000 (07:25 -0500)
commit50c26544c83a71e87efa487e4af063b1b5647c0f
tree82d4f3b2632a2cf06aff70550f37f80dc80d9543
parent53b8499f48a00dc876d56c76fbc79aafe5803529
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
78 files changed:
.gitignore
src/Makefile.am
src/context/cdhashset.h
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/node_manager.h
src/expr/type.cpp
src/expr/type.h
src/expr/type_node.h
src/options/Makefile.am
src/parser/smt2/Smt2.g
src/printer/smt2/smt2_printer.cpp
src/theory/arrays/array_info.h
src/theory/logic_info.cpp
src/theory/sets/.gitignore [new file with mode: 0644]
src/theory/sets/Makefile [new file with mode: 0644]
src/theory/sets/Makefile.am [new file with mode: 0644]
src/theory/sets/expr_patterns.h [new file with mode: 0644]
src/theory/sets/kinds [new file with mode: 0644]
src/theory/sets/options [new file with mode: 0644]
src/theory/sets/options_handlers.h [new file with mode: 0644]
src/theory/sets/term_info.h [new file with mode: 0644]
src/theory/sets/theory_sets.cpp [new file with mode: 0644]
src/theory/sets/theory_sets.h [new file with mode: 0644]
src/theory/sets/theory_sets_private.cpp [new file with mode: 0644]
src/theory/sets/theory_sets_private.h [new file with mode: 0644]
src/theory/sets/theory_sets_rewriter.cpp [new file with mode: 0644]
src/theory/sets/theory_sets_rewriter.h [new file with mode: 0644]
src/theory/sets/theory_sets_type_enumerator.h [new file with mode: 0644]
src/theory/sets/theory_sets_type_rules.h [new file with mode: 0644]
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/uf/equality_engine.h
src/util/Makefile.am
src/util/emptyset.cpp [new file with mode: 0644]
src/util/emptyset.h [new file with mode: 0644]
test/Makefile.am
test/regress/regress0/Makefile.am
test/regress/regress0/quantifiers/set8.smt2
test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2
test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2
test/regress/regress0/sets/Makefile [new file with mode: 0644]
test/regress/regress0/sets/Makefile.am [new file with mode: 0644]
test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 [new file with mode: 0644]
test/regress/regress0/sets/emptyset.smt2 [new file with mode: 0644]
test/regress/regress0/sets/eqtest.smt2 [new file with mode: 0644]
test/regress/regress0/sets/error1.smt2 [new file with mode: 0644]
test/regress/regress0/sets/error2.smt2 [new file with mode: 0644]
test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 [new file with mode: 0644]
test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 [new file with mode: 0644]
test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 [new file with mode: 0644]
test/regress/regress0/sets/setel-eq.smt2 [new file with mode: 0644]
test/regress/regress0/sets/sets-equal.smt2 [new file with mode: 0644]
test/regress/regress0/sets/sets-inter.smt2 [new file with mode: 0644]
test/regress/regress0/sets/sets-new.smt2 [new file with mode: 0644]
test/regress/regress0/sets/sets-sample.smt2 [new file with mode: 0644]
test/regress/regress0/sets/sets-sharing.smt2 [new file with mode: 0644]
test/regress/regress0/sets/sets-testlemma.smt2 [new file with mode: 0644]
test/regress/regress0/sets/sets-union.smt2 [new file with mode: 0644]
test/regress/regress0/sets/union-1a-flip.smt2 [new file with mode: 0644]
test/regress/regress0/sets/union-1a.smt2 [new file with mode: 0644]
test/regress/regress0/sets/union-1b-flip.smt2 [new file with mode: 0644]
test/regress/regress0/sets/union-1b.smt2 [new file with mode: 0644]
test/regress/regress0/sets/union-2.smt2 [new file with mode: 0644]
test/unit/theory/logic_info_white.h