diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/single_inv_partition.cpp | 39 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 79 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.h | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 1 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 |
8 files changed, 126 insertions, 49 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index d1a420e3d..0e8dfc9f4 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -29,6 +29,11 @@ namespace CVC4 { namespace theory { namespace quantifiers { +bool QAttributes::isStandard() const +{ + return !d_sygus && !d_quant_elim && !isFunDef() && d_name.isNull(); +} + QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) : d_quantEngine(qe) { @@ -52,6 +57,12 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve Trace("quant-attr-debug") << "Set sygus " << n << std::endl; SygusAttribute ca; n.setAttribute( ca, true ); + } + else if (attr == "quant-name") + { + Trace("quant-attr-debug") << "Set quant-name " << n << std::endl; + QuantNameAttribute qna; + n.setAttribute(qna, true); } else if (attr == "sygus-synth-grammar") { Assert( node_values.size()==1 ); Trace("quant-attr-debug") << "Set sygus synth grammar " << n << " to " @@ -265,6 +276,12 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ Trace("quant-attr") << "Attribute : sygus : " << q << std::endl; qa.d_sygus = true; } + if (avar.getAttribute(QuantNameAttribute())) + { + Trace("quant-attr") << "Attribute : quantifier name : " << avar + << " for " << q << std::endl; + qa.d_name = avar; + } if( avar.getAttribute(SynthesisAttribute()) ){ Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl; qa.d_synthesis = true; diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 87315de7c..fcb519712 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -51,6 +51,12 @@ typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAtt struct SygusAttributeId {}; typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute; +/**Attribute to give names to quantified formulas */ +struct QuantNameAttributeId +{ +}; +typedef expr::Attribute<QuantNameAttributeId, bool> QuantNameAttribute; + /** Attribute true for quantifiers that are synthesis conjectures */ struct SynthesisAttributeId {}; typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute; @@ -112,12 +118,23 @@ struct QAttributes /** the instantiation pattern list for this quantified formula (its 3rd child) */ Node d_ipl; + /** the name of this quantified formula */ + Node d_name; /** the quantifier id associated with this formula */ Node d_qid_num; /** is this quantified formula a rewrite rule? */ - bool isRewriteRule() { return !d_rr.isNull(); } + bool isRewriteRule() const { return !d_rr.isNull(); } /** is this quantified formula a function definition? */ - bool isFunDef() { return !d_fundef_f.isNull(); } + bool isFunDef() const { return !d_fundef_f.isNull(); } + /** + * Is this a standard quantifier? A standard quantifier is one that we can + * perform destructive updates (variable elimination, miniscoping, etc). + * + * A quantified formula is not standard if it is sygus, one for which + * we are performing quantifier elimination, is a function definition, or + * has a name. + */ + bool isStandard() const; }; /** This class caches information about attributes of quantified formulas diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index bc298fa9c..a8089d229 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1705,7 +1705,7 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& qa ){ bool is_strict_trigger = qa.d_hasPattern && options::userPatternsQuant()==USER_PAT_MODE_TRUST; - bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef() && !is_strict_trigger; + bool is_std = qa.isStandard() && !is_strict_trigger; if (computeOption == COMPUTE_ELIM_SYMBOLS) { return true; diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 890b7fcd3..0a0dac4ba 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -250,37 +250,28 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, // now must check if it has other bound variables std::vector<Node> bvs; TermUtil::getBoundVars(cr, bvs); - if (bvs.size() > d_si_vars.size()) + // bound variables must be contained in the single invocation variables + for (const Node& bv : bvs) { - // getBoundVars also collects functions in the rare case that we are - // synthesizing a function with 0 arguments - // take these into account below. - unsigned n_const_synth_fun = 0; - for (unsigned j = 0; j < bvs.size(); j++) + if (std::find(d_si_vars.begin(), d_si_vars.end(), bv) + == d_si_vars.end()) { - if (std::find(d_input_funcs.begin(), d_input_funcs.end(), bvs[j]) - != d_input_funcs.end()) + // getBoundVars also collects functions in the rare case that we are + // synthesizing a function with 0 arguments, take this into account + // here. + if (std::find(d_input_funcs.begin(), d_input_funcs.end(), bv) + == d_input_funcs.end()) { - n_const_synth_fun++; + Trace("si-prt") + << "...not ground single invocation." << std::endl; + ngroundSingleInvocation = true; + singleInvocation = false; } } - if (bvs.size() - n_const_synth_fun > d_si_vars.size()) - { - Trace("si-prt") << "...not ground single invocation." << std::endl; - ngroundSingleInvocation = true; - singleInvocation = false; - } - else - { - Trace("si-prt") << "...ground single invocation : success, after " - "removing 0-arg synth functions." - << std::endl; - } } - else + if (singleInvocation) { - Trace("si-prt") << "...ground single invocation : success." - << std::endl; + Trace("si-prt") << "...ground single invocation" << std::endl; } } else diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 322d49af6..b6a780b6c 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -87,9 +87,10 @@ void CegGrammarConstructor::collectTerms( Node n, std::map< TypeNode, std::vecto } while (!visit.empty()); } - - -Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, std::map< Node, Node >& templates_arg ) { +Node CegGrammarConstructor::process(Node q, + const std::map<Node, Node>& templates, + const std::map<Node, Node>& templates_arg) +{ // convert to deep embedding and finalize single invocation here // now, construct the grammar Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl; @@ -101,10 +102,7 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, NodeManager* nm = NodeManager::currentNM(); - std::vector< Node > qchildren; - std::map< Node, Node > synth_fun_vars; std::vector< Node > ebvl; - Node qbody_subs = q[1]; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ Node sf = q[0][i]; // if non-null, v encodes the syntactic restrictions (via an inductive @@ -161,19 +159,68 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, // normalize type SygusGrammarNorm sygus_norm(d_qe); tn = sygus_norm.normalizeSygusType(tn, sfvl); - // check if there is a template - std::map< Node, Node >::iterator itt = templates.find( sf ); + + std::map<Node, Node>::const_iterator itt = templates.find(sf); if( itt!=templates.end() ){ Node templ = itt->second; - TNode templ_arg = templates_arg[sf]; + std::map<Node, Node>::const_iterator itta = templates_arg.find(sf); + Assert(itta != templates_arg.end()); + TNode templ_arg = itta->second; Assert( !templ_arg.isNull() ); - Trace("cegqi-debug") << "Template for " << sf << " is : " << templ << " with arg " << templ_arg << std::endl; // if there is a template for this argument, make a sygus type on top of it if( options::sygusTemplEmbedGrammar() ){ + Trace("cegqi-debug") << "Template for " << sf << " is : " << templ + << " with arg " << templ_arg << std::endl; Trace("cegqi-debug") << " embed this template as a grammar..." << std::endl; tn = mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() ); - }else{ - // otherwise, apply it as a preprocessing pass + } + } + + // ev is the first-order variable corresponding to this synth fun + std::stringstream ssf; + ssf << "f" << sf; + Node ev = nm->mkBoundVar(ssf.str(), tn); + ebvl.push_back(ev); + Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev + << std::endl; + } + return process(q, templates, templates_arg, ebvl); +} + +Node CegGrammarConstructor::process(Node q, + const std::map<Node, Node>& templates, + const std::map<Node, Node>& templates_arg, + const std::vector<Node>& ebvl) +{ + Assert(q[0].getNumChildren() == ebvl.size()); + + NodeManager* nm = NodeManager::currentNM(); + + std::vector<Node> qchildren; + Node qbody_subs = q[1]; + std::map<Node, Node> synth_fun_vars; + for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++) + { + Node sf = q[0][i]; + synth_fun_vars[sf] = ebvl[i]; + Node sfvl = getSygusVarList(sf); + TypeNode tn = ebvl[i].getType(); + // check if there is a template + std::map<Node, Node>::const_iterator itt = templates.find(sf); + if (itt != templates.end()) + { + Node templ = itt->second; + std::map<Node, Node>::const_iterator itta = templates_arg.find(sf); + Assert(itta != templates_arg.end()); + TNode templ_arg = itta->second; + Assert(!templ_arg.isNull()); + // if there is a template for this argument, make a sygus type on top of + // it + if (!options::sygusTemplEmbedGrammar()) + { + // otherwise, apply it as a preprocessing pass + Trace("cegqi-debug") << "Template for " << sf << " is : " << templ + << " with arg " << templ_arg << std::endl; Trace("cegqi-debug") << " apply this template as a substituion during preprocess..." << std::endl; std::vector< Node > schildren; std::vector< Node > largs; @@ -212,14 +259,6 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, if( !dt.getSygusAllowAll() ){ d_is_syntax_restricted = true; } - - // ev is the first-order variable corresponding to this synth fun - std::stringstream ssf; - ssf << "f" << sf; - Node ev = nm->mkBoundVar(ssf.str(), tn); - ebvl.push_back( ev ); - synth_fun_vars[sf] = ev; - Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl; } qchildren.push_back(nm->mkNode(kind::BOUND_VAR_LIST, ebvl)); if( qbody_subs!=q[1] ){ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 16f4672b0..39f95527f 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -35,6 +35,7 @@ public: 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 @@ -48,8 +49,17 @@ public: * for some t if !templates[i].isNull(). */ Node process(Node q, - std::map<Node, Node>& templates, - std::map<Node, Node>& templates_arg); + const std::map<Node, Node>& templates, + const std::map<Node, Node>& templates_arg); + /** + * Same as above, but we have already determined that the set of first-order + * datatype variables that will quantify the deep embedding conjecture are + * the vector ebvl. + */ + Node process(Node q, + const std::map<Node, Node>& templates, + const std::map<Node, Node>& templates_arg, + const std::vector<Node>& ebvl); /** is the syntax restricted? */ bool isSyntaxRestricted() { return d_is_syntax_restricted; } /** does the syntax allow ITE expressions? */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index f4e44ff2f..74d8269f9 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -44,6 +44,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output out.handleUserAttribute( "conjecture", this ); out.handleUserAttribute( "fun-def", this ); out.handleUserAttribute( "sygus", this ); + out.handleUserAttribute("quant-name", this); out.handleUserAttribute("sygus-synth-grammar", this); out.handleUserAttribute( "sygus-synth-fun-var-list", this ); out.handleUserAttribute( "synthesis", this ); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f3489f5ad..de71a8b5e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -393,6 +393,8 @@ void TheoryEngine::preRegister(TNode preprocessed) { d_sharedTerms.addEqualityToPropagate(preprocessed); } + // the atom should not have free variables + Assert(!preprocessed.hasFreeVar()); // Pre-register the terms in the atom Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed); theories = Theory::setRemove(THEORY_BOOL, theories); |