diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-03 18:31:36 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-03 18:31:36 -0500 |
commit | 0fe081a56db369372584a5fcd35a4c4e4fb1c23f (patch) | |
tree | a24f9f3dbb0ede1faf09a276d96c2714d3bf75c0 /src/theory/sets/theory_sets.h | |
parent | 19ff08d652de2890eee4674d2a6debe10e879f1f (diff) |
Update sets inference manager to inherit from InferenceManagerBuffered (#5007)
This updates the inference manager of sets to inherit from the standard base class InferenceManagerBuffered.
It matches that base class almost exactly, with cosmetic changes.
Notice that sets currently has a design issue: the state object sends lemmas and hence currently requires a pointer to the theory. This will be untangled in a future PR.
This PR makes a few very minor changes to the behavior, including not to use the "preprocess" property for subtype lemmas.
Diffstat (limited to 'src/theory/sets/theory_sets.h')
-rw-r--r-- | src/theory/sets/theory_sets.h | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 7787c0f9b..fed74b1bb 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -21,6 +21,8 @@ #include <memory> +#include "theory/sets/inference_manager.h" +#include "theory/sets/solver_state.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -61,12 +63,6 @@ class TheorySets : public Theory //--------------------------------- standard check /** Post-check, called after the fact queue of the theory is processed. */ void postCheck(Effort level) override; - /** Pre-notify fact, return true if processed. */ - bool preNotifyFact(TNode atom, - bool pol, - TNode fact, - bool isPrereg, - bool isInternal) override; /** Notify fact */ void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override; //--------------------------------- end standard check @@ -102,6 +98,10 @@ class TheorySets : public Theory private: TheorySetsPrivate& d_theory; }; + /** The state of the sets solver at full effort */ + SolverState d_state; + /** The inference manager */ + InferenceManager d_im; /** The internal theory */ std::unique_ptr<TheorySetsPrivate> d_internal; /** Instance of the above class */ |