Modifying emptyset.h and sexpr. Adding SetLanguage.
authorTim King <taking@google.com>
Sat, 19 Dec 2015 01:19:07 +0000 (17:19 -0800)
committerTim King <taking@google.com>
Sat, 19 Dec 2015 01:19:07 +0000 (17:19 -0800)
commit5f207ba01302c3245e169bfbe2ed91ad0cd659cd
treee1131e8c2891e283ab028fba6a7a677bb4ac9f5f
parent7e4468ba0aa0b08eeb4ba1a86b1fdd839ae169d6
Modifying emptyset.h and sexpr. Adding SetLanguage.

- Modifies expr/emptyset.h to use SetType only as an incomplete type within expr/emptyset.h. This breaks the include cycle between expr/emptyset.h, expr/expr.h and expr/type.h.
- Refactors SExpr to avoid a potentially infinite cycle. This is likely overkill, but it works.
- Moving Expr::setlanguage and related utilities out of the Expr class and into their own file. This allows files in util/ to know the output language set on an ostream.
32 files changed:
doc/libcvc4.3_template.in
examples/api/sets.cpp
examples/api/strings.cpp
examples/hashsmt/sha1_collision.cpp
examples/hashsmt/sha1_inversion.cpp
examples/nra-translate/normalize.cpp
examples/sets-translate/sets_translate.cpp
examples/translator.cpp
src/compat/cvc3_compat.cpp
src/expr/datatype.cpp
src/expr/emptyset.cpp
src/expr/emptyset.h
src/expr/expr_template.cpp
src/expr/expr_template.h
src/expr/node.h
src/expr/sexpr.cpp
src/expr/sexpr.h
src/main/command_executor_portfolio.cpp
src/main/driver_unified.cpp
src/options/Makefile.am
src/options/language.h
src/options/set_language.cpp [new file with mode: 0644]
src/options/set_language.h [new file with mode: 0644]
src/parser/cvc/Cvc.g
src/parser/smt2/Smt2.g
src/printer/smt2/smt2_printer.cpp
src/smt/smt_engine.cpp
src/smt/smt_options_handler.cpp
src/theory/quantifiers/term_database.cpp
test/system/ouroborous.cpp
test/system/smt2_compliance.cpp
test/unit/util/boolean_simplification_black.h