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.

10 files changed, 206 insertions, 60 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 32e716ab2..4ad198a82 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -239,13 +239,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       options::fmfBound.set(true);
       Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
     }
-    // Turn off E-matching, since some bounded quantifiers introduced by strings
-    // (e.g. for replaceall) admit matching loops.
-    if (!options::eMatching.wasSetByUser())
-    {
-      options::eMatching.set(false);
-      Trace("smt") << "turning off E-matching, for strings-exp" << std::endl;
-    }
     // Do not eliminate extended arithmetic symbols from quantified formulas,
     // since some strategies, e.g. --re-elim-agg, introduce them.
     if (!options::elimExtArithQuant.wasSetByUser())
@@ -254,6 +247,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       Trace("smt") << "turning off elim-ext-arith-quant, for strings-exp"
                    << std::endl;
     }
+    // Note we allow E-matching by default to support combinations of sequences
+    // and quantifiers.
   }
   if (options::arraysExp())
   {
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 */
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 820e6f70f..966964bc8 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -23,6 +23,7 @@
 #include "options/strings_options.h"
 #include "proof/proof_manager.h"
 #include "smt/logic_exception.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/strings/arith_entail.h"
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/word.h"
@@ -34,6 +35,13 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
+/** Mapping to a dummy node for marking an attribute on internal quantified
+ * formulas */
+struct QInternalVarAttributeId
+{
+};
+typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
+
 StringsPreprocess::StringsPreprocess(SkolemCache* sc,
                                      context::UserContext* u,
                                      SequencesStatistics& stats)
@@ -295,7 +303,7 @@ Node StringsPreprocess::reduce(Node t,
     Node ux1lem = nm->mkNode(GEQ, n, ux1);
 
     lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eq, cb, ux1lem));
-    lem = nm->mkNode(FORALL, xbv, lem);
+    lem = mkForallInternal(xbv, lem);
     conc.push_back(lem);
 
     Node nonneg = nm->mkNode(GEQ, n, zero);
@@ -382,7 +390,7 @@ Node StringsPreprocess::reduce(Node t,
     Node ux1lem = nm->mkNode(GEQ, stoit, ux1);
 
     lem = nm->mkNode(OR, g.negate(), nm->mkNode(AND, eq, cb, ux1lem));
-    lem = nm->mkNode(FORALL, xbv, lem);
+    lem = mkForallInternal(xbv, lem);
     conc2.push_back(lem);
 
     Node sneg = nm->mkNode(LT, stoit, zero);
@@ -519,8 +527,8 @@ Node StringsPreprocess::reduce(Node t,
     flem.push_back(
         ufip1.eqNode(nm->mkNode(PLUS, ii, nm->mkNode(STRING_LENGTH, y))));
 
-    Node q = nm->mkNode(
-        FORALL, bvli, nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem)));
+    Node body = nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem));
+    Node q = mkForallInternal(bvli, body);
     lem.push_back(q);
 
     // assert:
@@ -689,8 +697,8 @@ Node StringsPreprocess::reduce(Node t,
             .eqNode(nm->mkNode(
                 STRING_CONCAT, pfxMatch, z, nm->mkNode(APPLY_UF, us, ip1))));
 
-    Node forall = nm->mkNode(
-        FORALL, bvli, nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem)));
+    Node body = nm->mkNode(OR, bound.negate(), nm->mkNode(AND, flem));
+    Node forall = mkForallInternal(bvli, body);
     lemmas.push_back(forall);
 
     // IF in_re(x, re.++(_*, y', _*))
@@ -745,8 +753,8 @@ Node StringsPreprocess::reduce(Node t,
 
     Node bound =
         nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr));
-    Node rangeA =
-        nm->mkNode(FORALL, bvi, nm->mkNode(OR, bound.negate(), ri.eqNode(res)));
+    Node body = nm->mkNode(OR, bound.negate(), ri.eqNode(res));
+    Node rangeA = mkForallInternal(bvi, body);
 
     // upper 65 ... 90
     // lower 97 ... 122
