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.

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index f764ce6467a1bca62a6a38fc2e2114bfcd88c7fe..f059767a6c29644941545785801af6327f4dd5c4 100644 (file)
--- 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 266de9a536ea343efc6e26d8911795ed3fb656f9..5547409de0b3423b6aeb6fffd46e0760524c6a7d 100644 (file)
--- 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