Add SmtGlobals Class
authorTim King <taking@google.com>
Wed, 6 Jan 2016 00:29:44 +0000 (16:29 -0800)
committerTim King <taking@google.com>
Wed, 6 Jan 2016 00:29:44 +0000 (16:29 -0800)
commit5eabda0f55cee3be81aa7ae126269c32e818322f
treeb873e4cb8e5d37ff3bb70596494bc5964aaef135
parentb717513e2a1d956c4456d13e0625957fc84c2449
Add SmtGlobals Class
- The options replayStream, lemmaInputChannel, lemmaOutputChannel have been removed due to their datatypes. These datatypes were previously pointers to types that were not usable from the options/ library.
- The option replayLog has been removed due to inconsistent memory management.
- SmtGlobals is a class that wraps a pointer to each of these removed options. These can each be set independently.
- There is a single SmtGlobals per SmtEngine with the lifetime of the SmtEngine.
- A pointer to this is freely given to the user of an SmtEngine to parameterize the solver after construction.
- Selected classes have been given a copy of this pointer in their constructors.
- Removed the dependence on Node from Result. Moving Result back into util/.
84 files changed:
contrib/alttheoryskel/theory_DIR.cpp
contrib/alttheoryskel/theory_DIR.h
contrib/theoryskel/theory_DIR.cpp
contrib/theoryskel/theory_DIR.h
examples/nra-translate/smt2toisat.cpp
examples/sets-translate/sets_translate.cpp
src/Makefile.am
src/base/Makefile.am
src/base/lemma_input_channel_forward.h [deleted file]
src/base/lemma_output_channel_forward.h [deleted file]
src/cvc4.i
src/expr/Makefile.am
src/expr/result.cpp [deleted file]
src/expr/result.h [deleted file]
src/expr/result.i [deleted file]
src/main/command_executor.h
src/main/command_executor_portfolio.cpp
src/main/driver_unified.cpp
src/main/main.cpp
src/main/portfolio.cpp
src/options/options.h
src/options/options_handler_interface.cpp
src/options/options_handler_interface.h
src/options/options_template.cpp
src/options/smt_options
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/prop/theory_proxy.h
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/smt/smt_globals.cpp [new file with mode: 0644]
src/smt/smt_globals.h [new file with mode: 0644]
src/smt/smt_options_handler.cpp
src/smt/smt_options_handler.h
src/smt_util/command.h
src/smt_util/lemma_input_channel.h
src/smt_util/lemma_output_channel.h
src/theory/arith/simplex.h
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arith/theory_arith_private.cpp
src/theory/arith/theory_arith_private.h
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/booleans/theory_bool.h
src/theory/builtin/theory_builtin.h
src/theory/bv/bitblaster_template.h
src/theory/bv/bv_eager_solver.h
src/theory/bv/bv_quick_check.h
src/theory/bv/bv_subtheory_bitblast.h
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv.h
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/theory_datatypes.h
src/theory/fp/theory_fp.cpp
src/theory/fp/theory_fp.h
src/theory/idl/theory_idl.cpp
src/theory/idl/theory_idl.h
src/theory/output_channel.h
src/theory/quantifiers/theory_quantifiers.cpp
src/theory/quantifiers/theory_quantifiers.h
src/theory/sets/theory_sets.cpp
src/theory/sets/theory_sets.h
src/theory/sets/theory_sets_private.cpp
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h
src/util/Makefile.am
src/util/result.cpp [new file with mode: 0644]
src/util/result.h [new file with mode: 0644]
src/util/result.i [new file with mode: 0644]
test/unit/prop/cnf_stream_white.h
test/unit/theory/theory_arith_white.h
test/unit/theory/theory_engine_white.h
test/unit/theory/theory_white.h