From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Jul 2022 18:54:05 +0000 (-0500)
Subject: Revert usage of seq.nth in reductions (#8939)
X-Git-Tag: cvc5-1.0.1~17
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c3987a63fc73fec73048d4ecfe2dff11327ef986;p=cvc5.git

Revert usage of seq.nth in reductions (#8939)

Fixes #8932. Fixes #8926.
---

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 8a6d53409..8d5687ec2 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -1073,10 +1073,12 @@ Node StringsPreprocess::simplifyRec(Node t, std::vector<Node>& asserts)
 }
 Node StringsPreprocess::mkCodePointAtIndex(Node x, Node i)
 {
-  // we use (SEQ_NTH, x, i) instead of
+  // we could use (SEQ_NTH, x, i) instead of
   // (STRING_TO_CODE, (STRING_SUBSTR, x, i, 1))
   NodeManager* nm = NodeManager::currentNM();
-  return nm->mkNode(SEQ_NTH, x, i);
+  return nm->mkNode(
+      STRING_TO_CODE,
+      nm->mkNode(STRING_SUBSTR, x, i, nm->mkConstInt(Rational(1))));
 }
 
 Node StringsPreprocess::processAssertion(Node n, std::vector<Node>& asserts)
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index d4fd132cd..a5979dd5b 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2645,6 +2645,7 @@ set(regress_1_tests
   regress1/strings/issue8915-str-unit-model.smt2
   regress1/strings/issue8916-str-unit-pairs.smt2
   regress1/strings/issue8918-str-nth-crange-red.smt2
+  regress1/strings/issue8932-cmi-unit.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
@@ -3121,6 +3122,7 @@ set(regress_3_tests
   regress3/strings-any-term.sy
   regress3/strings/extf_d_perf.smt2
   regress3/strings/indexof_re_red.smt2
+  regress3/strings/issue8926-sygus-inst.smt2
   regress3/strings/norn-dis-0707-3.smt2
   regress3/strings/replace_re_all.smt2
   regress3/unbdd_inv_gen_ex7.sy
diff --git a/test/regress/cli/regress1/strings/issue8932-cmi-unit.smt2 b/test/regress/cli/regress1/strings/issue8932-cmi-unit.smt2
new file mode 100644
index 000000000..436c44d79
--- /dev/null
+++ b/test/regress/cli/regress1/strings/issue8932-cmi-unit.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic QF_SLIA)
+(declare-fun v () String)
+(declare-fun X () Int)
+(declare-fun t () Int)
+(assert (and (< t (- 15)) (< (- 38) t)))
+(assert (not (str.< (str.++ (str.++ (str.from_int X) (str.from_int (- t))) v) "3lA")))
+(check-sat)
diff --git a/test/regress/cli/regress3/strings/issue8926-sygus-inst.smt2 b/test/regress/cli/regress3/strings/issue8926-sygus-inst.smt2
new file mode 100644
index 000000000..5373e520a
--- /dev/null
+++ b/test/regress/cli/regress3/strings/issue8926-sygus-inst.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --sygus-inst
+; EXPECT: sat
+(set-logic QF_SLIA)
+(declare-fun tstr () String)
+(assert (ite (str.prefixof "-" (str.substr tstr 0 (- (+ 0 2) 0))) (and (ite (= (- 1) (str.to_int (str.substr (str.substr tstr 0 (- (+ 0 2) 0)) 1 (- (str.len (str.substr tstr 0 (- (+ 0 2) 0))) 1)))) false true) (> (str.len (str.substr tstr 0 (- (+ 0 2) 0))) 1)) (ite (= (- 1) (str.to_int (str.substr tstr 0 (- (+ 0 2) 0)))) false true)))
+(assert (not (< (str.len tstr) (str.to_code (str.rev tstr)))))
+(assert (>= 3 (str.len tstr)))
+(check-sat)