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/inference_manager_buffered.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/inference_manager_buffered.h')
| -rw-r--r-- | src/theory/inference_manager_buffered.h | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index 62c3c9b55..e5ad4cb0a 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -37,11 +37,9 @@ class InferenceManagerBuffered : public TheoryInferenceManager ProofNodeManager* pnm); virtual ~InferenceManagerBuffered() {} /** - * Have we processed an inference during this call to check? In particular, - * this returns true if we have a pending fact or lemma, or have encountered - * a conflict. + * Do we have a pending fact or lemma? */ - bool hasProcessed() const; + bool hasPending() const; /** * Do we have a pending fact to add as an internal fact to the equality * engine? |