diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-30 13:18:26 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-30 13:18:26 -0500 |
commit | 67e5e3d2cf5e381bde65683b1244d1905e969a90 (patch) | |
tree | c38c93994578738d8df21305a377f7ff449e5455 /src | |
parent | 6ba68a1897838f3aefa6cbd254a1262326e446c7 (diff) |
Do not mark congruent terms are reduced (#4419)
This fixes a potential model soundness issue in strings where a justification for why a string term was reduced relied on a circular argument. The issue involved "reduced by congruence" which states that when f(a) = f(b) ^ a = b in the current context, then one of f(a) or f(b) can be ignored.
However, it may be the case that a is an extended function whose reduction relies on f(b). If we were to assume that f(b) can be ignored due to f(a), then our reduction of f(a) is circular: the reduction of f(a) in the context where a=b relies on itself.
This was causing an incorrect model for QF_S/2020-sygus-qgen/queries/query3214.smt2. The sequence of dependencies was:
[1] (str.contains (str.substr x 1 (+ (- 1) (str.len x))) "CA")
is congruent to
(str.contains (str.substr x (+ 2 (str.indexof x "CA" 1)) (+ (- 2) (str.len x) (* (- 1) (str.indexof x "CA" 1)))) "CA")
in the current context since they are equal and their arguments are equal.
[2] (str.substr x (+ 2 (str.indexof x "CA" 1)) (+ (- 2) (str.len x) (* (- 1) (str.indexof x "CA" 1))))
reduction relies on the length constraint:
(= (str.indexof x "CA" 1) (+ (- 2) (str.len sspre_66)))
[3] (str.indexof x "CA" 1)
reduction relies on:
(not (str.contains (str.substr x 1 (+ (- 1) (str.len x))) "CA"))
which was marked congruent above.
The benchmark now solves in 5 minutes 30 seconds (sat, with a correct model):
andrew@andrew-Latitude-7480:~/misc/strings$ time ajr-cvc4 query3214.smt2 --strings-exp --rewrite-divk --check-models --dump-models
sat
(model
(define-fun x () String "QACOACA")
)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/base_solver.cpp | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 8711973f4..df5263c45 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -130,9 +130,14 @@ void BaseSolver::checkInit() } else { - // mark as congruent : only process if neither has been - // reduced - d_im.markCongruent(nc, n); + // We cannot mark one of the terms as reduced here (via + // ExtTheory::markCongruent) since extended function terms + // rely on reductions to other extended function terms. We + // may have a pair of extended function terms f(a)=f(b) where + // the reduction of argument a depends on the term b. + // Thus, marking f(b) as reduced by virtue of the fact we + // have f(a) is incorrect, since then we are effectively + // assuming that the reduction of f(a) depends on itself. } // this node is congruent to another one, we can ignore it Trace("strings-process-debug") |