From c898b0ec2144cae0515625f95cc6e05abe2fa186 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 23 Jun 2022 10:42:07 -0500 Subject: [PATCH] Fix explanation for strings unit oob inference (#8908) Fixes #8906. --- src/theory/strings/base_solver.cpp | 8 +++++++- src/theory/uf/equality_engine.cpp | 1 + test/regress/cli/CMakeLists.txt | 1 + test/regress/cli/regress1/strings/issue8906-oob-exp.smt2 | 7 +++++++ 4 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 test/regress/cli/regress1/strings/issue8906-oob-exp.smt2 diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 998926802..0c01e8316 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -151,8 +151,14 @@ void BaseSolver::checkInit() Node scr = utils::mkCodeRange(s, d_cardSize); Node tcr = utils::mkCodeRange(t, d_cardSize); Node conc = nm->mkNode(OR, scr.notNode(), tcr.notNode()); + // We do not explain exp for two reasons. First, we are + // caching this inference based on the user context and thus + // it should not depend on the current explanation. Second, + // s or t may be concrete integers corresponding to code + // points of string constants, and thus are not guaranteed to + // be terms in the equality engine. d_im.sendInference( - exp, conc, InferenceId::STRINGS_UNIT_INJ_OOB); + exp, exp, conc, InferenceId::STRINGS_UNIT_INJ_OOB); } } else diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index d2f6b242f..131089219 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1277,6 +1277,7 @@ void EqualityEngine::explainPredicate(TNode p, bool polarity, void EqualityEngine::explainLit(TNode lit, std::vector& assumptions) { + Trace("eq-exp") << "explainLit: " << lit << std::endl; Assert(lit.getKind() != kind::AND); bool polarity = lit.getKind() != kind::NOT; TNode atom = polarity ? lit : lit[0]; diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index eeeae8692..1ced25e3c 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2627,6 +2627,7 @@ set(regress_1_tests regress1/strings/issue8347-has-skolem.smt2 regress1/strings/issue8434-nterm-str-rw.smt2 regress1/strings/issue8890-inj-oob.smt2 + regress1/strings/issue8906-oob-exp.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/cli/regress1/strings/issue8906-oob-exp.smt2 b/test/regress/cli/regress1/strings/issue8906-oob-exp.smt2 new file mode 100644 index 000000000..d2a61faf9 --- /dev/null +++ b/test/regress/cli/regress1/strings/issue8906-oob-exp.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unknown +(set-logic ALL) +(declare-const x1 Bool) +(declare-const x Int) +(assert (forall ((e String)) (or (exists ((e String)) (or (ite (str.prefixof "-" (str.at e 0)) false (= 1 (str.to_int (str.at e (+ x (str.len e)))))) x1))))) +(check-sat) -- 2.30.2