parser and core support for SMT-LIBv2 commands get-info, set-option, get-option,...
authorMorgan Deters <mdeters@gmail.com>
Tue, 5 Oct 2010 22:24:09 +0000 (22:24 +0000)
committerMorgan Deters <mdeters@gmail.com>
Tue, 5 Oct 2010 22:24:09 +0000 (22:24 +0000)
commit4c9f8d2b58d274e5bfea5fa28b02f005af71ef39
tree8db12e260b24978bbbed3363846f6daf7c0da04f
parent5e2f381b26d683691d9a040589536dc39c5831e0
parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
32 files changed:
src/context/cdlist.h
src/expr/command.cpp
src/expr/command.h
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/expr_template.cpp
src/expr/expr_template.h
src/expr/metakind_template.h
src/expr/node_manager.h
src/main/getopt.cpp
src/main/main.cpp
src/parser/parser.cpp
src/parser/parser.h
src/parser/smt/smt.h
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.cpp
src/parser/smt2/smt2.h
src/parser/smt2/smt2_input.h
src/smt/Makefile.am
src/smt/bad_option.h [new file with mode: 0644]
src/smt/noninteractive_exception.h [new file with mode: 0644]
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/theory/arith/kinds
src/theory/arrays/kinds
src/theory/booleans/kinds
src/theory/bv/kinds
src/theory/interrupted.h
src/theory/output_channel.h
src/theory/uf/kinds
src/util/options.h
src/util/sexpr.h