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")
)

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 8711973f4ba982bb249e4c5f5b300aaf74cee65a..df5263c45e6169f592533250e7145f51bca5b880 100644 (file)
--- 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")