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 8a6d53409efc04e414b3617e243ddbe8b8e70ad0..8d5687ec22f05b53507884dc414332d4a9f1b907 100644 (file)
--- 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 d4fd132cdf7bbfc1931a7545cb7abec39c330714..a5979dd5b5f757f21a67050b366074515ef9b302 100644 (file)
--- 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 (file)
index 0000000..436c44d
--- /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 (file)
index 0000000..5373e52
--- /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)