From: Andrew Reynolds Date: Thu, 23 Jun 2022 15:42:07 +0000 (-0500) Subject: Fix explanation for strings unit oob inference (#8908) X-Git-Tag: cvc5-1.0.1~36 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c898b0ec2144cae0515625f95cc6e05abe2fa186;p=cvc5.git Fix explanation for strings unit oob inference (#8908) Fixes #8906. --- 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)