Add TheoryState objects to each Theory (#4920)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 20 Aug 2020 20:50:38 +0000 (15:50 -0500)
committerGitHub <noreply@github.com>
Thu, 20 Aug 2020 20:50:38 +0000 (15:50 -0500)
commit01a9d18f2b2ce20cf7a0672a865cf0c2873d6f6a
tree52e7dfc5d157b11fa4bd00855ad46238b6615338
parentc110363ccf39c9415c1a32bda6273fe8221db182
Add TheoryState objects to each Theory (#4920)

This initializes all theories with a TheoryState object (apart from bool and builtin which do not require one).

Two additional theories are known to require special state objects: TheoryArith, which has a custom way of detecting when in conflict, and TheoryQuantifiers, which can leverage a special state object for the purposes of refactoring and splitting apart QuantifiersEngine further. All other theories use default TheoryState objects.

Notice this PR does not update the theories to use these states yet, it simply adds the objects.
22 files changed:
src/CMakeLists.txt
src/theory/arith/arith_state.cpp [new file with mode: 0644]
src/theory/arith/arith_state.h [new file with mode: 0644]
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arith/theory_arith_private.h
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.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/fp/theory_fp.cpp
src/theory/fp/theory_fp.h
src/theory/quantifiers/quantifiers_state.cpp [new file with mode: 0644]
src/theory/quantifiers/quantifiers_state.h [new file with mode: 0644]
src/theory/quantifiers/theory_quantifiers.cpp
src/theory/quantifiers/theory_quantifiers.h
src/theory/sep/theory_sep.cpp
src/theory/sep/theory_sep.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h