projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cc8ce1b) | patch
Add InferenceId as resources (#6339)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 20 Apr 2021 22:10:17 +0000 (00:10 +0200)
committerGitHub <noreply@github.com>
Tue, 20 Apr 2021 22:10:17 +0000 (22:10 +0000)
commit93fffd49080e29affbf9d5657046d57add929fa8
tree62c0f2de79b61a1e1df13d9da136c062baa0ec80tree
parentcc8ce1bcdf8d6a4b508723063879e891a6cbd8c3commit | 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.
src/smt/env.cpp diff | blob | history
src/smt/env.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/theory_inference_manager.cpp diff | blob | history
src/util/resource_manager.cpp diff | blob | history
src/util/resource_manager.h diff | blob | history