From 2cadfe31cfddaff7eff4cd220273d0bab3d2792d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 31 Aug 2016 17:44:42 -0500 Subject: [PATCH] Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly. --- src/options/quantifiers_options | 4 +- src/smt/smt_engine.cpp | 7 +- src/theory/quantifiers/ceg_instantiator.cpp | 62 ++- src/theory/quantifiers/inst_match.cpp | 14 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 417 ++++++++++++++---- src/theory/quantifiers/inst_strategy_cbqi.h | 35 ++ src/theory/quantifiers/term_database.cpp | 27 +- src/theory/quantifiers/term_database.h | 18 +- src/theory/quantifiers_engine.cpp | 44 +- src/theory/quantifiers_engine.h | 4 + src/theory/theory_engine.cpp | 9 + src/theory/theory_engine.h | 6 + 12 files changed, 525 insertions(+), 122 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 9f8f088de..f5561ad23 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -303,8 +303,10 @@ option cbqiNopt --cbqi-nopt bool :default true non-optimal bounds for counterexample-based quantifier instantiation option cbqiLitDepend --cbqi-lit-dep bool :default false dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation -option cbqiInnermost --cbqi-innermost bool :default false +option cbqiInnermost --cbqi-innermost bool :read-write :default false only process innermost quantified formulas in counterexample-based quantifier instantiation +option cbqiNestedQE --cbqi-nested-qe bool :default false + process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation option quantEpr --quant-epr bool :default false infer whether in effectively propositional fragment, use for cbqi diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3670e8cb9..82d3139b2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5138,6 +5138,8 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) ss << "While performing quantifier elimination, unexpected result : " << r << " for query."; InternalError(ss.str().c_str()); } + + #if 1 //get the instantiations for all quantified formulas std::map< Node, std::vector< Node > > insts; d_theoryEngine->getInstantiations( insts ); @@ -5168,7 +5170,10 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) ss << " that was not related to the query. Try option --simplification=none."; InternalError(ss.str().c_str()); } - } + } +#else + Node ret_n = d_theoryEngine->getInstantiatedConjunction( top_q ); +#endif Trace("smt-qe") << "Returned : " << ret_n << std::endl; ret_n = Rewriter::rewrite( ret_n.negate() ); return ret_n.toExpr(); diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index e4d12904e..d31851ec4 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -20,6 +20,7 @@ #include "theory/arith/theory_arith_private.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/theory_engine.h" #include "theory/bv/theory_bv_utils.h" @@ -372,7 +373,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: int ires = solve_arith( pv, satom, veq_c, val, vts_coeff_inf, vts_coeff_delta ); if( ires!=0 ){ //disequalities are either strict upper or lower bounds - unsigned rmax = ( atom.getKind()==GEQ && options::cbqiModel() ) ? 1 : 2; + unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2; for( unsigned r=0; r0 ? 0 : 1; mbp_bounds[index].push_back( uval ); mbp_coeff[index].push_back( veq_c ); + Trace("cbqi-inst-debug") << "Store bound " << index << " " << uval << " " << veq_c << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl; for( unsigned t=0; t<2; t++ ){ mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta ); } @@ -719,6 +723,13 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std:: //[5] resort to using value in model // do so if we are in effort=1, or if the variable is boolean, or if we are solving for a subfield of a datatype if( ( effort>0 || pvtn.isBoolean() || pvtn.isBitVector() || !curr_var.empty() ) && d_qe->getTermDatabase()->isClosedEnumerableType( pvtn ) ){ + +#ifdef CVC4_ASSERTIONS + if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){ + Trace("cbqi-warn") << "Had to resort to model value." << std::endl; + Assert( false ); + } +#endif Node mv = getModelValue( pv ); Node pv_coeff_m; Trace("cbqi-inst-debug") << "[5] " << i << "...try model value " << mv << std::endl; @@ -1222,25 +1233,27 @@ void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& ter } void CegInstantiator::presolve( Node q ) { - Trace("cbqi-presolve") << "CBQI presolve " << q << std::endl; //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing - std::vector< Node > vars; - std::map< Node, std::vector< Node > > teq; - for( unsigned i=0; i terms; - std::vector< Node > conj; - getPresolveEqConjuncts( vars, terms, teq, q, conj ); + //only if no nested quantifiers + if( !QuantifiersRewriter::containsQuantifiers( q[1] ) ){ + std::vector< Node > vars; + std::map< Node, std::vector< Node > > teq; + for( unsigned i=0; i terms; + std::vector< Node > conj; + getPresolveEqConjuncts( 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("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; - d_qe->getOutputChannel().lemma( lem, false, true ); + 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("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; + d_qe->getOutputChannel().lemma( lem, false, true ); + } } } @@ -1479,7 +1492,8 @@ struct sortCegVarOrder { void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) { - Assert( d_vars.empty() ); + //Assert( d_vars.empty() ); + d_vars.clear(); d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() ); //determine variable order: must do Reals before Ints @@ -1512,7 +1526,9 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st //remove ITEs IteSkolemMap iteSkolemMap; d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap); - Assert( d_aux_vars.empty() ); + //Assert( d_aux_vars.empty() ); + d_aux_vars.clear(); + d_aux_eq.clear(); for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl; d_aux_vars.push_back( i->first ); @@ -1601,6 +1617,7 @@ int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, No if( options::cbqiAll() ){ // when not pure LIA/LRA, we must check whether the lhs contains pv if( TermDb::containsTerm( val, pv ) ){ + Trace("cbqi-inst-debug") << "fail : contains bad term" << std::endl; return 0; } } @@ -1656,6 +1673,9 @@ int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, No } vts_coeff_inf = vts_coeff[0]; vts_coeff_delta = vts_coeff[1]; + Trace("cbqi-inst-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl; + }else{ + Trace("cbqi-inst-debug") << "fail : could not get monomial sum" << std::endl; } return ires; } diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 7e5424d9c..12e15d353 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -258,7 +258,11 @@ void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std:: } } }else{ - insts.push_back( qe->getInstantiation( q, terms, true ) ); + if( hasInstLemma() ){ + insts.push_back( getInstLemma() ); + }else{ + insts.push_back( qe->getInstantiation( q, terms, true ) ); + } } }else{ for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ @@ -428,13 +432,17 @@ void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std if( terms.size()==q[0].getNumChildren() ){ if( useActive ){ if( hasInstLemma() ){ - Node lem; + Node lem = getInstLemma(); if( std::find( active.begin(), active.end(), lem )!=active.end() ){ insts.push_back( lem ); } } }else{ - insts.push_back( qe->getInstantiation( q, terms, true ) ); + if( hasInstLemma() ){ + insts.push_back( getInstLemma() ); + }else{ + insts.push_back( qe->getInstantiation( q, terms, true ) ); + } } }else{ for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index b9a415e46..f3061f575 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/theory_engine.h" using namespace std; @@ -34,9 +35,13 @@ using namespace CVC4::theory::arith; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) - : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ) + : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), +d_elim_quants( qe->getSatContext() ), +d_nested_qe_waitlist_size( qe->getUserContext() ), +d_nested_qe_waitlist_proc( qe->getUserContext() ) //, d_added_inst( qe->getUserContext() ) { + d_qid_count = 0; } InstStrategyCbqi::~InstStrategyCbqi() throw(){} @@ -55,6 +60,103 @@ unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) { return QuantifiersEngine::QEFFORT_NONE; } +bool InstStrategyCbqi::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->getTermDatabase()->getCounterexampleLiteral( q ); + Node ceBody = d_quantEngine->getTermDatabase()->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->getTermDatabase()->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; + TermDb::computeVarContains( q, ics ); + d_parent_quant[q].clear(); + d_children_quant[q].clear(); + std::vector< Node > dep; + for( unsigned i=0; igetTermDatabase()->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; + TermDb::computeQuantContains( lem, quants ); + for( unsigned i=0; igetModel()->getAssertedQuantifier( i ); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine if( doCbqi( q ) ){ - if( !hasAddedCbqiLemma( q ) ){ - d_added_cbqi_lemma.insert( q ); - Trace("cbqi") << "Do cbqi for " << q << std::endl; - //add cbqi lemma - //get the counterexample literal - Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); - Node ceBody = d_quantEngine->getTermDatabase()->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") << "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->getTermDatabase()->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") << "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; - TermDb::computeVarContains( q, ics ); - d_parent_quant[q].clear(); - d_children_quant[q].clear(); - std::vector< Node > dep; - for( unsigned i=0; igetTermDatabase()->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") << "Counterexample dependency lemma : " << dep_lemma << std::endl; - d_quantEngine->getOutputChannel().lemma( dep_lemma ); - } - } - } + if( registerCbqiLemma( q ) ){ + Debug("cbqi-debug") << "Registered cbqi lemma." << std::endl; //set inactive the quantified formulas whose CE literals are asserted false }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ d_active_quant[q] = true; @@ -147,9 +180,24 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { 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.iffNode( 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{ @@ -204,9 +252,15 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) { // 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; - process( q, e, ee ); - if( d_quantEngine->inConflict() ){ - break; + Trace("cbqi") << "CBQI : Process " << q << " 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 ){ @@ -231,11 +285,79 @@ bool InstStrategyCbqi::checkComplete() { } } +Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){ + std::map< Node, Node >::iterator it = visited.find( n ); + if( it==visited.end() ){ + Node ret = n; + if( n.getKind()==FORALL ){ + QAttributes qa; + TermDb::computeQuantAttributes( n, qa ); + if( qa.d_qid_num==-1 ){ + 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 InstStrategyCbqi::preRegisterQuantifier( Node q ) { if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ if( !options::cbqiAll() && !options::cbqiSplx() ){ //take full ownership of the quantified formula d_quantEngine->setOwner( q, this ); + + //mark all nested quantifiers with id + if( options::cbqiNestedQE() ){ + std::map< Node, Node > visited; + Node mq = getIdMarkedQuantNode( q[1], visited ); + if( mq!=q[1] ){ + //do not do cbqi + d_do_cbqi[q] = false; + //instead do reduction + std::vector< Node > 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->getOutputChannel().lemma( mlem ); + } + } } } } @@ -244,6 +366,97 @@ void InstStrategyCbqi::registerQuantifier( Node q ) { } +Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& 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 (exists e. ceq[e,k]) is equivalent to quantifier-free formula C[k]. + // 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->getTermDatabase()->d_inst_constants[q].size()==inst_terms.size() ); + //replace inst constants with instantiation + Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermDatabase()->d_inst_constants[q].begin(), + d_quantEngine->getTermDatabase()->d_inst_constants[q].end(), + inst_terms.begin(), inst_terms.end() ); + if( doVts ){ + //do virtual term substitution + ret = Rewriter::rewrite( ret ); + ret = d_quantEngine->getTermDatabase()->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 InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ) { + std::map< Node, Node >::iterator it = visited.find( n ); + if( visited.find( n )==visited.end() ){ + Node ret = n; + if( n.getKind()==FORALL ){ + QAttributes qa; + TermDb::computeQuantAttributes( n, qa ); + if( qa.d_qid_num!=-1 ){ + //if it has an id, check whether we have done quantifier elimination for this id + std::map< int, 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; + } + } + } + }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 InstStrategyCbqi::doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ) { + std::map< Node, Node > visited; + return doNestedQERec( q, lem, visited, inst_terms, doVts ); +} + void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){ Trace("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; d_quantEngine->addLemma( lem, false ); @@ -299,14 +512,17 @@ int InstStrategyCbqi::hasNonCbqiVariable( Node q ){ bool InstStrategyCbqi::doCbqi( Node q ){ std::map< Node, bool >::iterator it = d_do_cbqi.find( q ); if( it==d_do_cbqi.end() ){ - bool ret = false; - if( d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){ - ret = true; - }else{ + bool ret = true; + if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){ //if has an instantiation pattern, don't do it if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ - ret = false; - }else{ + for( unsigned i=0; i visited; ret = !hasNonCbqiOperator( q[1], visited ); + }else{ + ret = false; } } } } - Trace("cbqi") << "doCbqi " << q << " returned " << ret << std::endl; + Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; d_do_cbqi[q] = ret; return ret; }else{ @@ -332,10 +550,20 @@ bool InstStrategyCbqi::doCbqi( Node q ){ } } -Node InstStrategyCbqi::getNextDecisionRequest(){ - // all counterexample literals that are not asserted - for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ - Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); +Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) { + if( proc.find( q )==proc.end() ){ + proc[q] = true; + //first check children + std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( q ); + if( itc!=d_children_quant.end() ){ + for( unsigned j=0; jsecond.size(); j++ ){ + Node d = getNextDecisionRequestProc( itc->second[j], proc ); + if( !d.isNull() ){ + return d; + } + } + } + //then check self if( hasAddedCbqiLemma( q ) ){ Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); bool value; @@ -343,6 +571,18 @@ Node InstStrategyCbqi::getNextDecisionRequest(){ Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl; return cel; } + } + } + return Node::null(); +} + +Node InstStrategyCbqi::getNextDecisionRequest(){ + std::map< Node, bool > proc; + for( unsigned i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + Node d = getNextDecisionRequestProc( q, proc ); + if( !d.isNull() ){ + return d; } } return Node::null(); @@ -755,6 +995,9 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { //d_added_inst.insert( d_curr_quant ); return true; }else{ + //this should never happen for monotonic selection strategies + Trace("cbqi-warn") << "Existing instantiation" << std::endl; + Assert( !options::cbqiNestedQE() || options::cbqiAll() ); return false; } } @@ -827,7 +1070,9 @@ void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) { void InstStrategyCegqi::presolve() { if( options::cbqiPreRegInst() ){ for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){ + Trace("cbqi-presolve") << "Presolve " << it->first << std::endl; it->second->presolve( it->first ); } } } + diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 18931f8f6..eb80de3ce 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -34,11 +34,14 @@ namespace quantifiers { class InstStrategyCbqi : public QuantifiersModule { typedef context::CDHashSet NodeSet; + typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; protected: bool d_cbqi_set_quant_inactive; 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; @@ -48,15 +51,47 @@ protected: /** whether to do cbqi for this quantified formula */ std::map< Node, bool > d_do_cbqi; /** register ce lemma */ + bool registerCbqiLemma( Node q ); virtual 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(); } /** helper functions */ int hasNonCbqiVariable( Node q ); bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ); + /** get next decision request with dependency checking */ + Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ); /** process functions */ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; virtual void process( Node q, Theory::Effort effort, int e ) = 0; +protected: + //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< int, Node > d_id_to_ce_quant; + std::map< Node, int > 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(){} + ~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; +public: + //do nested quantifier elimination + Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ); public: InstStrategyCbqi( QuantifiersEngine * qe ); ~InstStrategyCbqi() throw(); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5d8564adf..f253d655b 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1319,19 +1319,25 @@ bool TermDb::mayComplete( TypeNode tn ) { void TermDb::computeVarContains( Node n, std::vector< Node >& varContains ) { std::map< Node, bool > visited; - computeVarContains2( n, varContains, visited ); + computeVarContains2( n, INST_CONSTANT, varContains, visited ); } -void TermDb::computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ){ +void TermDb::computeQuantContains( Node n, std::vector< Node >& quantContains ) { + std::map< Node, bool > visited; + computeVarContains2( n, FORALL, quantContains, visited ); +} + + +void TermDb::computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ){ if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getKind()==INST_CONSTANT ){ + if( n.getKind()==k ){ if( std::find( varContains.begin(), varContains.end(), n )==varContains.end() ){ varContains.push_back( n ); } }else{ for( unsigned i=0; i::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return -1; + }else{ + return it->second.d_qid_num; + } +} + TermDbSygus::TermDbSygus( context::Context* c, QuantifiersEngine* qe ) : d_quantEngine( qe ){ d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 7ab3668eb..29b7b93c6 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -105,6 +105,11 @@ typedef expr::Attribute< QuantElimAttributeId, bool > QuantElimAttribute; struct QuantElimPartialAttributeId {}; typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAttribute; +/** Attribute for id number */ +struct QuantIdNumAttributeId {}; +typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; + + class QuantifiersEngine; namespace inst{ @@ -131,7 +136,7 @@ public: class QAttributes{ public: QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false), - d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){} + d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false), d_qid_num(-1){} ~QAttributes(){} bool d_hasPattern; Node d_rr; @@ -145,6 +150,7 @@ public: bool d_quant_elim; bool d_quant_elim_partial; Node d_ipl; + int d_qid_num; bool isRewriteRule() { return !d_rr.isNull(); } bool isFunDef() { return !d_fundef_f.isNull(); } }; @@ -301,8 +307,6 @@ private: /** map from universal quantifiers to the list of variables */ std::map< Node, std::vector< Node > > d_vars; std::map< Node, std::map< Node, unsigned > > d_var_num; - /** map from universal quantifiers to the list of instantiation constants */ - std::map< Node, std::vector< Node > > d_inst_constants; /** map from universal quantifiers to their inst constant body */ std::map< Node, Node > d_inst_const_body; /** map from universal quantifiers to their counterexample literals */ @@ -312,6 +316,8 @@ private: /** make instantiation constants for */ void makeInstantiationConstantsFor( Node q ); public: + /** map from universal quantifiers to the list of instantiation constants */ + std::map< Node, std::vector< Node > > d_inst_constants; /** get variable number */ unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; } /** get the i^th instantiation constant of q */ @@ -388,7 +394,7 @@ public: //for triggers private: /** helper function for compute var contains */ - static void computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ); + static void computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ); /** triggers for each operator */ std::map< Node, std::vector< inst::Trigger* > > d_op_triggers; /** helper for is instance of */ @@ -402,6 +408,8 @@ public: static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); /** get var contains for node n */ static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); + /** compute quant contains */ + static void computeQuantContains( Node n, std::vector< Node >& quantContains ); /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ static int isInstanceOf( Node n1, Node n2 ); /** filter all nodes that have instances */ @@ -541,6 +549,8 @@ public: bool isQAttrQuantElim( Node q ); /** is quant elim partial */ bool isQAttrQuantElimPartial( Node q ); + /** get quant id num */ + int getQAttrQuantIdNum( Node q ); /** compute quantifier attributes */ static void computeQuantAttributes( Node q, QAttributes& qa ); };/* class TermDb */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 603f6f5fd..57eb375d3 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -141,7 +141,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_rel_dom = NULL; d_builder = NULL; - d_trackInstLemmas = options::proof() && options::trackInstLemmas(); + d_trackInstLemmas = options::cbqiNestedQE() || ( options::proof() && options::trackInstLemmas() ); d_total_inst_count_debug = 0; //allow theory combination to go first, once initially @@ -627,6 +627,7 @@ void QuantifiersEngine::notifyCombineTheories() { } bool QuantifiersEngine::reduceQuantifier( Node q ) { + //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants BoolMap::const_iterator it = d_quants_red.find( q ); if( it==d_quants_red.end() ){ Node lem; @@ -733,7 +734,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ //register the quantifier, assert it to each module if( registerQuantifier( f ) ){ d_model->assertQuantifier( f ); - for( int i=0; i<(int)d_modules.size(); i++ ){ + for( unsigned i=0; iassertNode( f ); } addTermToDatabase( d_term_db->getInstConstantBody( f ), true ); @@ -1138,6 +1139,9 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo Assert( d_term_db->d_vars[q].size()==terms.size() ); Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts ); //do virtual term substitution Node orig_body = body; + if( options::cbqiNestedQE() && d_i_cbqi ){ + body = d_i_cbqi->doNestedQE( q, terms, body, doVts ); + } body = quantifiers::QuantifiersRewriter::preprocess( body, true ); Trace("inst-debug") << "...preprocess to " << body << std::endl; @@ -1443,6 +1447,42 @@ void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > > } } +void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts ) { + if( options::incrementalSolving() ){ + std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q ); + if( it!=d_c_inst_match_trie.end() ){ + std::vector< Node > active_lemmas; + it->second->getInstantiations( insts, it->first, this, false, active_lemmas ); + } + }else{ + std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.find( q ); + if( it!=d_inst_match_trie.end() ){ + std::vector< Node > active_lemmas; + it->second.getInstantiations( insts, it->first, this, false, active_lemmas ); + } + } +} + +Node QuantifiersEngine::getInstantiatedConjunction( Node q ) { + std::vector< Node > insts; + getInstantiations( q, insts ); + if( insts.empty() ){ + return NodeManager::currentNM()->mkConst(true); + }else{ + Node ret; + if( insts.size()==1 ){ + ret = insts[0]; + }else{ + ret = NodeManager::currentNM()->mkNode( kind::AND, insts ); + } + //have to remove q, TODO: avoid this in a better way + TNode tq = q; + TNode tt = d_term_db->d_true; + ret = ret.substitute( tq, tt ); + return ret; + } +} + QuantifiersEngine::Statistics::Statistics() : d_time("theory::QuantifiersEngine::time"), d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 7f0785340..bcc33327e 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -85,6 +85,7 @@ class EqualityQueryQuantifiersEngine; class QuantifiersEngine { friend class quantifiers::InstantiationEngine; + friend class quantifiers::InstStrategyCbqi; friend class quantifiers::InstStrategyCegqi; friend class quantifiers::ModelEngine; friend class quantifiers::RewriteEngine; @@ -372,7 +373,10 @@ public: /** print solution for synthesis conjectures */ void printSynthSolution( std::ostream& out ); /** get instantiations */ + void getInstantiations( Node q, std::vector< Node >& insts ); void getInstantiations( std::map< Node, std::vector< Node > >& insts ); + /** get instantiated conjunction */ + Node getInstantiatedConjunction( Node q ); /** get unsat core lemmas */ bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas ); bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 634c538e5..a14534efe 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1453,6 +1453,15 @@ void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& ins } } +Node TheoryEngine::getInstantiatedConjunction( Node q ) { + if( d_quantEngine ){ + return d_quantEngine->getInstantiatedConjunction( q ); + }else{ + Assert( false ); + return Node::null(); + } +} + static Node mkExplanation(const std::vector& explanation) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index bb7946dd8..4366f8d3a 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -789,6 +789,12 @@ public: * Get instantiations */ void getInstantiations( std::map< Node, std::vector< Node > >& insts ); + + /** + * Get instantiated conjunction, returns q[t1] ^ ... ^ q[tn] where t1...tn are current set of instantiations for q. + * Can be used for quantifier elimination when satisfiable and q[t1] ^ ... ^ q[tn] |= q + */ + Node getInstantiatedConjunction( Node q ); /** * Forwards an entailment check according to the given theoryOfMode. -- 2.30.2