projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c938a90) | patch
Add resource limiting to coverings solver (#8672)
authorGereon Kremer <gkremer@cs.stanford.edu>
Thu, 28 Apr 2022 00:51:20 +0000 (17:51 -0700)
committerGitHub <noreply@github.com>
Thu, 28 Apr 2022 00:51:20 +0000 (19:51 -0500)
commit25e24c210bdf0157e0f95c257ec3516bc57d7a1b
treed548e8370a0f0535291616eea16a52b41d03260dtree
parentc938a904ea20f8511ae3344a9e9246a792d01a2dcommit | diff
Add resource limiting to coverings solver (#8672)

Right now, resource limits are not checked while the coverings solver is computing. This PR adds a new resource and spends it within every recursive call of the coverings solver. This fixes cases where cvc5 does not honor the per-call time limit on QF_NRA.
src/theory/arith/nl/coverings/cdcac.cpp diff | blob | history
src/util/resource_manager.cpp diff | blob | history
src/util/resource_manager.h diff | blob | history