diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-18 15:52:30 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-18 15:52:30 -0500 |
| commit | aa8da1ff4e7f119408dbf14074b9a5efcb06618b (patch) | |
| tree | ae22e7d28eeb30f6ed60dd2fee6a9cd3c23f4a55 /src/CMakeLists.txt | |
| parent | 712f798dbcab7536c21f2e7bc5e971370d898743 (diff) | |
Introduce the theory state object (#4910)
This will be used as a standard way of querying and tracking state information in a Theory. The TheoryState object has a standard role in a number of the new standard templates for Theory:: methods.
The theory state is a collection of 4 Theory members (SAT context, user context, valuation, equality engine), as well as a SAT-context dependent "conflict" flag that indicates whether we have sent a conflict in this SAT conflict. It contains (safe) versions of equality engine queries, which are highly common in many theory solvers.
The next step will be to have the SolverState objects in theory of sets and strings inherit from this class.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 10cf23fdf..48bd99f44 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -818,6 +818,8 @@ libcvc4_add_sources( theory/theory_rewriter.cpp theory/theory_rewriter.h theory/theory_registrar.h + theory/theory_state.cpp + theory/theory_state.h theory/theory_test_utils.h theory/trust_node.cpp theory/trust_node.h |