diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-09 19:19:40 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-09 19:19:40 -0500 |
| commit | 92ed7681941b3b6d9c857724454860ac72d778d9 (patch) | |
| tree | 200455fb3d8046e9dc0e9c6ae8383e2b3a904bcc /src/preprocessing | |
| parent | 789f5b3c8c224deb48fe547303147e0d15e690ae (diff) | |
Towards proper use of resource managers (#4233)
Resource manager will be owned by SmtEngine in the future. This passes the resource manager cached by SmtEnginePrivate to the PropEngine created by SmtEngine instead of using the global pointer. It also makes a few preprocessing passes use the resource manager they already have access to and should use.
Diffstat (limited to 'src/preprocessing')
| -rw-r--r-- | src/preprocessing/passes/bool_to_bv.cpp | 3 | ||||
| -rw-r--r-- | src/preprocessing/passes/bv_to_bool.cpp | 3 |
2 files changed, 2 insertions, 4 deletions
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index b4d638595..e18e6f6c6 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -37,8 +37,7 @@ BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext) PreprocessingPassResult BoolToBV::applyInternal( AssertionPipeline* assertionsToPreprocess) { - NodeManager::currentResourceManager()->spendResource( - ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); size_t size = assertionsToPreprocess->size(); diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index 5b10f6644..33b41210a 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -45,8 +45,7 @@ BVToBool::BVToBool(PreprocessingPassContext* preprocContext) PreprocessingPassResult BVToBool::applyInternal( AssertionPipeline* assertionsToPreprocess) { - NodeManager::currentResourceManager()->spendResource( - ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); std::vector<Node> new_assertions; liftBvToBool(assertionsToPreprocess->ref(), new_assertions); for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) |