Refactor internally generated bounded quantified formulas (#7291)

This changes the attribute on internally generated bounded quantified formulas from `isInternal` to `isQuantBounded`. This makes it clear that bounded integers is the module that should process them.  It also moves the utility for constructing these quantified formulas from strings to BoundedIntegers itself.  This is to accommodate other theories, e.g. bags, that may make use of reductions to bounded quantifiers.

6 files changed, 100 insertions, 37 deletions

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 17023e6b9..1f7d7f37b 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -262,7 +262,7 @@ bool InstantiationEngine::shouldProcess(Node q)
   }
   // also ignore internal quantifiers
   QuantAttributes& qattr = d_qreg.getQuantAttributes();
-  if (qattr.isInternal(q))
+  if (qattr.isQuantBounded(q))
   {
     return false;
   }
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index fbc6cde75..8ef6155c2 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -31,12 +31,12 @@
 #include "theory/rewriter.h"
 #include "util/rational.h"
 
-using namespace cvc5;
-using namespace std;
-using namespace cvc5::theory;
-using namespace cvc5::theory::quantifiers;
 using namespace cvc5::kind;
 
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
 BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic(
     Env& env, Node r, Valuation valuation, bool isProxy)
     : DecisionStrategyFmf(env, valuation),
@@ -323,9 +323,9 @@ void BoundedIntegers::checkOwnership(Node f)
   {
     // only applying it to internal quantifiers
     QuantAttributes& qattr = d_qreg.getQuantAttributes();
-    if (!qattr.isInternal(f))
+    if (!qattr.isQuantBounded(f))
     {
-      Trace("bound-int") << "...not internal, skip" << std::endl;
+      Trace("bound-int") << "...not bounded, skip" << std::endl;
       return;
     }
   }
@@ -895,3 +895,63 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
     return true;
   }
 }
