Remove preregister instantiation heuristic (#5713)

This was a hack to improve the QF arithmetic solver by ensuring that certain instantiation lemmas were preregistered. This is no longer needed and will be a hindrance to the currently line of refactoring.

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index cb5785e6d1614ad014171b4073d667a8d7b17f1f..4aa612d5b2765bdb832837fd2f3177f6154123d6 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1667,14 +1667,6 @@ header = "options/quantifiers_options.h"
   default    = "false"
   help       = "use real infinity for vts in counterexample-based quantifier instantiation"
 
-[[option]]
-  name       = "cegqiPreRegInst"
-  category   = "regular"
-  long       = "cegqi-prereg-inst"
-  type       = "bool"
-  default    = "false"
-  help       = "preregister ground instantiations in counterexample-based quantifier instantiation"
-
 [[option]]
   name       = "cegqiMinBounds"
   category   = "regular"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index bbbe73cb15be7da10b90221f2ab6b03a81187b63..8b0986db6fed18577716762f0ec9c0264ee12d40 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1086,10 +1086,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       options::macrosQuant.set(false);
     }
-    if (!options::cegqiPreRegInst.wasSetByUser())
-    {
-      options::cegqiPreRegInst.set(true);
-    }
     // use tangent planes by default, since we want to put effort into
     // the verification step for sygus queries with non-linear arithmetic
     if (!options::nlExtTangentPlanes.wasSetByUser())
@@ -1135,7 +1131,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       // cannot do nested quantifier elimination in incremental mode
       options::cegqiNestedQE.set(false);
