diff options
Diffstat (limited to 'src/theory/theory_inference_manager.h')
-rw-r--r-- | src/theory/theory_inference_manager.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 92116648e..7fecacf82 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -329,6 +329,17 @@ class TheoryInferenceManager * decided with polarity pol, for details see OutputChannel::requirePhase. */ void requirePhase(TNode n, bool pol); + + /** + * Forward to OutputChannel::spendResource() to spend resources. + */ + void spendResource(ResourceManager::Resource r); + + /** + * Forward to OutputChannel::safePoint() to spend resources. + */ + void safePoint(ResourceManager::Resource r); + protected: /** * Process internal fact. This is a common helper method for the |