From 67e5e3d2cf5e381bde65683b1244d1905e969a90 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 30 Apr 2020 13:18:26 -0500 Subject: 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") ) --- src/theory/strings/base_solver.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'src') 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") -- cgit v1.2.3