diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-19 13:36:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-19 13:36:59 -0500 |
| commit | 31717bf7c014bf1971cabcc9b871de5818278126 (patch) | |
| tree | d7331da2db605b16b67920990ae6def5db03dfd9 /src/theory/theory_state.h | |
| parent | 466520464a8ed862c3a323bb2fbcc92332d9384b (diff) | |
Make sets and strings solver states inherit from TheoryState (#4918)
This is towards the new standard for theory solvers.
This PR makes the custom states of sets and strings inherit from the standard base class TheoryState. It also makes a minor change to InferenceManager/SolverState to make sets more in line with the plan for a standard base class InferenceManager.
Followup PRs will establish the official TheoryState classes for all other theories (which in most cases will be an instance of the base class).
Diffstat (limited to 'src/theory/theory_state.h')
| -rw-r--r-- | src/theory/theory_state.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 71197dddc..de6e6d477 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -34,10 +34,10 @@ class TheoryState TheoryState(context::Context* c, context::UserContext* u, Valuation val); virtual ~TheoryState() {} /** - * Finish initialize, ee is a pointer to the official equality engine + * Set equality engine, where ee is a pointer to the official equality engine * of theory. */ - virtual void finishInit(eq::EqualityEngine* ee); + void setEqualityEngine(eq::EqualityEngine* ee); /** Get the SAT context */ context::Context* getSatContext() const; /** Get the user context */ |