Make ExtTheory independent of Theory (#5010)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 3 Sep 2020 01:18:48 +0000 (20:18 -0500)
committerGitHub <noreply@github.com>
Thu, 3 Sep 2020 01:18:48 +0000 (18:18 -0700)
commit8b4444dad1647c89b313deedd22129252078fe1b
tree23dbe0b73868eb5d2bc45d640eba755fa9b50fd5
parent5f3d21a7402538af837eaf943b5252b1db90080b
Make ExtTheory independent of Theory (#5010)

This makes it so that ExtTheory uses a generic callback instead of relying on Theory.

The primary purpose of this commit is to eliminate the connection of TheoryBV and ExtTheory. This commit moves all things related to ExtTheory in BV into CoreSolver.

It also refactors the use of ExtTheory in strings and arithmetic.
22 files changed:
src/CMakeLists.txt
src/theory/arith/nl/ext_theory_callback.cpp [new file with mode: 0644]
src/theory/arith/nl/ext_theory_callback.h [new file with mode: 0644]
src/theory/arith/nl/nonlinear_extension.cpp
src/theory/arith/nl/nonlinear_extension.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/bv/bv_subtheory_core.cpp
src/theory/bv/bv_subtheory_core.h
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/ext_theory.cpp
src/theory/ext_theory.h
src/theory/strings/extf_solver.cpp
src/theory/strings/extf_solver.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory.h