From: Andrew Reynolds Date: Tue, 7 Nov 2017 01:18:09 +0000 (-0600) Subject: Updates to interface for Sygus grammar construction. (#1323) X-Git-Tag: cvc5-1.0.0~5507 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aaab8e0be83c093e27e0e4d4843cdd1e80e1157b;p=cvc5.git Updates to interface for Sygus grammar construction. (#1323) * Updates to interface for grammar construction. * Minor * Format --- diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index 3af623f13..5af8eafc8 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -50,7 +50,7 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe) d_ceg_si = new CegConjectureSingleInv(qe, this); d_ceg_pbe = new CegConjecturePbe(qe, this); d_ceg_proc = new CegConjectureProcess(qe); - d_ceg_gc = new CegGrammarConstructor(qe); + d_ceg_gc = new CegGrammarConstructor(qe, this); } CegConjecture::~CegConjecture() { diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp index 6152417a5..f6b2ab07a 100644 --- a/src/theory/quantifiers/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus_grammar_cons.cpp @@ -18,6 +18,7 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" +#include "theory/quantifiers/ce_guided_conjecture.h" #include "theory/quantifiers/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -28,10 +29,10 @@ namespace CVC4 { namespace theory { namespace quantifiers { - -CegGrammarConstructor::CegGrammarConstructor( QuantifiersEngine * qe ) : -d_qe( qe ), d_is_syntax_restricted(false), d_has_ite(true){ - +CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe, + CegConjecture* p) + : d_qe(qe), d_parent(p), d_is_syntax_restricted(false), d_has_ite(true) +{ } void CegGrammarConstructor::collectTerms( Node n, std::map< TypeNode, std::vector< Node > >& consts ){ @@ -91,14 +92,30 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute()); // sfvl may be null for constant synthesis functions Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl; + TypeNode tn; std::stringstream ss; ss << sf; if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){ tn = v.getType(); }else{ + // check which arguments are irrelevant + std::unordered_set arg_irrelevant; + // TODO (#1210) : get arg irrelevant based on conjecture-specific analysis + std::unordered_set term_irrelevant; + // convert to term + for (std::unordered_set::iterator ita = arg_irrelevant.begin(); + ita != arg_irrelevant.end(); + ++ita) + { + unsigned arg = *ita; + Assert(arg < sfvl.getNumChildren()); + term_irrelevant.insert(sfvl[arg]); + } + // make the default grammar - tn = mkSygusDefaultType( v.getType(), sfvl, ss.str(), extra_cons ); + tn = mkSygusDefaultType( + v.getType(), sfvl, ss.str(), extra_cons, term_irrelevant); } // check if there is a template std::map< Node, Node >::iterator itt = templates.find( sf ); @@ -283,13 +300,31 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor( TypeNode range, std::ve } } -void CegGrammarConstructor::mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons, - std::vector< CVC4::Datatype >& datatypes, std::set& unres ) { +void CegGrammarConstructor::mkSygusDefaultGrammar( + TypeNode range, + Node bvl, + const std::string& fun, + std::map >& extra_cons, + std::unordered_set& term_irrelevant, + std::vector& datatypes, + std::set& unres) +{ + Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " " + << range << std::endl; // collect the variables std::vector sygus_vars; if( !bvl.isNull() ){ for( unsigned i=0; i > ops; int startIndex = -1; - Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " " << range << std::endl; std::map< Type, Type > sygus_to_builtin; std::vector< TypeNode > types; @@ -529,16 +563,21 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( TypeNode range, Node bvl, con } } - -TypeNode CegGrammarConstructor::mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, - std::map< TypeNode, std::vector< Node > >& extra_cons ) { +TypeNode CegGrammarConstructor::mkSygusDefaultType( + TypeNode range, + Node bvl, + const std::string& fun, + std::map >& extra_cons, + std::unordered_set& term_irrelevant) +{ Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl; for( std::map< TypeNode, std::vector< Node > >::iterator it = extra_cons.begin(); it != extra_cons.end(); ++it ){ Trace("sygus-grammar-def") << " ...using " << it->second.size() << " extra constants for " << it->first << std::endl; } std::set unres; std::vector< CVC4::Datatype > datatypes; - mkSygusDefaultGrammar( range, bvl, fun, extra_cons, datatypes, unres ); + mkSygusDefaultGrammar( + range, bvl, fun, extra_cons, term_irrelevant, datatypes, unres); Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl; Assert( !datatypes.empty() ); std::vector types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres); diff --git a/src/theory/quantifiers/sygus_grammar_cons.h b/src/theory/quantifiers/sygus_grammar_cons.h index e8b09293c..4e486f88f 100644 --- a/src/theory/quantifiers/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus_grammar_cons.h @@ -24,38 +24,72 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class CegConjecture; + /** utility for constructing datatypes that correspond to syntactic restrictions, * and applying the deep embedding from Section 4 of Reynolds et al CAV 2015. */ class CegGrammarConstructor { public: - CegGrammarConstructor( QuantifiersEngine * qe ); - ~CegGrammarConstructor(){} - /** convert node n based on deep embedding (Section 4 of Reynolds et al CAV 2015) */ - Node process( Node q, std::map< Node, Node >& templates, std::map< Node, Node >& templates_arg ); - /** is the syntax restricted? */ - bool isSyntaxRestricted() { return d_is_syntax_restricted; } - /** does the syntax allow ITE expressions? */ - bool hasSyntaxITE() { return d_has_ite; } - // make the default sygus datatype type corresponding to builtin type range - // bvl is the set of free variables to include in the grammar - // fun is for naming - // extra_cons is a set of extra constant symbols to include in the grammar - static TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons ); - // make the default sygus datatype type corresponding to builtin type range - static TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun ){ - std::map< TypeNode, std::vector< Node > > extra_cons; - return mkSygusDefaultType( range, bvl, fun, extra_cons ); + CegGrammarConstructor(QuantifiersEngine* qe, CegConjecture* p); + ~CegGrammarConstructor() {} + /** process + * This converts node q based on its deep embedding + * (Section 4 of Reynolds et al CAV 2015). + * The syntactic restrictions are associated with + * the functions-to-synthesize using the attribute + * SygusSynthGrammarAttribute. + * The arguments templates and template_args + * indicate templates for the function to synthesize, + * in particular the solution for the i^th function + * to synthesis must be of the form + * templates[i]{ templates_arg[i] -> t } + * for some t if !templates[i].isNull(). + */ + Node process(Node q, + std::map& templates, + std::map& templates_arg); + /** is the syntax restricted? */ + bool isSyntaxRestricted() { return d_is_syntax_restricted; } + /** does the syntax allow ITE expressions? */ + bool hasSyntaxITE() { return d_has_ite; } + /** make the default sygus datatype type corresponding to builtin type range + * bvl is the set of free variables to include in the grammar + * fun is for naming + * extra_cons is a set of extra constant symbols to include in the grammar + * term_irrelevant is a set of terms that should not be included in the + * grammar. + */ + static TypeNode mkSygusDefaultType( + TypeNode range, + Node bvl, + const std::string& fun, + std::map >& extra_cons, + std::unordered_set& term_irrelevant); + /** make the default sygus datatype type corresponding to builtin type range */ + static TypeNode mkSygusDefaultType(TypeNode range, + Node bvl, + const std::string& fun) + { + std::map > extra_cons; + std::unordered_set term_irrelevant; + return mkSygusDefaultType(range, bvl, fun, extra_cons, term_irrelevant); } - // make the sygus datatype type that encodes the solution space (lambda templ_arg. templ[templ_arg]) where templ_arg - // has syntactic restrictions encoded by sygus type templ_arg_sygus_type - // bvl is the set of free variables to include in the frammar - // fun is for naming + /** make the sygus datatype type that encodes the solution space (lambda + * templ_arg. templ[templ_arg]) where templ_arg + * has syntactic restrictions encoded by sygus type templ_arg_sygus_type + * bvl is the set of free variables to include in the grammar + * fun is for naming + */ static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun ); private: /** reference to quantifier engine */ QuantifiersEngine * d_qe; + /** parent conjecture + * This contains global information about the synthesis conjecture. + */ + CegConjecture* d_parent; /** is the syntax restricted? */ bool d_is_syntax_restricted; /** does the syntax allow ITE expressions? */ @@ -71,11 +105,19 @@ private: static void mkSygusConstantsForType( TypeNode type, std::vector& ops ); // collect the list of types that depend on type range static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ); - // helper function for function mkSygusDefaultGrammar - // collects a set of mutually recursive datatypes "datatypes" corresponding to encoding type "range" to SyGuS - // unres is used for the resulting call to mkMutualDatatypeTypes - static void mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons, - std::vector< CVC4::Datatype >& datatypes, std::set& unres ); + /** helper function for function mkSygusDefaultType + * Collects a set of mutually recursive datatypes "datatypes" corresponding to + * encoding type "range" to SyGuS. + * unres is used for the resulting call to mkMutualDatatypeTypes + */ + static void mkSygusDefaultGrammar( + TypeNode range, + Node bvl, + const std::string& fun, + std::map >& extra_cons, + std::unordered_set& term_irrelevant, + std::vector& datatypes, + std::set& unres); // helper function for mkSygusTemplateType static TypeNode mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun, unsigned& tcount );