diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-06 17:04:52 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-06 17:04:52 -0500 |
commit | dd84403eb19b769d80b4c57ae690ba14c02df041 (patch) | |
tree | aa63f0f909ecd7063e38f7121c17cafb431abdf4 /src/smt/smt_engine.cpp | |
parent | c87ee73ad3d51c238700f236c18e425b80e8e7ac (diff) |
Minor clean up, fixes related to sygus.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 125 |
1 files changed, 63 insertions, 62 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 021798132..3a138e4b7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4420,71 +4420,72 @@ Result SmtEngine::checkSynth(const Expr& e) throw(TypeCheckingException, ModalEx Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl; Expr e_check = e; Node conj = Node::fromExpr( e ); - Assert( conj.getKind()==kind::FORALL ); - //possibly run quantifier elimination to make formula into single invocation - if( conj[1].getKind()==kind::EXISTS ){ - Node conj_se = conj[1][1]; - - Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl; - quantifiers::SingleInvocationPartition sip( kind::APPLY ); - sip.init( conj_se ); - Trace("smt-synth") << "...finished, got:" << std::endl; - sip.debugPrint("smt-synth"); - - if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){ - //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f. - //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ), - // and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f. We invoke synthesis solver on this result. - - //create new smt engine to do quantifier elimination - SmtEngine smt_qe( d_exprManager ); - smt_qe.setLogic(getLogicInfo()); - Trace("smt-synth") << "Property is non-ground single invocation, run QE to obtain single invocation." << std::endl; - //partition variables - std::vector< Node > qe_vars; - std::vector< Node > nqe_vars; - for( unsigned i=0; i<sip.d_all_vars.size(); i++ ){ - Node v = sip.d_all_vars[i]; - if( std::find( sip.d_si_vars.begin(), sip.d_si_vars.end(), v )==sip.d_si_vars.end() ){ - qe_vars.push_back( v ); - }else{ - nqe_vars.push_back( v ); - } - } - std::vector< Node > orig; - std::vector< Node > subs; - //skolemize non-qe variables - for( unsigned i=0; i<nqe_vars.size(); i++ ){ - Node k = NodeManager::currentNM()->mkSkolem( "k", nqe_vars[i].getType(), "qe for non-ground single invocation" ); - orig.push_back( nqe_vars[i] ); - subs.push_back( k ); - Trace("smt-synth") << " subs : " << nqe_vars[i] << " -> " << k << std::endl; - } - for( std::map< Node, bool >::iterator it = sip.d_funcs.begin(); it != sip.d_funcs.end(); ++it ){ - orig.push_back( sip.d_func_inv[it->first] ); - Node k = NodeManager::currentNM()->mkSkolem( "k", sip.d_func_fo_var[it->first].getType(), "qe for function in non-ground single invocation" ); - subs.push_back( k ); - Trace("smt-synth") << " subs : " << sip.d_func_inv[it->first] << " -> " << k << std::endl; - } - Node conj_se_ngsi = sip.getFullSpecification(); - Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() ); - Assert( !qe_vars.empty() ); - conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs ); + if( conj.getKind()==kind::FORALL ){ + //possibly run quantifier elimination to make formula into single invocation + if( conj[1].getKind()==kind::EXISTS ){ + Node conj_se = conj[1][1]; + + Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl; + quantifiers::SingleInvocationPartition sip( kind::APPLY ); + sip.init( conj_se ); + Trace("smt-synth") << "...finished, got:" << std::endl; + sip.debugPrint("smt-synth"); - Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl; - Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false ); - Trace("smt-synth") << "Result : " << qe_res << std::endl; + if( !sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation() ){ + //We are in the case where our synthesis conjecture is exists f. forall xy. P( f( x ), x, y ), P does not contain f. + //The following will run QE on (exists z x.) exists y. P( z, x, y ) to obtain Q( z, x ), + // and then constructs exists f. forall x. Q( f( x ), x ), where Q does not contain f. We invoke synthesis solver on this result. - //create single invocation conjecture - Node qe_res_n = Node::fromExpr( qe_res ); - qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() ); - if( !nqe_vars.empty() ){ - qe_res_n = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, nqe_vars ), qe_res_n ); + //create new smt engine to do quantifier elimination + SmtEngine smt_qe( d_exprManager ); + smt_qe.setLogic(getLogicInfo()); + Trace("smt-synth") << "Property is non-ground single invocation, run QE to obtain single invocation." << std::endl; + //partition variables + std::vector< Node > qe_vars; + std::vector< Node > nqe_vars; + for( unsigned i=0; i<sip.d_all_vars.size(); i++ ){ + Node v = sip.d_all_vars[i]; + if( std::find( sip.d_si_vars.begin(), sip.d_si_vars.end(), v )==sip.d_si_vars.end() ){ + qe_vars.push_back( v ); + }else{ + nqe_vars.push_back( v ); + } + } + std::vector< Node > orig; + std::vector< Node > subs; + //skolemize non-qe variables + for( unsigned i=0; i<nqe_vars.size(); i++ ){ + Node k = NodeManager::currentNM()->mkSkolem( "k", nqe_vars[i].getType(), "qe for non-ground single invocation" ); + orig.push_back( nqe_vars[i] ); + subs.push_back( k ); + Trace("smt-synth") << " subs : " << nqe_vars[i] << " -> " << k << std::endl; + } + for( std::map< Node, bool >::iterator it = sip.d_funcs.begin(); it != sip.d_funcs.end(); ++it ){ + orig.push_back( sip.d_func_inv[it->first] ); + Node k = NodeManager::currentNM()->mkSkolem( "k", sip.d_func_fo_var[it->first].getType(), "qe for function in non-ground single invocation" ); + subs.push_back( k ); + Trace("smt-synth") << " subs : " << sip.d_func_inv[it->first] << " -> " << k << std::endl; + } + Node conj_se_ngsi = sip.getFullSpecification(); + Node conj_se_ngsi_subs = conj_se_ngsi.substitute( orig.begin(), orig.end(), subs.begin(), subs.end() ); + Assert( !qe_vars.empty() ); + conj_se_ngsi_subs = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, qe_vars ), conj_se_ngsi_subs ); + + Trace("smt-synth") << "Run quantifier elimination on " << conj_se_ngsi_subs << std::endl; + Expr qe_res = smt_qe.doQuantifierElimination( conj_se_ngsi_subs.toExpr(), true, false ); + Trace("smt-synth") << "Result : " << qe_res << std::endl; + + //create single invocation conjecture + Node qe_res_n = Node::fromExpr( qe_res ); + qe_res_n = qe_res_n.substitute( subs.begin(), subs.end(), orig.begin(), orig.end() ); + if( !nqe_vars.empty() ){ + qe_res_n = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, nqe_vars ), qe_res_n ); + } + Assert( conj.getNumChildren()==3 ); + qe_res_n = NodeManager::currentNM()->mkNode( kind::FORALL, conj[0], qe_res_n, conj[2] ); + Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n << std::endl; + e_check = qe_res_n.toExpr(); } - Assert( conj.getNumChildren()==3 ); - qe_res_n = NodeManager::currentNM()->mkNode( kind::FORALL, conj[0], qe_res_n, conj[2] ); - Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n << std::endl; - e_check = qe_res_n.toExpr(); } } |