+
+/**
+ * Attribute true for quantifiers that have been internally generated and
+ * should be processed with the bounded integers module, e.g. quantified
+ * formulas from reductions of string operators.
+ *
+ * Currently, this attribute is used for indicating that E-matching should
+ * not be applied, as E-matching should not be applied to quantifiers
+ * generated internally.
+ *
+ * This attribute can potentially be generalized to an identifier indicating
+ * the internal source of the quantified formula (of which strings reduction
+ * is one possibility).
+ */
+struct BoundedQuantAttributeId
+{
+};
+typedef expr::Attribute<BoundedQuantAttributeId, bool> BoundedQuantAttribute;
+/**
+ * Mapping to a dummy node for marking an attribute on internal quantified
+ * formulas. This ensures that reductions are deterministic.
+ */
+struct QInternalVarAttributeId
+{
+};
+typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
+
+Node BoundedIntegers::mkBoundedForall(Node bvl, Node body)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  QInternalVarAttribute qiva;
+  Node qvar;
+  if (bvl.hasAttribute(qiva))
+  {
+    qvar = bvl.getAttribute(qiva);
+  }
+  else
+  {
+    SkolemManager* sm = nm->getSkolemManager();
+    qvar = sm->mkDummySkolem("qinternal", nm->booleanType());
+    // this dummy variable marks that the quantified formula is internal
+    qvar.setAttribute(BoundedQuantAttribute(), true);
+    // remember the dummy variable
+    bvl.setAttribute(qiva, qvar);
+  }
+  // make the internal attribute, and put it in a singleton list
+  Node ip = nm->mkNode(INST_ATTRIBUTE, qvar);
+  Node ipl = nm->mkNode(INST_PATTERN_LIST, ip);
+  // make the overall formula
+  return nm->mkNode(FORALL, bvl, body, ipl);
+}
+
+bool BoundedIntegers::isBoundedForallAttribute(Node var)
+{
+  return var.getAttribute(BoundedQuantAttribute());
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 2c3a86fc7..6602961e9 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -216,6 +216,22 @@ private:
   /** Identify this module */
   std::string identify() const override { return "BoundedIntegers"; }
 
+  /**
+   * Make internal quantified formula with bound variable list bvl and body.
+   * Internally, we get a node corresponding to marking a quantified formula as
+   * a "bounded quantified formula". This node is provided as the third argument
+   * of the FORALL returned by this method. This ensures that E-matching is not
+   * applied to the quantified formula, and that this module is the one that
+   * handles it.
+   */
+  static Node mkBoundedForall(Node bvl, Node body);
+  /**
+   * Has this node been marked as an annotation for a bounded quantified
+   * formula? This is true for the annotation in the formula returned by the
+   * above method.
+   */
+  static bool isBoundedForallAttribute(Node var);
+
  private:
   /**
    * Set that variable v of quantified formula q has a finite bound, where
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 8e099b5a4..a8ad07734 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -360,6 +360,8 @@ bool ModelEngine::shouldProcess(Node q)
 {
   if (!d_qreg.hasOwnership(q, this))
   {
+    // if we don't have ownership, another module has taken responsibility
+    // for processing q.
     return false;
   }
   // if finite model finding or fmf bound is on, we process everything
@@ -367,10 +369,10 @@ bool ModelEngine::shouldProcess(Node q)
   {
     return true;
   }
-  // otherwise, we are only using model-based instantiation for internal
-  // quantified formulas
+  // otherwise, we are only using model-based instantiation for internally
+  // generated bounded quantified formulas
   QuantAttributes& qattr = d_qreg.getQuantAttributes();
-  return qattr.isInternal(q);
+  return qattr.isQuantBounded(q);
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 1a0e03bfc..18a039fbf 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -17,6 +17,7 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/term_util.h"
 #include "util/rational.h"
@@ -32,7 +33,7 @@ namespace quantifiers {
 
 bool QAttributes::isStandard() const
 {
-  return !d_sygus && !d_quant_elim && !isFunDef() && !d_isInternal;
+  return !d_sygus && !d_quant_elim && !isFunDef() && !d_isQuantBounded;
 }
 
 QuantAttributes::QuantAttributes() {}
@@ -297,10 +298,11 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
           qa.d_quant_elim_partial = true;
           //don't set owner, should happen naturally
         }
-        if (avar.getAttribute(InternalQuantAttribute()))
+        if (BoundedIntegers::isBoundedForallAttribute(avar))
         {
-          Trace("quant-attr") << "Attribute : internal : " << q << std::endl;
-          qa.d_isInternal = true;
+          Trace("quant-attr")
+              << "Attribute : bounded quantifiers : " << q << std::endl;
+          qa.d_isQuantBounded = true;
         }
         if( avar.hasAttribute(QuantIdNumAttribute()) ){
           qa.d_qid_num = avar;
@@ -357,12 +359,12 @@ bool QuantAttributes::isQuantElimPartial( Node q ) {
   }
 }
 
-bool QuantAttributes::isInternal(Node q) const
+bool QuantAttributes::isQuantBounded(Node q) const
 {
   std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
   if (it != d_qattr.end())
   {
-    return it->second.d_isInternal;
+    return it->second.d_isQuantBounded;
   }
   return false;
 }
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index cb25546dd..53f59b0e5 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -94,23 +94,6 @@ struct AbsTypeFunDefAttributeId
 };
 typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute;
 
-/**
- * Attribute true for quantifiers that have been internally generated, e.g.
- * for reductions of string operators.
- *
- * Currently, this attribute is used for indicating that E-matching should
- * not be applied, as E-matching should not be applied to quantifiers
- * generated for strings reductions.
- *
- * This attribute can potentially be generalized to an identifier indicating
- * the internal source of the quantified formula (of which strings reduction
- * is one possibility).
- */
-struct InternalQuantAttributeId
-{
-};
-typedef expr::Attribute<InternalQuantAttributeId, bool> InternalQuantAttribute;
-
 namespace quantifiers {
 
 /** This struct stores attributes for a single quantified formula */
@@ -124,7 +107,7 @@ struct QAttributes
         d_qinstLevel(-1),
         d_quant_elim(false),
         d_quant_elim_partial(false),
-        d_isInternal(false)
+        d_isQuantBounded(false)
   {
   }
   ~QAttributes(){}
@@ -146,8 +129,8 @@ struct QAttributes
   bool d_quant_elim;
   /** is this formula marked for partial quantifier elimination? */
   bool d_quant_elim_partial;
-  /** Is this formula internally generated? */
-  bool d_isInternal;
+  /** Is this formula internally generated and belonging to bounded integers? */
+  bool d_isQuantBounded;
   /** the instantiation pattern list for this quantified formula (its 3rd child)
    */
   Node d_ipl;
@@ -222,7 +205,7 @@ class QuantAttributes
   /** is quant elim partial */
   bool isQuantElimPartial( Node q );
   /** is internal quantifier */
-  bool isInternal(Node q) const;
+  bool isQuantBounded(Node q) const;
   /** get quant name, which is used for :qid */
   Node getQuantName(Node q) const;
   /** Print quantified formula q, possibly using its name, if it has one */