diff options
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 105 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 10 |
2 files changed, 85 insertions, 30 deletions
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index efe23d6cb..c3ca5cfe6 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -125,13 +125,14 @@ void CegConjectureSingleInv::initialize() { Trace("cegqi-si-debug2") << "Make variable " << pv << " for " << prog << std::endl; for( unsigned k=1; k<inv.getNumChildren(); k++ ){ Assert( !single_invoke_args[prog][k-1].empty() ); - if( single_invoke_args[prog][k-1].size()==1 ){ + if( single_invoke_args[prog][k-1].size()==1 && single_invoke_args[prog][k-1][0].getKind()==BOUND_VARIABLE ){ invc.push_back( single_invoke_args[prog][k-1][0] ); }else{ //introduce fresh variable, assign all Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" ); new_vars.push_back( v ); invc.push_back( v ); + d_single_inv_arg_sk.push_back( v ); for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){ Node arg = single_invoke_args[prog][k-1][i]; @@ -207,36 +208,60 @@ void CegConjectureSingleInv::initialize() { if( !it->first.isNull() ){ // apply substitution for skolem variables std::vector< Node > vars; - d_single_inv_arg_sk.clear(); + std::vector< Node > sks; for( unsigned j=0; j<it->first.getNumChildren(); j++ ){ std::stringstream ss; - ss << "k_" << it->first[j]; + 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] ); - d_single_inv_arg_sk.push_back( v ); + sks.push_back( v ); + } + bd = bd.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() ); + for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ + Node n = itam->second; + d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); } - bd = bd.substitute( vars.begin(), vars.end(), d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() ); Trace("cegqi-si-debug") << " -> " << bd << std::endl; } - d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); - //equality resolution - for( unsigned j=0; j<tmp.size(); j++ ){ - Node conj = tmp[j]; - std::map< Node, std::vector< Node > > case_vals; - bool exh = processSingleInvLiteral( conj, false, case_vals ); - Trace("cegqi-si-er") << "Conjunct " << conj << " gives equality restrictions, exh = " << exh << " : " << std::endl; - for( std::map< Node, std::vector< Node > >::iterator it = case_vals.begin(); it != case_vals.end(); ++it ){ - Trace("cegqi-si-er") << " " << it->first << " -> "; - for( unsigned k=0; k<it->second.size(); k++ ){ - Trace("cegqi-si-er") << it->second[k] << " "; + for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ + Node n = itam->second; + //check if all variables are arguments of this + std::vector< Node > n_args; + for( unsigned i=1; i<n.getNumChildren(); i++ ){ + n_args.push_back( n[i] ); + } + for( unsigned i=0; i<d_single_inv_arg_sk.size(); i++ ){ + if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){ + Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain all variables." << std::endl; + singleInvocation = false; + //exit( 57 ); + break; + } + } + } + if( singleInvocation ){ + d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); + Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; + /* + //equality resolution + for( unsigned j=0; j<tmp.size(); j++ ){ + Node conj = tmp[j]; + std::map< Node, std::vector< Node > > case_vals; + bool exh = processSingleInvLiteral( conj, false, case_vals ); + Trace("cegqi-si-er") << "Conjunct " << conj << " gives equality restrictions, exh = " << exh << " : " << std::endl; + for( std::map< Node, std::vector< Node > >::iterator it = case_vals.begin(); it != case_vals.end(); ++it ){ + Trace("cegqi-si-er") << " " << it->first << " -> "; + for( unsigned k=0; k<it->second.size(); k++ ){ + Trace("cegqi-si-er") << it->second[k] << " "; + } + Trace("cegqi-si-er") << std::endl; } - Trace("cegqi-si-er") << std::endl; } - + */ } } - Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; }else{ Trace("cegqi-si") << "Property is not single invocation." << std::endl; if( options::cegqiSingleInvAbort() ){ @@ -338,7 +363,7 @@ bool CegConjectureSingleInv::analyzeSygusTerm( Node n, std::map< Node, std::vect void CegConjectureSingleInv::check( QuantifiersEngine * qe, std::vector< Node >& lems ) { - if( !d_single_inv.isNull() ) { + if( !d_single_inv.isNull() ) { eq::EqualityEngine* ee = qe->getMasterEqualityEngine(); Trace("cegqi-engine") << " * single invocation: " << std::endl; std::vector< Node > subs; @@ -349,7 +374,7 @@ void CegConjectureSingleInv::check( QuantifiersEngine * qe, std::vector< Node >& Node pv = d_single_inv_sk[i]; Trace("cegqi-engine") << " * " << v; Trace("cegqi-engine") << " (" << pv << ")"; - Trace("cegqi-engine") << " -> "; + Trace("cegqi-engine") << " -> "; Node slv; if( ee->hasTerm( pv ) ){ Node r = ee->getRepresentative( pv ); @@ -569,13 +594,41 @@ Node CegConjectureSingleInv::getSolution( unsigned i, Node varList ){ Assert( !d_lemmas_produced.empty() ); Node s = constructSolution( i, 0 ); //TODO : not in grammar + Node prog = d_quant[0][i]; + Node prog_app = d_single_inv_app_map[prog]; std::vector< Node > vars; - for( unsigned i=0; i<varList.getNumChildren(); i++ ){ - vars.push_back( varList[i] ); + std::vector< Node > subs; + Trace("cegqi-si-debug") << "Get solution for " << prog << ", which is applied as " << prog_app << std::endl; + Assert( prog_app.getNumChildren()==varList.getNumChildren()+1 ); + for( unsigned i=1; i<prog_app.getNumChildren(); i++ ){ + vars.push_back( prog_app[i] ); + subs.push_back( varList[i-1] ); } - Assert( vars.size()==d_single_inv_arg_sk.size() ); - s = s.substitute( d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end(), vars.begin(), vars.end() ); - return s; + s = s.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + if( Trace.isOn("cegqi-si-warn") ){ + //debug solution + if( !debugSolution( s ) ){ + Trace("cegqi-si-warn") << "WARNING : solution " << s << " contains free constants." << std::endl; + //exit( 47 ); + }else{ + //exit( 49 ); + } + } + return s; +} + +bool CegConjectureSingleInv::debugSolution( Node sol ) { + if( sol.getKind()==SKOLEM ){ + return false; + }else{ + for( unsigned i=0; i<sol.getNumChildren(); i++ ){ + if( !debugSolution( sol[i] ) ){ + return false; + } + } + return true; + } + } }
\ No newline at end of file diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 64c65a2fe..0c34490f8 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -29,18 +29,20 @@ class CegConjecture; class CegConjectureSingleInv { -private: +private: CegConjecture * d_parent; 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::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 ); bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ); - + Node constructSolution( unsigned i, unsigned index ); int classifyTerm( Node n, std::map< Node, int >& subs_from_model ); void collectProgVars( Node n, std::vector< Node >& vars ); Node applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs ); + + bool debugSolution( Node sol ); public: CegConjectureSingleInv( Node q, CegConjecture * p ); // original conjecture @@ -65,7 +67,7 @@ public: public: //get the single invocation lemma Node getSingleInvLemma( Node guard ); - //initialize + //initialize void initialize(); //check void check( QuantifiersEngine * qe, std::vector< Node >& lems ); |