Remove replay and use-theory options and idl (#4186)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 31 Mar 2020 19:27:04 +0000 (14:27 -0500)
committerGitHub <noreply@github.com>
Tue, 31 Mar 2020 19:27:04 +0000 (14:27 -0500)
commit63f887783e003546bf8de4501774a79dbcf8d4b0
tree2932cf5aa5c81746f5747d48c1ea73ea47c0a624
parent5272f5d02f109b7dbfdb5088a1efbf7d13b64487
Remove replay and use-theory options and idl (#4186)

Towards disentangling Options / NodeManager / SmtEngine.

This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work.

The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it.

The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging.

It also removes the solver in src/theory/idl, which cannot be enabled after this commit.
52 files changed:
CMakeLists.txt
cmake/ConfigCompetition.cmake
cmake/ConfigDebug.cmake
cmake/ConfigProduction.cmake
cmake/ConfigTesting.cmake
configure.sh
src/CMakeLists.txt
src/base/configuration.cpp
src/base/configuration.h
src/base/configuration_private.h
src/bindings/java/CMakeLists.txt
src/cvc4.i
src/expr/CMakeLists.txt
src/expr/expr_stream.h [deleted file]
src/expr/expr_stream.i [deleted file]
src/expr/metakind_template.h
src/expr/mkmetakind
src/main/command_executor.cpp
src/main/command_executor.h
src/main/driver_unified.cpp
src/options/CMakeLists.txt
src/options/idl_options.toml [deleted file]
src/options/options.h
src/options/options_handler.cpp
src/options/options_handler.h
src/options/options_public_functions.cpp
src/options/options_template.cpp
src/options/smt_options.toml
src/options/theory_options.toml
src/parser/cvc/Cvc.g
src/parser/parser.h
src/prop/minisat/core/Solver.cc
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/prop/theory_proxy.h
src/smt/managed_ostreams.cpp
src/smt/managed_ostreams.h
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/theory/idl/idl_assertion.cpp [deleted file]
src/theory/idl/idl_assertion.h [deleted file]
src/theory/idl/idl_assertion_db.cpp [deleted file]
src/theory/idl/idl_assertion_db.h [deleted file]
src/theory/idl/idl_model.cpp [deleted file]
src/theory/idl/idl_model.h [deleted file]
src/theory/idl/kinds [deleted file]
src/theory/idl/theory_idl.cpp [deleted file]
src/theory/idl/theory_idl.h [deleted file]
src/theory/mktheorytraits
src/theory/theory_engine.cpp
src/theory/theory_engine.h