diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-21 00:10:17 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-20 22:10:17 +0000 |
| commit | 93fffd49080e29affbf9d5657046d57add929fa8 (patch) | |
| tree | 62c0f2de79b61a1e1df13d9da136c062baa0ec80 /src/theory | |
| parent | cc8ce1bcdf8d6a4b508723063879e891a6cbd8c3 (diff) | |
Add InferenceId as resources (#6339)
This PR extends the resource manager to consider theory::InferenceId a resource we can spend. This should give us a robust way to have the resource limiting cover a lot of theory reasoning. To make use of this, TheoryInferenceManager now spends these resources.
Also, it makes the ResourceManager properly use the options from the Env class.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/theory_inference_manager.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 3bc7351fe..ad988e534 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -15,6 +15,7 @@ #include "theory/theory_inference_manager.h" +#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/output_channel.h" #include "theory/rewriter.h" @@ -118,6 +119,7 @@ void TheoryInferenceManager::conflict(TNode conf, InferenceId id) void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id) { d_conflictIdStats << id; + smt::currentResourceManager()->spendResource(id); Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")" << std::endl; d_theoryState.notifyInConflict(); @@ -250,6 +252,7 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem, } } d_lemmaIdStats << id; + smt::currentResourceManager()->spendResource(id); Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl; d_numCurrentLemmas++; d_out.trustedLemma(tlem, p); @@ -370,6 +373,7 @@ bool TheoryInferenceManager::processInternalFact(TNode atom, ProofGenerator* pg) { d_factIdStats << iid; + smt::currentResourceManager()->spendResource(iid); Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode()) << ")" << std::endl; // make the node corresponding to the explanation |