Allow E-matching by default when strings are enabled (#5117)

This does not disable E-matching when strings are enabled with --strings-exp, due to potential applications where strings are combined with user-provided quantified formulas.

Notice that by default, we do not want E-matching applied to quantified formulas corresponding to reductions for extended string functions. To correct this, all quantified formulas generated by strings are marked with an "internal quantified formula" attribute, which causes E-matching to ignore them. This feature can in theory be generalized later for other internal sources of quantified formulas.

4 files changed, 120 insertions, 43 deletions

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index a00ac6c86..ad9c53e0f 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -18,19 +18,21 @@
 #include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
 using namespace CVC4::theory::inst;
 
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
 InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe)
     : QuantifiersModule(qe),
       d_instStrategies(),
@@ -123,42 +125,64 @@ void InstantiationEngine::reset_round( Theory::Effort e ){
 void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
 {
   CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time);
-  if (quant_e == QEFFORT_STANDARD)
+  if (quant_e != QEFFORT_STANDARD)
   {
-    double clSet = 0;
-    if( Trace.isOn("inst-engine") ){
-      clSet = double(clock())/double(CLOCKS_PER_SEC);
-      Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
-    }
-    //collect all active quantified formulas belonging to this
-    bool quantActive = false;
-    d_quants.clear();
-    for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-      Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
-      if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
-        quantActive = true;
-        d_quants.push_back( q );
-      }
+    return;
+  }
+  double clSet = 0;
+  if (Trace.isOn("inst-engine"))
+  {
+    clSet = double(clock()) / double(CLOCKS_PER_SEC);
+    Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e
+                         << "---" << std::endl;
+  }
+  // collect all active quantified formulas belonging to this
+  bool quantActive = false;
+  d_quants.clear();
+  FirstOrderModel* m = d_quantEngine->getModel();
+  size_t nquant = m->getNumAssertedQuantifiers();
+  for (size_t i = 0; i < nquant; i++)
+  {
+    Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true);
+    if (shouldProcess(q) && m->isQuantifierActive(q))
+    {
+      quantActive = true;
+      d_quants.push_back(q);
     }
-    Trace("inst-engine-debug") << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/";
-    Trace("inst-engine-debug") << d_quantEngine->getModel()->getNumAssertedQuantifiers() << " " << quantActive << std::endl;
-    if( quantActive ){
-      unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
-      doInstantiationRound( e );
-      if( d_quantEngine->inConflict() ){
-        Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting);
-        Trace("inst-engine") << "Conflict, added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
-      }else if( d_quantEngine->hasAddedLemma() ){
-        Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting)  << std::endl;
-      }
-    }else{
-      d_quants.clear();
+  }
+  Trace("inst-engine-debug")
+      << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/";
+  Trace("inst-engine-debug") << nquant << " " << quantActive << std::endl;
+  if (quantActive)
+  {
+    unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+    doInstantiationRound(e);
+    if (d_quantEngine->inConflict())
+    {
+      Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting);
+      Trace("inst-engine") << "Conflict, added lemmas = "
+                           << (d_quantEngine->getNumLemmasWaiting()
+                               - lastWaiting)
+                           << std::endl;
     }
-    if( Trace.isOn("inst-engine") ){
-      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-      Trace("inst-engine") << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl;
+    else if (d_quantEngine->hasAddedLemma())
+    {
+      Trace("inst-engine") << "Added lemmas = "
+                           << (d_quantEngine->getNumLemmasWaiting()
+                               - lastWaiting)
+                           << std::endl;
     }
   }
+  else
+  {
+    d_quants.clear();
+  }
+  if (Trace.isOn("inst-engine"))
+  {
+    double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
+    Trace("inst-engine") << "Finished instantiation engine, time = "
+                         << (clSet2 - clSet) << std::endl;
+  }
 }
 
 bool InstantiationEngine::checkCompleteFor( Node q ) {
@@ -185,7 +209,7 @@ void InstantiationEngine::checkOwnership(Node q)
 
 void InstantiationEngine::registerQuantifier(Node q)
 {
-  if (!d_quantEngine->hasOwnership(q, this))
+  if (!shouldProcess(q))
   {
     return;
   }
@@ -225,3 +249,22 @@ void InstantiationEngine::addUserNoPattern(Node q, Node pat) {
     d_i_ag->addUserNoPattern(q, pat);
   }
 }
+
+bool InstantiationEngine::shouldProcess(Node q)
+{
+  if (!d_quantEngine->hasOwnership(q, this))
+  {
+    return false;
+  }
+  // also ignore internal quantifiers
+  QuantAttributes* qattr = d_quantEngine->getQuantAttributes();
+  if (qattr->isInternal(q))
+  {
+    return false;
+  }
+  return true;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 1bd3af99c..f2f013f1c 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -88,6 +88,8 @@ class InstantiationEngine : public QuantifiersModule {
   std::string identify() const override { return "InstEngine"; }
 
  private:
+  /** Return true if this module should process quantified formula q */
+  bool shouldProcess(Node q);
   /** for computing relevance of quantifiers */
   std::unique_ptr<QuantRelevance> d_quant_rel;
 }; /* class InstantiationEngine */
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 8961a7c90..808137fd6 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -30,7 +30,8 @@ namespace quantifiers {
 
 bool QAttributes::isStandard() const
 {
-  return !d_sygus && !d_quant_elim && !isFunDef() && d_name.isNull();
+  return !d_sygus && !d_quant_elim && !isFunDef() && d_name.isNull()
+         && !d_isInternal;
 }
 
 QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) : 
@@ -250,6 +251,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()))
+        {
+          Trace("quant-attr") << "Attribute : internal : " << q << std::endl;
+          qa.d_isInternal = true;
+        }
         if( avar.hasAttribute(QuantIdNumAttribute()) ){
           qa.d_qid_num = avar;
           Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
@@ -304,6 +310,16 @@ bool QuantAttributes::isQuantElimPartial( Node q ) {
   }
 }
 
+bool QuantAttributes::isInternal(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 false;
+}
+
 Node QuantAttributes::getQuantName(Node q) const
 {
   std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index e9abbc9ed..88f291b2b 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -88,11 +88,24 @@ struct SygusVarToTermAttributeId
 typedef expr::Attribute<SygusVarToTermAttributeId, Node>
     SygusVarToTermAttribute;
 
-namespace quantifiers {
+/**
+ * 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;
 
-/** Attribute priority for rewrite rules */
-//struct RrPriorityAttributeId {};
-//typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute;
+namespace quantifiers {
 
 /** This struct stores attributes for a single quantified formula */
 struct QAttributes
@@ -103,7 +116,8 @@ struct QAttributes
         d_sygus(false),
         d_qinstLevel(-1),
         d_quant_elim(false),
-        d_quant_elim_partial(false)
+        d_quant_elim_partial(false),
+        d_isInternal(false)
   {
   }
   ~QAttributes(){}
@@ -123,6 +137,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;
   /** the instantiation pattern list for this quantified formula (its 3rd child)
    */
   Node d_ipl;
@@ -192,12 +208,12 @@ public:
   bool isSygus( Node q );
   /** get instantiation level */
   int getQuantInstLevel( Node q );
-  /** get rewrite rule priority */
-  int getRewriteRulePriority( Node q );
   /** is quant elim */
   bool isQuantElim( Node q );
   /** is quant elim partial */
   bool isQuantElimPartial( Node q );
+  /** is internal quantifier */
+  bool isInternal(Node q) const;
   /** get quant name, which is used for :qid */
   Node getQuantName(Node q) const;
   /** get (internal) quant id num */