diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-29 14:38:19 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-29 07:38:19 -0500 |
| commit | 8431e9d49b71774092ca29c85855cbdf5bf09c53 (patch) | |
| tree | bcd71d6e0526282331c8e62e657f530eb68da86e /src/theory/quantifiers/cegqi | |
| parent | 9e5a4a3e6aca1b25cf1af4a6392003cb5ecb8866 (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.
Diffstat (limited to 'src/theory/quantifiers/cegqi')
| -rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 10 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.h | 2 |
2 files changed, 8 insertions, 4 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index f764ce646..f059767a6 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -57,10 +57,11 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersState& qs, d_incomplete_check(false), d_added_cbqi_lemma(qs.getUserContext()), d_vtsCache(new VtsTermCache(qim)), - d_bv_invert(nullptr) + d_bv_invert(nullptr), + d_small_const_multiplier( + NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000))), + d_small_const(d_small_const_multiplier) { - d_small_const = - NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000)); d_check_vts_lemma_lc = false; if (options::cegqiBv()) { @@ -437,7 +438,8 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { if( d_check_vts_lemma_lc ){ Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl; d_check_vts_lemma_lc = false; - d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const ); + d_small_const = NodeManager::currentNM()->mkNode( + MULT, d_small_const, d_small_const_multiplier); d_small_const = Rewriter::rewrite( d_small_const ); //heuristic for now, until we know how to do nested quantification Node delta = d_vtsCache->getVtsDelta(true, false); diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 266de9a53..5547409de 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -176,6 +176,8 @@ class InstStrategyCegqi : public QuantifiersModule * form inf > (1/c)^1, inf > (1/c)^2, .... */ bool d_check_vts_lemma_lc; + /** a multiplier used to make d_small_const even smaller over time */ + const Node d_small_const_multiplier; /** a small constant, used as a coefficient above */ Node d_small_const; //---------------------- end for vts delta minimization |