From cd6db957a9c780216624fac2d58fd8a9ea51aec2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 7 Jul 2022 14:15:07 -0500 Subject: [PATCH] Do not eagerly preprocess seq.nth (#8937) Fixes #8936. --- src/theory/strings/theory_strings_preprocess.cpp | 7 ++++++- src/theory/strings/theory_strings_preprocess.h | 4 ++++ test/regress/cli/CMakeLists.txt | 1 + .../cli/regress1/seq/issue8936-nth-eager-red.smt2 | 9 +++++++++ .../cli/regress1/strings/issue6777-seq-nth-eval-cm.smt2 | 2 +- 5 files changed, 21 insertions(+), 2 deletions(-) create mode 100644 test/regress/cli/regress1/seq/issue8936-nth-eager-red.smt2 diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 8d5687ec2..8c0ab9038 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -1065,7 +1065,12 @@ Node StringsPreprocess::simplifyRec(Node t, std::vector& asserts) if( changed ){ tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc ); } - retNode = simplify(tmp, asserts); + // We cannot statically reduce seq.nth due to it being partial function. + // Reducing it here would violate the functional property of seq.nth. + if (tmp.getKind() != SEQ_NTH) + { + retNode = simplify(tmp, asserts); + } } d_visited[t] = retNode; return retNode; diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 49691d35c..9b10066ea 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -83,6 +83,8 @@ class StringsPreprocess : protected EnvObj * (exists k) asserts => t = t' * is valid, where k are the free skolems introduced when constructing * asserts. + * + * This method is called only for eager preprocessing of extended functions. */ Node processAssertion(Node t, std::vector& asserts); @@ -97,6 +99,8 @@ class StringsPreprocess : protected EnvObj * Applies simplify to all top-level extended function subterms of t. New * assertions created in this reduction are added to asserts. The argument * visited stores a cache of previous results. + * + * This method is called only for eager preprocessing of extended functions. */ Node simplifyRec(Node t, std::vector& asserts); /** diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index a5979dd5b..67c6cc8d4 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2440,6 +2440,7 @@ set(regress_1_tests regress1/sep/wand-simp-unsat.smt2 regress1/seq/issue8148-2-const-mv.smt2 regress1/seq/issue8148-const-mv.smt2 + regress1/seq/issue8936-nth-eager-red.smt2 regress1/sets/choose.cvc.smt2 regress1/sets/choose1.smt2 regress1/sets/choose2.smt2 diff --git a/test/regress/cli/regress1/seq/issue8936-nth-eager-red.smt2 b/test/regress/cli/regress1/seq/issue8936-nth-eager-red.smt2 new file mode 100644 index 000000000..acbb67b80 --- /dev/null +++ b/test/regress/cli/regress1/seq/issue8936-nth-eager-red.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp --no-strings-lazy-pp +; EXPECT: unsat +(set-logic ALL) +(declare-fun a () (Seq Int)) +(declare-fun b () (Seq Int)) +(declare-fun c () Int) +(assert (= a b)) +(assert (not (= (seq.nth a c) (seq.nth b c)))) +(check-sat) diff --git a/test/regress/cli/regress1/strings/issue6777-seq-nth-eval-cm.smt2 b/test/regress/cli/regress1/strings/issue6777-seq-nth-eval-cm.smt2 index afa6fa238..7b75f724b 100644 --- a/test/regress/cli/regress1/strings/issue6777-seq-nth-eval-cm.smt2 +++ b/test/regress/cli/regress1/strings/issue6777-seq-nth-eval-cm.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -q +; COMMAND-LINE: --strings-exp -q ; EXPECT: sat (set-logic ALL) (set-info :status sat) -- 2.30.2