diff options
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5506b0120..0770efc7b 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -47,6 +47,7 @@ #include "theory/uf/equality_engine.h" #include "theory/valuation.h" #include "util/hash.h" +#include "util/resource_manager.h" #include "util/statistics_registry.h" #include "util/unsafe_interrupt_exception.h" @@ -281,8 +282,9 @@ class TheoryEngine { EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory) : d_engine(engine), d_statistics(theory), d_theory(theory) {} - void safePoint(uint64_t amount) override { - spendResource(amount); + void safePoint(ResourceManager::Resource r) override + { + spendResource(r); if (d_engine->d_interrupted) { throw theory::Interrupted(); } @@ -323,8 +325,9 @@ class TheoryEngine { d_engine->setIncomplete(d_theory); } - void spendResource(unsigned amount) override { - d_engine->spendResource(amount); + void spendResource(ResourceManager::Resource r) override + { + d_engine->spendResource(r); } void handleUserAttribute(const char* attr, theory::Theory* t) override { @@ -481,7 +484,7 @@ public: void interrupt(); /** "Spend" a resource during a search or preprocessing.*/ - void spendResource(unsigned amount); + void spendResource(ResourceManager::Resource r); /** * Adds a theory. Only one theory per TheoryId can be present, so if |