Fix reduction for seq.nth for strings (#8919)

Fixes #8918.

diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp
index 9dcf2140f184b08c2b1b3fc46cb8ccee55a7a476..9a20504532f902b22b5836ec821ed690dfb9742b 100644 (file)
--- a/src/preprocessing/passes/strings_eager_pp.cpp
+++ b/src/preprocessing/passes/strings_eager_pp.cpp
@@ -33,7 +33,7 @@ PreprocessingPassResult StringsEagerPp::applyInternal(
 {
   NodeManager* nm = NodeManager::currentNM();
   theory::strings::SkolemCache skc(nullptr);
-  theory::strings::StringsPreprocess pp(&skc);
+  theory::strings::StringsPreprocess pp(d_env, &skc);
   for (size_t i = 0, nasserts = assertionsToPreprocess->size(); i < nasserts;
        ++i)
   {

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index d51f812d98c1fd6df130afb13d2b78f5f681f51e..24c1a0ba99d0c7840a3c47174a9cfdb75bf5f77e 100644 (file)
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -48,7 +48,7 @@ ExtfSolver::ExtfSolver(Env& env,
       d_csolver(cs),
       d_extt(et),
       d_statistics(statistics),
-      d_preproc(d_termReg.getSkolemCache(), &statistics.d_reductions),
+      d_preproc(env, d_termReg.getSkolemCache(), &statistics.d_reductions),
       d_hasExtf(context(), false),
       d_extfInferCache(context()),
       d_reduced(userContext())

diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index 7b177241c74ca0c7122ffdf28b5180b46732cbc2..973991209d0eee5c69c73ca988e0fb1c90862290 100644 (file)
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -331,7 +331,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       // we do not use optimizations
       SkolemCache skc(nullptr);
       std::vector<Node> conj;
-      ret = StringsPreprocess::reduce(t, conj, &skc);
+      ret = StringsPreprocess::reduce(t, conj, &skc, d_alphaCard);
       conj.push_back(t.eqNode(ret));
       ret = nm->mkAnd(conj);
     }

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 2847886379f5dafa55c6dde4d2083f23a163d552..8a6d53409efc04e414b3617e243ddbe8b8e70ad0 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -35,9 +35,10 @@ namespace cvc5::internal {
 namespace theory {
 namespace strings {
 
-StringsPreprocess::StringsPreprocess(SkolemCache* sc,
+StringsPreprocess::StringsPreprocess(Env& env,
+                                     SkolemCache* sc,
                                      HistogramStat<Kind>* statReductions)
-    : d_sc(sc), d_statReductions(statReductions)
+    : EnvObj(env), d_sc(sc), d_statReductions(statReductions)
 {
 }
 
@@ -47,7 +48,8 @@ StringsPreprocess::~StringsPreprocess(){
 
 Node StringsPreprocess::reduce(Node t,
                                std::vector<Node>& asserts,
-                               SkolemCache* sc)
+                               SkolemCache* sc,
+                               size_t alphaCard)
 {
   Trace("strings-preprocess-debug")
       << "StringsPreprocess::reduce: " << t << std::endl;
@@ -514,7 +516,13 @@ Node StringsPreprocess::reduce(Node t,
     Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n);
     Node lsk2 = nm->mkNode(STRING_LENGTH, sk2);
     Node b13 = nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, t12));
-    Node b1 = nm->mkNode(AND, b11, b12, b13);
+    std::vector<Node> bchildren { b11, b12, b13 };
+    if (s.getType().isString())
+    {
+      Node crange = utils::mkCodeRange(skt, alphaCard);
+      bchildren.push_back(crange);
+    }
+    Node b1 = nm->mkNode(AND, bchildren);
 
     // the lemma for `seq.nth`
     Node lemma = nm->mkNode(IMPLIES, cond, b1);
@@ -524,6 +532,7 @@ Node StringsPreprocess::reduce(Node t,
     // IMPLIES: s = sk1 ++ unit(skt) ++ sk2 AND
     //          len( sk1 ) = n AND
     //          len( sk2 ) = len( s )- (n+1)
+    // We also ensure skt is a valid code point if s is of type String
     asserts.push_back(lemma);
     retNode = skt;
   }
@@ -1001,7 +1010,7 @@ Node StringsPreprocess::simplify(Node t, std::vector<Node>& asserts)
 {
   size_t prev_asserts = asserts.size();
   // call the static reduce routine
-  Node retNode = reduce(t, asserts, d_sc);
+  Node retNode = reduce(t, asserts, d_sc, options().strings.stringsAlphaCard);
   if( t!=retNode ){
     Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl;
     if (!asserts.empty())

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index e1b2e852b5005d0e1b138d2050d3d68e622d3c35..49691d35c6f68a02f32ae66ca2a090c3c86d0121 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -19,7 +19,9 @@
 #define CVC5__THEORY__STRINGS__PREPROCESS_H
 
 #include <vector>
+
 #include "context/cdhashmap.h"
+#include "smt/env_obj.h"
 #include "theory/rewriter.h"
 #include "theory/strings/sequences_stats.h"
 #include "theory/strings/skolem_cache.h"
@@ -37,9 +39,11 @@ namespace strings {
  * used for reducing extended functions on-demand during the "extended function
  * reductions" inference schema of TheoryStrings.
  */
-class StringsPreprocess {
+class StringsPreprocess : protected EnvObj
+{
  public:
-  StringsPreprocess(SkolemCache* sc,
+  StringsPreprocess(Env& env,
+                    SkolemCache* sc,
                     HistogramStat<Kind>* statReductions = nullptr);
   ~StringsPreprocess();
   /** The reduce routine
@@ -61,9 +65,13 @@ class StringsPreprocess {
    * @param asserts The vector for storing the assertions that correspond to
    * the reduction of t,
    * @param sc The skolem cache for generating new variables,
+   * @param alphaCard The cardinality of the alphabet
    * @return The reduced form of t.
    */
-  static Node reduce(Node t, std::vector<Node>& asserts, SkolemCache* sc);
+  static Node reduce(Node t,
+                     std::vector<Node>& asserts,
+                     SkolemCache* sc,
+                     size_t alphaCard);
   /**
    * Calls the above method for the skolem cache owned by this class, and
    * records statistics.

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 13f2778411dc46716e55445db43bc35401e354a4..2ecf50241601583bef7bcf8b2ac82f6014c70af1 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2638,6 +2638,7 @@ set(regress_1_tests
   regress1/strings/issue8890-inj-oob.smt2
   regress1/strings/issue8906-oob-exp.smt2
   regress1/strings/issue8915-str-unit-model.smt2
+  regress1/strings/issue8918-str-nth-crange-red.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/cli/regress1/strings/issue8918-str-nth-crange-red.smt2 b/test/regress/cli/regress1/strings/issue8918-str-nth-crange-red.smt2
new file mode 100644 (file)
index 0000000..168648a
--- /dev/null
+++ b/test/regress/cli/regress1/strings/issue8918-str-nth-crange-red.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp --no-strings-lazy-pp
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () String)
+(assert (<= (str.to_int (str.++ "0" (str.from_int (ite (str.prefixof "-" (str.at a 2)) 0 (str.to_int (str.at a 2)))))) (- 1)))
+(check-sat)