From ee0701f8c94b659594b033fa218b588a0d23acd7 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 3 Feb 2015 00:21:52 +0100 Subject: [PATCH] Solutions for single invocation conjectures. --- .../quantifiers/ce_guided_single_inv.cpp | 105 +++++++++++++----- 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; 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; ifirst.isNull() ){ // apply substitution for skolem variables std::vector< Node > vars; - d_single_inv_arg_sk.clear(); + std::vector< Node > sks; for( unsigned j=0; jfirst.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 > 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; ksecond.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; imkNode( FORALL, pbvl, bd ); + Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; + /* + //equality resolution + for( unsigned j=0; j > 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; ksecond.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 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 >& 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 ); -- 2.30.2