diff options
Diffstat (limited to 'src/theory/quantifiers')
4 files changed, 0 insertions, 97 deletions
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<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 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<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 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 |