From: Andrew Reynolds Date: Mon, 17 Sep 2018 23:49:08 +0000 (-0500) Subject: Move inst_strategy_cbqi to inst_strategy_cegqi (#2477) X-Git-Tag: cvc5-1.0.0~4637 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=603c0ccc4614024dfcd34333cd427ac56e229a47;p=cvc5.git Move inst_strategy_cbqi to inst_strategy_cegqi (#2477) --- diff --git a/src/Makefile.am b/src/Makefile.am index caad72fd5..bdba671ca 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -450,8 +450,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/cegqi/ceg_dt_instantiator.h \ theory/quantifiers/cegqi/ceg_epr_instantiator.cpp \ theory/quantifiers/cegqi/ceg_epr_instantiator.h \ - theory/quantifiers/cegqi/inst_strategy_cbqi.cpp \ - theory/quantifiers/cegqi/inst_strategy_cbqi.h \ + theory/quantifiers/cegqi/inst_strategy_cegqi.cpp \ + theory/quantifiers/cegqi/inst_strategy_cegqi.h \ theory/quantifiers/conjecture_generator.cpp \ theory/quantifiers/conjecture_generator.h \ theory/quantifiers/dynamic_rewrite.cpp \ diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp deleted file mode 100644 index 8c9b39ea4..000000000 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ /dev/null @@ -1,698 +0,0 @@ -/********************* */ -/*! \file inst_strategy_cbqi.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of counterexample-guided quantifier instantiation strategies - **/ -#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" - -#include "expr/node_algorithm.h" -#include "options/quantifiers_options.h" -#include "smt/term_formula_removal.h" -#include "theory/arith/partial_model.h" -#include "theory/arith/theory_arith.h" -#include "theory/arith/theory_arith_private.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/quant_epr.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" -#include "theory/theory_engine.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - -bool CegqiOutputInstStrategy::doAddInstantiation(std::vector& subs) -{ - return d_out->doAddInstantiation(subs); -} - -bool CegqiOutputInstStrategy::isEligibleForInstantiation(Node n) -{ - return d_out->isEligibleForInstantiation(n); -} - -bool CegqiOutputInstStrategy::addLemma(Node lem) -{ - return d_out->addLemma(lem); -} - -InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) - : QuantifiersModule(qe), - d_cbqi_set_quant_inactive(false), - d_incomplete_check(false), - d_added_cbqi_lemma(qe->getUserContext()), - d_elim_quants(qe->getSatContext()), - d_out(new CegqiOutputInstStrategy(this)), - d_nested_qe_waitlist_size(qe->getUserContext()), - d_nested_qe_waitlist_proc(qe->getUserContext()) -//, d_added_inst( qe->getUserContext() ) -{ - d_qid_count = 0; - d_small_const = - NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000)); - d_check_vts_lemma_lc = false; -} - -InstStrategyCegqi::~InstStrategyCegqi() {} - -bool InstStrategyCegqi::needsCheck(Theory::Effort e) -{ - return e>=Theory::EFFORT_LAST_CALL; -} - -QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e) -{ - for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ - return QEFFORT_STANDARD; - } - } - return QEFFORT_NONE; -} - -bool InstStrategyCegqi::registerCbqiLemma(Node q) -{ - if( !hasAddedCbqiLemma( q ) ){ - d_added_cbqi_lemma.insert( q ); - Trace("cbqi-debug") << "Do cbqi for " << q << std::endl; - //add cbqi lemma - //get the counterexample literal - Node ceLit = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); - Node ceBody = d_quantEngine->getTermUtil()->getInstConstantBody( q ); - if( !ceBody.isNull() ){ - //add counterexample lemma - Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); - //require any decision on cel to be phase=true - d_quantEngine->addRequirePhase( ceLit, true ); - Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; - //add counterexample lemma - lem = Rewriter::rewrite( lem ); - Trace("cbqi-lemma") << "Counterexample lemma : " << lem << std::endl; - registerCounterexampleLemma( q, lem ); - - //totality lemmas for EPR - QuantEPR * qepr = d_quantEngine->getQuantEPR(); - if( qepr!=NULL ){ - for( unsigned i=0; iisEPR( tn ) ){ - //add totality lemma - std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn ); - if( itc!=qepr->d_consts.end() ){ - Assert( !itc->second.empty() ); - Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ); - std::vector< Node > disj; - for( unsigned j=0; jsecond.size(); j++ ){ - disj.push_back( ic.eqNode( itc->second[j] ) ); - } - Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ); - Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl; - d_quantEngine->getOutputChannel().lemma( tlem ); - }else{ - Assert( false ); - } - }else{ - Assert( !options::cbqiAll() ); - } - } - } - } - - //compute dependencies between quantified formulas - if( options::cbqiLitDepend() || options::cbqiInnermost() ){ - std::vector< Node > ics; - TermUtil::computeInstConstContains(q, ics); - d_parent_quant[q].clear(); - d_children_quant[q].clear(); - std::vector< Node > dep; - for( unsigned i=0; igetTermUtil()->getCounterexampleLiteral( qi ); - dep.push_back( qi ); - dep.push_back( qicel ); - } - } - if( !dep.empty() ){ - Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) ); - Trace("cbqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl; - d_quantEngine->getOutputChannel().lemma( dep_lemma ); - } - } - - //must register all sub-quantifiers of counterexample lemma, register their lemmas - std::vector< Node > quants; - TermUtil::computeQuantContains( lem, quants ); - for( unsigned i=0; i>::iterator itds = - d_dstrat.find(q); - DecisionStrategy* dlds = nullptr; - if (itds == d_dstrat.end()) - { - d_dstrat[q].reset( - new DecisionStrategySingleton("CexLiteral", - ceLit, - d_quantEngine->getSatContext(), - d_quantEngine->getValuation())); - dlds = d_dstrat[q].get(); - } - else - { - dlds = itds->second.get(); - } - // it is appended to the list of strategies - d_quantEngine->getTheoryEngine()->getDecisionManager()->registerStrategy( - DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds); - return true; - }else{ - return false; - } -} - -void InstStrategyCegqi::reset_round(Theory::Effort effort) -{ - d_cbqi_set_quant_inactive = false; - d_incomplete_check = false; - d_active_quant.clear(); - //check if any cbqi lemma has not been added yet - for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine - if( doCbqi( q ) ){ - Assert( hasAddedCbqiLemma( q ) ); - if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ - d_active_quant[q] = true; - Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; - Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); - bool value; - if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ - Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl; - if( !value ){ - if( d_quantEngine->getValuation().isDecision( cel ) ){ - Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; - }else{ - Trace("cbqi") << "Inactive : " << q << std::endl; - d_quantEngine->getModel()->setQuantifierActive( q, false ); - d_cbqi_set_quant_inactive = true; - d_active_quant.erase( q ); - d_elim_quants.insert( q ); - Trace("cbqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl; - //process from waitlist - while( d_nested_qe_waitlist_proc[q]=0 ); - Assert( index<(int)d_nested_qe_waitlist[q].size() ); - Node nq = d_nested_qe_waitlist[q][index]; - Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts ); - Node dqelem = nq.eqNode( nqeqn ); - Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl; - d_quantEngine->getOutputChannel().lemma( dqelem ); - d_nested_qe_waitlist_proc[q] = index + 1; - } - } - } - }else{ - Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl; - } - } - } - } - - //refinement: only consider innermost active quantified formulas - if( options::cbqiInnermost() ){ - if( !d_children_quant.empty() && !d_active_quant.empty() ){ - Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl; - std::vector< Node > ninner; - for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ - std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first ); - if( itc!=d_children_quant.end() ){ - for( unsigned j=0; jsecond.size(); j++ ){ - if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){ - Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl; - ninner.push_back( it->first ); - break; - } - } - } - } - Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl; - for( unsigned i=0; iinConflict() ); - double clSet = 0; - if( Trace.isOn("cbqi-engine") ){ - clSet = double(clock())/double(CLOCKS_PER_SEC); - Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl; - } - unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); - for( int ee=0; ee<=1; ee++ ){ - //for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - // Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - // if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ - for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ - Node q = it->first; - Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl; - if( d_nested_qe.find( q )==d_nested_qe.end() ){ - process( q, e, ee ); - if( d_quantEngine->inConflict() ){ - break; - } - }else{ - Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl; - Assert( false ); - } - } - if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ - break; - } - } - if( Trace.isOn("cbqi-engine") ){ - if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ - Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; - } - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl; - } - } -} - -bool InstStrategyCegqi::checkComplete() -{ - if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){ - return false; - }else{ - return true; - } -} - -bool InstStrategyCegqi::checkCompleteFor(Node q) -{ - std::map::iterator it = d_do_cbqi.find(q); - if( it!=d_do_cbqi.end() ){ - return it->second != CEG_UNHANDLED; - }else{ - return false; - } -} - -Node InstStrategyCegqi::getIdMarkedQuantNode(Node n, - std::map& visited) -{ - std::map< Node, Node >::iterator it = visited.find( n ); - if( it==visited.end() ){ - Node ret = n; - if( n.getKind()==FORALL ){ - QAttributes qa; - QuantAttributes::computeQuantAttributes( n, qa ); - if( qa.d_qid_num.isNull() ){ - std::vector< Node > rc; - rc.push_back( n[0] ); - rc.push_back( getIdMarkedQuantNode( n[1], visited ) ); - Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() ); - QuantIdNumAttribute ida; - avar.setAttribute(ida,d_qid_count); - d_qid_count++; - std::vector< Node > iplc; - iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) ); - if( n.getNumChildren()==3 ){ - for( unsigned i=0; imkNode( INST_PATTERN_LIST, iplc ) ); - ret = NodeManager::currentNM()->mkNode( FORALL, rc ); - } - }else if( n.getNumChildren()>0 ){ - std::vector< Node > children; - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - bool childChanged = false; - for( unsigned i=0; imkNode( n.getKind(), children ); - } - } - visited[n] = ret; - return ret; - }else{ - return it->second; - } -} - -void InstStrategyCegqi::checkOwnership(Node q) -{ - if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ - if (d_do_cbqi[q] == CEG_HANDLED) - { - //take full ownership of the quantified formula - d_quantEngine->setOwner( q, this ); - } - } -} - -void InstStrategyCegqi::preRegisterQuantifier(Node q) -{ - // mark all nested quantifiers with id - if (options::cbqiNestedQE()) - { - if( d_quantEngine->getOwner(q)==this ) - { - std::map visited; - Node mq = getIdMarkedQuantNode(q[1], visited); - if (mq != q[1]) - { - // do not do cbqi, we are reducing this quantified formula to a marked - // one - d_do_cbqi[q] = CEG_UNHANDLED; - // instead do reduction - std::vector qqc; - qqc.push_back(q[0]); - qqc.push_back(mq); - if (q.getNumChildren() == 3) - { - qqc.push_back(q[2]); - } - Node qq = NodeManager::currentNM()->mkNode(FORALL, qqc); - Node mlem = NodeManager::currentNM()->mkNode(IMPLIES, q, qq); - Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl; - d_quantEngine->addLemma(mlem); - } - } - } - if( doCbqi( q ) ){ - // get the instantiator - if (options::cbqiPreRegInst()) - { - getInstantiator(q); - } - // register the cbqi lemma - if( registerCbqiLemma( q ) ){ - Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl; - } - } -} - -Node InstStrategyCegqi::doNestedQENode( - Node q, Node ceq, Node n, std::vector& inst_terms, bool doVts) -{ - // there is a nested quantified formula (forall y. nq[y,x]) such that - // q is (forall y. nq[y,t]) for ground terms t, - // ceq is (forall y. nq[y,e]) for CE variables e. - // we call this function when we know (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e]. - // in this case, q is equivalent to the quantifier-free formula C[t]. - if( d_nested_qe.find( ceq )==d_nested_qe.end() ){ - d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq ); - Trace("cbqi-nqe") << "CE quantifier elimination : " << std::endl; - Trace("cbqi-nqe") << " " << ceq << std::endl; - Trace("cbqi-nqe") << " " << d_nested_qe[ceq] << std::endl; - //should not contain quantifiers - Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) ); - } - Assert( d_quantEngine->getTermUtil()->d_inst_constants[q].size()==inst_terms.size() ); - //replace inst constants with instantiation - Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(), - d_quantEngine->getTermUtil()->d_inst_constants[q].end(), - inst_terms.begin(), inst_terms.end() ); - if( doVts ){ - //do virtual term substitution - ret = Rewriter::rewrite( ret ); - ret = d_quantEngine->getTermUtil()->rewriteVtsSymbols( ret ); - } - Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl; - Trace("cbqi-nqe") << " " << n << std::endl; - Trace("cbqi-nqe") << " " << ret << std::endl; - return ret; -} - -Node InstStrategyCegqi::doNestedQERec(Node q, - Node n, - std::map& visited, - std::vector& inst_terms, - bool doVts) -{ - if( visited.find( n )==visited.end() ){ - Node ret = n; - if( n.getKind()==FORALL ){ - QAttributes qa; - QuantAttributes::computeQuantAttributes( n, qa ); - if( !qa.d_qid_num.isNull() ){ - //if it has an id, check whether we have done quantifier elimination for this id - std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num ); - if( it!=d_id_to_ce_quant.end() ){ - Node ceq = it->second; - bool doNestedQe = d_elim_quants.contains( ceq ); - if( doNestedQe ){ - ret = doNestedQENode( q, ceq, n, inst_terms, doVts ); - }else{ - Trace("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl; - Node nr = Rewriter::rewrite( n ); - Trace("cbqi-nqe") << " " << ceq << std::endl; - Trace("cbqi-nqe") << " " << nr << std::endl; - int wlsize = d_nested_qe_waitlist_size[ceq] + 1; - d_nested_qe_waitlist_size[ceq] = wlsize; - if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){ - d_nested_qe_waitlist[ceq][wlsize] = nr; - }else{ - d_nested_qe_waitlist[ceq].push_back( nr ); - } - d_nested_qe_info[nr].d_q = q; - d_nested_qe_info[nr].d_inst_terms.clear(); - d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() ); - d_nested_qe_info[nr].d_doVts = doVts; - //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true. - Assert( !options::cbqiInnermost() ); - } - } - } - }else if( n.getNumChildren()>0 ){ - std::vector< Node > children; - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - bool childChanged = false; - for( unsigned i=0; imkNode( n.getKind(), children ); - } - } - visited[n] = ret; - return ret; - }else{ - return n; - } -} - -Node InstStrategyCegqi::doNestedQE(Node q, - std::vector& inst_terms, - Node lem, - bool doVts) -{ - std::map< Node, Node > visited; - return doNestedQERec( q, lem, visited, inst_terms, doVts ); -} - -void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) -{ - // must register with the instantiator - // must explicitly remove ITEs so that we record dependencies - std::vector ce_vars; - TermUtil* tutil = d_quantEngine->getTermUtil(); - for (unsigned i = 0, nics = tutil->getNumInstantiationConstants(q); i < nics; - i++) - { - ce_vars.push_back(tutil->getInstantiationConstant(q, i)); - } - std::vector lems; - lems.push_back(lem); - CegInstantiator* cinst = getInstantiator(q); - cinst->registerCounterexampleLemma(lems, ce_vars); - for (unsigned i = 0, size = lems.size(); i < size; i++) - { - Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] - << std::endl; - d_quantEngine->addLemma(lems[i], false); - } -} - -bool InstStrategyCegqi::doCbqi(Node q) -{ - std::map::iterator it = d_do_cbqi.find(q); - if( it==d_do_cbqi.end() ){ - CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine); - Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; - d_do_cbqi[q] = ret; - return ret != CEG_UNHANDLED; - } - return it->second != CEG_UNHANDLED; -} - -void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { - if( e==0 ){ - CegInstantiator * cinst = getInstantiator( q ); - Trace("inst-alg") << "-> Run cegqi for " << q << std::endl; - d_curr_quant = q; - if( !cinst->check() ){ - d_incomplete_check = true; - d_check_vts_lemma_lc = true; - } - d_curr_quant = Node::null(); - }else if( e==1 ){ - //minimize the free delta heuristically on demand - 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 = Rewriter::rewrite( d_small_const ); - //heuristic for now, until we know how to do nested quantification - Node delta = d_quantEngine->getTermUtil()->getVtsDelta( true, false ); - if( !delta.isNull() ){ - Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl; - Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const ); - d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); - } - std::vector< Node > inf; - d_quantEngine->getTermUtil()->getVtsTerms( inf, true, false, false ); - for( unsigned i=0; imkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst() ) ); - d_quantEngine->getOutputChannel().lemma( inf_lem_lb ); - } - } - } -} - -bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { - Assert( !d_curr_quant.isNull() ); - //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma - if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){ - d_cbqi_set_quant_inactive = true; - d_incomplete_check = true; - d_quantEngine->getInstantiate()->recordInstantiation( - d_curr_quant, subs, false, false); - return true; - }else{ - //check if we need virtual term substitution (if used delta or infinity) - bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false ); - if (d_quantEngine->getInstantiate()->addInstantiation( - d_curr_quant, subs, false, false, used_vts)) - { - ++(d_quantEngine->d_statistics.d_instantiations_cbqi); - //d_added_inst.insert( d_curr_quant ); - return true; - }else{ - //this should never happen for monotonic selection strategies - Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl; - return false; - } - } -} - -bool InstStrategyCegqi::addLemma( Node lem ) { - return d_quantEngine->addLemma( lem ); -} - -bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { - if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){ - if( n.getAttribute(VirtualTermSkolemAttribute()) ){ - // virtual terms are allowed - return true; - }else{ - TypeNode tn = n.getType(); - if( tn.isSort() ){ - QuantEPR * qepr = d_quantEngine->getQuantEPR(); - if( qepr!=NULL ){ - //legal if in the finite set of constants of type tn - if( qepr->isEPRConstant( tn, n ) ){ - return true; - } - } - } - //only legal if current quantified formula contains n - return expr::hasSubterm(d_curr_quant, n); - } - }else{ - return true; - } -} - -CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { - std::map>::iterator it = - d_cinst.find(q); - if( it==d_cinst.end() ){ - d_cinst[q].reset( - new CegInstantiator(d_quantEngine, d_out.get(), true, true)); - return d_cinst[q].get(); - } - return it->second.get(); -} - -void InstStrategyCegqi::presolve() { - if (!options::cbqiPreRegInst()) - { - return; - } - for (std::pair>& ci : d_cinst) - { - Trace("cbqi-presolve") << "Presolve " << ci.first << std::endl; - ci.second->presolve(ci.first); - } -} - diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h deleted file mode 100644 index c3cbf8100..000000000 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h +++ /dev/null @@ -1,207 +0,0 @@ -/********************* */ -/*! \file inst_strategy_cbqi.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief counterexample-guided quantifier instantiation - **/ - - -#include "cvc4_private.h" - -#ifndef __CVC4__INST_STRATEGY_CBQI_H -#define __CVC4__INST_STRATEGY_CBQI_H - -#include "theory/decision_manager.h" -#include "theory/quantifiers/cegqi/ceg_instantiator.h" -#include "util/statistics_registry.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class InstStrategyCegqi; - -/** - * An output channel class, used by instantiator objects below. The methods - * of this class call the corresponding functions of InstStrategyCegqi below. - */ -class CegqiOutputInstStrategy : public CegqiOutput -{ - public: - CegqiOutputInstStrategy(InstStrategyCegqi* out) : d_out(out) {} - /** The module whose functions we call. */ - InstStrategyCegqi* d_out; - /** add instantiation */ - bool doAddInstantiation(std::vector& subs) override; - /** is eligible for instantiation */ - bool isEligibleForInstantiation(Node n) override; - /** add lemma */ - bool addLemma(Node lem) override; -}; - -/** - * Counterexample-guided quantifier instantiation module. - * - * This class manages counterexample-guided instantiation strategies for all - * asserted quantified formulas. - */ -class InstStrategyCegqi : public QuantifiersModule -{ - typedef context::CDHashSet NodeSet; - typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; - - public: - InstStrategyCegqi(QuantifiersEngine* qe); - ~InstStrategyCegqi(); - - /** whether to do counterexample-guided instantiation for quantifier q */ - bool doCbqi(Node q); - /** needs check at effort */ - bool needsCheck(Theory::Effort e) override; - /** needs model at effort */ - QEffort needsModel(Theory::Effort e) override; - /** reset round */ - void reset_round(Theory::Effort e) override; - /** check */ - void check(Theory::Effort e, QEffort quant_e) override; - /** check complete */ - bool checkComplete() override; - /** check complete for quantified formula */ - bool checkCompleteFor(Node q) override; - /** check ownership */ - void checkOwnership(Node q) override; - /** identify */ - std::string identify() const override { return std::string("Cegqi"); } - /** get instantiator for quantifier */ - CegInstantiator* getInstantiator(Node q); - /** pre-register quantifier */ - void preRegisterQuantifier(Node q) override; - // presolve - void presolve() override; - /** Do nested quantifier elimination. */ - Node doNestedQE(Node q, std::vector& inst_terms, Node lem, bool doVts); - - //------------------- interface for CegqiOutputInstStrategy - /** Instantiate the current quantified formula forall x. Q with x -> subs. */ - bool doAddInstantiation(std::vector& subs); - /** - * Are we allowed to instantiate the current quantified formula with n? This - * includes restrictions such as if n is a variable, it must occur free in - * the current quantified formula. - */ - bool isEligibleForInstantiation(Node n); - /** Add lemma lem via the output channel of this class. */ - bool addLemma(Node lem); - //------------------- end interface for CegqiOutputInstStrategy - - protected: - /** set quantified formula inactive - * - * This flag is set to true during a full effort check if at least one - * quantified formula is set "inactive", that is, its negation is - * unsatisfiable in the current context. - */ - bool d_cbqi_set_quant_inactive; - /** incomplete check - * - * This is set to true during a full effort check if this strategy could - * not find an instantiation for at least one asserted quantified formula. - */ - bool d_incomplete_check; - /** whether we have added cbqi lemma */ - NodeSet d_added_cbqi_lemma; - /** whether we have added cbqi lemma */ - NodeSet d_elim_quants; - /** parent guards */ - std::map< Node, std::vector< Node > > d_parent_quant; - std::map< Node, std::vector< Node > > d_children_quant; - std::map< Node, bool > d_active_quant; - /** Whether cegqi handles each quantified formula. */ - std::map d_do_cbqi; - /** - * An output channel used by instantiators for communicating with this - * class. - */ - std::unique_ptr d_out; - /** - * The instantiator for each quantified formula q registered to this class. - * This object is responsible for finding instantiatons for q. - */ - std::map> d_cinst; - /** - * The decision strategy for each quantified formula q registered to this - * class. - */ - std::map> d_dstrat; - /** the current quantified formula we are processing */ - Node d_curr_quant; - //---------------------- for vts delta minimization - /** - * Whether we will use vts delta minimization. If this flag is true, we - * add lemmas on demand of the form delta < c^1, delta < c^2, ... where c - * is a small (< 1) constant. This heuristic is used in strategies where - * vts delta cannot be fully eliminated from assertions (for example, when - * using nested quantifiers and a non-innermost instantiation strategy). - * The same strategy applies for vts infinity, which we add lemmas of the - * form inf > (1/c)^1, inf > (1/c)^2, .... - */ - bool d_check_vts_lemma_lc; - /** a small constant, used as a coefficient above */ - Node d_small_const; - //---------------------- end for vts delta minimization - /** register ce lemma */ - bool registerCbqiLemma( Node q ); - /** register counterexample lemma - * - * This is called when we have constructed lem, the negation of the body of - * quantified formula q, skolemized with the instantiation constants of q. - * This function is used for setting up the proper information in the - * instantiator for q. - */ - void registerCounterexampleLemma(Node q, Node lem); - /** has added cbqi lemma */ - bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); } - /** process functions */ - void process(Node q, Theory::Effort effort, int e); - - //for identification - uint64_t d_qid_count; - //nested qe map - std::map< Node, Node > d_nested_qe; - //mark ids on quantifiers - Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ); - // id to ce quant - std::map< Node, Node > d_id_to_ce_quant; - std::map< Node, Node > d_ce_quant_to_id; - //do nested quantifier elimination recursive - Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ); - Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ); - //elimination information (for delayed elimination) - class NestedQEInfo { - public: - NestedQEInfo() : d_doVts(false){} - ~NestedQEInfo(){} - Node d_q; - std::vector< Node > d_inst_terms; - bool d_doVts; - }; - std::map< Node, NestedQEInfo > d_nested_qe_info; - NodeIntMap d_nested_qe_waitlist_size; - NodeIntMap d_nested_qe_waitlist_proc; - std::map< Node, std::vector< Node > > d_nested_qe_waitlist; - -}; - - -} -} -} - -#endif diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp new file mode 100644 index 000000000..3ea3e72e4 --- /dev/null +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -0,0 +1,698 @@ +/********************* */ +/*! \file inst_strategy_cegqi.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of counterexample-guided quantifier instantiation strategies + **/ +#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" + +#include "expr/node_algorithm.h" +#include "options/quantifiers_options.h" +#include "smt/term_formula_removal.h" +#include "theory/arith/partial_model.h" +#include "theory/arith/theory_arith.h" +#include "theory/arith/theory_arith_private.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quant_epr.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" +#include "theory/theory_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +bool CegqiOutputInstStrategy::doAddInstantiation(std::vector& subs) +{ + return d_out->doAddInstantiation(subs); +} + +bool CegqiOutputInstStrategy::isEligibleForInstantiation(Node n) +{ + return d_out->isEligibleForInstantiation(n); +} + +bool CegqiOutputInstStrategy::addLemma(Node lem) +{ + return d_out->addLemma(lem); +} + +InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) + : QuantifiersModule(qe), + d_cbqi_set_quant_inactive(false), + d_incomplete_check(false), + d_added_cbqi_lemma(qe->getUserContext()), + d_elim_quants(qe->getSatContext()), + d_out(new CegqiOutputInstStrategy(this)), + d_nested_qe_waitlist_size(qe->getUserContext()), + d_nested_qe_waitlist_proc(qe->getUserContext()) +//, d_added_inst( qe->getUserContext() ) +{ + d_qid_count = 0; + d_small_const = + NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000)); + d_check_vts_lemma_lc = false; +} + +InstStrategyCegqi::~InstStrategyCegqi() {} + +bool InstStrategyCegqi::needsCheck(Theory::Effort e) +{ + return e>=Theory::EFFORT_LAST_CALL; +} + +QuantifiersModule::QEffort InstStrategyCegqi::needsModel(Theory::Effort e) +{ + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + return QEFFORT_STANDARD; + } + } + return QEFFORT_NONE; +} + +bool InstStrategyCegqi::registerCbqiLemma(Node q) +{ + if( !hasAddedCbqiLemma( q ) ){ + d_added_cbqi_lemma.insert( q ); + Trace("cbqi-debug") << "Do cbqi for " << q << std::endl; + //add cbqi lemma + //get the counterexample literal + Node ceLit = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); + Node ceBody = d_quantEngine->getTermUtil()->getInstConstantBody( q ); + if( !ceBody.isNull() ){ + //add counterexample lemma + Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); + //require any decision on cel to be phase=true + d_quantEngine->addRequirePhase( ceLit, true ); + Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; + //add counterexample lemma + lem = Rewriter::rewrite( lem ); + Trace("cbqi-lemma") << "Counterexample lemma : " << lem << std::endl; + registerCounterexampleLemma( q, lem ); + + //totality lemmas for EPR + QuantEPR * qepr = d_quantEngine->getQuantEPR(); + if( qepr!=NULL ){ + for( unsigned i=0; iisEPR( tn ) ){ + //add totality lemma + std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn ); + if( itc!=qepr->d_consts.end() ){ + Assert( !itc->second.empty() ); + Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ); + std::vector< Node > disj; + for( unsigned j=0; jsecond.size(); j++ ){ + disj.push_back( ic.eqNode( itc->second[j] ) ); + } + Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ); + Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl; + d_quantEngine->getOutputChannel().lemma( tlem ); + }else{ + Assert( false ); + } + }else{ + Assert( !options::cbqiAll() ); + } + } + } + } + + //compute dependencies between quantified formulas + if( options::cbqiLitDepend() || options::cbqiInnermost() ){ + std::vector< Node > ics; + TermUtil::computeInstConstContains(q, ics); + d_parent_quant[q].clear(); + d_children_quant[q].clear(); + std::vector< Node > dep; + for( unsigned i=0; igetTermUtil()->getCounterexampleLiteral( qi ); + dep.push_back( qi ); + dep.push_back( qicel ); + } + } + if( !dep.empty() ){ + Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) ); + Trace("cbqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl; + d_quantEngine->getOutputChannel().lemma( dep_lemma ); + } + } + + //must register all sub-quantifiers of counterexample lemma, register their lemmas + std::vector< Node > quants; + TermUtil::computeQuantContains( lem, quants ); + for( unsigned i=0; i>::iterator itds = + d_dstrat.find(q); + DecisionStrategy* dlds = nullptr; + if (itds == d_dstrat.end()) + { + d_dstrat[q].reset( + new DecisionStrategySingleton("CexLiteral", + ceLit, + d_quantEngine->getSatContext(), + d_quantEngine->getValuation())); + dlds = d_dstrat[q].get(); + } + else + { + dlds = itds->second.get(); + } + // it is appended to the list of strategies + d_quantEngine->getTheoryEngine()->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, dlds); + return true; + }else{ + return false; + } +} + +void InstStrategyCegqi::reset_round(Theory::Effort effort) +{ + d_cbqi_set_quant_inactive = false; + d_incomplete_check = false; + d_active_quant.clear(); + //check if any cbqi lemma has not been added yet + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine + if( doCbqi( q ) ){ + Assert( hasAddedCbqiLemma( q ) ); + if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ + d_active_quant[q] = true; + Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; + Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); + bool value; + if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ + Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl; + if( !value ){ + if( d_quantEngine->getValuation().isDecision( cel ) ){ + Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; + }else{ + Trace("cbqi") << "Inactive : " << q << std::endl; + d_quantEngine->getModel()->setQuantifierActive( q, false ); + d_cbqi_set_quant_inactive = true; + d_active_quant.erase( q ); + d_elim_quants.insert( q ); + Trace("cbqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl; + //process from waitlist + while( d_nested_qe_waitlist_proc[q]=0 ); + Assert( index<(int)d_nested_qe_waitlist[q].size() ); + Node nq = d_nested_qe_waitlist[q][index]; + Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts ); + Node dqelem = nq.eqNode( nqeqn ); + Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl; + d_quantEngine->getOutputChannel().lemma( dqelem ); + d_nested_qe_waitlist_proc[q] = index + 1; + } + } + } + }else{ + Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl; + } + } + } + } + + //refinement: only consider innermost active quantified formulas + if( options::cbqiInnermost() ){ + if( !d_children_quant.empty() && !d_active_quant.empty() ){ + Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl; + std::vector< Node > ninner; + for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ + std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first ); + if( itc!=d_children_quant.end() ){ + for( unsigned j=0; jsecond.size(); j++ ){ + if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){ + Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl; + ninner.push_back( it->first ); + break; + } + } + } + } + Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl; + for( unsigned i=0; iinConflict() ); + double clSet = 0; + if( Trace.isOn("cbqi-engine") ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); + Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl; + } + unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); + for( int ee=0; ee<=1; ee++ ){ + //for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + // Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + // if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ + Node q = it->first; + Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl; + if( d_nested_qe.find( q )==d_nested_qe.end() ){ + process( q, e, ee ); + if( d_quantEngine->inConflict() ){ + break; + } + }else{ + Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl; + Assert( false ); + } + } + if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ + break; + } + } + if( Trace.isOn("cbqi-engine") ){ + if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ + Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; + } + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl; + } + } +} + +bool InstStrategyCegqi::checkComplete() +{ + if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){ + return false; + }else{ + return true; + } +} + +bool InstStrategyCegqi::checkCompleteFor(Node q) +{ + std::map::iterator it = d_do_cbqi.find(q); + if( it!=d_do_cbqi.end() ){ + return it->second != CEG_UNHANDLED; + }else{ + return false; + } +} + +Node InstStrategyCegqi::getIdMarkedQuantNode(Node n, + std::map& visited) +{ + std::map< Node, Node >::iterator it = visited.find( n ); + if( it==visited.end() ){ + Node ret = n; + if( n.getKind()==FORALL ){ + QAttributes qa; + QuantAttributes::computeQuantAttributes( n, qa ); + if( qa.d_qid_num.isNull() ){ + std::vector< Node > rc; + rc.push_back( n[0] ); + rc.push_back( getIdMarkedQuantNode( n[1], visited ) ); + Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() ); + QuantIdNumAttribute ida; + avar.setAttribute(ida,d_qid_count); + d_qid_count++; + std::vector< Node > iplc; + iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) ); + if( n.getNumChildren()==3 ){ + for( unsigned i=0; imkNode( INST_PATTERN_LIST, iplc ) ); + ret = NodeManager::currentNM()->mkNode( FORALL, rc ); + } + }else if( n.getNumChildren()>0 ){ + std::vector< Node > children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + bool childChanged = false; + for( unsigned i=0; imkNode( n.getKind(), children ); + } + } + visited[n] = ret; + return ret; + }else{ + return it->second; + } +} + +void InstStrategyCegqi::checkOwnership(Node q) +{ + if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ + if (d_do_cbqi[q] == CEG_HANDLED) + { + //take full ownership of the quantified formula + d_quantEngine->setOwner( q, this ); + } + } +} + +void InstStrategyCegqi::preRegisterQuantifier(Node q) +{ + // mark all nested quantifiers with id + if (options::cbqiNestedQE()) + { + if( d_quantEngine->getOwner(q)==this ) + { + std::map visited; + Node mq = getIdMarkedQuantNode(q[1], visited); + if (mq != q[1]) + { + // do not do cbqi, we are reducing this quantified formula to a marked + // one + d_do_cbqi[q] = CEG_UNHANDLED; + // instead do reduction + std::vector qqc; + qqc.push_back(q[0]); + qqc.push_back(mq); + if (q.getNumChildren() == 3) + { + qqc.push_back(q[2]); + } + Node qq = NodeManager::currentNM()->mkNode(FORALL, qqc); + Node mlem = NodeManager::currentNM()->mkNode(IMPLIES, q, qq); + Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl; + d_quantEngine->addLemma(mlem); + } + } + } + if( doCbqi( q ) ){ + // get the instantiator + if (options::cbqiPreRegInst()) + { + getInstantiator(q); + } + // register the cbqi lemma + if( registerCbqiLemma( q ) ){ + Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl; + } + } +} + +Node InstStrategyCegqi::doNestedQENode( + Node q, Node ceq, Node n, std::vector& inst_terms, bool doVts) +{ + // there is a nested quantified formula (forall y. nq[y,x]) such that + // q is (forall y. nq[y,t]) for ground terms t, + // ceq is (forall y. nq[y,e]) for CE variables e. + // we call this function when we know (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e]. + // in this case, q is equivalent to the quantifier-free formula C[t]. + if( d_nested_qe.find( ceq )==d_nested_qe.end() ){ + d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq ); + Trace("cbqi-nqe") << "CE quantifier elimination : " << std::endl; + Trace("cbqi-nqe") << " " << ceq << std::endl; + Trace("cbqi-nqe") << " " << d_nested_qe[ceq] << std::endl; + //should not contain quantifiers + Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) ); + } + Assert( d_quantEngine->getTermUtil()->d_inst_constants[q].size()==inst_terms.size() ); + //replace inst constants with instantiation + Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(), + d_quantEngine->getTermUtil()->d_inst_constants[q].end(), + inst_terms.begin(), inst_terms.end() ); + if( doVts ){ + //do virtual term substitution + ret = Rewriter::rewrite( ret ); + ret = d_quantEngine->getTermUtil()->rewriteVtsSymbols( ret ); + } + Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl; + Trace("cbqi-nqe") << " " << n << std::endl; + Trace("cbqi-nqe") << " " << ret << std::endl; + return ret; +} + +Node InstStrategyCegqi::doNestedQERec(Node q, + Node n, + std::map& visited, + std::vector& inst_terms, + bool doVts) +{ + if( visited.find( n )==visited.end() ){ + Node ret = n; + if( n.getKind()==FORALL ){ + QAttributes qa; + QuantAttributes::computeQuantAttributes( n, qa ); + if( !qa.d_qid_num.isNull() ){ + //if it has an id, check whether we have done quantifier elimination for this id + std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num ); + if( it!=d_id_to_ce_quant.end() ){ + Node ceq = it->second; + bool doNestedQe = d_elim_quants.contains( ceq ); + if( doNestedQe ){ + ret = doNestedQENode( q, ceq, n, inst_terms, doVts ); + }else{ + Trace("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl; + Node nr = Rewriter::rewrite( n ); + Trace("cbqi-nqe") << " " << ceq << std::endl; + Trace("cbqi-nqe") << " " << nr << std::endl; + int wlsize = d_nested_qe_waitlist_size[ceq] + 1; + d_nested_qe_waitlist_size[ceq] = wlsize; + if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){ + d_nested_qe_waitlist[ceq][wlsize] = nr; + }else{ + d_nested_qe_waitlist[ceq].push_back( nr ); + } + d_nested_qe_info[nr].d_q = q; + d_nested_qe_info[nr].d_inst_terms.clear(); + d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() ); + d_nested_qe_info[nr].d_doVts = doVts; + //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true. + Assert( !options::cbqiInnermost() ); + } + } + } + }else if( n.getNumChildren()>0 ){ + std::vector< Node > children; + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + bool childChanged = false; + for( unsigned i=0; imkNode( n.getKind(), children ); + } + } + visited[n] = ret; + return ret; + }else{ + return n; + } +} + +Node InstStrategyCegqi::doNestedQE(Node q, + std::vector& inst_terms, + Node lem, + bool doVts) +{ + std::map< Node, Node > visited; + return doNestedQERec( q, lem, visited, inst_terms, doVts ); +} + +void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) +{ + // must register with the instantiator + // must explicitly remove ITEs so that we record dependencies + std::vector ce_vars; + TermUtil* tutil = d_quantEngine->getTermUtil(); + for (unsigned i = 0, nics = tutil->getNumInstantiationConstants(q); i < nics; + i++) + { + ce_vars.push_back(tutil->getInstantiationConstant(q, i)); + } + std::vector lems; + lems.push_back(lem); + CegInstantiator* cinst = getInstantiator(q); + cinst->registerCounterexampleLemma(lems, ce_vars); + for (unsigned i = 0, size = lems.size(); i < size; i++) + { + Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] + << std::endl; + d_quantEngine->addLemma(lems[i], false); + } +} + +bool InstStrategyCegqi::doCbqi(Node q) +{ + std::map::iterator it = d_do_cbqi.find(q); + if( it==d_do_cbqi.end() ){ + CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine); + Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; + d_do_cbqi[q] = ret; + return ret != CEG_UNHANDLED; + } + return it->second != CEG_UNHANDLED; +} + +void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { + if( e==0 ){ + CegInstantiator * cinst = getInstantiator( q ); + Trace("inst-alg") << "-> Run cegqi for " << q << std::endl; + d_curr_quant = q; + if( !cinst->check() ){ + d_incomplete_check = true; + d_check_vts_lemma_lc = true; + } + d_curr_quant = Node::null(); + }else if( e==1 ){ + //minimize the free delta heuristically on demand + 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 = Rewriter::rewrite( d_small_const ); + //heuristic for now, until we know how to do nested quantification + Node delta = d_quantEngine->getTermUtil()->getVtsDelta( true, false ); + if( !delta.isNull() ){ + Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl; + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); + } + std::vector< Node > inf; + d_quantEngine->getTermUtil()->getVtsTerms( inf, true, false, false ); + for( unsigned i=0; imkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst() ) ); + d_quantEngine->getOutputChannel().lemma( inf_lem_lb ); + } + } + } +} + +bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { + Assert( !d_curr_quant.isNull() ); + //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma + if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){ + d_cbqi_set_quant_inactive = true; + d_incomplete_check = true; + d_quantEngine->getInstantiate()->recordInstantiation( + d_curr_quant, subs, false, false); + return true; + }else{ + //check if we need virtual term substitution (if used delta or infinity) + bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false ); + if (d_quantEngine->getInstantiate()->addInstantiation( + d_curr_quant, subs, false, false, used_vts)) + { + ++(d_quantEngine->d_statistics.d_instantiations_cbqi); + //d_added_inst.insert( d_curr_quant ); + return true; + }else{ + //this should never happen for monotonic selection strategies + Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl; + return false; + } + } +} + +bool InstStrategyCegqi::addLemma( Node lem ) { + return d_quantEngine->addLemma( lem ); +} + +bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { + if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){ + if( n.getAttribute(VirtualTermSkolemAttribute()) ){ + // virtual terms are allowed + return true; + }else{ + TypeNode tn = n.getType(); + if( tn.isSort() ){ + QuantEPR * qepr = d_quantEngine->getQuantEPR(); + if( qepr!=NULL ){ + //legal if in the finite set of constants of type tn + if( qepr->isEPRConstant( tn, n ) ){ + return true; + } + } + } + //only legal if current quantified formula contains n + return expr::hasSubterm(d_curr_quant, n); + } + }else{ + return true; + } +} + +CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { + std::map>::iterator it = + d_cinst.find(q); + if( it==d_cinst.end() ){ + d_cinst[q].reset( + new CegInstantiator(d_quantEngine, d_out.get(), true, true)); + return d_cinst[q].get(); + } + return it->second.get(); +} + +void InstStrategyCegqi::presolve() { + if (!options::cbqiPreRegInst()) + { + return; + } + for (std::pair>& ci : d_cinst) + { + Trace("cbqi-presolve") << "Presolve " << ci.first << std::endl; + ci.second->presolve(ci.first); + } +} + diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h new file mode 100644 index 000000000..0a19727b8 --- /dev/null +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -0,0 +1,207 @@ +/********************* */ +/*! \file inst_strategy_cegqi.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief counterexample-guided quantifier instantiation + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H +#define __CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H + +#include "theory/decision_manager.h" +#include "theory/quantifiers/cegqi/ceg_instantiator.h" +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class InstStrategyCegqi; + +/** + * An output channel class, used by instantiator objects below. The methods + * of this class call the corresponding functions of InstStrategyCegqi below. + */ +class CegqiOutputInstStrategy : public CegqiOutput +{ + public: + CegqiOutputInstStrategy(InstStrategyCegqi* out) : d_out(out) {} + /** The module whose functions we call. */ + InstStrategyCegqi* d_out; + /** add instantiation */ + bool doAddInstantiation(std::vector& subs) override; + /** is eligible for instantiation */ + bool isEligibleForInstantiation(Node n) override; + /** add lemma */ + bool addLemma(Node lem) override; +}; + +/** + * Counterexample-guided quantifier instantiation module. + * + * This class manages counterexample-guided instantiation strategies for all + * asserted quantified formulas. + */ +class InstStrategyCegqi : public QuantifiersModule +{ + typedef context::CDHashSet NodeSet; + typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; + + public: + InstStrategyCegqi(QuantifiersEngine* qe); + ~InstStrategyCegqi(); + + /** whether to do counterexample-guided instantiation for quantifier q */ + bool doCbqi(Node q); + /** needs check at effort */ + bool needsCheck(Theory::Effort e) override; + /** needs model at effort */ + QEffort needsModel(Theory::Effort e) override; + /** reset round */ + void reset_round(Theory::Effort e) override; + /** check */ + void check(Theory::Effort e, QEffort quant_e) override; + /** check complete */ + bool checkComplete() override; + /** check complete for quantified formula */ + bool checkCompleteFor(Node q) override; + /** check ownership */ + void checkOwnership(Node q) override; + /** identify */ + std::string identify() const override { return std::string("Cegqi"); } + /** get instantiator for quantifier */ + CegInstantiator* getInstantiator(Node q); + /** pre-register quantifier */ + void preRegisterQuantifier(Node q) override; + // presolve + void presolve() override; + /** Do nested quantifier elimination. */ + Node doNestedQE(Node q, std::vector& inst_terms, Node lem, bool doVts); + + //------------------- interface for CegqiOutputInstStrategy + /** Instantiate the current quantified formula forall x. Q with x -> subs. */ + bool doAddInstantiation(std::vector& subs); + /** + * Are we allowed to instantiate the current quantified formula with n? This + * includes restrictions such as if n is a variable, it must occur free in + * the current quantified formula. + */ + bool isEligibleForInstantiation(Node n); + /** Add lemma lem via the output channel of this class. */ + bool addLemma(Node lem); + //------------------- end interface for CegqiOutputInstStrategy + + protected: + /** set quantified formula inactive + * + * This flag is set to true during a full effort check if at least one + * quantified formula is set "inactive", that is, its negation is + * unsatisfiable in the current context. + */ + bool d_cbqi_set_quant_inactive; + /** incomplete check + * + * This is set to true during a full effort check if this strategy could + * not find an instantiation for at least one asserted quantified formula. + */ + bool d_incomplete_check; + /** whether we have added cbqi lemma */ + NodeSet d_added_cbqi_lemma; + /** whether we have added cbqi lemma */ + NodeSet d_elim_quants; + /** parent guards */ + std::map< Node, std::vector< Node > > d_parent_quant; + std::map< Node, std::vector< Node > > d_children_quant; + std::map< Node, bool > d_active_quant; + /** Whether cegqi handles each quantified formula. */ + std::map d_do_cbqi; + /** + * An output channel used by instantiators for communicating with this + * class. + */ + std::unique_ptr d_out; + /** + * The instantiator for each quantified formula q registered to this class. + * This object is responsible for finding instantiatons for q. + */ + std::map> d_cinst; + /** + * The decision strategy for each quantified formula q registered to this + * class. + */ + std::map> d_dstrat; + /** the current quantified formula we are processing */ + Node d_curr_quant; + //---------------------- for vts delta minimization + /** + * Whether we will use vts delta minimization. If this flag is true, we + * add lemmas on demand of the form delta < c^1, delta < c^2, ... where c + * is a small (< 1) constant. This heuristic is used in strategies where + * vts delta cannot be fully eliminated from assertions (for example, when + * using nested quantifiers and a non-innermost instantiation strategy). + * The same strategy applies for vts infinity, which we add lemmas of the + * form inf > (1/c)^1, inf > (1/c)^2, .... + */ + bool d_check_vts_lemma_lc; + /** a small constant, used as a coefficient above */ + Node d_small_const; + //---------------------- end for vts delta minimization + /** register ce lemma */ + bool registerCbqiLemma( Node q ); + /** register counterexample lemma + * + * This is called when we have constructed lem, the negation of the body of + * quantified formula q, skolemized with the instantiation constants of q. + * This function is used for setting up the proper information in the + * instantiator for q. + */ + void registerCounterexampleLemma(Node q, Node lem); + /** has added cbqi lemma */ + bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); } + /** process functions */ + void process(Node q, Theory::Effort effort, int e); + + //for identification + uint64_t d_qid_count; + //nested qe map + std::map< Node, Node > d_nested_qe; + //mark ids on quantifiers + Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ); + // id to ce quant + std::map< Node, Node > d_id_to_ce_quant; + std::map< Node, Node > d_ce_quant_to_id; + //do nested quantifier elimination recursive + Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ); + Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ); + //elimination information (for delayed elimination) + class NestedQEInfo { + public: + NestedQEInfo() : d_doVts(false){} + ~NestedQEInfo(){} + Node d_q; + std::vector< Node > d_inst_terms; + bool d_doVts; + }; + std::map< Node, NestedQEInfo > d_nested_qe_info; + NodeIntMap d_nested_qe_waitlist_size; + NodeIntMap d_nested_qe_waitlist_proc; + std::map< Node, std::vector< Node > > d_nested_qe_waitlist; + +}; + + +} +} +} + +#endif diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 13597c338..96a28cde6 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -17,7 +17,7 @@ #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" +#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 09829e894..b27163549 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -20,7 +20,7 @@ #include "context/cdlist.h" #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" #include "theory/quantifiers/inst_match_trie.h" -#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" +#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 305f3182d..516f31efc 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -22,7 +22,7 @@ #include "theory/quantifiers/alpha_equivalence.h" #include "theory/quantifiers/anti_skolem.h" #include "theory/quantifiers/bv_inverter.h" -#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" +#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/conjecture_generator.h" #include "theory/quantifiers/ematching/inst_strategy_e_matching.h" #include "theory/quantifiers/ematching/instantiation_engine.h"