projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9e5a4a3) | patch
Avoid exponential explosion of small constant in CEGQI (#6461)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 29 Apr 2021 12:38:19 +0000 (14:38 +0200)
committerGitHub <noreply@github.com>
Thu, 29 Apr 2021 12:38:19 +0000 (07:38 -0500)
commit8431e9d49b71774092ca29c85855cbdf5bf09c53
treebcd71d6e0526282331c8e62e657f530eb68da86etree
parent9e5a4a3e6aca1b25cf1af4a6392003cb5ecb8866commit | diff
Avoid exponential explosion of small constant in CEGQI (#6461)

This PR fixes an issue that can lead to an exponential explosion of a rational constant for repeated calls to the cegqi instantiation strategy. The d_small_const variable was squared regularly, we now simply multiply it with its original value.
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h diff | blob | history