diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-02-19 16:59:58 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-19 16:59:58 -0800 |
commit | 508ecb3007a2b6aa8b76b28dc8282247b5dba957 (patch) | |
tree | b80cab956e6b40b4cd783ceb78393006c09782b5 /src/preprocessing/passes | |
parent | 9705504973f6f85c6be4944c615984df7b614f67 (diff) |
resource manager: Add statistic for every resource. (#3772)
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).
Fixes #3751.
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r-- | src/preprocessing/passes/apply_substs.cpp | 3 | ||||
-rw-r--r-- | src/preprocessing/passes/bool_to_bv.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/bv_to_bool.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/ite_simp.cpp | 4 | ||||
-rw-r--r-- | src/preprocessing/passes/non_clausal_simp.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/static_learning.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 2 |
8 files changed, 10 insertions, 9 deletions
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 791bb2dc7..98313efda 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -52,7 +52,8 @@ PreprocessingPassResult ApplySubsts::applyInternal( } Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i] << std::endl; - d_preprocContext->spendResource(options::preprocessStep()); + d_preprocContext->spendResource( + ResourceManager::Resource::PreprocessStep); assertionsToPreprocess->replace(i, theory::Rewriter::rewrite(substMap.apply( (*assertionsToPreprocess)[i]))); diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index 7787d7631..30b64fd74 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -36,7 +36,7 @@ PreprocessingPassResult BoolToBV::applyInternal( AssertionPipeline* assertionsToPreprocess) { NodeManager::currentResourceManager()->spendResource( - options::preprocessStep()); + ResourceManager::Resource::PreprocessStep); unsigned size = assertionsToPreprocess->size(); for (unsigned i = 0; i < size; ++i) diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index 3d3762ecd..0637c541f 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -45,7 +45,7 @@ PreprocessingPassResult BVToBool::applyInternal( AssertionPipeline* assertionsToPreprocess) { NodeManager::currentResourceManager()->spendResource( - options::preprocessStep()); + ResourceManager::Resource::PreprocessStep); std::vector<Node> new_assertions; liftBvToBool(assertionsToPreprocess->ref(), new_assertions); for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index bda38a6df..6ad97f4a3 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -32,7 +32,7 @@ IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext) PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) { - d_preprocContext->spendResource(options::preprocessStep()); + d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); // Remove all of the ITE occurrences and normalize d_preprocContext->getIteRemover()->run( diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index ad00ec204..7f7c4c95f 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -234,12 +234,12 @@ ITESimp::ITESimp(PreprocessingPassContext* preprocContext) PreprocessingPassResult ITESimp::applyInternal( AssertionPipeline* assertionsToPreprocess) { - d_preprocContext->spendResource(options::preprocessStep()); + d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); size_t nasserts = assertionsToPreprocess->size(); for (size_t i = 0; i < nasserts; ++i) { - d_preprocContext->spendResource(options::preprocessStep()); + d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); Node simp = simpITE(&d_iteUtilities, (*assertionsToPreprocess)[i]); assertionsToPreprocess->replace(i, simp); if (simp.isConst() && !simp.getConst<bool>()) diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 139bf96a9..03f38370b 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -56,7 +56,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( { Assert(!options::unsatCores() && !options::fewerPreprocessingHoles()); - d_preprocContext->spendResource(options::preprocessStep()); + d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); theory::booleans::CircuitPropagator* propagator = d_preprocContext->getCircuitPropagator(); diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index 7af9f7fac..ec3982e03 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -30,7 +30,7 @@ PreprocessingPassResult StaticLearning::applyInternal( AssertionPipeline* assertionsToPreprocess) { NodeManager::currentResourceManager()->spendResource( - options::preprocessStep()); + ResourceManager::Resource::PreprocessStep); for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 1695ae2ff..8a2c58b99 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -813,7 +813,7 @@ void UnconstrainedSimplifier::processUnconstrained() PreprocessingPassResult UnconstrainedSimplifier::applyInternal( AssertionPipeline* assertionsToPreprocess) { - d_preprocContext->spendResource(options::preprocessStep()); + d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); std::vector<Node>& assertions = assertionsToPreprocess->ref(); |