From: Andrew Reynolds Date: Tue, 8 Jun 2021 23:47:40 +0000 (-0500) Subject: Fix for 2 dimensional dependent bounded quantifiers (#6710) X-Git-Tag: cvc5-1.0.0~1626 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ccd52accc3bd19c5bc5203d091d1fc0f8d48f8a3;p=cvc5.git 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. --- 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)