diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_attributes.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 17 |
1 files changed, 17 insertions, 0 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; |