From 85da37188e1b206fb3dccf202633cf4c1d22da7c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 22 Dec 2020 01:49:28 -0600 Subject: [PATCH] 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. --- src/options/quantifiers_options.toml | 8 --- src/smt/set_defaults.cpp | 5 -- .../quantifiers/cegqi/ceg_instantiator.cpp | 72 ------------------- .../quantifiers/cegqi/ceg_instantiator.h | 6 -- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 17 ----- .../quantifiers/cegqi/inst_strategy_cegqi.h | 2 - test/regress/regress0/sygus/aig-si.sy | 2 +- .../quantifiers/issue4243-prereg-inc.smt2 | 1 - .../regress/regress1/sygus/parity-si-rcons.sy | 2 +- 9 files changed, 2 insertions(+), 113 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index cb5785e6d..4aa612d5b 100644 --- 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 bbbe73cb1..8b0986db6 100644 --- 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 4e00a08e7..561450dc9 100644 --- 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 >::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 ps_vars; - std::map< Node, std::vector< Node > > teq; - for( unsigned i=0; i 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 49268c180..b8a337cdb 100644 --- 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 4884b4e3b..db76efd9d 100644 --- 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>& 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 2ca232699..1860962c7 100644 --- 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 9d3af67fb..3b8be96fd 100644 --- 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 92c8ac47b..b304a2371 100644 --- 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 aea7e32f3..16ade4ee5 100644 --- 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) -- 2.30.2