Add extensionality option for strings disequalities (#7229)

Towards the strings array solver.

Extensionality for disequalities is disabled by default, but will be used when the strings array solver is enabled.

6 files changed, 89 insertions, 1 deletions

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 90e363f28..d46e5055e 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -182,3 +182,11 @@ name   = "Strings Theory"
   type       = "bool"
   default    = "true"
   help       = "perform eager context-dependent evaluation for applications of string kinds"
+
+[[option]]
+  name       = "stringsDeqExt"
+  category   = "regular"
+  long       = "strings-deq-ext"
+  type       = "bool"
+  default    = "false"
+  help       = "use extensionality for string disequalities"
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 7bb87819e..fce867688 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -397,6 +397,8 @@ const char* toString(InferenceId i)
     case InferenceId::STRINGS_DEQ_LENS_EQ: return "STRINGS_DEQ_LENS_EQ";
     case InferenceId::STRINGS_DEQ_NORM_EMP: return "STRINGS_DEQ_NORM_EMP";
     case InferenceId::STRINGS_DEQ_LENGTH_SP: return "STRINGS_DEQ_LENGTH_SP";
+    case InferenceId::STRINGS_DEQ_EXTENSIONALITY:
+      return "STRINGS_DEQ_EXTENSIONALITY";
     case InferenceId::STRINGS_CODE_PROXY: return "STRINGS_CODE_PROXY";
     case InferenceId::STRINGS_CODE_INJ: return "STRINGS_CODE_INJ";
     case InferenceId::STRINGS_RE_NF_CONFLICT: return "STRINGS_RE_NF_CONFLICT";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 4c6140872..3def963ea 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -673,6 +673,10 @@ enum class InferenceId
   // is unknown, we apply the inference:
   //   len(s) != len(t) V len(s) = len(t)
   STRINGS_DEQ_LENGTH_SP,
+  // Disequality extensionality
+  // x != y => ( seq.len(x) != seq.len(y) or
+  //             ( seq.nth(x, d) != seq.nth(y, d) ^ 0 <= d < seq.len(x) ) )
+  STRINGS_DEQ_EXTENSIONALITY,
   //-------------------- codes solver
   // str.to_code( v ) = rewrite( str.to_code(c) )
   // where v is the proxy variable for c.
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 98a0e819c..2dfc73756 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -47,7 +47,8 @@ CoreSolver::CoreSolver(Env& env,
       d_im(im),
       d_termReg(tr),
       d_bsolver(bs),
-      d_nfPairs(context())
+      d_nfPairs(context()),
+      d_extDeq(userContext())
 {
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
@@ -2080,6 +2081,12 @@ void CoreSolver::processDeq(Node ni, Node nj)
     return;
   }
 
+  if (options::stringsDeqExt())
+  {
+    processDeqExtensionality(ni, nj);
+    return;
+  }
+
   nfi = nfni.d_nf;
   nfj = nfnj.d_nf;
 
@@ -2441,6 +2448,56 @@ bool CoreSolver::processSimpleDeq(std::vector<Node>& nfi,
   return false;
 }
 
+void CoreSolver::processDeqExtensionality(Node n1, Node n2)
+{
+  // hash based on equality
+  Node eq = n1 < n2 ? n1.eqNode(n2) : n2.eqNode(n1);
+  NodeSet::const_iterator it = d_extDeq.find(eq);
+  if (it != d_extDeq.end())
+  {
+    // already processed
+    return;
+  }
+  d_extDeq.insert(eq);
+
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemCache* sc = d_termReg.getSkolemCache();
+  TypeNode intType = nm->integerType();
+  Node k = sc->mkTypedSkolemCached(
+      intType, n1, n2, SkolemCache::SK_DEQ_DIFF, "diff");
+  Node deq = eq.negate();
+  Node ss1, ss2;
+  if (n1.getType().isString())
+  {
+    // substring of length 1
+    ss1 = nm->mkNode(STRING_SUBSTR, n1, k, d_one);
+    ss2 = nm->mkNode(STRING_SUBSTR, n2, k, d_one);
+  }
+  else
+  {
+    // as an optimization, for sequences, use seq.nth
+    ss1 = nm->mkNode(SEQ_NTH, n1, k);
+    ss2 = nm->mkNode(SEQ_NTH, n2, k);
+  }
+  // disequality between nth/substr
+  Node conc1 = ss1.eqNode(ss2).negate();
+
+  // The skolem k is in the bounds of at least
+  // one string/sequence
+  Node len1 = nm->mkNode(STRING_LENGTH, n1);
+  Node len2 = nm->mkNode(STRING_LENGTH, n2);
+  Node conc2 = nm->mkNode(LEQ, d_zero, k);
+  Node conc3 = nm->mkNode(LT, k, len1);
+  Node lenDeq = nm->mkNode(EQUAL, len1, len2).negate();
+
+  std::vector<Node> concs = {conc1, conc2, conc3};
+  Node conc = nm->mkNode(OR, lenDeq, nm->mkAnd(concs));
+  // A != B => ( seq.len(A) != seq.len(B) or
+  //             ( seq.nth(A, d) != seq.nth(B, d) ^ 0 <= d < seq.len(A) ) )
+  d_im.sendInference(
+      {deq}, conc, InferenceId::STRINGS_DEQ_EXTENSIONALITY, false, true);
+}
+
 void CoreSolver::addNormalFormPair( Node n1, Node n2 ){
   if (n1>n2)
   {
diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h
index 35d37ce12..adf17de4d 100644
--- a/src/theory/strings/core_solver.h
+++ b/src/theory/strings/core_solver.h
@@ -19,6 +19,7 @@
 #ifndef CVC5__THEORY__STRINGS__CORE_SOLVER_H
 #define CVC5__THEORY__STRINGS__CORE_SOLVER_H
 
+#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "smt/env_obj.h"
@@ -81,6 +82,7 @@ class CoreSolver : protected EnvObj
 {
   friend class InferenceManager;
   using NodeIntMap = context::CDHashMap<Node, int>;
+  using NodeSet = context::CDHashSet<Node>;
 
  public:
   CoreSolver(Env& env,
@@ -469,6 +471,16 @@ class CoreSolver : protected EnvObj
                         Node nj,
                         size_t& index,
                         bool isRev);
+  /**
+   * Process disequality by extensionality. If necessary, this may result
+   * in inferences that follow from this disequality of the form:
+   *   (not (= n1 n2)) => (not (= k1 k2))
+   * where k1, k2 are either strings of length one or elements of a sequence.
+   *
+   * @param n1 The first string in the disequality
+   * @param n2 The second string in the disequality
+   */
+  void processDeqExtensionality(Node n1, Node n2);
   //--------------------------end for checkNormalFormsDeq
 
   /** The solver state object */
@@ -522,6 +534,8 @@ class CoreSolver : protected EnvObj
    * the argument number of the t1 ... tn they were generated from.
    */
   std::map<Node, std::vector<int> > d_flat_form_index;
+  /** Set of equalities for which we have applied extensionality. */
+  NodeSet d_extDeq;
 }; /* class CoreSolver */
 
 }  // namespace strings
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index f0376dbc6..dabe333ae 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -149,6 +149,9 @@ class SkolemCache
     // forall s, n.
     //  k(s, n) is some undefined value of sort U
     SK_NTH,
+    // Diff index for disequalities
+    // a != b => substr(a,k,1) != substr(b,k,1)
+    SK_DEQ_DIFF
   };
   /**
    * Returns a skolem of type string that is cached for (a,b,id) and has