-      options::cegqiPreRegInst.set(false);
     }
     if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
     {

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 4e00a08e7114cf5b33d78625aabe7ac23f73fd77..561450dc98afc0f875ac97e2e2ffa4e3f93a3f59 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1326,78 +1326,6 @@ bool CegInstantiator::check() {
   return false;
 }
 
-void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) {
-  if( n.getKind()==FORALL || n.getKind()==EXISTS ){
-    //do nothing
-    return;
-  }
-  if (n.getKind() == EQUAL)
-  {
-    for (unsigned i = 0; i < 2; i++)
-    {
-      Node nn = n[i == 0 ? 1 : 0];
-      std::map<Node, std::vector<Node> >::iterator it = teq.find(n[i]);
-      if (it != teq.end() && !expr::hasFreeVar(nn)
-          && std::find(it->second.begin(), it->second.end(), nn)
-                 == it->second.end())
-      {
-        it->second.push_back(nn);
-        Trace("cegqi-presolve") << "  - " << n[i] << " = " << nn << std::endl;
-      }
-    }
-  }
-  for (const Node& nc : n)
-  {
-    collectPresolveEqTerms(nc, teq);
-  }
-}
-
-void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms,
-                             std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) {
-  if( conj.size()<1000 ){
-    if( terms.size()==f[0].getNumChildren() ){
-      Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
-      conj.push_back( c );
-    }else{
-      unsigned i = terms.size();
-      Node v = f[0][i];
-      terms.push_back( Node::null() );
-      for( unsigned j=0; j<teq[v].size(); j++ ){
-        terms[i] = teq[v][j];
-        getPresolveEqConjuncts( vars, terms, teq, f, conj );
-      }
-      terms.pop_back();
-    }
-  }
-}
-
-void CegInstantiator::presolve( Node q ) {
-  //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing
-  //only if no nested quantifiers
-  if (!expr::hasClosure(q[1]))
-  {
-    std::vector< Node > ps_vars;
-    std::map< Node, std::vector< Node > > teq;
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      ps_vars.push_back( q[0][i] );
-      teq[q[0][i]].clear();
-    }
-    collectPresolveEqTerms( q[1], teq );
-    std::vector< Node > terms;
-    std::vector< Node > conj;
-    getPresolveEqConjuncts( ps_vars, terms, teq, q, conj );
-
-    if( !conj.empty() ){
-      Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
-      Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
-      lem = NodeManager::currentNM()->mkNode( OR, g, lem );
-      Trace("cegqi-presolve-debug") << "Presolve lemma : " << lem << std::endl;
-      Assert(!expr::hasFreeVar(lem));
-      d_qe->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
-    }
-  }
-}
-
 void CegInstantiator::processAssertions() {
   Trace("cegqi-proc") << "--- Process assertions, #var = " << d_vars.size()
                      << std::endl;

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index 49268c180809bb113e96b78aa21e6e36b7cb9f9f..b8a337cdbf8a76f398ba7fa7a60e710e104104ec 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -216,12 +216,6 @@ class CegInstantiator {
    * on the output channel d_out of this class.
    */
   bool check();
-  /** presolve for quantified formula
-   *
-   * This initializes formulas that help static learning of the quantifier-free
-   * solver. It is only called if the option --cbqi-prereg-inst is used.
-   */
-  void presolve(Node q);
   /** Register the counterexample lemma
    *
    * @param lem contains the counterexample lemma of the quantified formula we

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 4884b4e3ba1bdd5eecccf2f1371c03ebe1507140..db76efd9d9db0f715287428c6777b0b5fae6e3ab 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -353,11 +353,6 @@ void InstStrategyCegqi::preRegisterQuantifier(Node q)
       // will process using nested quantifier elimination
       return;
     }
-    // get the instantiator
-    if (options::cegqiPreRegInst())
-    {
-      getInstantiator(q);
-    }
     // register the cbqi lemma
     if( registerCbqiLemma( q ) ){
       Trace("cegqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
@@ -538,18 +533,6 @@ BvInverter* InstStrategyCegqi::getBvInverter() const
   return d_bv_invert.get();
 }
 
-void InstStrategyCegqi::presolve() {
-  if (!options::cegqiPreRegInst())
-  {
-    return;
-  }
-  for (std::pair<const Node, std::unique_ptr<CegInstantiator>>& ci : d_cinst)
-  {
-    Trace("cegqi-presolve") << "Presolve " << ci.first << std::endl;
-    ci.second->presolve(ci.first);
-  }
-}
-
 bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister)
 {
   if (d_nestedQe != nullptr)

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index 2ca232699460b8c53e0a7fdc5bb304c5581d4501..1860962c755b3573b216a91b0e1ffd540a890f13 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -98,8 +98,6 @@ class InstStrategyCegqi : public QuantifiersModule
   BvInverter* getBvInverter() const;
   /** pre-register quantifier */
   void preRegisterQuantifier(Node q) override;
-  // presolve
-  void presolve() override;
 
   /**
    * Rewrite the instantiation inst of quantified formula q for terms; return

diff --git a/test/regress/regress0/sygus/aig-si.sy b/test/regress/regress0/sygus/aig-si.sy
index 9d3af67fb210c482120cadb7936ea7d7a87d5b19..3b8be96fd0db5f6fa40d2067c9d761b5e7b93472 100644 (file)
--- a/test/regress/regress0/sygus/aig-si.sy
+++ b/test/regress/regress0/sygus/aig-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --cegqi --cegqi-prereg-inst --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --cegqi --sygus-out=status
 (set-logic BV)
 
 (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool

diff --git a/test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2 b/test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2
index 92c8ac47bcf38edff619679b5c4a7dad9ecb208b..b304a23716c8b5ac60529cdce8bd8191cca63ebb 100644 (file)
--- a/test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2
+++ b/test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2
@@ -3,7 +3,6 @@
 (set-logic BV)
 (set-info :status sat)
 (declare-fun _substvar_16_ () Bool)
-(set-option :cegqi-prereg-inst true)
 (set-option :check-models true)
 (declare-fun v2 () Bool)
 (push 1)

diff --git a/test/regress/regress1/sygus/parity-si-rcons.sy b/test/regress/regress1/sygus/parity-si-rcons.sy
index aea7e32f3c1c60be082ef9edaa35e884450cfd14..16ade4ee505f3eff4cadcb7512af1193f045fe20 100644 (file)
--- a/test/regress/regress1/sygus/parity-si-rcons.sy
+++ b/test/regress/regress1/sygus/parity-si-rcons.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --cegqi-prereg-inst --sygus-si-rcons=try --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --sygus-si-rcons=try --sygus-out=status
 
 (set-logic BV)