question about equality in the theory of arrays

Question

I am wondering if this should return unsat? It doesn't return after running for 30 mins on both z3 and cvc5.

; asserts that l1 = l2 up to index len
(define-fun-rec list-eq (   (l1 (Array Int Int))  (l2 (Array Int Int))   (len Int)  ) Bool
  (ite (< len 0)
       true
       (ite (= len 0)
            (= (select l1 0) (select l2 0))
            (list-eq l1 l2 (- len 1)))))


(assert
(not 
(=> (list-eq out in i)
    (list-eq (store out i (select in i)) in i)
)))

Answer 1

There're a few problems here, let me address them separately.

First, your definition of list-eq is not really checking if two arrays are equal at all. All it's doing is checking if the given arrays store the same value at index 0. Note that your call to select always uses 0 as the argument; otherwise it simply recurses down; which isn't comparing the corresponding elements. You probably meant something like:

; check if two arrays are equivalent between 0 and len, inclusive (so len+1 elements are checked.)
(define-fun-rec list-eq ((l1 (Array Int Int))  (l2 (Array Int Int)) (len Int)) Bool
  (or (< len 0)
      (and (= (select l1 len) (select l2 len))
           (list-eq l1 l2 (- len 1)))))

But making this change isn't going to help; because recursive functions are hard for SMT solvers to deal with. (You typically need induction to prove things about recursive functions, and SMT solvers don't do induction.) Instead, use something like:

(define-fun list-eq ((l1 (Array Int Int)) (l2 (Array Int Int)) (len Int)) Bool
   (forall ((i Int)) (=> (and (<= 0 i) (< i len)) (= (select l1 i) (select l2 i)))))

Now, quantifiers are hard for SMT solvers too; but they can deal with them better compared to recursive definitions. So, our entire program becomes:

(set-logic ALL)

(define-fun list-eq ((l1 (Array Int Int)) (l2 (Array Int Int)) (len Int)) Bool
   (forall ((i Int)) (=> (and (<= 0 i) (< i len)) (= (select l1 i) (select l2 i)))))

(declare-const in  (Array Int Int))
(declare-const out (Array Int Int))
(declare-const i   Int)

(assert
(not (=> (list-eq out in i)
         (list-eq (store out i (select in i)) in i))))

(check-sat)

And you'll see that both cvc5 and z3 can answer unsat fairly quickly for this version of the problem.

I should add that heavy use of quantifiers will again lead the solvers to never-ending loops; but in general they handle quantifiers much better than they handle recursive definitions.