From 8431e9d49b71774092ca29c85855cbdf5bf09c53 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 29 Apr 2021 14:38:19 +0200 Subject: [PATCH] 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 | 10 ++++++---- 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 -- 2.30.2