diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 1116 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 92 | ||||
-rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 89 | ||||
-rw-r--r-- | src/theory/quantifiers/fun_def_process.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 112 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 36 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 20 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 32 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 33 |
11 files changed, 959 insertions, 584 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 3ddd5e157..7d1c06b8e 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -32,394 +32,18 @@ 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 ); - } - } +CegInstantiator::CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out ) : d_qe( qe ), d_out( out ){ + d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); + d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + d_true = NodeManager::currentNM()->mkConst( true ); } -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 ){ +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; } @@ -429,26 +53,32 @@ void CegConjectureSingleInv::computeProgVars( Node n ){ d_inelig[n] = true; return; } + if( d_has_delta.find( n[i] )!=d_has_delta.end() ){ + d_has_delta[n] = true; + } for( std::map< Node, bool >::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){ d_prog_var[n][it->first] = true; } } + if( n==d_n_delta ){ + d_has_delta[n] = true; + } } } -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 ); @@ -456,7 +86,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v while( !eqc_i.isFinished() ){ Node n = *eqc_i; if( n!=pv ){ - Trace("cegqi-si-inst-debug") << i << "...try based on equal term " << n << std::endl; + Trace("cegqi-si-inst-debug") << "[1] " << i << "...try based on equal term " << n << std::endl; //compute d_subs_fv, which program variables are contained in n computeProgVars( n ); //must be an eligible term @@ -475,10 +105,16 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v ns = n; proc = true; } + if( d_has_delta.find( ns )!=d_has_delta.end() ){ + //also must set delta to zero + ns = ns.substitute( (TNode)d_n_delta, (TNode)d_zero ); + ns = Rewriter::rewrite( ns ); + computeProgVars( ns ); + } 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; } } @@ -487,7 +123,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v ++eqc_i; } } - + //[2] : we can solve an equality for pv ///iterate over equivalence classes to find cases where we can solve for the variable if( pvtn.isInteger() || pvtn.isReal() ){ @@ -520,7 +156,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v for( unsigned j=0; j<lhs.size(); j++ ){ //if this term or the another has pv in it, try to solve for it if( hasVar || lhs_v[j] ){ - Trace("cegqi-si-inst-debug") << i << "...try based on equality " << lhs[j] << " " << ns << std::endl; + Trace("cegqi-si-inst-debug") << "[2] " << i << "...try based on equality " << lhs[j] << " " << ns << std::endl; Node eq_lhs = lhs[j]; Node eq_rhs = ns; //make the same coefficient @@ -541,6 +177,9 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; std::map< Node, Node > msum; if( QuantArith::getMonomialSumLit( eq, msum ) ){ + if( !d_n_delta.isNull() ){ + msum.erase( d_n_delta ); + } if( Trace.isOn("cegqi-si-inst-debug") ){ Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); @@ -558,7 +197,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; } } @@ -577,7 +216,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v ++eqcs_i; } } - + //[3] directly look at assertions TheoryId tid = Theory::theoryOf( pv ); Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); @@ -589,34 +228,42 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v bool pol = lit.getKind()!=NOT; if( tid==THEORY_ARITH ){ if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){ - Assert( atom[1].isConst() ); - computeProgVars( atom[0] ); + Assert( atom.getKind()!=GEQ || atom[1].isConst() ); + Node atom_lhs; + Node atom_rhs; + if( atom.getKind()==GEQ ){ + atom_lhs = atom[0]; + atom_rhs = atom[1]; + }else{ + atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); + atom_lhs = Rewriter::rewrite( atom_lhs ); + atom_rhs = d_zero; + } + + computeProgVars( atom_lhs ); //must be an eligible term - if( d_inelig.find( atom[0] )==d_inelig.end() ){ + if( d_inelig.find( atom_lhs )==d_inelig.end() ){ //apply substitution to LHS of atom - Node atom_lhs; - Node atom_rhs; - if( !d_prog_var[atom[0]].empty() ){ + if( !d_prog_var[atom_lhs].empty() ){ Node atom_lhs_coeff; - atom_lhs = applySubstitution( atom[0], subs, vars, coeff, has_coeff, atom_lhs_coeff ); + atom_lhs = applySubstitution( atom_lhs, subs, vars, coeff, has_coeff, atom_lhs_coeff ); if( !atom_lhs.isNull() ){ computeProgVars( atom_lhs ); - atom_rhs = atom[1]; if( !atom_lhs_coeff.isNull() ){ atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_coeff, atom_rhs ) ); } } - }else{ - atom_lhs = atom[0]; - atom_rhs = atom[1]; } //if it contains pv if( !atom_lhs.isNull() && d_prog_var[atom_lhs].find( pv )!=d_prog_var[atom_lhs].end() ){ Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); - Trace("cegqi-si-inst-debug") << "From assertion : " << atom << ", pol = " << pol << std::endl; - Trace("cegqi-si-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; + Trace("cegqi-si-inst-debug") << "[3] From assertion : " << atom << ", pol = " << pol << std::endl; + Trace("cegqi-si-inst-debug") << " substituted : " << satom << ", pol = " << pol << std::endl; std::map< Node, Node > msum; if( QuantArith::getMonomialSumLit( satom, msum ) ){ + if( !d_n_delta.isNull() ){ + msum.erase( d_n_delta ); + } if( Trace.isOn("cegqi-si-inst-debug") ){ Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); @@ -670,9 +317,11 @@ 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; } + }else{ + Trace("cegqi-si-inst-debug") << "...already processed." << std::endl; } } } @@ -684,13 +333,13 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v } } } - - //[4] resort to using value in model + + //[4] resort to using value in model if( effort>0 ){ 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 ); + Trace("cegqi-si-inst-debug") << i << "[4] ...try model value " << mv << std::endl; + return addInstantiationInc( mv, pv, pv_coeff_m, 9, subs, vars, coeff, has_coeff, subs_typ, i, 1 ); }else{ return false; } @@ -698,9 +347,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 @@ -714,7 +363,7 @@ bool CegConjectureSingleInv::addInstantiationInc( Node n, Node pv, Node pv_coeff a_coeff.push_back( pv_coeff ); a_has_coeff.push_back( pv ); } - + bool success = true; std::map< int, Node > prev_subs; std::map< int, Node > prev_coeff; @@ -763,7 +412,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 +440,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(); @@ -825,32 +473,31 @@ bool CegConjectureSingleInv::addInstantiationCoeff( std::vector< Node >& subs, s if( !veq_c.isNull() ){ subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION, veq[1], veq_c ); if( subs_typ[index]>=1 && subs_typ[index]<=2 ){ - subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], - NodeManager::currentNM()->mkNode( ITE, - NodeManager::currentNM()->mkNode( EQUAL, - NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), - NodeManager::currentNM()->mkConst( Rational( 0 ) ) ), - NodeManager::currentNM()->mkConst( Rational( 0 ) ), - NodeManager::currentNM()->mkConst( Rational( 1 ) ) ) + subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], + NodeManager::currentNM()->mkNode( ITE, + NodeManager::currentNM()->mkNode( EQUAL, + NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), + d_zero ), + d_zero, d_one ) ); } } 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 /* if( subs_typ[index]==0 && !veq_c.isNull() ){ - subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], - NodeManager::currentNM()->mkNode( ITE, - NodeManager::currentNM()->mkNode( EQUAL, - NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), + subs[index] = NodeManager::currentNM()->mkNode( PLUS, subs[index], + NodeManager::currentNM()->mkNode( ITE, + NodeManager::currentNM()->mkNode( EQUAL, + NodeManager::currentNM()->mkNode( INTS_MODULUS, veq[1], veq_c ), NodeManager::currentNM()->mkConst( Rational( 0 ) ) ), 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 +509,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 +521,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++ ){ @@ -882,52 +529,25 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v prev[i] = subs[i]; if( d_n_delta.isNull() ){ d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", vars[i].getType(), "delta for cegqi" ); - Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); + Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, d_zero ); d_qe->getOutputChannel().lemma( delta_lem ); } 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 +629,550 @@ Node CegConjectureSingleInv::applySubstitution( Node n, std::vector< Node >& sub } } -void CegConjectureSingleInv::check( std::vector< Node >& lems ) { +//check if delta has a lower bound L +// if so, add lemma L>0 => L>d +void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { + if( !d_n_delta.isNull() ){ + Theory* theory = d_qe->getTheoryEngine()->theoryOf( THEORY_ARITH ); + if( theory && d_qe->getTheoryEngine()->isTheoryEnabled( THEORY_ARITH ) ){ + context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (unsigned j = 0; it != it_end; ++ it, ++j) { + Node lit = (*it).assertion; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + if( atom.getKind()==GEQ || ( pol && atom.getKind()==EQUAL ) ){ + Assert( atom.getKind()!=GEQ || atom[1].isConst() ); + Node atom_lhs; + Node atom_rhs; + if( atom.getKind()==GEQ ){ + atom_lhs = atom[0]; + atom_rhs = atom[1]; + }else{ + atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); + atom_lhs = Rewriter::rewrite( atom_lhs ); + atom_rhs = d_zero; + } + computeProgVars( atom_lhs ); + //must be an eligible term with delta + if( d_inelig.find( atom_lhs )==d_inelig.end() && d_has_delta.find( atom_lhs )!=d_has_delta.end() ){ + Node satom = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); + Trace("cegqi-delta") << "Delta assertion : " << atom << ", pol = " << pol << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( satom, msum ) ){ + Node vatom; + //isolate delta in the inequality + int ires = QuantArith::isolate( d_n_delta, msum, vatom, atom.getKind(), true ); + if( ((ires==1)==pol) || ( ires!=0 && lit.getKind()==EQUAL ) ){ + Node val = vatom[ ires==1 ? 1 : 0 ]; + Node pvm = vatom[ ires==1 ? 0 : 1 ]; + //get monomial + if( pvm!=d_n_delta ){ + Node veq_c; + Node veq_v; + if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ + Assert( veq_v==d_n_delta ); + val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / veq_c.getConst<Rational>() ) ); + val = Rewriter::rewrite( val ); + }else{ + val = Node::null(); + } + } + if( !val.isNull() ){ + Node lem1 = NodeManager::currentNM()->mkNode( GT, val, d_zero ); + lem1 = Rewriter::rewrite( lem1 ); + if( !lem1.isConst() || lem1==d_true ){ + Node lem2 = NodeManager::currentNM()->mkNode( GT, val, d_n_delta ); + Node lem = lem1==d_true ? lem2 : NodeManager::currentNM()->mkNode( OR, lem1.negate(), lem2 ); + lems.push_back( lem ); + Trace("cegqi-delta") << "...lemma : " << lem << std::endl; + } + } + }else{ + Trace("cegqi-delta") << "...wrong polarity." << std::endl; + } + } + } + } + } + } + } +} + +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 ); +} + +bool CegqiOutputSingleInv::addLemma( Node n ) { + return d_out->addLemma( 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 ); + } + } + } + } + } } } - Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + 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; +} + +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(); +} + +bool CegConjectureSingleInv::addLemma( Node n ) { + d_curr_lemmas.push_back( n ); + return true; +} + +void CegConjectureSingleInv::check( std::vector< Node >& lems ) { + if( !d_single_inv.isNull() ) { + Assert( d_cinst!=NULL ); + d_curr_lemmas.clear(); + //check if there are delta lemmas + d_cinst->getDeltaLemmas( d_curr_lemmas ); + //if not, do ce-guided instantiation + if( d_curr_lemmas.empty() ){ + //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..b5ebe3d7c 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -28,12 +28,78 @@ 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; + virtual bool addLemma( Node lem ) = 0; +}; + +class CegInstantiator +{ +private: + Node d_zero; + Node d_one; + Node d_true; + 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; + std::map< Node, bool > d_has_delta; +private: + //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; + //delta + Node d_n_delta; + //check : add instantiations based on valuation of d_vars + void check(); + // get delta lemmas : on-demand force minimality of d_n_delta + void getDeltaLemmas( std::vector< Node >& lems ); +}; + + +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 ); + bool addLemma( Node lem ); +}; + + + 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 +133,14 @@ 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 ); + // add lemma + bool addLemma( Node lem ); public: CegConjectureSingleInv( CegConjecture * p ); // original conjecture diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index cb772a31f..0bc365ec7 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -38,19 +38,19 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { Node n = assertions[i][1][0]; Assert( n.getKind()==APPLY_UF ); Node f = n.getOperator(); - + //check if already defined, if so, throw error if( d_sorts.find( f )!=d_sorts.end() ){ Message() << "Cannot define function " << f << " more than once." << std::endl; exit( 0 ); } - + //create a sort S that represents the inputs of the function std::stringstream ss; ss << "I_" << f; TypeNode iType = NodeManager::currentNM()->mkSort( ss.str() ); d_sorts[f] = iType; - + //create functions f1...fn mapping from this sort to concrete elements for( unsigned j=0; j<n.getNumChildren(); j++ ){ TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() ); @@ -58,7 +58,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { ss << f << "_arg_" << j; d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) ); } - + //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn] std::vector< Node > children; Node bv = NodeManager::currentNM()->mkBoundVar("?i", iType ); @@ -70,7 +70,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], bv ) ); } Node bd = assertions[i][1].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - + Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl; Trace("fmf-fun-def") << " to " << std::endl; assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ); @@ -81,8 +81,9 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { } //second pass : rewrite assertions for( unsigned i=0; i<assertions.size(); i++ ){ - bool is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end(); + int is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end() ? 1 : 0; std::vector< Node > constraints; + Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl; Node n = simplify( assertions[i], true, true, constraints, is_fd ); Assert( constraints.empty() ); if( n!=assertions[i] ){ @@ -95,7 +96,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { } } -Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def ) { +Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def ) { Trace("fmf-fun-def-debug") << "Simplify " << n << " " << pol << " " << hasPol << " " << is_fun_def << std::endl; if( n.getKind()==FORALL ){ Node c = simplify( n[1], pol, hasPol, constraints, is_fun_def ); @@ -104,51 +105,51 @@ Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& co }else{ return n; } - }else if( n.getType().isBoolean() && n.getKind()!=APPLY_UF ){ - std::vector< Node > children; - bool childChanged = false; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node c = n[i]; - //do not process LHS of definition - if( !is_fun_def || i!=0 ){ - bool newHasPol; - bool newPol; - QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); - //get child constraints - std::vector< Node > cconstraints; - c = simplify( n[i], newPol, newHasPol, cconstraints ); - constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() ); + }else{ + Node nn = n; + bool isBool = n.getType().isBoolean(); + if( isBool && n.getKind()!=APPLY_UF && is_fun_def!=2 ){ + std::vector< Node > children; + bool childChanged = false; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node c = n[i]; + //do not process LHS of definition + if( is_fun_def!=1 || i!=0 ){ + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); + //get child constraints + std::vector< Node > cconstraints; + c = simplify( n[i], newPol, newHasPol, cconstraints, is_fun_def==1 ? 2 : 0 ); + constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() ); + } + children.push_back( c ); + childChanged = c!=n[i] || childChanged; } - children.push_back( c ); - childChanged = c!=n[i] || childChanged; - } - if( !constraints.empty() || childChanged ){ - std::vector< Node > c; if( childChanged ){ - c.push_back( NodeManager::currentNM()->mkNode( n.getKind(), children ) ); - }else{ - c.push_back( n ); + nn = n; } - if( hasPol ){ - //conjoin with current - for( unsigned i=0; i<constraints.size(); i++ ){ - if( pol ){ - c.push_back( constraints[i] ); - }else{ - c.push_back( constraints[i].negate() ); - } + }else{ + //simplify term + simplifyTerm( n, constraints ); + } + if( !constraints.empty() && isBool && hasPol ){ + std::vector< Node > c; + c.push_back( nn ); + //conjoin with current + for( unsigned i=0; i<constraints.size(); i++ ){ + if( pol ){ + c.push_back( constraints[i] ); + }else{ + c.push_back( constraints[i].negate() ); } - constraints.clear(); - }else{ - //must add at higher level } + constraints.clear(); return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( pol ? AND : OR, c ); + }else{ + return nn; } - }else{ - //simplify term - simplifyTerm( n, constraints ); } - return n; } void FunDefFmf::simplifyTerm( Node n, std::vector< Node >& constraints ) { diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index 40364eeb7..63aa1bf94 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -36,7 +36,7 @@ private: //defined functions to injections input -> argument elements std::map< Node, std::vector< Node > > d_input_arg_inj; //simplify - Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def = false ); + Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, int is_fun_def = 0 ); //simplify term void simplifyTerm( Node n, std::vector< Node >& constraints ); public: diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index c205a280e..f97c4040b 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -346,3 +346,115 @@ 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 ); +} + +bool CegqiOutputInstStrategy::addLemma( Node lem ) { + return d_out->addLemma( lem ); +} + + +InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( qe ) { + d_out = new CegqiOutputInstStrategy( this ); +} + +void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { + d_check_delta_lemma = true; +} + +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 ); + if( d_n_delta.isNull() ){ + d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for cegqi inst strategy" ); + Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); + d_quantEngine->getOutputChannel().lemma( delta_lem ); + } + cinst->d_n_delta = d_n_delta; + 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; + } + if( d_check_delta_lemma ){ + Trace("inst-alg") << "-> Get delta lemmas for cegqi..." << std::endl; + d_check_delta_lemma = false; + std::vector< Node > dlemmas; + cinst->getDeltaLemmas( dlemmas ); + Trace("inst-alg") << "...got " << dlemmas.size() << " delta lemmas." << std::endl; + if( !dlemmas.empty() ){ + bool addedLemma = false; + for( unsigned i=0; i<dlemmas.size(); i++ ){ + if( addLemma( dlemmas[i] ) ){ + addedLemma = true; + } + } + if( addedLemma ){ + return STATUS_UNKNOWN; + } + } + } + Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; + 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() ); + /* + std::stringstream siss; + if( Trace.isOn("inst-cegqi") || Trace.isOn("inst-cegqi-debug") ){ + 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; + } + } + */ + return d_quantEngine->addInstantiation( d_curr_quant, subs, false ); +} + +bool InstStrategyCegqi::addLemma( Node lem ) { + return d_quantEngine->addLemma( lem ); +} + +bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { + if( n.getKind()==INST_CONSTANT ){ + //only legal if current quantified formula contains n + return TermDb::containsTerm( d_curr_quant, n ); + }else{ + return true; + } +} + + + + + + + + + + + + + diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 72ab5d247..9435fc97c 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,41 @@ 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 ); + bool addLemma( Node lem ); +}; + +class InstStrategyCegqi : public InstStrategy { +private: + CegqiOutputInstStrategy * d_out; + std::map< Node, CegInstantiator * > d_cinst; + Node d_n_delta; + Node d_curr_quant; + bool d_check_delta_lemma; + /** 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 ); + bool addLemma( Node lem ); + /** 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..cb01fd373 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 ); + } } } @@ -136,9 +143,9 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //check each instantiation strategy for( size_t i=0; i<d_instStrategies.size(); ++i ){ InstStrategy* is = d_instStrategies[i]; - Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl; + Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl; int quantStatus = is->process( f, effort, e_use ); - Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl; + Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl; if( quantStatus==InstStrategy::STATUS_UNFINISHED ){ finished = false; } @@ -178,11 +185,14 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); + Debug("quantifiers") << "Process " << n << "..." << std::endl; //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine if( !d_quantEngine->hasOwnership( n, this ) ){ d_quant_active[n] = false; + Debug("quantifiers") << " Quantifier has owner." << std::endl; }else if( !d_quantEngine->getModel()->isQuantifierActive( n ) ){ d_quant_active[n] = false; + Debug("quantifiers") << " Quantifier is not active (from model)." << std::endl; //it is not active if we have found the skolemized negation is unsat }else if( options::cbqi() && hasAddedCbqiLemma( n ) ){ Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n ); 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..a529e37d0 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -44,6 +44,10 @@ option clauseSplit --clause-split bool :default false # forall x. P( x ) => f( S( x ) ) = x option preSkolemQuant --pre-skolem-quant bool :read-write :default false apply skolemization eagerly to bodies of quantified formulas +option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true + apply skolemization to nested quantified formulass +option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true + apply skolemization to quantified formulas aggressively # Whether to perform agressive miniscoping option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false perform aggressive miniscoping for quantifiers @@ -220,8 +224,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/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index a78fa8d7b..991043157 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -285,7 +285,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){ }else{ std::vector< Node > children; Kind k = body[0].getKind(); - + if( body[0].getKind()==OR || body[0].getKind()==AND ){ k = body[0].getKind()==AND ? OR : AND; for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ @@ -1210,7 +1210,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v return nn.negate(); }else if( n.getKind()==kind::FORALL ){ if( polarity ){ - if( options::preSkolemQuant() ){ + if( options::preSkolemQuant() && ( options::preSkolemQuantNested() || fvs.empty() ) ){ vector< Node > children; children.push_back( n[0] ); //add children to current scope @@ -1245,20 +1245,22 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v if( containsQuantifiers( n ) ){ if( n.getType().isBoolean() ){ if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){ - Node nn; - //must remove structure - if( n.getKind()==kind::ITE ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); - }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); - }else if( n.getKind()==kind::IMPLIES ){ - nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); + if( options::preSkolemQuantAgg() ){ + Node nn; + //must remove structure + if( n.getKind()==kind::ITE ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); + }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); + }else if( n.getKind()==kind::IMPLIES ){ + nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); + } + return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); } - return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ vector< Node > children; for( int i=0; i<(int)n.getNumChildren(); i++ ){ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a475a8912..ba75af873 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -417,7 +417,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ Trace("quant") << " : " << f << std::endl; ++(d_statistics.d_num_quant); Assert( f.getKind()==FORALL ); - + //check whether we should apply a reduction bool reduced = false; if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){ @@ -567,7 +567,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Trace("inst") << std::endl; Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) ); } - if( options::cbqi() ){ + if( options::cbqi() && !options::cbqi2() ){ for( int i=0; i<(int)terms.size(); i++ ){ if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; @@ -589,7 +589,6 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std } setInstantiationLevelAttr( body, f[1], maxInstLevel+1 ); } - Trace("inst-debug") << "*** Lemma is " << lem << std::endl; ++(d_statistics.d_instantiations); return true; }else{ @@ -673,13 +672,17 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std Trace("partial-inst") << "Partial instantiation : " << f << std::endl; Trace("partial-inst") << " : " << body << std::endl; }else{ - //do optimized version - Node icb = d_term_db->getInstConstantBody( f ); - body = getSubstitute( icb, terms ); - if( Debug.isOn("check-inst") ){ - Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - if( body!=body2 ){ - Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl; + if( options::cbqi() ){ + body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + }else{ + //do optimized version + Node icb = d_term_db->getInstConstantBody( f ); + body = getSubstitute( icb, terms ); + if( Debug.isOn("check-inst") ){ + Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + if( body!=body2 ){ + Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl; + } } } } @@ -722,16 +725,16 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ if( doCache ){ - Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl; lem = Rewriter::rewrite(lem); + Trace("inst-add-debug2") << "Adding lemma : " << lem << std::endl; if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ //d_curr_out->lemma( lem, false, true ); d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); - Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl; + Trace("inst-add-debug2") << "Added lemma : " << lem << std::endl; return true; }else{ - Debug("inst-engine-debug") << "Duplicate." << std::endl; + Trace("inst-add-debug2") << "Duplicate." << std::endl; return false; } }else{ @@ -899,11 +902,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] ); @@ -945,7 +946,7 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { out << "Internal error : module for synth solution not found." << std::endl; } } - + QuantifiersEngine::Statistics::Statistics(): d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), |