Add quantifier name attribute. (#1756)

1 files changed, 19 insertions, 2 deletions

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