Renaming of SMT2 operator names, kinds for set theory
authorKshitij Bansal <kshitij@cs.nyu.edu>
Sun, 22 Jun 2014 05:17:27 +0000 (01:17 -0400)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Sun, 22 Jun 2014 21:37:25 +0000 (17:37 -0400)
commitb8ddf766460bfcf475e08ff52c889246e78f76cc
treeb631495d0801191c1e6b283854b5b30c11547fea
parent44d05f7def63e5f675f80dab8829c5759db7e065
Renaming of SMT2 operator names, kinds for set theory

* SET_SINGLETON kind renamed to just SINGLETON
* "setenum" smt2 opertor renamed to "singleton"[1]
* "in" smt2 operator renamed to "member"[2]

[1] It was anyhow accepting exactly one argument, so was bit misleading
    to call set enumerator.

[2] The corresponding kind was called MEMBER, so this will also make them
    consistent. Only inconsistency now is for subset: kind is called
    SUBSET but operator is called "subseteq".
53 files changed:
examples/sets-translate/sets_translate.cpp
src/parser/smt2/smt2.cpp
src/printer/smt2/smt2_printer.cpp
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/trigger.cpp
src/theory/sets/expr_patterns.h
src/theory/sets/kinds
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_type_enumerator.h
src/theory/sets/theory_sets_type_rules.h
test/regress/regress0/bug567.smt2
test/regress/regress0/sets/copy_check_heap_access_33_4.smt2
test/regress/regress0/sets/emptyset.smt2
test/regress/regress0/sets/eqtest.smt2
test/regress/regress0/sets/error2.smt2
test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2
test/regress/regress0/sets/fuzz14418.smt2
test/regress/regress0/sets/fuzz15201.smt2
test/regress/regress0/sets/fuzz31811.smt2
test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2
test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2
test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2
test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2
test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2
test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2
test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2
test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2
test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2
test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2
test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2
test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2
test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2
test/regress/regress0/sets/mar2014/sharing-preregister.smt2
test/regress/regress0/sets/mar2014/small.smt2
test/regress/regress0/sets/mar2014/smaller.smt2
test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
test/regress/regress0/sets/setel-eq.smt2
test/regress/regress0/sets/setofsets-disequal.smt2
test/regress/regress0/sets/sets-equal.smt2
test/regress/regress0/sets/sets-inter.smt2
test/regress/regress0/sets/sets-new.smt2
test/regress/regress0/sets/sets-sample.smt2
test/regress/regress0/sets/sets-sharing.smt2
test/regress/regress0/sets/sets-union.smt2
test/regress/regress0/sets/sharingbug.smt2
test/regress/regress0/sets/union-1a-flip.smt2
test/regress/regress0/sets/union-1a.smt2
test/regress/regress0/sets/union-1b-flip.smt2
test/regress/regress0/sets/union-1b.smt2
test/regress/regress0/sets/union-2.smt2