From: ajreynol Date: Mon, 23 Mar 2015 14:09:25 +0000 (+0100) Subject: Decouple counter-example guided quantifier instantiation from Sygus. X-Git-Tag: cvc5-1.0.0~6372 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8beb91c3113dae4a858a30c7a21387e833d60527;p=cvc5.git Decouple counter-example guided quantifier instantiation from Sygus. --- 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,872 +31,1002 @@ 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; imkSkolem( 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; + +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_vars.begin(), d_vars.end(), n )!=d_vars.end() ){ + d_prog_var[n][n] = true; + }else if( !d_out->isEligibleForInstantiation( n ) ){ + d_inelig[n] = true; + return; + } + for( unsigned i=0; i::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){ + d_prog_var[n][it->first] = true; + } } - 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 > 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; jsecond.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& 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_vars[i]; + TypeNode pvtn = pv.getType(); + + if( (i+1)hasTerm( pv ) ){ + Node pvr = ee->getRepresentative( pv ); + eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); + 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; + //compute d_subs_fv, which program variables are contained in n + computeProgVars( n ); + //must be an eligible term + if( d_inelig.find( n )==d_inelig.end() ){ + Node ns; + Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) + bool proc = false; + if( !d_prog_var[n].empty() ){ + ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff, false ); + if( !ns.isNull() ){ + computeProgVars( ns ); + //substituted version must be new and cannot contain pv + proc = subs_proc[0][pv_coeff].find( ns )==subs_proc[0][pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end(); + } + }else{ + ns = n; + proc = true; + } + 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, effort ) ){ + return true; } } } } + ++eqc_i; } } - } - 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; kmkSkolem( "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; imkNode( 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 lhs; + std::vector< bool > lhs_v; + std::vector< Node > lhs_coeff; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + computeProgVars( n ); + //must be an eligible term + if( d_inelig.find( n )==d_inelig.end() ){ + Node ns; + Node pv_coeff; + if( !d_prog_var[n].empty() ){ + ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff ); + if( !ns.isNull() ){ + computeProgVars( ns ); + } + }else{ + ns = n; + } + if( !ns.isNull() ){ + bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); + for( unsigned j=0; jmkNode( MULT, pv_coeff, eq_lhs ); + eq_lhs = Rewriter::rewrite( eq_lhs ); + } + if( !lhs_coeff[j].isNull() ){ + Trace("cegqi-si-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl; + eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs ); + eq_rhs = Rewriter::rewrite( eq_rhs ); + } + } + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + if( Trace.isOn("cegqi-si-inst-debug") ){ + Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); + Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; + } + Node veq; + if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){ + Trace("cegqi-si-inst-debug") << "...isolated equality " << veq << "." << std::endl; + Node veq_c; + if( veq[0]!=pv ){ + Node veq_v; + if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ + Assert( veq_v==pv ); + } + } + 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, effort ) ){ + return true; + } + } + } + } + } + } + lhs.push_back( ns ); + lhs_v.push_back( hasVar ); + lhs_coeff.push_back( pv_coeff ); } } + ++eqc_i; } } + ++eqcs_i; } - 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; isecond.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; jmkNode( 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; jfirst.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::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; imkNode( 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; igetTheoryEngine()->theoryOf( tid ); + if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) { + context::CDList::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( tid==THEORY_ARITH ){ + if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){ + Assert( atom[1].isConst() ); + computeProgVars( atom[0] ); + //must be an eligible term + if( d_inelig.find( atom[0] )==d_inelig.end() ){ + //apply substitution to LHS of atom + Node atom_lhs; + Node atom_rhs; + if( !d_prog_var[atom[0]].empty() ){ + Node atom_lhs_coeff; + atom_lhs = applySubstitution( atom[0], 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; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( satom, msum ) ){ + if( Trace.isOn("cegqi-si-inst-debug") ){ + Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); + Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; + } + Node vatom; + //isolate pv in the inequality + int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true ); + if( ires!=0 ){ + Trace("cegqi-si-inst-debug") << "...isolated atom " << vatom << "." << std::endl; + Node val = vatom[ ires==1 ? 1 : 0 ]; + Node pvm = vatom[ ires==1 ? 0 : 1 ]; + //get monomial + Node veq_c; + if( pvm!=pv ){ + Node veq_v; + if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ + Assert( veq_v==pv ); + } + } + //disequalities are both strict upper and lower bounds + unsigned rmax = atom.getKind()==GEQ ? 1 : 2; + for( unsigned r=0; rmkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else if( pvtn.isReal() ){ + //now is strict inequality + uires = uires*2; + }else{ + Assert( false ); + } + } + }else{ + Assert( atom.getKind()==EQUAL && !pol ); + if( pvtn.isInteger() ){ + uires = r==0 ? -1 : 1; + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else if( pvtn.isReal() ){ + uires = r==0 ? -2 : 2; + }else{ + Assert( false ); + } + } + 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, effort ) ){ + return true; + } + } + } + } + } + } } } } } } } - } - 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; i0 ){ + 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, 1 ); }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 false; } } - 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; + +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 + std::vector< Node > a_subs; + a_subs.push_back( n ); + std::vector< Node > a_var; + a_var.push_back( pv ); + std::vector< Node > a_coeff; + std::vector< Node > a_has_coeff; + if( !pv_coeff.isNull() ){ + 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; + std::vector< Node > new_has_coeff; + for( unsigned j=0; jmkNode( MULT, coeff[j], a_pv_coeff ) ); + } } - } - //did not match, now see if it contains v - }else if( ( n.getKind()==OR && !pol ) || ( n.getKind()==AND && pol ) ){ - for( unsigned i=0; i >& 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 << std::endl; + success = addInstantiation( subs, vars, coeff, has_coeff, subs_typ, i+1, effort ); + if( !success ){ + subs.pop_back(); + vars.pop_back(); + coeff.pop_back(); + if( !pv_coeff.isNull() ){ + has_coeff.pop_back(); + } + subs_typ.pop_back(); } - analyzeSygusConjunct( n[0][0], n[0][1], children, prog_invoke, progs, contains, false ); + } + if( success ){ + return true; }else{ - if( pol ){ - n = TermDb::simpleNegate( n ); + //revert substitution information + for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ + subs[it->first] = it->second; } - Trace("cegqi-si") << "Sygus conjunct : " << n << std::endl; - children[p].push_back( n ); - for( unsigned i=0; i::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){ + coeff[it->first] = it->second; } - bool success = analyzeSygusTerm( n, prog_invoke[n], contains[n] ); - for( unsigned i=0; i >::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; jsecond.size(); j++ ){ - Trace("cegqi-si") << " " << it->second[j] << std::endl; - } + for( unsigned i=0; i >& 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 ); +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 ); + }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(); + Node prev = subs[index]; + Assert( !coeff[index].isNull() ); + Trace("cegqi-si-inst-debug") << "Normalize substitution for " << coeff[index] << " * " << vars[index] << " = " << subs[index] << ", stype = " << subs_typ[index] << std::endl; + if( vars[index].getType().isInteger() ){ + //must ensure that divisibility constraints are met + //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful + Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, coeff[index], vars[index] ); + Node eq_rhs = subs[index]; + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( eq, msum ) ){ + Node veq; + if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){ + Node veq_c; + if( veq[0]!=vars[index] ){ + Node veq_v; + if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ + Assert( veq_v==vars[index] ); + } + } + subs[index] = veq[1]; + 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 ) ) ) + ); + } + } + Trace("cegqi-si-inst-debug") << "...normalize integers : " << subs[index] << std::endl; + 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 ), + 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 ) ){ + return true; + } + } + */ + } } - } - for( unsigned i=0; imkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / coeff[index].getConst() ), 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 ) ){ + return true; } + }else{ + Assert( false ); } - }else{ - //record this conjunct contains n - contains[n] = true; + subs[index] = prev; + Trace("cegqi-si-inst-debug") << "...failed." << std::endl; + return false; } - return true; } - - -void CegConjectureSingleInv::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() ){ - 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() ){ - d_inelig[n] = true; - return; - } - for( unsigned i=0; i::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){ - d_prog_var[n][it->first] = true; +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; imkSkolem( "delta", vars[i].getType(), "delta for cegqi" ); + Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); + d_qe->getOutputChannel().lemma( delta_lem ); } + subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta ); + } + } + //check if we have already added this instantiation + 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 success; } -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 ); - }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]; - TypeNode pvtn = pv.getType(); - - if( (i+1)hasTerm( pv ) ){ - Node pvr = ee->getRepresentative( pv ); - eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); - 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; - //compute d_subs_fv, which program variables are contained in n - computeProgVars( n ); - //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ - Node ns; - Node pv_coeff; //coefficient of pv in the equality we solve (null is 1) - bool proc = false; - if( !d_prog_var[n].empty() ){ - ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff, false ); - if( !ns.isNull() ){ - computeProgVars( ns ); - //substituted version must be new and cannot contain pv - proc = subs_proc[0][pv_coeff].find( ns )==subs_proc[0][pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end(); - } + +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 ) ); + bool req_coeff = false; + if( !has_coeff.empty() ){ + for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){ + if( std::find( has_coeff.begin(), has_coeff.end(), it->first )!=has_coeff.end() ){ + req_coeff = true; + break; + } + } + } + if( !req_coeff ){ + Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + if( n!=nret ){ + nret = Rewriter::rewrite( nret ); + } + //result is nret + return nret; + }else{ + if( try_coeff ){ + //must convert to monomial representation + std::map< Node, Node > msum; + if( QuantArith::getMonomialSum( n, msum ) ){ + std::map< Node, Node > msum_coeff; + std::map< Node, Node > msum_term; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + //check if in substitution + std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first ); + if( its!=vars.end() ){ + int index = its-vars.begin(); + if( coeff[index].isNull() ){ + //apply substitution + msum_term[it->first] = subs[index]; + }else{ + //apply substitution, multiply to ensure no divisibility conflict + msum_term[it->first] = subs[index]; + //relative coefficient + msum_coeff[it->first] = coeff[index]; + if( pv_coeff.isNull() ){ + pv_coeff = coeff[index]; }else{ - ns = n; - proc = true; + pv_coeff = NodeManager::currentNM()->mkNode( MULT, pv_coeff, coeff[index] ); } - 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 ) ){ - return true; + } + }else{ + msum_term[it->first] = it->first; + } + } + //make sum with normalized coefficient + Assert( !pv_coeff.isNull() ); + pv_coeff = Rewriter::rewrite( pv_coeff ); + Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_coeff << std::endl; + std::vector< Node > children; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + Node c_coeff; + if( !msum_coeff[it->first].isNull() ){ + c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_coeff.getConst() / msum_coeff[it->first].getConst() ) ); + }else{ + c_coeff = pv_coeff; + } + if( !it->second.isNull() ){ + c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second ); + } + Node c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] ); + children.push_back( c ); + Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl; + } + Node nret = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); + nret = Rewriter::rewrite( nret ); + //result is ( nret / pv_coeff ) + return nret; + }else{ + Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl; + } + } + // failed to apply the substitution + return Node::null(); + } +} + +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() ) { + Assert( d_single_inv.getKind()==FORALL ); + d_single_inv_var.clear(); + d_single_inv_sk.clear(); + for( unsigned i=0; imkSkolem( 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 > 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; jsecond.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 lhs; - std::vector< bool > lhs_v; - std::vector< Node > lhs_coeff; - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - while( !eqc_i.isFinished() ){ - Node n = *eqc_i; - computeProgVars( n ); - //must be an eligible term - if( d_inelig.find( n )==d_inelig.end() ){ - Node ns; - Node pv_coeff; - if( !d_prog_var[n].empty() ){ - ns = applySubstitution( n, subs, vars, coeff, has_coeff, pv_coeff ); - if( !ns.isNull() ){ - computeProgVars( ns ); - } - }else{ - ns = n; - } - if( !ns.isNull() ){ - bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end(); - for( unsigned j=0; jmkNode( MULT, pv_coeff, eq_lhs ); - eq_lhs = Rewriter::rewrite( eq_lhs ); - } - if( !lhs_coeff[j].isNull() ){ - Trace("cegqi-si-inst-debug") << "...mult rhs by " << lhs_coeff[j] << std::endl; - eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff[j], eq_rhs ); - eq_rhs = Rewriter::rewrite( eq_rhs ); - } - } - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ - if( Trace.isOn("cegqi-si-inst-debug") ){ - Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); - Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; - } - Node veq; - if( QuantArith::isolate( pv, msum, veq, EQUAL, true )!=0 ){ - Trace("cegqi-si-inst-debug") << "...isolated equality " << veq << "." << std::endl; - Node veq_c; - if( veq[0]!=pv ){ - Node veq_v; - if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==pv ); - } - } - 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 ) ){ - return true; - } - } - } - } - } - } - lhs.push_back( ns ); - lhs_v.push_back( hasVar ); - lhs_coeff.push_back( pv_coeff ); + } + 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; kmkSkolem( "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; imkNode( 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; jgetTheoryEngine()->theoryOf( tid ); - if (theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid)) { - context::CDList::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( tid==THEORY_ARITH ){ - if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol ) ){ - Assert( atom[1].isConst() ); - computeProgVars( atom[0] ); - //must be an eligible term - if( d_inelig.find( atom[0] )==d_inelig.end() ){ - //apply substitution to LHS of atom - Node atom_lhs; - Node atom_rhs; - if( !d_prog_var[atom[0]].empty() ){ - Node atom_lhs_coeff; - atom_lhs = applySubstitution( atom[0], 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; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( satom, msum ) ){ - if( Trace.isOn("cegqi-si-inst-debug") ){ - Trace("cegqi-si-inst-debug") << "...got monomial sum: " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "cegqi-si-inst-debug" ); - Trace("cegqi-si-inst-debug") << "isolate for " << pv << "..." << std::endl; - } - Node vatom; - //isolate pv in the inequality - int ires = QuantArith::isolate( pv, msum, vatom, atom.getKind(), true ); - if( ires!=0 ){ - Trace("cegqi-si-inst-debug") << "...isolated atom " << vatom << "." << std::endl; - Node val = vatom[ ires==1 ? 1 : 0 ]; - Node pvm = vatom[ ires==1 ? 0 : 1 ]; - //get monomial - Node veq_c; - if( pvm!=pv ){ - Node veq_v; - if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){ - Assert( veq_v==pv ); - } - } - //disequalities are both strict upper and lower bounds - unsigned rmax = atom.getKind()==GEQ ? 1 : 2; - for( unsigned r=0; rmkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else if( pvtn.isReal() ){ - //now is strict inequality - uires = uires*2; - }else{ - Assert( false ); - } - } - }else{ - Assert( atom.getKind()==EQUAL && !pol ); - if( pvtn.isInteger() ){ - uires = r==0 ? -1 : 1; - uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); - uval = Rewriter::rewrite( uval ); - }else if( pvtn.isReal() ){ - uires = r==0 ? -2 : 2; - }else{ - Assert( false ); - } - } - 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 ) ){ - return true; - } - } - } - } - } - } + 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; isecond.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; jmkNode( 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; jfirst.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::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; imkNode( 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; i0 ){ - 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 ); - }else{ - return false; + } + 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::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 ) { - //must ensure variables have been computed for n - computeProgVars( n ); - //substitute into previous substitutions, when applicable - std::vector< Node > a_subs; - a_subs.push_back( n ); - std::vector< Node > a_var; - a_var.push_back( pv ); - std::vector< Node > a_coeff; - std::vector< Node > a_has_coeff; - if( !pv_coeff.isNull() ){ - 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; - std::vector< Node > new_has_coeff; - for( unsigned j=0; jmkNode( MULT, coeff[j], a_pv_coeff ) ); - } - } - if( subs[j]!=prev_subs[j] ){ - computeProgVars( subs[j] ); - } +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 " << n << std::endl; - success = addInstantiation( subs, vars, coeff, has_coeff, subs_typ, i+1, lems, effort ); - if( !success ){ - subs.pop_back(); - vars.pop_back(); - coeff.pop_back(); - if( !pv_coeff.isNull() ){ - has_coeff.pop_back(); + 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; + } } - subs_typ.pop_back(); + //did not match, now see if it contains v + }else if( ( n.getKind()==OR && !pol ) || ( n.getKind()==AND && pol ) ){ + for( unsigned i=0; i::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ - subs[it->first] = it->second; - } - for( std::map< int, Node >::iterator it = prev_coeff.begin(); it != prev_coeff.end(); it++ ){ - coeff[it->first] = it->second; - } - for( unsigned i=0; i& 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 ) { - if( j==has_coeff.size() ){ - return addInstantiation( subs, vars, subs_typ, lems ); - }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(); - Node prev = subs[index]; - Assert( !coeff[index].isNull() ); - Trace("cegqi-si-inst-debug") << "Normalize substitution for " << coeff[index] << " * " << vars[index] << " = " << subs[index] << ", stype = " << subs_typ[index] << std::endl; - if( vars[index].getType().isInteger() ){ - //must ensure that divisibility constraints are met - //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful - Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, coeff[index], vars[index] ); - Node eq_rhs = subs[index]; - Node eq = eq_lhs.eqNode( eq_rhs ); - eq = Rewriter::rewrite( eq ); - Trace("cegqi-si-inst-debug") << "...equality is " << eq << std::endl; - std::map< Node, Node > msum; - if( QuantArith::getMonomialSumLit( eq, msum ) ){ - Node veq; - if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){ - Node veq_c; - if( veq[0]!=vars[index] ){ - Node veq_v; - if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){ - Assert( veq_v==vars[index] ); - } - } - subs[index] = veq[1]; - 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 ) ) ) - ); - } - } - Trace("cegqi-si-inst-debug") << "...normalize integers : " << subs[index] << std::endl; - if( addInstantiationCoeff( subs, vars, coeff, has_coeff, subs_typ, j+1, lems ) ){ - 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 ), - 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 ) ){ - return true; - } - } - */ - } +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; imkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / coeff[index].getConst() ), 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 ) ){ - return true; + } + }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 >::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; jsecond.size(); j++ ){ + Trace("cegqi-si") << " " << it->second[j] << std::endl; } - }else{ - Assert( false ); } - subs[index] = prev; - Trace("cegqi-si-inst-debug") << "...failed." << std::endl; - return false; + return success; } + return true; } -bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::vector< int >& subs_typ, std::vector< Node >& lems ) { - // do delta rationals - std::map< int, Node > prev; - for( unsigned i=0; imkSkolem( "delta", vars[i].getType(), "delta for cegqi" ); - Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); - d_qe->getOutputChannel().lemma( delta_lem ); +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; imkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta ); } + }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; - siss << " * single invocation: " << std::endl; - for( unsigned j=0; j " << ( subs_typ[j]==9 ? "M:" : "") << subs[j] << std::endl; + if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){ + siss << " * single invocation: " << std::endl; + for( unsigned j=0; j " << ( 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() ); @@ -906,10 +1036,6 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v Trace("cegqi-si-inst-debug") << siss.str(); Trace("cegqi-si-inst-debug") << " * success = " << !alreadyExists << std::endl; if( alreadyExists ){ - //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; @@ -917,7 +1043,7 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v 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_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() ); @@ -926,103 +1052,18 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs, std::v } } - -Node CegConjectureSingleInv::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 ) ); - bool req_coeff = false; - if( !has_coeff.empty() ){ - for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){ - if( std::find( has_coeff.begin(), has_coeff.end(), it->first )!=has_coeff.end() ){ - req_coeff = true; - break; - } - } - } - if( !req_coeff ){ - Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - if( n!=nret ){ - nret = Rewriter::rewrite( nret ); - } - //result is nret - return nret; - }else{ - if( try_coeff ){ - //must convert to monomial representation - std::map< Node, Node > msum; - if( QuantArith::getMonomialSum( n, msum ) ){ - std::map< Node, Node > msum_coeff; - std::map< Node, Node > msum_term; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - //check if in substitution - std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first ); - if( its!=vars.end() ){ - int index = its-vars.begin(); - if( coeff[index].isNull() ){ - //apply substitution - msum_term[it->first] = subs[index]; - }else{ - //apply substitution, multiply to ensure no divisibility conflict - msum_term[it->first] = subs[index]; - //relative coefficient - msum_coeff[it->first] = coeff[index]; - if( pv_coeff.isNull() ){ - pv_coeff = coeff[index]; - }else{ - pv_coeff = NodeManager::currentNM()->mkNode( MULT, pv_coeff, coeff[index] ); - } - } - }else{ - msum_term[it->first] = it->first; - } - } - //make sum with normalized coefficient - Assert( !pv_coeff.isNull() ); - pv_coeff = Rewriter::rewrite( pv_coeff ); - Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_coeff << std::endl; - std::vector< Node > children; - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - Node c_coeff; - if( !msum_coeff[it->first].isNull() ){ - c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_coeff.getConst() / msum_coeff[it->first].getConst() ) ); - }else{ - c_coeff = pv_coeff; - } - if( !it->second.isNull() ){ - c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second ); - } - Node c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] ); - children.push_back( c ); - Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl; - } - Node nret = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); - nret = Rewriter::rewrite( nret ); - //result is ( nret / pv_coeff ) - return nret; - }else{ - Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl; - } - } - // failed to apply the substitution - return Node::null(); - } +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() ) { - 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; - } - } - Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + 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; igetTermDatabase()->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(preq) ); - nodeChanged = true; } //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){ // Node req = qe->getPhaseReqEquality( f, trNodes[i] );