From ca2a39f7650fb311d5a45b5a95861605ad5a80af Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 29 Jun 2022 16:02:54 -0500 Subject: [PATCH] Fix reduction for seq.nth for strings (#8919) Fixes #8918. --- src/preprocessing/passes/strings_eager_pp.cpp | 2 +- src/theory/strings/extf_solver.cpp | 2 +- src/theory/strings/proof_checker.cpp | 2 +- .../strings/theory_strings_preprocess.cpp | 19 ++++++++++++++----- .../strings/theory_strings_preprocess.h | 14 +++++++++++--- test/regress/cli/CMakeLists.txt | 1 + .../strings/issue8918-str-nth-crange-red.smt2 | 6 ++++++ 7 files changed, 35 insertions(+), 11 deletions(-) create mode 100644 test/regress/cli/regress1/strings/issue8918-str-nth-crange-red.smt2 diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp index 9dcf2140f..9a2050453 100644 --- 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 d51f812d9..24c1a0ba9 100644 --- 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 7b177241c..973991209 100644 --- 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 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 284788637..8a6d53409 100644 --- 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* 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& 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 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& 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 e1b2e852b..49691d35c 100644 --- 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 + #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* 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& asserts, SkolemCache* sc); + static Node reduce(Node t, + std::vector& 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 13f277841..2ecf50241 100644 --- 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 index 000000000..168648a4f --- /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) -- 2.30.2