diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 318 |
1 files changed, 177 insertions, 141 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index d4735b3d8..aa20c1f76 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -138,159 +138,195 @@ void CegSingleInv::initialize(Node q) } } // compute single invocation partition - if( options::cegqiSingleInvMode()!=CEGQI_SI_MODE_NONE ){ - Node qq; - if( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ){ - qq = q[1][0][1]; - }else{ - qq = TermUtil::simpleNegate( q[1] ); - } - //process the single invocation-ness of the property - if( !d_sip->init( progs, qq ) ){ - Trace("cegqi-si") << "...not single invocation (type mismatch)" << std::endl; - }else{ - Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl; - d_sip->debugPrint( "cegqi-si" ); + Node qq; + if (q[1].getKind() == NOT && q[1][0].getKind() == FORALL) + { + qq = q[1][0][1]; + } + else + { + qq = TermUtil::simpleNegate(q[1]); + } + // process the single invocation-ness of the property + if (!d_sip->init(progs, qq)) + { + Trace("cegqi-si") << "...not single invocation (type mismatch)" + << std::endl; + return; + } + Trace("cegqi-si") << "- Partitioned to single invocation parts : " + << std::endl; + d_sip->debugPrint("cegqi-si"); + + // map from program to bound variables + std::vector<Node> funcs; + d_sip->getFunctions(funcs); + for (unsigned j = 0, size = funcs.size(); j < size; j++) + { + Assert(std::find(progs.begin(), progs.end(), funcs[j]) != progs.end()); + d_prog_to_sol_index[funcs[j]] = j; + } - //map from program to bound variables - std::vector<Node> funcs; - d_sip->getFunctions(funcs); - for (unsigned j = 0, size = funcs.size(); j < size; j++) + // check if it is single invocation + if (d_sip->isPurelySingleInvocation()) + { + // We are fully single invocation, set single invocation if we haven't + // disabled single invocation techniques. + if (options::cegqiSingleInvMode() != CEGQI_SI_MODE_NONE) + { + d_single_invocation = true; + return; + } + } + // We are processing without single invocation techniques, now check if + // we should fix an invariant template (post-condition strengthening or + // pre-condition weakening). + SygusInvTemplMode tmode = options::sygusInvTemplMode(); + if (tmode != SYGUS_INV_TEMPL_MODE_NONE) + { + // currently only works for single predicate synthesis + if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate()) + { + tmode = SYGUS_INV_TEMPL_MODE_NONE; + } + else if (!options::sygusInvTemplWhenSyntax()) + { + // only use invariant templates if no syntactic restrictions + if (CegGrammarConstructor::hasSyntaxRestrictions(q)) { - Assert(std::find(progs.begin(), progs.end(), funcs[j]) != progs.end()); - d_prog_to_sol_index[funcs[j]] = j; + tmode = SYGUS_INV_TEMPL_MODE_NONE; } + } + } + + if (tmode == SYGUS_INV_TEMPL_MODE_NONE) + { + // not processing invariant templates + return; + } + // if we are doing invariant templates, then construct the template + Trace("cegqi-si") << "- Do transition inference..." << std::endl; + d_ti[q].process(qq); + Trace("cegqi-inv") << std::endl; + if (d_ti[q].d_func.isNull()) + { + // the invariant could not be inferred + return; + } + NodeManager* nm = NodeManager::currentNM(); + // map the program back via non-single invocation map + Node prog = d_ti[q].d_func; + std::vector<Node> prog_templ_vars; + prog_templ_vars.insert( + prog_templ_vars.end(), d_ti[q].d_vars.begin(), d_ti[q].d_vars.end()); + d_trans_pre[prog] = d_ti[q].getComponent(1); + d_trans_post[prog] = d_ti[q].getComponent(-1); + Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl; + Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; + std::vector<Node> sivars; + d_sip->getSingleInvocationVariables(sivars); + Node invariant = d_sip->getFunctionInvocationFor(prog); + Assert(!invariant.isNull()); + invariant = invariant.substitute(sivars.begin(), + sivars.end(), + prog_templ_vars.begin(), + prog_templ_vars.end()); + Trace("cegqi-inv") << " invariant : " << invariant << std::endl; - //check if it is single invocation - if (!d_sip->isPurelySingleInvocation()) + // store simplified version of quantified formula + d_simp_quant = d_sip->getFullSpecification(); + std::vector<Node> new_bv; + for( const Node& v : sivars ) + { + new_bv.push_back(nm->mkBoundVar(v.getType())); + } + d_simp_quant = d_simp_quant.substitute( + sivars.begin(), sivars.end(), new_bv.begin(), new_bv.end()); + Assert(q[1].getKind() == NOT && q[1][0].getKind() == FORALL); + for (const Node& v : q[1][0][0]) + { + new_bv.push_back(v); + } + d_simp_quant = + nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, new_bv), d_simp_quant) + .negate(); + d_simp_quant = Rewriter::rewrite(d_simp_quant); + d_simp_quant = nm->mkNode(FORALL, q[0], d_simp_quant, q[2]); + Trace("cegqi-si") << "Rewritten quantifier : " << d_simp_quant << std::endl; + + // construct template argument + d_templ_arg[prog] = nm->mkSkolem("I", invariant.getType()); + + // construct template + Node templ; + if (options::sygusInvAutoUnfold()) + { + if (d_ti[q].isComplete()) + { + Trace("cegqi-inv-auto-unfold") + << "Automatic deterministic unfolding... " << std::endl; + // auto-unfold + DetTrace dt; + int init_dt = d_ti[q].initializeTrace(dt); + if (init_dt == 0) { - SygusInvTemplMode tmode = options::sygusInvTemplMode(); - if (tmode != SYGUS_INV_TEMPL_MODE_NONE) + Trace("cegqi-inv-auto-unfold") << " Init : "; + dt.print("cegqi-inv-auto-unfold"); + Trace("cegqi-inv-auto-unfold") << std::endl; + unsigned counter = 0; + unsigned status = 0; + while (counter < 100 && status == 0) { - // currently only works for single predicate synthesis - if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate()) - { - tmode = SYGUS_INV_TEMPL_MODE_NONE; - } - else if (!options::sygusInvTemplWhenSyntax()) - { - // only use invariant templates if no syntactic restrictions - if (CegGrammarConstructor::hasSyntaxRestrictions(q)) - { - tmode = SYGUS_INV_TEMPL_MODE_NONE; - } - } + status = d_ti[q].incrementTrace(dt); + counter++; + Trace("cegqi-inv-auto-unfold") << " #" << counter << " : "; + dt.print("cegqi-inv-auto-unfold"); + Trace("cegqi-inv-auto-unfold") + << "...status = " << status << std::endl; } - - if (tmode != SYGUS_INV_TEMPL_MODE_NONE) + if (status == 1) { - //if we are doing invariant templates, then construct the template - Trace("cegqi-si") << "- Do transition inference..." << std::endl; - d_ti[q].process( qq ); - Trace("cegqi-inv") << std::endl; - if( !d_ti[q].d_func.isNull() ){ - // map the program back via non-single invocation map - Node prog = d_ti[q].d_func; - std::vector< Node > prog_templ_vars; - prog_templ_vars.insert( prog_templ_vars.end(), d_ti[q].d_vars.begin(), d_ti[q].d_vars.end() ); - d_trans_pre[prog] = d_ti[q].getComponent( 1 ); - d_trans_post[prog] = d_ti[q].getComponent( -1 ); - Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl; - Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; - std::vector<Node> sivars; - d_sip->getSingleInvocationVariables(sivars); - Node invariant = d_sip->getFunctionInvocationFor(prog); - Assert(!invariant.isNull()); - invariant = invariant.substitute(sivars.begin(), - sivars.end(), - prog_templ_vars.begin(), - prog_templ_vars.end()); - Trace("cegqi-inv") << " invariant : " << invariant << std::endl; - - // store simplified version of quantified formula - d_simp_quant = d_sip->getFullSpecification(); - std::vector< Node > new_bv; - for (unsigned j = 0, size = sivars.size(); j < size; j++) - { - new_bv.push_back( - NodeManager::currentNM()->mkBoundVar(sivars[j].getType())); - } - d_simp_quant = d_simp_quant.substitute( - sivars.begin(), sivars.end(), new_bv.begin(), new_bv.end()); - Assert( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ); - for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){ - new_bv.push_back( q[1][0][0][j] ); - } - d_simp_quant = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_bv ), d_simp_quant ).negate(); - d_simp_quant = Rewriter::rewrite( d_simp_quant ); - d_simp_quant = NodeManager::currentNM()->mkNode( kind::FORALL, q[0], d_simp_quant, q[2] ); - Trace("cegqi-si") << "Rewritten quantifier : " << d_simp_quant << std::endl; - - //construct template argument - d_templ_arg[prog] = NodeManager::currentNM()->mkSkolem( "I", invariant.getType() ); - - //construct template - Node templ; - if( options::sygusInvAutoUnfold() ){ - if( d_ti[q].isComplete() ){ - Trace("cegqi-inv-auto-unfold") << "Automatic deterministic unfolding... " << std::endl; - // auto-unfold - DetTrace dt; - int init_dt = d_ti[q].initializeTrace( dt ); - if( init_dt==0 ){ - Trace("cegqi-inv-auto-unfold") << " Init : "; - dt.print("cegqi-inv-auto-unfold"); - Trace("cegqi-inv-auto-unfold") << std::endl; - unsigned counter = 0; - unsigned status = 0; - while( counter<100 && status==0 ){ - status = d_ti[q].incrementTrace( dt ); - counter++; - Trace("cegqi-inv-auto-unfold") << " #" << counter << " : "; - dt.print("cegqi-inv-auto-unfold"); - Trace("cegqi-inv-auto-unfold") << "...status = " << status << std::endl; - } - if( status==1 ){ - // we have a trivial invariant - templ = d_ti[q].constructFormulaTrace( dt ); - Trace("cegqi-inv") << "By finite deterministic terminating trace, a solution invariant is : " << std::endl; - Trace("cegqi-inv") << " " << templ << std::endl; - // FIXME : this should be unnecessary - templ = NodeManager::currentNM()->mkNode( AND, templ, d_templ_arg[prog] ); - } - }else{ - Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl; - } - } - } - Trace("cegqi-inv") << "Make the template... " << tmode << " " - << templ << std::endl; - if( templ.isNull() ){ - if (tmode == SYGUS_INV_TEMPL_MODE_PRE) - { - //d_templ[prog] = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] ); - templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], d_templ_arg[prog] ); - }else{ - Assert(tmode == SYGUS_INV_TEMPL_MODE_POST); - //d_templ[prog] = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) ); - templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], d_templ_arg[prog] ); - } - } - Trace("cegqi-inv") << " template (pre-substitution) : " << templ << std::endl; - Assert( !templ.isNull() ); - // subsitute the template arguments - Assert(prog_templ_vars.size() == prog_vars[prog].size()); - templ = templ.substitute( prog_templ_vars.begin(), prog_templ_vars.end(), prog_vars[prog].begin(), prog_vars[prog].end() ); - Trace("cegqi-inv") << " template : " << templ << std::endl; - d_templ[prog] = templ; - } + // we have a trivial invariant + templ = d_ti[q].constructFormulaTrace(dt); + Trace("cegqi-inv") << "By finite deterministic terminating trace, a " + "solution invariant is : " + << std::endl; + Trace("cegqi-inv") << " " << templ << std::endl; + // this should be unnecessary + templ = nm->mkNode(AND, templ, d_templ_arg[prog]); } - }else{ - //we are fully single invocation - d_single_invocation = true; } + else + { + Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl; + } + } + } + Trace("cegqi-inv") << "Make the template... " << tmode << " " << templ + << std::endl; + if (templ.isNull()) + { + if (tmode == SYGUS_INV_TEMPL_MODE_PRE) + { + templ = nm->mkNode(OR, d_trans_pre[prog], d_templ_arg[prog]); + } + else + { + Assert(tmode == SYGUS_INV_TEMPL_MODE_POST); + templ = nm->mkNode(AND, d_trans_post[prog], d_templ_arg[prog]); } } + Trace("cegqi-inv") << " template (pre-substitution) : " << templ + << std::endl; + Assert(!templ.isNull()); + // subsitute the template arguments + Assert(prog_templ_vars.size() == prog_vars[prog].size()); + templ = templ.substitute(prog_templ_vars.begin(), + prog_templ_vars.end(), + prog_vars[prog].begin(), + prog_vars[prog].end()); + Trace("cegqi-inv") << " template : " << templ << std::endl; + d_templ[prog] = templ; } void CegSingleInv::finishInit(bool syntaxRestricted) |