From 741b11e0a2572e5ddf2e135a11db28154c5face7 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 8 Apr 2018 14:36:20 -0500
Subject: [PATCH] Add quantifier name attribute. (#1756)

---
 .../quantifiers/quantifiers_attributes.cpp    | 17 +++++++++++++++
 .../quantifiers/quantifiers_attributes.h      | 21 +++++++++++++++++--
 .../quantifiers/quantifiers_rewriter.cpp      |  2 +-
 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 );
-- 
2.30.2