summaryrefslogtreecommitdiff
path: root/src/theory/theory_inference_manager.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_inference_manager.h')
-rw-r--r--src/theory/theory_inference_manager.h11
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback