Refactor resource manager (#6322)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Mon, 12 Apr 2021 20:58:14 +0000 (22:58 +0200)
committerGitHub <noreply@github.com>
Mon, 12 Apr 2021 20:58:14 +0000 (20:58 +0000)
commitaf398235ef9f3a909991fddbb71d43434d6cf3a1
tree8ae4533255a4bf63c808824f67552b588c301649
parentc422f03d3169d4dc8d5b333de12be14e9121bc93
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.
57 files changed:
src/decision/decision_engine.cpp
src/options/mkoptions.py
src/options/options.h
src/options/options_handler.cpp
src/options/options_handler.h
src/options/options_public_functions.cpp
src/options/smt_options.toml
src/preprocessing/passes/apply_substs.cpp
src/preprocessing/passes/bool_to_bv.cpp
src/preprocessing/passes/bv_to_bool.cpp
src/preprocessing/passes/ite_removal.cpp
src/preprocessing/passes/ite_simp.cpp
src/preprocessing/passes/non_clausal_simp.cpp
src/preprocessing/passes/static_learning.cpp
src/preprocessing/passes/theory_preprocess.cpp
src/preprocessing/passes/unconstrained_simplifier.cpp
src/preprocessing/preprocessing_pass_context.h
src/prop/bv_sat_solver_notify.h
src/prop/bvminisat/bvminisat.h
src/prop/bvminisat/core/Solver.cc
src/prop/bvminisat/core/Solver.h
src/prop/cnf_stream.cpp
src/prop/minisat/core/Solver.cc
src/prop/minisat/core/Solver.h
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/prop/theory_proxy.h
src/smt/expand_definitions.cpp
src/smt/process_assertions.cpp
src/smt/process_assertions.h
src/smt/smt_engine.cpp
src/smt/smt_solver.cpp
src/theory/arith/theory_arith_private.cpp
src/theory/bv/bitblast/bitblaster.h
src/theory/bv/bitblast/eager_bitblaster.cpp
src/theory/bv/bitblast/lazy_bitblaster.cpp
src/theory/bv/bitblast/lazy_bitblaster.h
src/theory/bv/bv_eager_solver.cpp
src/theory/bv/bv_solver_lazy.cpp
src/theory/bv/bv_solver_lazy.h
src/theory/bv/bv_subtheory_bitblast.cpp
src/theory/bv/bv_subtheory_core.cpp
src/theory/bv/bv_subtheory_inequality.cpp
src/theory/engine_output_channel.cpp
src/theory/engine_output_channel.h
src/theory/output_channel.h
src/theory/quantifiers/instantiate.cpp
src/theory/rewriter.cpp
src/theory/theory.cpp
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/theory_inference_manager.cpp
src/theory/theory_inference_manager.h
src/util/resource_manager.cpp
src/util/resource_manager.h
test/unit/test_smt.h