Move quantifiers attributes to quantifiers registry (#5929)

This moves the utility class beneath quantifiers registry.

12 files changed, 71 insertions, 19 deletions

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index e4881b112..442532e82 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -469,7 +469,8 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
 bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
   Assert(!d_curr_quant.isNull());
   //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
-  if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){
+  if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant))
+  {
     d_cbqi_set_quant_inactive = true;
     d_incomplete_check = true;
     d_quantEngine->getInstantiate()->recordInstantiation(
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 3e344f7fb..0d1f1ec18 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -263,8 +263,8 @@ bool InstantiationEngine::shouldProcess(Node q)
     return false;
   }
   // also ignore internal quantifiers
-  QuantAttributes* qattr = d_quantEngine->getQuantAttributes();
-  if (qattr->isInternal(q))
+  QuantAttributes& qattr = d_qreg.getQuantAttributes();
+  if (qattr.isInternal(q))
   {
     return false;
   }
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 8d9cfd3a3..d8d3aa098 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -51,8 +51,8 @@ Trigger::Trigger(QuantifiersEngine* qe,
   }
   if (Trace.isOn("trigger"))
   {
-    quantifiers::QuantAttributes* qa = d_quantEngine->getQuantAttributes();
-    Trace("trigger") << "Trigger for " << qa->quantToString(q) << ": "
+    quantifiers::QuantAttributes& qa = d_qreg.getQuantAttributes();
+    Trace("trigger") << "Trigger for " << qa.quantToString(q) << ": "
                      << std::endl;
     for (const Node& n : d_nodes)
     {
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index ad5d5dba7..ac43cb5d0 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -263,7 +263,8 @@ bool QuantAttributes::isSygus( Node q ) {
   }
 }
 
-int QuantAttributes::getQuantInstLevel( Node q ) {
+int64_t QuantAttributes::getQuantInstLevel(Node q)
+{
   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
   if( it==d_qattr.end() ){
     return -1;
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 740588b84..4322a3e88 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -139,7 +139,7 @@ struct QAttributes
   Node d_sygusSideCondition;
   /** stores the maximum instantiation level allowed for this quantified formula
    * (-1 means allow any) */
-  int d_qinstLevel;
+  int64_t d_qinstLevel;
   /** is this formula marked for quantifier elimination? */
   bool d_quant_elim;
   /** is this formula marked for partial quantifier elimination? */
@@ -214,7 +214,7 @@ class QuantAttributes
   /** is sygus conjecture */
   bool isSygus( Node q );
   /** get instantiation level */
-  int getQuantInstLevel( Node q );
+  int64_t getQuantInstLevel(Node q);
   /** is quant elim */
   bool isQuantElim( Node q );
   /** is quant elim partial */
diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp
index e6d4c75fe..19da90a12 100644
--- a/src/theory/quantifiers/quantifiers_registry.cpp
+++ b/src/theory/quantifiers/quantifiers_registry.cpp
@@ -21,6 +21,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+QuantifiersRegistry::QuantifiersRegistry() : d_quantAttr() {}
+
 void QuantifiersRegistry::registerQuantifier(Node q)
 {
   if (d_inst_constants.find(q) != d_inst_constants.end())
@@ -44,6 +46,8 @@ void QuantifiersRegistry::registerQuantifier(Node q)
     InstConstantAttribute ica;
     ic.setAttribute(ica, q);
   }
+  // compute attributes
+  d_quantAttr.computeAttributes(q);
 }
 
 bool QuantifiersRegistry::reset(Theory::Effort e) { return true; }
@@ -169,6 +173,27 @@ Node QuantifiersRegistry::substituteInstConstants(Node n,
                       terms.end());
 }
 
+QuantAttributes& QuantifiersRegistry::getQuantAttributes()
+{
+  return d_quantAttr;
+}
+Node QuantifiersRegistry::getNameForQuant(Node q) const
+{
+  Node name = d_quantAttr.getQuantName(q);
+  if (!name.isNull())
+  {
+    return name;
+  }
+  return q;
+}
+
+bool QuantifiersRegistry::getNameForQuant(Node q, Node& name, bool req) const
+{
+  name = getNameForQuant(q);
+  // if we have a name, or we did not require one
+  return name != q || !req;
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h
index b89a2c01b..66e1aee75 100644
--- a/src/theory/quantifiers/quantifiers_registry.h
+++ b/src/theory/quantifiers/quantifiers_registry.h
@@ -19,6 +19,7 @@
 
 #include "expr/node.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 
 namespace CVC4 {
 namespace theory {
@@ -39,7 +40,7 @@ class QuantifiersRegistry : public QuantifiersUtil
   friend class Instantiate;
 
  public:
-  QuantifiersRegistry() {}
+  QuantifiersRegistry();
   ~QuantifiersRegistry() {}
   /**
    * Register quantifier, which allocates the instantiation constants for q.
@@ -84,6 +85,19 @@ class QuantifiersRegistry : public QuantifiersUtil
   /** substitute { instantiation constants of q -> terms } in n */
   Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms);
   //----------------------------- end instantiation constants
+  /** Get quantifiers attributes utility class */
+  QuantAttributes& getQuantAttributes();
+  /**
+   * Get quantifiers name, which returns a variable corresponding to the name of
+   * quantified formula q if q has a name, or otherwise returns q itself.
+   */
+  Node getNameForQuant(Node q) const;
+  /**
+   * Get name for quantified formula. Returns true if q has a name or if req
+   * is false. Sets name to the result of the above method.
+   */
+  bool getNameForQuant(Node q, Node& name, bool req = true) const;
+
  private:
   /**
    * Maps quantified formulas to the module that owns them, if any module has
@@ -104,6 +118,8 @@ class QuantifiersRegistry : public QuantifiersUtil
   std::map<Node, Node> d_inst_constants_map;
   /** map from universal quantifiers to the list of instantiation constants */
   std::map<Node, std::vector<Node> > d_inst_constants;
+  /** The quantifiers attributes class */
+  QuantAttributes d_quantAttr;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 909a9aecc..723f11979 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -43,10 +43,12 @@ namespace quantifiers {
 SynthConjecture::SynthConjecture(QuantifiersEngine* qe,
                                  QuantifiersState& qs,
                                  QuantifiersInferenceManager& qim,
+                                 QuantifiersRegistry& qr,
                                  SygusStatistics& s)
     : d_qe(qe),
       d_qstate(qs),
       d_qim(qim),
+      d_qreg(qr),
       d_stats(s),
       d_tds(qe->getTermDatabaseSygus()),
       d_hasSolution(false),
@@ -223,7 +225,7 @@ void SynthConjecture::assign(Node q)
     Assert(d_master != nullptr);
   }
 
-  Assert(d_qe->getQuantAttributes()->isSygus(q));
+  Assert(d_qreg.getQuantAttributes().isSygus(q));
   // if the base instantiation is an existential, store its variables
   if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL)
   {
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index ca3f2983b..85f2783a9 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -85,6 +85,7 @@ class SynthConjecture
   SynthConjecture(QuantifiersEngine* qe,
                   QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
+                  QuantifiersRegistry& qr,
                   SygusStatistics& s);
   ~SynthConjecture();
   /** presolve */
@@ -206,6 +207,8 @@ class SynthConjecture
   QuantifiersState& d_qstate;
   /** Reference to the quantifiers inference manager */
   QuantifiersInferenceManager& d_qim;
+  /** The quantifiers registry */
+  QuantifiersRegistry& d_qreg;
   /** reference to the statistics of parent */
   SygusStatistics& d_stats;
   /** term database sygus of d_qe */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index e4c8c6cec..3aa782272 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -39,7 +39,7 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe,
       d_sqp(qe)
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
-      new SynthConjecture(d_quantEngine, qs, qim, d_statistics)));
+      new SynthConjecture(d_quantEngine, qs, qim, qr, d_statistics)));
   d_conj = d_conjs.back().get();
 }
 
