diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-31 23:35:57 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-31 21:35:57 -0700 |
| commit | 9b7f2b6b541f192acf2dc525076a4aa0e995be14 (patch) | |
| tree | e4773cdf7a312e90eeaa850d412b05a53ebd942c /src/theory/inference_manager_buffered.h | |
| parent | fa05eb5599e2ac0b2d4c1e0e943fee6353b52430 (diff) | |
Add the inference manager for datatypes (#4968)
This is in preparation for converting datatypes to the new standard. It adds a specialized version of inference manager buffered that datatypes uses. This required adding several utility methods to its base classes.
A follow up PR will connect this to TheoryDatatypes.
Diffstat (limited to 'src/theory/inference_manager_buffered.h')
| -rw-r--r-- | src/theory/inference_manager_buffered.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index bb46ef566..596a346de 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -145,6 +145,12 @@ class InferenceManagerBuffered : public TheoryInferenceManager * phase requirements and clears d_pendingReqPhase. */ void doPendingPhaseRequirements(); + /** Clear pending facts, without processing */ + void clearPendingFacts(); + /** Clear pending lemmas, without processing */ + void clearPendingLemmas(); + /** Clear pending phase requirements, without processing */ + void clearPendingPhaseRequirements(); protected: /** A set of pending lemmas */ |