diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-08 14:36:20 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-08 14:36:20 -0500 |
commit | 741b11e0a2572e5ddf2e135a11db28154c5face7 (patch) | |
tree | 01bdbe6c55be84b6446d286fb8d6e3f6af6cfe91 /src/theory/quantifiers | |
parent | 67d245bfe914ae2594ecad8a9140d468270adf88 (diff) |
Add quantifier name attribute. (#1756)
Diffstat (limited to 'src/theory/quantifiers')
-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/theory_quantifiers.cpp | 1 |
4 files changed, 38 insertions, 3 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/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 ); |