@@ -159,8 +159,8 @@ void SynthEngine::assignConjecture(Node q)
   // allocate a new synthesis conjecture if not assigned
   if (d_conjs.back()->isAssigned())
   {
-    d_conjs.push_back(std::unique_ptr<SynthConjecture>(
-        new SynthConjecture(d_quantEngine, d_qstate, d_qim, d_statistics)));
+    d_conjs.push_back(std::unique_ptr<SynthConjecture>(new SynthConjecture(
+        d_quantEngine, d_qstate, d_qim, d_qreg, d_statistics)));
   }
   d_conjs.back()->assign(q);
 }
@@ -169,8 +169,8 @@ void SynthEngine::checkOwnership(Node q)
 {
   // take ownership of quantified formulas with sygus attribute, and function
   // definitions when options::sygusRecFun is true.
-  QuantAttributes* qa = d_quantEngine->getQuantAttributes();
-  if (qa->isSygus(q) || (options::sygusRecFun() && qa->isFunDef(q)))
+  QuantAttributes& qa = d_qreg.getQuantAttributes();
+  if (qa.isSygus(q) || (options::sygusRecFun() && qa.isFunDef(q)))
   {
     d_qreg.setOwner(q, this, 2);
   }
@@ -184,7 +184,7 @@ void SynthEngine::registerQuantifier(Node q)
   {
     return;
   }
-  if (d_quantEngine->getQuantAttributes()->isFunDef(q))
+  if (d_qreg.getQuantAttributes().isFunDef(q))
   {
     Assert(options::sygusRecFun());
     // If it is a recursive function definition, add it to the function
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 28eb715a3..f111b23ce 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -936,7 +936,8 @@ bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
 {
   if( options::instMaxLevel()!=-1 ){
     if( n.hasAttribute(InstLevelAttribute()) ){
-      int fml = f.isNull() ? -1 : d_quantEngine->getQuantAttributes()->getQuantInstLevel( f );
+      int64_t fml =
+          f.isNull() ? -1 : d_qreg.getQuantAttributes().getQuantInstLevel(f);
       unsigned ml = fml>=0 ? fml : options::instMaxLevel();
 
       if( n.getAttribute(InstLevelAttribute())>ml ){
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 591b7f85f..036b63b27 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -42,9 +42,12 @@ typedef expr::Attribute<TermDepthAttributeId, uint64_t> TermDepthAttribute;
 struct ContainsUConstAttributeId {};
 typedef expr::Attribute<ContainsUConstAttributeId, uint64_t> ContainsUConstAttribute;
 
-//for quantifier instantiation level
+/**
+ * for quantifier instantiation level.
+ */
 struct QuantInstLevelAttributeId {};
-typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t> QuantInstLevelAttribute;
+typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t>
+    QuantInstLevelAttribute;
 
 /** Attribute for id number */
 struct QuantIdNumAttributeId {};