diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-28 15:21:21 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-28 15:21:21 +0100 |
commit | 1b6de21ad4a182111bc7aaa1898f4f638f5e1184 (patch) | |
tree | 9473cecbddb7eeba201c8e33a70e72cc6bc575b9 | |
parent | 3d82de01011931ee352715ac4f45c7bbc66f2201 (diff) |
Minor refactor CEGQI.
-rw-r--r-- | src/theory/quantifiers/ambqi_builder.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 524 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.h | 30 |
3 files changed, 300 insertions, 256 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 353b6d1c4..f047276b0 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -441,7 +441,7 @@ void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef } Assert( vchildren.empty() ); if( incomplete ){ - Trace("ajr-temp") << "Construct incomplete entry." << std::endl; + Trace("ambqi-check-debug2") << "Construct incomplete entry." << std::endl; //if a child is unknown, we must return unknown construct_entry( entry, entry_def, val_unk ); diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 089fd973e..a034bb8c1 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -43,13 +43,271 @@ CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active d_refine_count = 0; } -void CegInstantiation::CegConjecture::assign( Node q ) { +void CegInstantiation::CegConjecture::assign( QuantifiersEngine * qe, Node q ) { Assert( d_quant.isNull() ); Assert( q.getKind()==FORALL ); d_quant = q; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) ); } + //construct base instantiation + d_base_inst = Rewriter::rewrite( qe->getInstantiation( q, d_candidates ) ); + Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; + if( qe->getTermDatabase()->isQAttrSygus( q ) ){ + CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj ); + Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl; + //store the inner variables for each disjunct + for( unsigned j=0; j<d_base_disj.size(); j++ ){ + d_inner_vars_disj.push_back( std::vector< Node >() ); + //if the disjunct is an existential, store it + if( d_base_disj[j].getKind()==NOT && d_base_disj[j][0].getKind()==FORALL ){ + for( unsigned k=0; k<d_base_disj[j][0][0].getNumChildren(); k++ ){ + d_inner_vars.push_back( d_base_disj[j][0][0][k] ); + d_inner_vars_disj[j].push_back( d_base_disj[j][0][0][k] ); + } + } + } + analyzeSygusConjecture(); + d_syntax_guided = true; + }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){ + d_syntax_guided = false; + }else{ + Assert( false ); + } +} + + + +void CegInstantiation::CegConjecture::analyzeSygusConjecture() { + Node q = d_quant; + // 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 + if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){ + //try to phrase as single invocation property + bool singleInvocation = true; + Trace("cegqi-analyze") << "...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-analyze-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-analyze-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-analyze") << "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 ); + Node pv = NodeManager::currentNM()->mkBoundVar( "F", inv.getType() ); + d_single_inv_map[prog] = pv; + pbvs.push_back( pv ); + Trace("cegqi-analyze-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 ){ + 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 ); + + 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-analyze-debug") << " ..." << arg << " occurs in "; + Trace("cegqi-analyze-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-analyze-debug") << " ..." << arg << " occurs in invocation " << inv << " of " << prog << " in " << conj << std::endl; + Trace("cegqi-analyze-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-analyze") << " " << prog << " -> " << sinv << std::endl; + d_single_inv_app_map[prog] = sinv; + } + //construct the single invocation version of the property + Trace("cegqi-analyze") << "Single invocation formula conjuncts are : " << std::endl; + //std::vector< Node > si_conj; + Assert( !pbvs.empty() ); + Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs ); + Node si; + for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ + Assert( si.isNull() ); + std::vector< Node > tmp; + 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-analyze-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 ); + Trace("cegqi-analyze") << " " << curr; + tmp.push_back( curr.negate() ); + if( !it->first.isNull() ){ + Trace("cegqi-analyze-debug") << " under " << it->first; + } + Trace("cegqi-analyze") << std::endl; + } + Assert( !tmp.empty() ); + Node bd = tmp.size()==1 ? tmp[0] : NodeManager::currentNM()->mkNode( OR, tmp ); + if( !it->first.isNull() ){ + // apply substitution for skolem variables + std::vector< Node > vars; + d_single_inv_arg_sk.clear(); + for( unsigned j=0; j<it->first.getNumChildren(); j++ ){ + std::stringstream ss; + ss << "k_" << it->first[j]; + Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" ); + vars.push_back( it->first[j] ); + d_single_inv_arg_sk.push_back( v ); + } + bd = bd.substitute( vars.begin(), vars.end(), d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() ); + + Trace("cegqi-analyze-debug") << " -> " << bd << std::endl; + } + si = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); + } + Trace("cegqi-analyze-debug") << "...formula is : " << si << std::endl; + d_single_inv = si; + }else{ + Trace("cegqi-analyze") << "Property is not single invocation." << std::endl; + } + } +} + +bool CegInstantiation::CegConjecture::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 = n.negate(); + } + Trace("cegqi-analyze") << "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-analyze") << " Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl; + for( unsigned j=0; j<it->second.size(); j++ ){ + Trace("cegqi-analyze") << " " << it->second[j] << std::endl; + } + } + return success; + } + return true; +} + +bool CegInstantiation::CegConjecture::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 CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){ @@ -64,6 +322,27 @@ void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){ Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() ); Trace("cegqi") << "Add candidate lemma : " << lem << std::endl; qe->getOutputChannel().lemma( lem ); + }else if( !d_single_inv.isNull() ){ + Assert( d_single_inv.getKind()==FORALL ); + std::vector< Node > vars; + 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" ); + vars.push_back( d_single_inv[0][i] ); + d_single_inv_sk.push_back( k ); + } + Node inst = d_single_inv[1].substitute( vars.begin(), vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); + Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), inst.negate() ); + Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl; + /* inactive for now (until figure out how to use it) + qe->getOutputChannel().lemma( lem ); + if( Trace.isOn("cegqi-debug") ){ + lem = Rewriter::rewrite( lem ); + Trace("cegqi-debug") << "...rewritten : " << lem << std::endl; + } + */ } } } @@ -133,31 +412,8 @@ void CegInstantiation::registerQuantifier( Node q ) { if( d_quantEngine->getOwner( q )==this ){ if( !d_conj->isAssigned() ){ Trace("cegqi") << "Register conjecture : " << q << std::endl; - d_conj->assign( q ); - //construct base instantiation - d_conj->d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj->d_candidates ) ); - Trace("cegqi") << "Base instantiation is : " << d_conj->d_base_inst << std::endl; - if( getTermDatabase()->isQAttrSygus( q ) ){ - collectDisjuncts( d_conj->d_base_inst, d_conj->d_base_disj ); - Trace("cegqi") << "Conjecture has " << d_conj->d_base_disj.size() << " disjuncts." << std::endl; - //store the inner variables for each disjunct - for( unsigned j=0; j<d_conj->d_base_disj.size(); j++ ){ - d_conj->d_inner_vars_disj.push_back( std::vector< Node >() ); - //if the disjunct is an existential, store it - if( d_conj->d_base_disj[j].getKind()==NOT && d_conj->d_base_disj[j][0].getKind()==FORALL ){ - for( unsigned k=0; k<d_conj->d_base_disj[j][0][0].getNumChildren(); k++ ){ - d_conj->d_inner_vars.push_back( d_conj->d_base_disj[j][0][0][k] ); - d_conj->d_inner_vars_disj[j].push_back( d_conj->d_base_disj[j][0][0][k] ); - } - } - } - analyzeSygusConjecture( q ); - d_conj->d_syntax_guided = true; - }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ - d_conj->d_syntax_guided = false; - }else{ - Assert( false ); - } + d_conj->assign( d_quantEngine, q ); + //fairness if( options::ceGuidedInstFair()!=CEGQI_FAIR_NONE ){ std::vector< Node > mc; @@ -499,220 +755,4 @@ void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) { out << n << std::endl; } -void CegInstantiation::analyzeSygusConjecture( Node q ) { - // 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 - if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){ - //try to phrase as single invocation property - bool singleInvocation = true; - Trace("cegqi-analyze") << "...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-analyze-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-analyze-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-analyze") << "Property is single invocation with : " << std::endl; - 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 ); - d_single_inv_map[q][prog] = NodeManager::currentNM()->mkSkolem( "F", inv.getType(), "single invocation function variable" ); - Trace("cegqi-analyze-debug2") << "Make variable " << d_single_inv_map[q][prog] << " 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 ){ - 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 ); - - 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-analyze-debug") << " ..." << arg << " occurs in "; - Trace("cegqi-analyze-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-analyze-debug") << " ..." << arg << " occurs in invocation " << inv << " of " << prog << " in " << conj << std::endl; - Trace("cegqi-analyze-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-analyze") << " " << prog << " -> " << sinv << std::endl; - d_single_inv_app_map[q][prog] = sinv; - } - //construct the single invocation version of the property - Trace("cegqi-analyze") << "Single invocation formula conjuncts are : " << std::endl; - std::vector< Node > si_conj; - for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ - std::vector< Node > tmp; - 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[q][prog] ); - Trace("cegqi-analyze-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[q][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 ); - Trace("cegqi-analyze") << " " << curr; - if( it->first.isNull() ){ - si_conj.push_back( curr.negate() ); - }else{ - tmp.push_back( curr ); - Trace("cegqi-analyze-debug") << " under " << it->first; - } - Trace("cegqi-analyze") << std::endl; - } - if( !it->first.isNull() ){ - Assert( !tmp.empty() ); - Node bd = tmp.size()==1 ? tmp[0] : NodeManager::currentNM()->mkNode( AND, tmp ); - Node curr = NodeManager::currentNM()->mkNode( FORALL, it->first, bd ).negate(); - si_conj.push_back( curr ); - Trace("cegqi-analyze-debug") << " -> " << curr << std::endl; - } - } - Node si = si_conj.size()==1 ? si_conj[0] : NodeManager::currentNM()->mkNode( OR, si_conj ); - Trace("cegqi-analyze-debug") << "...formula is : " << si << std::endl; - d_single_inv[q] = si; - }else{ - Trace("cegqi-analyze") << "Property is not single invocation." << std::endl; - } - } -} - -bool CegInstantiation::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 = n.negate(); - } - Trace("cegqi-analyze") << "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-analyze") << " Program " << progs[i] << " is invoked " << it->second.size() << " times " << std::endl; - for( unsigned j=0; j<it->second.size(); j++ ){ - Trace("cegqi-analyze") << " " << it->second[j] << std::endl; - } - } - return success; - } - return true; -} - -bool CegInstantiation::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; -} - } diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 8b3d56a2a..ad94b51a5 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -67,11 +67,27 @@ private: /** refine count */ unsigned d_refine_count; /** assign */ - void assign( Node q ); + void assign( QuantifiersEngine * qe, Node q ); /** is assigned */ bool isAssigned() { return !d_quant.isNull(); } /** current extential quantifeirs whose couterexamples we must refine */ std::vector< std::vector< Node > > d_ce_sk; + private: //for single invocation + void analyzeSygusConjecture(); + bool analyzeSygusConjunct( Node n, Node p, 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 ); + bool analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains ); + public: + Node d_single_inv; + //map from programs to variables in single invocation property + std::map< Node, Node > d_single_inv_map; + //map from programs to evaluator term representing the above variable + std::map< Node, Node > d_single_inv_app_map; + //list of skolems for each argument of programs + std::vector< Node > d_single_inv_arg_sk; + //list of skolems for each program + std::vector< Node > d_single_inv_sk; public: //for fairness /** the cardinality literals */ std::map< int, Node > d_lits; @@ -107,18 +123,6 @@ private: /** get model term */ Node getModelTerm( Node n ); private: - std::map< Node, Node > d_single_inv; - //map from programs to variables in single invocation property - std::map< Node, std::map< Node, Node > > d_single_inv_map; - //map from programs to evaluator term representing the above variable - std::map< Node, std::map< Node, Node > > d_single_inv_app_map; -private: - void analyzeSygusConjecture( Node q ); - bool analyzeSygusConjunct( Node n, Node p, 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 ); - bool analyzeSygusTerm( Node n, std::map< Node, std::vector< Node > >& prog_invoke, std::map< Node, bool >& contains ); -private: /** print sygus term */ void printSygusTerm( std::ostream& out, Node n ); public: |