Introduce the theory state object (#4910)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 18 Aug 2020 20:52:30 +0000 (15:52 -0500)
committerGitHub <noreply@github.com>
Tue, 18 Aug 2020 20:52:30 +0000 (15:52 -0500)
commitaa8da1ff4e7f119408dbf14074b9a5efcb06618b
treeae22e7d28eeb30f6ed60dd2fee6a9cd3c23f4a55
parent712f798dbcab7536c21f2e7bc5e971370d898743
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.
src/CMakeLists.txt
src/theory/theory.cpp
src/theory/theory.h
src/theory/theory_state.cpp [new file with mode: 0644]
src/theory/theory_state.h [new file with mode: 0644]