The Tuesday Afternoon Catch-All Commit (TACAC):
authorMorgan Deters <mdeters@gmail.com>
Wed, 26 Sep 2012 03:07:01 +0000 (03:07 +0000)
committerMorgan Deters <mdeters@gmail.com>
Wed, 26 Sep 2012 03:07:01 +0000 (03:07 +0000)
commit7f84ff856af53047c2af2c1c1987340f9075ec7c
tree6e49732af41fccb76edbc004f6e62f1751cebc64
parent60c0b1855d20aeb67ac16312bb4dd00664e28f8f
The Tuesday Afternoon Catch-All Commit (TACAC):

* --early-exit and --no-early-exit command line options (the former is default for all builds except debug builds)

* New SEXPR kind for doing lists of things (we previously used TUPLEs for this purpose, but TUPLEs will be used in future by the datatypes theory, and so cannot have function symbols in them, etc.).

* SMT-LIB compliant output for (set-option :produce-unsat-cores true) and (get-unsat-core)

(this commit was certified error- and warning-free by the test-and-commit script.)
14 files changed:
src/expr/command.cpp
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/mkmetakind
src/expr/node_manager.h
src/expr/type.cpp
src/expr/type.h
src/expr/type_node.cpp
src/expr/type_node.h
src/main/driver_unified.cpp
src/main/options
src/smt/options_handlers.h
src/theory/builtin/kinds
src/theory/builtin/theory_builtin_type_rules.h