@@ -780,8 +788,8 @@ Node StringsPreprocess::reduce(Node t,
 
     Node bound =
         nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr));
-    Node rangeA = nm->mkNode(
-        FORALL, bvi, nm->mkNode(OR, bound.negate(), ssr.eqNode(ssx)));
+    Node body = nm->mkNode(OR, bound.negate(), ssr.eqNode(ssx));
+    Node rangeA = mkForallInternal(bvi, body);
     // assert:
     //   len(r) = len(x) ^
     //   forall i. 0 <= i < len(r) =>
@@ -982,6 +990,30 @@ void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){
   }
 }
 
+Node StringsPreprocess::mkForallInternal(Node bvl, Node body)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  QInternalVarAttribute qiva;
+  Node qvar;
+  if (bvl.hasAttribute(qiva))
+  {
+    qvar = bvl.getAttribute(qiva);
+  }
+  else
+  {
+    qvar = nm->mkSkolem("qinternal", nm->booleanType());
+    // this dummy variable marks that the quantified formula is internal
+    qvar.setAttribute(InternalQuantAttribute(), 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);
+}
+
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index f84ae4247..124a09a4c 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -100,6 +100,14 @@ class StringsPreprocess {
   Node simplifyRec(Node t,
                    std::vector<Node>& asserts,
                    std::map<Node, Node>& visited);
+  /**
+   * Make internal quantified formula with bound variable list bvl and body.
+   * Internally, we get a node corresponding to marking a quantified formula as
+   * an "internal" one. 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.
+   */
+  static Node mkForallInternal(Node bvl, Node body);
 };
 
 }/* CVC4::theory::strings namespace */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d118690ed..87b3c7310 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1640,6 +1640,8 @@ set(regress_1_tests
   regress1/quantifiers/set-choice-koikonomou.cvc
   regress1/quantifiers/set8.smt2
   regress1/quantifiers/seu169+1.smt2
+  regress1/quantifiers/seq-solved-enum.smt2
+  regress1/quantifiers/seq-unsolved-ematch.smt2
   regress1/quantifiers/small-pipeline-fixpoint-3.smt2
   regress1/quantifiers/smtcomp-qbv-053118.smt2
   regress1/quantifiers/smtlib384a03.smt2
diff --git a/test/regress/regress1/quantifiers/seq-solved-enum.smt2 b/test/regress/regress1/quantifiers/seq-solved-enum.smt2
new file mode 100644
index 000000000..cff3d3ca0
--- /dev/null
+++ b/test/regress/regress1/quantifiers/seq-solved-enum.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --strings-exp --full-saturate-quant
+; EXPECT: unsat
+(set-logic ALL)
+
+(declare-fun s () (Seq Int))
+
+(declare-fun x () Int)
+
+(declare-fun y () Int)
+
+(assert (and (<= 0 x) (<= x y) (< y (seq.len s))))
+
+(assert (forall ((i Int) (j Int)) (=> (and (<= 0 i) (<= i j) (< j (seq.len s))) (<= (seq.nth s i) (seq.nth s j)))))
+
+(assert (not (<= (seq.nth s x) (seq.nth s y))))
+
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/seq-unsolved-ematch.smt2 b/test/regress/regress1/quantifiers/seq-unsolved-ematch.smt2
new file mode 100644
index 000000000..044607dfe
--- /dev/null
+++ b/test/regress/regress1/quantifiers/seq-unsolved-ematch.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --strings-exp --full-saturate-quant
+; EXPECT: unsat
+(set-logic ALL)
+
+(declare-fun s () (Seq Int))
+
+(declare-fun x () Int)
+
+(assert (and (<= 0 x) (< x (seq.len s))))
+
+(assert (forall ((i Int)) (=> (and (<= 0 i) (< i (seq.len s))) (= (seq.nth s i) 0))))
+
+(assert (not (= (seq.nth s x) 0)))
+
+(check-sat)