diff options
-rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 945 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 80 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 64 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 32 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 4 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 |
9 files changed, 667 insertions, 478 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3e4afc0c9..7844cede5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1377,7 +1377,7 @@ void SmtEngine::setDefaults() { } //implied options... - if( options::recurseCbqi() ){ + if( options::recurseCbqi() || options::cbqi2() ){ options::cbqi.set( true ); } if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 3ddd5e157..0fef2aa42 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -31,395 +31,17 @@ using namespace CVC4::theory::quantifiers; using namespace std; namespace CVC4 { - -CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( p ){ - d_sol = NULL; - d_c_inst_match_trie = NULL; -} - -Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { - if( !d_single_inv.isNull() ) { - Assert( d_single_inv.getKind()==FORALL ); - d_single_inv_var.clear(); - d_single_inv_sk.clear(); - for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){ - std::stringstream ss; - ss << "k_" << d_single_inv[0][i]; - Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" ); - d_single_inv_var.push_back( d_single_inv[0][i] ); - d_single_inv_sk.push_back( k ); - d_single_inv_sk_index[k] = i; - } - Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); - inst = TermDb::simpleNegate( inst ); - Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; - return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst ); - }else{ - return Node::null(); - } -} - -void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { - //initialize data - d_sol = new CegConjectureSingleInvSol( qe ); - d_qe = qe; - d_quant = q; - if( options::incrementalSolving() ){ - d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() ); - } - //process - Trace("cegqi-si") << "Initialize cegqi-si for " << q << std::endl; - // conj -> conj* - std::map< Node, std::vector< Node > > children; - // conj X prog -> inv* - std::map< Node, std::map< Node, std::vector< Node > > > prog_invoke; - std::vector< Node > progs; - std::map< Node, std::map< Node, bool > > contains; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - progs.push_back( q[0][i] ); - } - //collect information about conjunctions - bool singleInvocation = false; - if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){ - singleInvocation = true; - //try to phrase as single invocation property - Trace("cegqi-si") << "...success." << std::endl; - std::map< Node, std::vector< Node > > invocations; - std::map< Node, std::map< int, std::vector< Node > > > single_invoke_args; - std::map< Node, std::map< int, std::map< Node, std::vector< Node > > > > single_invoke_args_from; - for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ - for( unsigned j=0; j<it->second.size(); j++ ){ - Node conj = it->second[j]; - Trace("cegqi-si-debug") << "Process child " << conj << " from " << it->first << std::endl; - std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( conj ); - if( itp!=prog_invoke.end() ){ - for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ - if( it2->second.size()>1 ){ - singleInvocation = false; - break; - }else if( it2->second.size()==1 ){ - Node prog = it2->first; - Node inv = it2->second[0]; - Assert( inv[0]==prog ); - invocations[prog].push_back( inv ); - for( unsigned k=1; k<inv.getNumChildren(); k++ ){ - Node arg = inv[k]; - Trace("cegqi-si-debug") << "process : " << arg << " occurs in position " << k-1 << " in invocation " << inv << " of " << prog << " in " << conj << std::endl; - single_invoke_args_from[prog][k-1][arg].push_back( conj ); - if( std::find( single_invoke_args[prog][k-1].begin(), single_invoke_args[prog][k-1].end(), arg )==single_invoke_args[prog][k-1].end() ){ - single_invoke_args[prog][k-1].push_back( arg ); - } - } - } - } - } - } - } - if( singleInvocation ){ - Trace("cegqi-si") << "Property is single invocation with : " << std::endl; - std::vector< Node > pbvs; - std::vector< Node > new_vars; - std::map< Node, std::vector< Node > > new_assumptions; - for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){ - Assert( !it->second.empty() ); - Node prog = it->first; - Node inv = it->second[0]; - std::vector< Node > invc; - invc.push_back( inv.getOperator() ); - invc.push_back( prog ); - std::stringstream ss; - ss << "F_" << prog; - Node pv = NodeManager::currentNM()->mkBoundVar( ss.str(), inv.getType() ); - d_single_inv_map[prog] = pv; - d_single_inv_map_to_prog[pv] = prog; - pbvs.push_back( pv ); - Trace("cegqi-si-debug2") << "Make variable " << pv << " for " << prog << std::endl; - for( unsigned k=1; k<inv.getNumChildren(); k++ ){ - Assert( !single_invoke_args[prog][k-1].empty() ); - if( single_invoke_args[prog][k-1].size()==1 && single_invoke_args[prog][k-1][0].getKind()==BOUND_VARIABLE ){ - invc.push_back( single_invoke_args[prog][k-1][0] ); - }else{ - //introduce fresh variable, assign all - Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" ); - new_vars.push_back( v ); - invc.push_back( v ); - d_single_inv_arg_sk.push_back( v ); - - for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){ - Node arg = single_invoke_args[prog][k-1][i]; - Node asum = NodeManager::currentNM()->mkNode( arg.getType().isBoolean() ? IFF : EQUAL, v, arg ).negate(); - Trace("cegqi-si-debug") << " ..." << arg << " occurs in "; - Trace("cegqi-si-debug") << single_invoke_args_from[prog][k-1][arg].size() << " invocations at position " << (k-1) << " of " << prog << "." << std::endl; - for( unsigned j=0; j<single_invoke_args_from[prog][k-1][arg].size(); j++ ){ - Node conj = single_invoke_args_from[prog][k-1][arg][j]; - Trace("cegqi-si-debug") << " ..." << arg << " occurs in invocation " << inv << " of " << prog << " in " << conj << std::endl; - Trace("cegqi-si-debug") << " ...add assumption " << asum << " to " << conj << std::endl; - if( std::find( new_assumptions[conj].begin(), new_assumptions[conj].end(), asum )==new_assumptions[conj].end() ){ - new_assumptions[conj].push_back( asum ); - } - } - } - } - } - Node sinv = NodeManager::currentNM()->mkNode( APPLY_UF, invc ); - Trace("cegqi-si") << " " << prog << " -> " << sinv << std::endl; - d_single_inv_app_map[prog] = sinv; - } - //construct the single invocation version of the property - Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl; - //std::vector< Node > si_conj; - Assert( !pbvs.empty() ); - Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs ); - for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ - //should hold since we prevent miniscoping - Assert( d_single_inv.isNull() ); - std::vector< Node > conjuncts; - for( unsigned i=0; i<it->second.size(); i++ ){ - Node c = it->second[i]; - std::vector< Node > disj; - //insert new assumptions - disj.insert( disj.end(), new_assumptions[c].begin(), new_assumptions[c].end() ); - //get replaced version - Node cr; - std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( c ); - if( itp!=prog_invoke.end() ){ - std::vector< Node > terms; - std::vector< Node > subs; - for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ - if( !it2->second.empty() ){ - Node prog = it2->first; - Node inv = it2->second[0]; - Assert( it2->second.size()==1 ); - terms.push_back( inv ); - subs.push_back( d_single_inv_map[prog] ); - Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl; - } - } - cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); - }else{ - cr = c; - } - if( cr.getKind()==OR ){ - for( unsigned j=0; j<cr.getNumChildren(); j++ ){ - disj.push_back( cr[j] ); - } - }else{ - disj.push_back( cr ); - } - Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ); - curr = TermDb::simpleNegate( curr ); - Trace("cegqi-si") << " " << curr; - conjuncts.push_back( curr ); - if( !it->first.isNull() ){ - Trace("cegqi-si-debug") << " under " << it->first; - } - Trace("cegqi-si") << std::endl; - } - Assert( !conjuncts.empty() ); - //make the skolems for the existential - if( !it->first.isNull() ){ - std::vector< Node > vars; - std::vector< Node > sks; - for( unsigned j=0; j<it->first.getNumChildren(); j++ ){ - std::stringstream ss; - ss << "a_" << it->first[j]; - Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" ); - vars.push_back( it->first[j] ); - sks.push_back( v ); - } - //substitute conjunctions - for( unsigned i=0; i<conjuncts.size(); i++ ){ - conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); - } - d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() ); - //substitute single invocation applications - for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ - Node n = itam->second; - d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); - } - } - //ensure that this is a ground property - for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ - Node n = itam->second; - //check if all variables are arguments of this - std::vector< Node > n_args; - for( unsigned i=1; i<n.getNumChildren(); i++ ){ - n_args.push_back( n[i] ); - } - for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){ - if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){ - Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl; - //try to do variable elimination on d_single_inv_arg_sk[i] - if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){ - Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl; - d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 ); - i--; - }else{ - singleInvocation = false; - //exit( 57 ); - } - break; - } - } - } - - if( singleInvocation ){ - Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); - d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); - Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; - if( options::eMatching.wasSetByUser() ){ - Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv ); - std::vector< Node > patTerms; - std::vector< Node > exclude; - inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude ); - if( !patTerms.empty() ){ - Trace("cegqi-si-em") << "Triggers : " << std::endl; - for( unsigned i=0; i<patTerms.size(); i++ ){ - Trace("cegqi-si-em") << " " << patTerms[i] << std::endl; - } - } - } - } - } - } - } - if( !singleInvocation ){ - Trace("cegqi-si") << "Property is not single invocation." << std::endl; - if( options::cegqiSingleInvAbort() ){ - Message() << "Property is not single invocation." << std::endl; - exit( 0 ); - } - } -} - -bool CegConjectureSingleInv::doVariableElimination( Node v, std::vector< Node >& conjuncts ) { - //all conjuncts containing v must contain a literal v != s for some s - // if so, do DER on all such conjuncts - TNode s; - for( unsigned i=0; i<conjuncts.size(); i++ ){ - int status = 0; - if( getVariableEliminationTerm( true, true, v, conjuncts[i], s, status ) ){ - Trace("cegqi-si-debug") << "Substitute " << s << " for " << v << " in " << conjuncts[i] << std::endl; - Assert( !s.isNull() ); - conjuncts[i] = conjuncts[i].substitute( v, s ); - }else{ - if( status==1 ){ - Trace("cegqi-si-debug") << "Conjunct " << conjuncts[i] << " contains " << v << " but not in disequality." << std::endl; - return false; - }else{ - Trace("cegqi-si-debug") << "Conjunct does not contain " << v << "." << std::endl; - } - } - } - return true; -} - -bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol, Node v, Node n, TNode& s, int& status ) { - if( hasPol ){ - if( n.getKind()==NOT ){ - return getVariableEliminationTerm( !pol, true, v, n[0], s, status ); - }else if( pol && n.getKind()==EQUAL ){ - for( unsigned r=0; r<2; r++ ){ - if( n[r]==v ){ - status = 1; - Node ss = n[r==0 ? 1 : 0]; - if( s.isNull() ){ - s = ss; - } - return ss==s; - } - } - //did not match, now see if it contains v - }else if( ( n.getKind()==OR && !pol ) || ( n.getKind()==AND && pol ) ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( getVariableEliminationTerm( pol, true, v, n[i], s, status ) ){ - return true; - } - } - return false; - } - } - if( n==v ){ - status = 1; - }else{ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - getVariableEliminationTerm( pol, false, v, n[i], s, status ); - } - } - return false; -} - -bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children, - std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, - std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) { - if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){ - return false; - } - } - }else if( pol && n.getKind()==NOT && n[0].getKind()==FORALL ){ - if( !p.isNull() ){ - //do not allow nested quantifiers - return false; - } - analyzeSygusConjunct( n[0][0], n[0][1], children, prog_invoke, progs, contains, false ); - }else{ - if( pol ){ - n = TermDb::simpleNegate( n ); - } - Trace("cegqi-si") << "Sygus conjunct : " << n << std::endl; - children[p].push_back( n ); - for( unsigned i=0; i<progs.size(); i++ ){ - prog_invoke[n][progs[i]].clear(); - } - bool success = analyzeSygusTerm( n, prog_invoke[n], contains[n] ); - for( unsigned i=0; i<progs.size(); i++ ){ - std::map< Node, std::vector< Node > >::iterator it = prog_invoke[n].find( progs[i] ); - Trace("cegqi-si") << " Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl; - for( unsigned j=0; j<it->second.size(); j++ ){ - Trace("cegqi-si") << " " << it->second[j] << std::endl; - } - } - return success; - } - return true; -} - -bool CegConjectureSingleInv::analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains ) { - if( n.getNumChildren()>0 ){ - if( n.getKind()==FORALL ){ - //do not allow nested quantifiers - return false; - } - //look at first argument in evaluator - Node p = n[0]; - std::map< Node, std::vector< Node > >::iterator it = prog_invoke.find( p ); - if( it!=prog_invoke.end() ){ - if( std::find( it->second.begin(), it->second.end(), n )==it->second.end() ){ - it->second.push_back( n ); - } - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( !analyzeSygusTerm( n[i], prog_invoke, contains ) ){ - return false; - } - } - }else{ - //record this conjunct contains n - contains[n] = true; - } - return true; -} - - - -void CegConjectureSingleInv::computeProgVars( Node n ){ + +CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ) : d_qe( qe ), d_out( out ){ + +} + +void CegInstantiator::computeProgVars( Node n ){ if( d_prog_var.find( n )==d_prog_var.end() ){ d_prog_var[n].clear(); - if( std::find( d_single_inv_sk.begin(), d_single_inv_sk.end(), n )!=d_single_inv_sk.end() ){ + if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){ d_prog_var[n][n] = true; - }else if( n.getKind()==SKOLEM && std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )==d_single_inv_arg_sk.end() ){ + }else if( !d_out->isEligibleForInstantiation( n ) ){ d_inelig[n] = true; return; } @@ -436,19 +58,19 @@ void CegConjectureSingleInv::computeProgVars( Node n ){ } } -bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, std::vector< Node >& lems, unsigned effort ){ - if( i==d_single_inv_sk.size() ){ - return addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, 0, lems ); +bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, + unsigned i, unsigned effort ){ + if( i==d_vars.size() ){ + return addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, 0 ); }else{ eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); std::map< int, std::map< Node, std::map< Node, bool > > > subs_proc; - Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; - Node pv = d_single_inv_sk[i]; + //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]]; + Node pv = d_vars[i]; TypeNode pvtn = pv.getType(); - if( (i+1)<d_single_inv_arg_sk.size() || effort!=2 ){ + if( (i+1)<d_vars.size() || effort!=2 ){ //[1] easy case : pv is in the equivalence class as another term not containing pv if( ee->hasTerm( pv ) ){ Node pvr = ee->getRepresentative( pv ); @@ -478,7 +100,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v if( proc ){ //try the substitution subs_proc[0][ns][pv_coeff] = true; - if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, has_coeff, subs_typ, i, lems, effort ) ){ + if( addInstantiationInc( ns, pv, pv_coeff, 0, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){ return true; } } @@ -558,7 +180,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v } if( subs_proc[0][veq[1]].find( veq_c )==subs_proc[0][veq[1]].end() ){ subs_proc[0][veq[1]][veq_c] = true; - if( addInstantiationInc( veq[1], pv, veq_c, 0, subs, vars, coeff, has_coeff, subs_typ, i, lems, effort ) ){ + if( addInstantiationInc( veq[1], pv, veq_c, 0, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){ return true; } } @@ -670,7 +292,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v } if( subs_proc[uires][uval].find( veq_c )==subs_proc[uires][uval].end() ){ subs_proc[uires][uval][veq_c] = true; - if( addInstantiationInc( uval, pv, veq_c, uires, subs, vars, coeff, has_coeff, subs_typ, i, lems, effort ) ){ + if( addInstantiationInc( uval, pv, veq_c, uires, subs, vars, coeff, has_coeff, subs_typ, i, effort ) ){ return true; } } @@ -690,7 +312,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v Node mv = d_qe->getModel()->getValue( pv ); Node pv_coeff_m; Trace("cegqi-si-inst-debug") << i << "...try model value " << mv << std::endl; - return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, lems, 1 ); + return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, 1 ); }else{ return false; } @@ -698,9 +320,9 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v } -bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, std::vector< Node >& lems, unsigned effort ) { +bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, + unsigned i, unsigned effort ) { //must ensure variables have been computed for n computeProgVars( n ); //substitute into previous substitutions, when applicable @@ -763,7 +385,7 @@ bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff Trace("cegqi-si-inst-debug") << pv_coeff << "*"; } Trace("cegqi-si-inst-debug") << pv << " -> " << n << std::endl; - success = addInstantiation( subs, vars, coeff, has_coeff, subs_typ, i+1, lems, effort ); + success = addInstantiation( subs, vars, coeff, has_coeff, subs_typ, i+1, effort ); if( !success ){ subs.pop_back(); vars.pop_back(); @@ -791,11 +413,10 @@ bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff } } -bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned j, std::vector< Node >& lems ) { +bool CegInstantiator::addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, unsigned j ) { if( j==has_coeff.size() ){ - return addInstantiation( subs, vars, subs_typ, lems ); + return addInstantiation( subs, vars, subs_typ ); }else{ Assert( std::find( vars.begin(), vars.end(), has_coeff[j] )!=vars.end() ); unsigned index = std::find( vars.begin(), vars.end(), has_coeff[j] )-vars.begin(); @@ -836,7 +457,7 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s } } Trace("cegqi-si-inst-debug") << "...normalize integers : " << subs[index] << std::endl; - if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1, lems ) ){ + if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){ return true; } //equalities are both upper and lower bounds @@ -850,7 +471,7 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s NodeManager::currentNM()->mkConst( Rational( 0 ) ), NodeManager::currentNM()->mkConst( Rational( 1 ) ) ) ); - if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1, lems ) ){ + if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){ return true; } } @@ -862,7 +483,7 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s subs[index] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / coeff[index].getConst<Rational>() ), subs[index] ); subs[index] = Rewriter::rewrite( subs[index] ); Trace("cegqi-si-inst-debug") << "...success, reals : " << subs[index] << std::endl; - if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1, lems ) ){ + if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1 ) ){ return true; } }else{ @@ -874,7 +495,7 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s } } -bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ, std::vector< Node >& lems ) { +bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ) { // do delta rationals std::map< int, Node > prev; for( unsigned i=0; i<subs.size(); i++ ){ @@ -888,46 +509,19 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta ); } } - std::stringstream siss; - siss << " * single invocation: " << std::endl; - for( unsigned j=0; j<vars.size(); j++ ){ - Node v = d_single_inv_map_to_prog[d_single_inv[0][j]]; - siss << " * " << v; - siss << " (" << vars[j] << ")"; - siss << " -> " << ( subs_typ[j]==9 ? "M:" : "") << subs[j] << std::endl; - } //check if we have already added this instantiation - bool alreadyExists; - if( options::incrementalSolving() ){ - alreadyExists = !d_c_inst_match_trie->addInstMatch( d_qe, d_single_inv, subs, d_qe->getUserContext() ); - }else{ - alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs ); - } - Trace("cegqi-si-inst-debug") << siss.str(); - Trace("cegqi-si-inst-debug") << " * success = " << !alreadyExists << std::endl; - if( alreadyExists ){ + bool success = d_out->addInstantiation( subs, subs_typ ); + if( !success ){ //revert the substitution for( std::map< int, Node >::iterator it = prev.begin(); it != prev.end(); ++it ){ subs[it->first] = it->second; } - return false; - }else{ - Trace("cegqi-engine") << siss.str() << std::endl; - Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); - lem = Rewriter::rewrite( lem ); - Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; - if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){ - lems.push_back( lem ); - d_lemmas_produced.push_back( lem ); - d_inst.push_back( std::vector< Node >() ); - d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() ); - } - return true; } + return success; } -Node CegConjectureSingleInv::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, +Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff ) { Assert( d_prog_var.find( n )!=d_prog_var.end() ); Assert( n==Rewriter::rewrite( n ) ); @@ -1009,20 +603,467 @@ Node CegConjectureSingleInv::applySubstitution( Node n, std::vector< Node >& sub } } -void CegConjectureSingleInv::check( std::vector< Node >& lems ) { +void CegInstantiator::check() { + for( unsigned r=0; r<2; r++ ){ + std::vector< Node > subs; + std::vector< Node > vars; + std::vector< Node > coeff; + std::vector< Node > has_coeff; + std::vector< int > subs_typ; + //try to add an instantiation + if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){ + return; + } + } + Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; +} + + +bool CegqiOutputSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) { + return d_out->addInstantiation( subs, subs_typ ); +} + +bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) { + return d_out->isEligibleForInstantiation( n ); +} + + + +CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( p ){ + d_sol = NULL; + d_c_inst_match_trie = NULL; + d_cinst = NULL; +} + +Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { if( !d_single_inv.isNull() ) { - for( unsigned r=0; r<2; r++ ){ - std::vector< Node > subs; - std::vector< Node > vars; - std::vector< Node > coeff; - std::vector< Node > has_coeff; - std::vector< int > subs_typ; - //try to add an instantiation - if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, lems, r==0 ? 0 : 2 ) ){ - return; + Assert( d_single_inv.getKind()==FORALL ); + d_single_inv_var.clear(); + d_single_inv_sk.clear(); + for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){ + std::stringstream ss; + ss << "k_" << d_single_inv[0][i]; + Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" ); + d_single_inv_var.push_back( d_single_inv[0][i] ); + d_single_inv_sk.push_back( k ); + d_single_inv_sk_index[k] = i; + } + Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); + inst = TermDb::simpleNegate( inst ); + Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; + + //initialize the instantiator for this + CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this ); + d_cinst = new CegInstantiator( d_qe, cosi ); + d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); + + return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst ); + }else{ + return Node::null(); + } +} + +void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { + //initialize data + d_sol = new CegConjectureSingleInvSol( qe ); + d_qe = qe; + d_quant = q; + if( options::incrementalSolving() ){ + d_c_inst_match_trie = new inst::CDInstMatchTrie( qe->getUserContext() ); + } + //process + Trace("cegqi-si") << "Initialize cegqi-si for " << q << std::endl; + // conj -> conj* + std::map< Node, std::vector< Node > > children; + // conj X prog -> inv* + std::map< Node, std::map< Node, std::vector< Node > > > prog_invoke; + std::vector< Node > progs; + std::map< Node, std::map< Node, bool > > contains; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + progs.push_back( q[0][i] ); + } + //collect information about conjunctions + bool singleInvocation = false; + if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){ + singleInvocation = true; + //try to phrase as single invocation property + Trace("cegqi-si") << "...success." << std::endl; + std::map< Node, std::vector< Node > > invocations; + std::map< Node, std::map< int, std::vector< Node > > > single_invoke_args; + std::map< Node, std::map< int, std::map< Node, std::vector< Node > > > > single_invoke_args_from; + for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ + for( unsigned j=0; j<it->second.size(); j++ ){ + Node conj = it->second[j]; + Trace("cegqi-si-debug") << "Process child " << conj << " from " << it->first << std::endl; + std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( conj ); + if( itp!=prog_invoke.end() ){ + for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ + if( it2->second.size()>1 ){ + singleInvocation = false; + break; + }else if( it2->second.size()==1 ){ + Node prog = it2->first; + Node inv = it2->second[0]; + Assert( inv[0]==prog ); + invocations[prog].push_back( inv ); + for( unsigned k=1; k<inv.getNumChildren(); k++ ){ + Node arg = inv[k]; + Trace("cegqi-si-debug") << "process : " << arg << " occurs in position " << k-1 << " in invocation " << inv << " of " << prog << " in " << conj << std::endl; + single_invoke_args_from[prog][k-1][arg].push_back( conj ); + if( std::find( single_invoke_args[prog][k-1].begin(), single_invoke_args[prog][k-1].end(), arg )==single_invoke_args[prog][k-1].end() ){ + single_invoke_args[prog][k-1].push_back( arg ); + } + } + } + } + } + } + } + if( singleInvocation ){ + Trace("cegqi-si") << "Property is single invocation with : " << std::endl; + std::vector< Node > pbvs; + std::vector< Node > new_vars; + std::map< Node, std::vector< Node > > new_assumptions; + for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){ + Assert( !it->second.empty() ); + Node prog = it->first; + Node inv = it->second[0]; + std::vector< Node > invc; + invc.push_back( inv.getOperator() ); + invc.push_back( prog ); + std::stringstream ss; + ss << "F_" << prog; + Node pv = NodeManager::currentNM()->mkBoundVar( ss.str(), inv.getType() ); + d_single_inv_map[prog] = pv; + d_single_inv_map_to_prog[pv] = prog; + pbvs.push_back( pv ); + Trace("cegqi-si-debug2") << "Make variable " << pv << " for " << prog << std::endl; + for( unsigned k=1; k<inv.getNumChildren(); k++ ){ + Assert( !single_invoke_args[prog][k-1].empty() ); + if( single_invoke_args[prog][k-1].size()==1 && single_invoke_args[prog][k-1][0].getKind()==BOUND_VARIABLE ){ + invc.push_back( single_invoke_args[prog][k-1][0] ); + }else{ + //introduce fresh variable, assign all + Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" ); + new_vars.push_back( v ); + invc.push_back( v ); + d_single_inv_arg_sk.push_back( v ); + + for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){ + Node arg = single_invoke_args[prog][k-1][i]; + Node asum = NodeManager::currentNM()->mkNode( arg.getType().isBoolean() ? IFF : EQUAL, v, arg ).negate(); + Trace("cegqi-si-debug") << " ..." << arg << " occurs in "; + Trace("cegqi-si-debug") << single_invoke_args_from[prog][k-1][arg].size() << " invocations at position " << (k-1) << " of " << prog << "." << std::endl; + for( unsigned j=0; j<single_invoke_args_from[prog][k-1][arg].size(); j++ ){ + Node conj = single_invoke_args_from[prog][k-1][arg][j]; + Trace("cegqi-si-debug") << " ..." << arg << " occurs in invocation " << inv << " of " << prog << " in " << conj << std::endl; + Trace("cegqi-si-debug") << " ...add assumption " << asum << " to " << conj << std::endl; + if( std::find( new_assumptions[conj].begin(), new_assumptions[conj].end(), asum )==new_assumptions[conj].end() ){ + new_assumptions[conj].push_back( asum ); + } + } + } + } + } + Node sinv = NodeManager::currentNM()->mkNode( APPLY_UF, invc ); + Trace("cegqi-si") << " " << prog << " -> " << sinv << std::endl; + d_single_inv_app_map[prog] = sinv; + } + //construct the single invocation version of the property + Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl; + //std::vector< Node > si_conj; + Assert( !pbvs.empty() ); + Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs ); + for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ + //should hold since we prevent miniscoping + Assert( d_single_inv.isNull() ); + std::vector< Node > conjuncts; + for( unsigned i=0; i<it->second.size(); i++ ){ + Node c = it->second[i]; + std::vector< Node > disj; + //insert new assumptions + disj.insert( disj.end(), new_assumptions[c].begin(), new_assumptions[c].end() ); + //get replaced version + Node cr; + std::map< Node, std::map< Node, std::vector< Node > > >::iterator itp = prog_invoke.find( c ); + if( itp!=prog_invoke.end() ){ + std::vector< Node > terms; + std::vector< Node > subs; + for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ + if( !it2->second.empty() ){ + Node prog = it2->first; + Node inv = it2->second[0]; + Assert( it2->second.size()==1 ); + terms.push_back( inv ); + subs.push_back( d_single_inv_map[prog] ); + Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl; + } + } + cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + }else{ + cr = c; + } + if( cr.getKind()==OR ){ + for( unsigned j=0; j<cr.getNumChildren(); j++ ){ + disj.push_back( cr[j] ); + } + }else{ + disj.push_back( cr ); + } + Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ); + curr = TermDb::simpleNegate( curr ); + Trace("cegqi-si") << " " << curr; + conjuncts.push_back( curr ); + if( !it->first.isNull() ){ + Trace("cegqi-si-debug") << " under " << it->first; + } + Trace("cegqi-si") << std::endl; + } + Assert( !conjuncts.empty() ); + //make the skolems for the existential + if( !it->first.isNull() ){ + std::vector< Node > vars; + std::vector< Node > sks; + for( unsigned j=0; j<it->first.getNumChildren(); j++ ){ + std::stringstream ss; + ss << "a_" << it->first[j]; + Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" ); + vars.push_back( it->first[j] ); + sks.push_back( v ); + } + //substitute conjunctions + for( unsigned i=0; i<conjuncts.size(); i++ ){ + conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + } + d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() ); + //substitute single invocation applications + for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ + Node n = itam->second; + d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + } + } + //ensure that this is a ground property + for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ + Node n = itam->second; + //check if all variables are arguments of this + std::vector< Node > n_args; + for( unsigned i=1; i<n.getNumChildren(); i++ ){ + n_args.push_back( n[i] ); + } + for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){ + if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){ + Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl; + //try to do variable elimination on d_single_inv_arg_sk[i] + if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){ + Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl; + d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 ); + i--; + }else{ + singleInvocation = false; + //exit( 57 ); + } + break; + } + } + } + + if( singleInvocation ){ + Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); + d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); + Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; + if( options::eMatching.wasSetByUser() ){ + Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv ); + std::vector< Node > patTerms; + std::vector< Node > exclude; + inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude ); + if( !patTerms.empty() ){ + Trace("cegqi-si-em") << "Triggers : " << std::endl; + for( unsigned i=0; i<patTerms.size(); i++ ){ + Trace("cegqi-si-em") << " " << patTerms[i] << std::endl; + } + } + } + } + } + } + } + if( !singleInvocation ){ + Trace("cegqi-si") << "Property is not single invocation." << std::endl; + if( options::cegqiSingleInvAbort() ){ + Message() << "Property is not single invocation." << std::endl; + exit( 0 ); + } + } +} + +bool CegConjectureSingleInv::doVariableElimination( Node v, std::vector< Node >& conjuncts ) { + //all conjuncts containing v must contain a literal v != s for some s + // if so, do DER on all such conjuncts + TNode s; + for( unsigned i=0; i<conjuncts.size(); i++ ){ + int status = 0; + if( getVariableEliminationTerm( true, true, v, conjuncts[i], s, status ) ){ + Trace("cegqi-si-debug") << "Substitute " << s << " for " << v << " in " << conjuncts[i] << std::endl; + Assert( !s.isNull() ); + conjuncts[i] = conjuncts[i].substitute( v, s ); + }else{ + if( status==1 ){ + Trace("cegqi-si-debug") << "Conjunct " << conjuncts[i] << " contains " << v << " but not in disequality." << std::endl; + return false; + }else{ + Trace("cegqi-si-debug") << "Conjunct does not contain " << v << "." << std::endl; + } + } + } + return true; +} + +bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol, Node v, Node n, TNode& s, int& status ) { + if( hasPol ){ + if( n.getKind()==NOT ){ + return getVariableEliminationTerm( !pol, true, v, n[0], s, status ); + }else if( pol && n.getKind()==EQUAL ){ + for( unsigned r=0; r<2; r++ ){ + if( n[r]==v ){ + status = 1; + Node ss = n[r==0 ? 1 : 0]; + if( s.isNull() ){ + s = ss; + } + return ss==s; + } + } + //did not match, now see if it contains v + }else if( ( n.getKind()==OR && !pol ) || ( n.getKind()==AND && pol ) ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( getVariableEliminationTerm( pol, true, v, n[i], s, status ) ){ + return true; + } + } + return false; + } + } + if( n==v ){ + status = 1; + }else{ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + getVariableEliminationTerm( pol, false, v, n[i], s, status ); + } + } + return false; +} + +bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children, + std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, + std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) { + if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){ + return false; + } + } + }else if( pol && n.getKind()==NOT && n[0].getKind()==FORALL ){ + if( !p.isNull() ){ + //do not allow nested quantifiers + return false; + } + analyzeSygusConjunct( n[0][0], n[0][1], children, prog_invoke, progs, contains, false ); + }else{ + if( pol ){ + n = TermDb::simpleNegate( n ); + } + Trace("cegqi-si") << "Sygus conjunct : " << n << std::endl; + children[p].push_back( n ); + for( unsigned i=0; i<progs.size(); i++ ){ + prog_invoke[n][progs[i]].clear(); + } + bool success = analyzeSygusTerm( n, prog_invoke[n], contains[n] ); + for( unsigned i=0; i<progs.size(); i++ ){ + std::map< Node, std::vector< Node > >::iterator it = prog_invoke[n].find( progs[i] ); + Trace("cegqi-si") << " Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl; + for( unsigned j=0; j<it->second.size(); j++ ){ + Trace("cegqi-si") << " " << it->second[j] << std::endl; + } + } + return success; + } + return true; +} + +bool CegConjectureSingleInv::analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains ) { + if( n.getNumChildren()>0 ){ + if( n.getKind()==FORALL ){ + //do not allow nested quantifiers + return false; + } + //look at first argument in evaluator + Node p = n[0]; + std::map< Node, std::vector< Node > >::iterator it = prog_invoke.find( p ); + if( it!=prog_invoke.end() ){ + if( std::find( it->second.begin(), it->second.end(), n )==it->second.end() ){ + it->second.push_back( n ); + } + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( !analyzeSygusTerm( n[i], prog_invoke, contains ) ){ + return false; } } - Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + }else{ + //record this conjunct contains n + contains[n] = true; + } + return true; +} + +bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ){ + std::stringstream siss; + if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){ + siss << " * single invocation: " << std::endl; + for( unsigned j=0; j<d_single_inv_sk.size(); j++ ){ + Node v = d_single_inv_map_to_prog[d_single_inv[0][j]]; + siss << " * " << v; + siss << " (" << d_single_inv_sk[j] << ")"; + siss << " -> " << ( subs_typ[j]==9 ? "M:" : "") << subs[j] << std::endl; + } + } + bool alreadyExists; + if( options::incrementalSolving() ){ + alreadyExists = !d_c_inst_match_trie->addInstMatch( d_qe, d_single_inv, subs, d_qe->getUserContext() ); + }else{ + alreadyExists = !d_inst_match_trie.addInstMatch( d_qe, d_single_inv, subs ); + } + Trace("cegqi-si-inst-debug") << siss.str(); + Trace("cegqi-si-inst-debug") << " * success = " << !alreadyExists << std::endl; + if( alreadyExists ){ + return false; + }else{ + Trace("cegqi-engine") << siss.str() << std::endl; + Node lem = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), subs.begin(), subs.end() ); + lem = Rewriter::rewrite( lem ); + Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; + if( std::find( d_lemmas_produced.begin(), d_lemmas_produced.end(), lem )==d_lemmas_produced.end() ){ + d_curr_lemmas.push_back( lem ); + d_lemmas_produced.push_back( lem ); + d_inst.push_back( std::vector< Node >() ); + d_inst.back().insert( d_inst.back().end(), subs.begin(), subs.end() ); + } + return true; + } +} + +bool CegConjectureSingleInv::isEligibleForInstantiation( Node n ) { + return n.getKind()!=SKOLEM || std::find( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), n )!=d_single_inv_arg_sk.end(); +} + +void CegConjectureSingleInv::check( std::vector< Node >& lems ) { + if( !d_single_inv.isNull() ) { + Assert( d_cinst!=NULL ); + d_curr_lemmas.clear(); + //call check for instantiator + d_cinst->check(); + //add lemmas + lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() ); } } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 3bc870d78..9e65b0c24 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -28,12 +28,68 @@ namespace quantifiers { class CegConjecture; +class CegqiOutput +{ +public: + virtual bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) = 0; + virtual bool isEligibleForInstantiation( Node n ) = 0; +}; + +class CegInstantiator +{ +private: + QuantifiersEngine * d_qe; + CegqiOutput * d_out; + //program variable contains cache + std::map< Node, std::map< Node, bool > > d_prog_var; + std::map< Node, bool > d_inelig; +private: + Node d_n_delta; + //for adding instantiations during check + void computeProgVars( Node n ); + // effort=0 : do not use model value, 1: use model value, 2: one must use model value + bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, + unsigned i, unsigned effort ); + bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, + unsigned i, unsigned effort ); + bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, + unsigned j ); + bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ ); + Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, + std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true ); +public: + CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ); + //the CE variables + std::vector< Node > d_vars; + void check(); +}; + + +class CegConjectureSingleInv; + +class CegqiOutputSingleInv : public CegqiOutput +{ +public: + CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){} + CegConjectureSingleInv * d_out; + bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); + bool isEligibleForInstantiation( Node n ); +}; + + + class CegConjectureSingleInv { + friend class CegqiOutputSingleInv; private: QuantifiersEngine * d_qe; CegConjecture * d_parent; CegConjectureSingleInvSol * d_sol; + //the instantiator + CegInstantiator * d_cinst; //for recognizing when conjecture is single invocation bool analyzeSygusConjunct( Node n, Node p, std::map< Node, std::vector< Node > >& children, std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, @@ -67,26 +123,12 @@ private: Node d_orig_solution; Node d_solution; Node d_sygus_solution; - //program variable contains cache - std::map< Node, std::map< Node, bool > > d_prog_var; - std::map< Node, bool > d_inelig; private: - Node d_n_delta; - //for adding instantiations during check - void computeProgVars( Node n ); - // effort=0 : do not use model value, 1: use model value, 2: one must use model value - bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, std::vector< Node >& lems, unsigned effort ); - bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int styp, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned i, std::vector< Node >& lems, unsigned effort ); - bool addInstantiationCoeff( std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, std::vector< int >& subs_typ, - unsigned j, std::vector< Node >& lems ); - bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ, std::vector< Node >& lems ); - Node applySubstitution( Node n, std::vector< Node >& subs, std::vector< Node >& vars, - std::vector< Node >& coeff, std::vector< Node >& has_coeff, Node& pv_coeff, bool try_coeff = true ); + std::vector< Node > d_curr_lemmas; + //add instantiation + bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); + //is eligible for instantiation + bool isEligibleForInstantiation( Node n ); public: CegConjectureSingleInv( CegConjecture * p ); // original conjecture diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index c205a280e..fe992b619 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -346,3 +346,67 @@ Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){ Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta ); return mkRationalNode(qmodel); } + + + +bool CegqiOutputInstStrategy::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) { + return d_out->addInstantiation( subs, subs_typ ); +} + +bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) { + return d_out->isEligibleForInstantiation( n ); +} + + +InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( qe ) { + d_out = new CegqiOutputInstStrategy( this ); +} + +void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { + +} + +int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { + if( e<2 ){ + return STATUS_UNFINISHED; + }else if( e==2 ){ + CegInstantiator * cinst; + std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f ); + if( it==d_cinst.end() ){ + cinst = new CegInstantiator( d_quantEngine, d_out ); + for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ + cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) ); + } + d_cinst[f] = cinst; + }else{ + cinst = it->second; + } + d_curr_quant = f; + cinst->check(); + d_curr_quant = Node::null(); + + return STATUS_UNKNOWN; + } +} + +bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) { + Assert( !d_curr_quant.isNull() ); + return d_quantEngine->addInstantiation( d_curr_quant, subs, false ); +} + +bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { + return true; +} + + + + + + + + + + + + + diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 72ab5d247..e139d0b6f 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -22,6 +22,7 @@ #include "theory/arith/arithvar.h" #include "util/statistics_registry.h" +#include "theory/quantifiers/ce_guided_single_inv.h" namespace CVC4 { namespace theory { @@ -80,6 +81,37 @@ public: }; +//generalized counterexample guided quantifier instantiation + +class InstStrategyCegqi; + +class CegqiOutputInstStrategy : public CegqiOutput +{ +public: + CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){} + InstStrategyCegqi * d_out; + bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); + bool isEligibleForInstantiation( Node n ); +}; + +class InstStrategyCegqi : public InstStrategy { +private: + CegqiOutputInstStrategy * d_out; + std::map< Node, CegInstantiator * > d_cinst; + Node d_curr_quant; + /** process functions */ + void processResetInstantiationRound( Theory::Effort effort ); + int process( Node f, Theory::Effort effort, int e ); +public: + InstStrategyCegqi( QuantifiersEngine * qe ); + ~InstStrategyCegqi(){} + + bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ); + bool isEligibleForInstantiation( Node n ); + /** identify */ + std::string identify() const { return std::string("Cegqi"); } +}; + } } } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 52139a0b8..9c3035c85 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -31,7 +31,7 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst; InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) : -QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_setIncomplete( setIncomplete ){ +QuantifiersModule( qe ), d_isup(NULL), d_i_ag(NULL), d_i_lte(NULL), d_i_fs(NULL), d_i_splx(NULL), d_i_cegqi( NULL ), d_setIncomplete( setIncomplete ){ } @@ -41,6 +41,7 @@ InstantiationEngine::~InstantiationEngine() { delete d_i_lte; delete d_i_fs; delete d_i_splx; + delete d_i_cegqi; } void InstantiationEngine::finishInit(){ @@ -72,8 +73,14 @@ void InstantiationEngine::finishInit(){ //counterexample-based quantifier instantiation if( options::cbqi() ){ - d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ); - d_instStrategies.push_back( d_i_splx ); + if( !options::cbqi2() || options::cbqi.wasSetByUser() ){ + d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ); + d_instStrategies.push_back( d_i_splx ); + } + if( options::cbqi2() ){ + d_i_cegqi = new InstStrategyCegqi( d_quantEngine ); + d_instStrategies.push_back( d_i_cegqi ); + } } } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index c69136933..8a733ac1d 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -29,6 +29,7 @@ class InstStrategyAutoGenTriggers; class InstStrategyLocalTheoryExt; class InstStrategyFreeVariable; class InstStrategySimplex; +class InstStrategyCegqi; /** instantiation strategy class */ class InstStrategy { @@ -68,6 +69,8 @@ private: InstStrategyFreeVariable * d_i_fs; /** simplex (cbqi) */ InstStrategySimplex * d_i_splx; + /** generic cegqi */ + InstStrategyCegqi * d_i_cegqi; private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; /** whether the instantiation engine should set incomplete if it cannot answer SAT */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index a7440639b..62790432d 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -220,8 +220,10 @@ option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true generalize based on content in global search space narrowing # older implementation -option cbqi --enable-cbqi bool :read-write :default false +option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation +option cbqi2 --cbqi2 bool :read-write :default false + turns on new implementation of counterexample-based quantifier instantiation option recurseCbqi --cbqi-recurse bool :default false turns on recursive counterexample-based quantifier instantiation diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a475a8912..888cdbce0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -899,11 +899,9 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ // doing literal-based matching (consider polarity of literals) for( int i=0; i<(int)nodes.size(); i++ ){ Node prev = nodes[i]; - bool nodeChanged = false; if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){ bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] ); nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) ); - nodeChanged = true; } //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){ // Node req = qe->getPhaseReqEquality( f, trNodes[i] ); |