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/sets/inference_manager.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/sets/inference_manager.h')
| -rw-r--r-- | src/theory/sets/inference_manager.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h index ba6be9905..3278b848e 100644 --- a/src/theory/sets/inference_manager.h +++ b/src/theory/sets/inference_manager.h @@ -109,6 +109,12 @@ class InferenceManager /** Have we sent lem as a lemma in the current user context? */ bool hasLemmaCached(Node lem) const; + /** + * Send conflict. + * @param conf The conflict node to be sent on the output channel + */ + void conflict(Node conf); + private: /** constants */ Node d_true; |