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/theory/theory.cpp | |
| 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/theory/theory.cpp')
| -rw-r--r-- | src/theory/theory.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 02f84526f..9669d97e0 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -82,6 +82,7 @@ Theory::Theory(TheoryId id, d_valuation(valuation), d_equalityEngine(nullptr), d_allocEqualityEngine(nullptr), + d_theoryState(nullptr), d_proofsEnabled(false) { smtStatisticsRegistry()->registerStat(&d_checkTime); |