From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 26 Apr 2021 07:34:14 +0000 (-0500)
Subject: Do not process looping word equations over sequences (#6434)
X-Git-Tag: cvc5-1.0.0~1835
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b6d3dc39fcd1cd71d263a4ff6949d77d671c73b9;p=cvc5.git

Do not process looping word equations over sequences (#6434)
---

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 2abe2de82..ed220c1eb 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1771,23 +1771,27 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
                                                       int index,
                                                       CoreInferInfo& info)
 {
+  NodeManager* nm = NodeManager::currentNM();
+  Node conc;
+  const std::vector<Node>& veci = nfi.d_nf;
+  const std::vector<Node>& vecoi = nfj.d_nf;
+
+  TypeNode stype = veci[loop_index].getType();
+
   if (options::stringProcessLoopMode() == options::ProcessLoopMode::ABORT)
   {
     throw LogicException("Looping word equation encountered.");
   }
-  else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE)
+  else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE
+           || stype.isSequence())
   {
+    // note we cannot convert looping word equations into regular expressions if
+    // we are handling sequences, since there is no analog for regular
+    // expressions over sequences currently
     d_im.setIncomplete(IncompleteId::STRINGS_LOOP_SKIP);
     return ProcessLoopResult::SKIPPED;
   }
 
-  NodeManager* nm = NodeManager::currentNM();
-  Node conc;
-  const std::vector<Node>& veci = nfi.d_nf;
-  const std::vector<Node>& vecoi = nfj.d_nf;
-
-  TypeNode stype = veci[loop_index].getType();
-
   Trace("strings-loop") << "Detected possible loop for " << veci[loop_index]
                         << std::endl;
   Trace("strings-loop") << " ... (X)= " << vecoi[index] << std::endl;