From 31717bf7c014bf1971cabcc9b871de5818278126 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 Aug 2020 13:36:59 -0500 Subject: 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). --- src/theory/sets/inference_manager.h | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/theory/sets/inference_manager.h') 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; -- cgit v1.2.3