diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-12 22:58:14 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-12 20:58:14 +0000 |
commit | af398235ef9f3a909991fddbb71d43434d6cf3a1 (patch) | |
tree | 8ae4533255a4bf63c808824f67552b588c301649 /src/preprocessing/passes | |
parent | c422f03d3169d4dc8d5b333de12be14e9121bc93 (diff) |
Refactor resource manager (#6322)
This PR does another round of refactoring of the resource manager and related code.
- it moves the Resource enum out of the ResourceManager class
- it treats the resources in a generic way (storing the statistics in a vector) instead of the manual treatment we had before
- weights no longer live in the options, but in the ResourceManager and are changed accordingly in the ResourceManager constructor
- following the generic treatment of resources, it also removes all the resource-specific options --x-step in favor of a generic --rweight name=weight
- removed several unused methods from the ResourceManager
Note that we handle the Resource enum in a way that allows to easily use other enums as additional resources, for example InferenceId. The general idea is that we will at some point have sensible default weights (so that the cumulative resources somewhat simulate the solver runtime) and users (almost) never need to modify them.
Diffstat (limited to 'src/preprocessing/passes')
-rw-r--r-- | src/preprocessing/passes/apply_substs.cpp | 2 | ||||
-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/theory_preprocess.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 2 |
9 files changed, 10 insertions, 10 deletions
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 324cd89b9..20c173316 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -53,7 +53,7 @@ PreprocessingPassResult ApplySubsts::applyInternal( } Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i] << std::endl; - d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(Resource::PreprocessStep); assertionsToPreprocess->replaceTrusted( i, tlsm.apply((*assertionsToPreprocess)[i])); Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i] diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index dfa0c378d..7fd54420f 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -41,7 +41,7 @@ BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext) PreprocessingPassResult BoolToBV::applyInternal( AssertionPipeline* assertionsToPreprocess) { - d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(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 c30017f31..71719e064 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -48,7 +48,7 @@ BVToBool::BVToBool(PreprocessingPassContext* preprocContext) PreprocessingPassResult BVToBool::applyInternal( AssertionPipeline* assertionsToPreprocess) { - d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(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 278192c97..068e47f13 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -40,7 +40,7 @@ IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext) PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) { - d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(Resource::PreprocessStep); IteSkolemMap& imap = assertions->getIteSkolemMap(); // Remove all of the ITE occurrences and normalize diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index efa50e0a0..f79c7fec9 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -236,12 +236,12 @@ ITESimp::ITESimp(PreprocessingPassContext* preprocContext) PreprocessingPassResult ITESimp::applyInternal( AssertionPipeline* assertionsToPreprocess) { - d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(Resource::PreprocessStep); size_t nasserts = assertionsToPreprocess->size(); for (size_t i = 0; i < nasserts; ++i) { - d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(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 e2b8c0276..c9f20d774 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -77,7 +77,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( Assert(!options::unsatCores() || isProofEnabled()) << "Unsat cores with non-clausal simp only supported with new proofs"; - d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(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 278252da9..09d24d900 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -33,7 +33,7 @@ StaticLearning::StaticLearning(PreprocessingPassContext* preprocContext) PreprocessingPassResult StaticLearning::applyInternal( AssertionPipeline* assertionsToPreprocess) { - d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(Resource::PreprocessStep); for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 88cc8112d..cc8820226 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -37,7 +37,7 @@ TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext) PreprocessingPassResult TheoryPreprocess::applyInternal( AssertionPipeline* assertions) { - d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(Resource::PreprocessStep); IteSkolemMap& imap = assertions->getIteSkolemMap(); prop::PropEngine* propEngine = d_preprocContext->getPropEngine(); diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 922c3bdd5..15b3c62df 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -846,7 +846,7 @@ void UnconstrainedSimplifier::processUnconstrained() PreprocessingPassResult UnconstrainedSimplifier::applyInternal( AssertionPipeline* assertionsToPreprocess) { - d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(Resource::PreprocessStep); const std::vector<Node>& assertions = assertionsToPreprocess->ref(); |