From ccd52accc3bd19c5bc5203d091d1fc0f8d48f8a3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 8 Jun 2021 18:47:40 -0500 Subject: Fix for 2 dimensional dependent bounded quantifiers (#6710) This updates 2-dim dependent bounded quantifiers to not map constants to terms when computing ranges, when the type of the variable is closed enumerable. This is require to fix an incorrect model (possible solution unsoundness) issue in the reduction of str.indexof_re. Fixes the 1st, 4th and 5th benchmarks from #6653. Fixes #6635. --- src/theory/quantifiers/fmf/bounded_integers.cpp | 17 ++++++++++++++++- src/theory/rep_set.cpp | 3 +++ src/theory/strings/theory_strings_preprocess.cpp | 2 +- test/regress/CMakeLists.txt | 4 ++++ test/regress/regress1/strings/issue6635-rre.smt2 | 6 ++++++ test/regress/regress1/strings/issue6653-4-rre.smt2 | 6 ++++++ test/regress/regress1/strings/issue6653-rre-small.smt2 | 6 ++++++ test/regress/regress1/strings/issue6653-rre.smt2 | 8 ++++++++ 8 files changed, 50 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/strings/issue6635-rre.smt2 create mode 100644 test/regress/regress1/strings/issue6653-4-rre.smt2 create mode 100644 test/regress/regress1/strings/issue6653-rre-small.smt2 create mode 100644 test/regress/regress1/strings/issue6653-rre.smt2 diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index b0f6e63bf..5ecc33778 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -716,7 +716,22 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl; int vo = rsi->getVariableOrder(i); Assert(q[0][vo] == d_set[q][i]); - Node t = rsi->getCurrentTerm(vo, true); + TypeNode tn = d_set[q][i].getType(); + // If the type of tn is not closed enumerable, we must map the value back + // to a term that appears in the same equivalence class as the constant. + // Notice that this is to ensure that unhandled values (e.g. uninterpreted + // constants, datatype values) do not enter instantiations/lemmas, which + // can lead to refutation unsoundness. However, it is important that we + // conversely do *not* map terms to values in other cases. In particular, + // replacing a constant c with a term t can lead to solution unsoundness + // if we are instantiating a quantified formula that corresponds to a + // reduction for t, since then the reduction is using circular reasoning: + // the current value of t is being used to reason about the range of + // its axiomatization. This is limited to reductions in the theory of + // strings, which use quantification on integers only. Note this + // impacts only quantified formulas with 2+ dimensions and dependencies + // between dimensions, e.g. str.indexof_re reduction. + Node t = rsi->getCurrentTerm(vo, !tn.isClosedEnumerable()); Trace("bound-int-rsi") << "term : " << t << std::endl; vars.push_back( d_set[q][i] ); subs.push_back( t ); diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index d0eee1886..f6af5b680 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -429,14 +429,17 @@ Node RepSetIterator::getCurrentTerm(unsigned i, bool valTerm) const << d_domain_elements[i].size() << std::endl; Assert(0 <= curr && curr < d_domain_elements[i].size()); Node t = d_domain_elements[i][curr]; + Trace("rsi-debug") << "rsi : term = " << t << std::endl; if (valTerm) { Node tt = d_rs->getTermForRepresentative(t); if (!tt.isNull()) { + Trace("rsi-debug") << "rsi : return rep term = " << tt << std::endl; return tt; } } + Trace("rsi-debug") << "rsi : return" << std::endl; return t; } diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index b0d538064..dbb6d4cf3 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -323,7 +323,7 @@ Node StringsPreprocess::reduce(Node t, // n <= i < ite(skk = -1, len(s), skk) ^ 0 < l <= len(s) - i => // ~in_re(substr(s, i, l), r)) ^ // (skk != -1 => - // exists l. 0 <= l < len(s) - skk ^ in_re(substr(s, skk, l), r)) + // exists l. 0 <= l <= len(s) - skk ^ in_re(substr(s, skk, l), r)) // // Note that this reduction relies on eager reduction lemmas being sent to // properly limit the range of skk. diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a5a687f9f..4ee8e513e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2126,7 +2126,11 @@ set(regress_1_tests regress1/strings/issue6337-replace-re.smt2 regress1/strings/issue6567-empty-re-range.smt2 regress1/strings/issue6604-2.smt2 + regress1/strings/issue6635-rre.smt2 regress1/strings/issue6653-2-update-c-len.smt2 + regress1/strings/issue6653-4-rre.smt2 + regress1/strings/issue6653-rre.smt2 + regress1/strings/issue6653-rre-small.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue6635-rre.smt2 b/test/regress/regress1/strings/issue6635-rre.smt2 new file mode 100644 index 000000000..cbca77783 --- /dev/null +++ b/test/regress/regress1/strings/issue6635-rre.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg +; EXPECT: unsat +(set-logic ALL) +(declare-fun a () String) +(assert (str.in_re (str.replace_re a (re.++ (str.to_re "A") (re.union (str.to_re "") (str.to_re (str.from_code (str.len a))))) "AB") (re.+ (str.to_re "A")))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-4-rre.smt2 b/test/regress/regress1/strings/issue6653-4-rre.smt2 new file mode 100644 index 000000000..8de99a334 --- /dev/null +++ b/test/regress/regress1/strings/issue6653-4-rre.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg +; EXPECT: sat +(set-logic ALL) +(declare-fun x () String) +(assert (str.in_re (str.replace_re x (str.to_re "A") x) (re.++ (re.comp (str.to_re "A")) (str.to_re "A") re.allchar))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-rre-small.smt2 b/test/regress/regress1/strings/issue6653-rre-small.smt2 new file mode 100644 index 000000000..c4b6a497b --- /dev/null +++ b/test/regress/regress1/strings/issue6653-rre-small.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --strings-exp --strings-fmf --re-elim --re-elim-agg +; EXPECT: sat +(set-logic ALL) +(declare-fun a () String) +(assert (str.in_re a (re.+ (str.to_re (str.replace_re a (str.to_re a) "A"))))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-rre.smt2 b/test/regress/regress1/strings/issue6653-rre.smt2 new file mode 100644 index 000000000..66b7dd64e --- /dev/null +++ b/test/regress/regress1/strings/issue6653-rre.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg +; EXPECT: sat +(set-logic ALL) +(declare-fun a () String) +(declare-fun b () String) +(assert (str.in_re (str.replace_re b (str.to_re (str.replace_all a (str.++ b "a") b)) (str.++ b "a")) (re.+ (str.to_re "b")))) +(assert (str.in_re a (re.* (re.range "a" "b")))) +(check-sat) -- cgit v1.2.3