z3/spacer returning UNSAT for sat-instance

[jena-kling]

Hey everyone,

for this case z3 returns unexpectedly UNSAT:

(set-logic HORN)

(declare-datatypes ((arr_int_tuple 0)) (((arr_int_tuple (d (Array Int Int)) (e Int)))))
(declare-datatypes ((dtp 0)) (((dtp (g (Array Int arr_int_tuple)) (h Int)))))

(declare-fun p (Int (Array Int dtp) (Array Int dtp)) Bool)
(declare-fun bin_p_arr ((Array Int dtp) (Array Int dtp)) Bool)
(declare-fun p_arr ((Array Int dtp)) Bool)

(assert (forall ((aj (Array Int dtp))) (p 1 aj aj)))
(assert (forall ((aj (Array Int dtp)) (ak (Array Int dtp))) (=> (bin_p_arr aj aj) (bin_p_arr aj ak))))
(assert (forall ((aj (Array Int dtp)) (ak (Array Int dtp)))
  (=>  (p_arr aj) (not (p 3 aj ak)))))
(assert (forall ((aj (Array Int dtp)) (ak (Array Int dtp)) (ap dtp))
  (or (p (h ap) aj ak) (not (bin_p_arr aj ak)) (not (= (h ap) 0)))))
(assert (forall ((aj (Array Int dtp)) (ak (Array Int dtp)))
  (or (p_arr ak) (not (bin_p_arr aj aj)) (not (p 0 aj ak)))))
(assert (forall ((aj (Array Int dtp)))
  (let ((a!1 (e (select (g (select aj 0)) 0))))
    (or (p_arr aj) (<= a!1 0)))))
(assert (forall ((aj (Array Int dtp)) (ak (Array Int dtp)))
  (let ((a!1 (e (select (g (select ak 0)) 0))))
    (or (not (p 0 aj ak)) (not (<= a!1 0)) (p 3 aj aj)))))
(assert (forall ((aj (Array Int dtp)) (ak (Array Int dtp)) (o (Array Int dtp)) (r arr_int_tuple))
  (let ((a!1 (e (select (g (select ak 0)) 0)))
        (a!2 (e (select (g (select aj 0)) 0)))
        (a!3 (store (g (select ak 0)) 1 (arr_int_tuple (store (d r) 0 0) 0))))
    (or (<= (+ a!1 (* (- 1) a!2)) 0) (bin_p_arr aj (store o 0 (dtp a!3 0)))))))

(check-sat)

A model is given by:

(define-fun bin_p_arr ((x!0 (Array Int dtp)) (x!1 (Array Int dtp))) Bool
    (let ((a!1 (e (select (g (select x!0 0)) 0)))
          (a!2 (e (select (g (select x!1 0)) 0))))
      (not (>= (+ a!1 (* (- 1) a!2)) 0))))
(define-fun p ((x!0 Int) (x!1 (Array Int dtp)) (x!2 (Array Int dtp))) Bool
  (let ((a!1 (e (select (g (select x!1 0)) 0)))
        (a!2 (e (select (g (select x!2 0)) 0))))
  (let ((a!3 (not (>= (+ a!1 (* (- 1) a!2)) 0))))
    (and (or (not (>= x!0 3)) (not (>= a!1 0))) (or (not (<= x!0 0)) a!3)))))
(define-fun p_arr ((A (Array Int dtp))) Bool (>= (e (select (g (select A 0)) 0)) 1))

Contrary to #7466 , this seems to be independent from slicing as we also have

$ z3 fp.xform.slice=false test.smt2 
unsat

I am using Z3 version 4.13.0 - 64 bit.
Is this also a bug?

[hgvk94]

Initially, I suspected it to be a bug in the new mbp. But that doesn't seem to be the case. Looking into it....

[hgvk94]

This problem exposes 2 bugs: one in the previous MBP and one in QEL. In the previous MBP, variable are not removed. In QEL, one of the axioms is not applied properly (the rule to factor out read terms as new variables)

To reproduce the QEL issue:
(declare-datatypes ((arr_int_tuple 0)) (((arr_int_tuple (d (Array Int Int)) (e Int))))) (declare-datatypes ((dtp 0)) (((dtp (g (Array Int arr_int_tuple)) (h Int))))) (declare-fun a () (dtp)) (declare-fun b () (dtp)) (assert (and (<= (e (select (g a) 0)) 0) (not (<= (e (select (g a) 0)) (e (select (g b) 0)))))) (check-sat) (mbp (and (<= (e (select (g a) 0)) 0) (not (<= (e (select (g a) 0)) (e (select (g b) 0))))) (a))
returns true where it should have returned (<= (e (select (g b) 0)) (-1))

[NikolajBjorner]

The function to_lits_qe_lite(lits, non_core); walks m_lits that are initialized in one place.
It is called from m_tg.qel, which is called twice in mbq_qel: void operator()(app_ref_vector &vars, expr_ref &fml, model &mdl)
The first call replaces (g a) by a fresh variable in fml, and removes a from the set of variables to eliminate
The second call revives (g a) from m_lits.

[hgvk94]

We have two terms t1 == (e (select (g a) 0) and t2 == (e (select (g b) 0).
We have the inequality t2 <= t1. LIA implies that t1 <= 0 and therefore t2 <= 0. But t1 is eliminated in the array+adt mbp. The solution would be to have a better integration between array and int mbp.

[NikolajBjorner]

regardless of cause and effect, here is a simpler example:

(declare-datatypes ((arr_int_tuple 0)) (((arr_int_tuple (d (Array Int Int)) (e Int))))) 
(declare-datatypes ((dtp 0)) (((dtp (g (Array Int arr_int_tuple)) (h Int))))) 
;(declare-fun a () (dtp)) 
(declare-fun b () (dtp)) 
(declare-const x (Array Int arr_int_tuple))

(assert (and (<= (e (select x 0)) 0) (not (<= (e (select x 0)) (e (select (g b) 0)))))) 
(check-sat) 
(mbp (and 
       (<= (e (select x 0)) 0) 
       (not (<= (e (select x 0)) (e (select (g b) 0))))) 

(x))

It bypasses the lifting of (g a) and a into fresh variables.

[hgvk94]

What QEL is missing is the project rule in the earlier mbp: https://github.com/Z3Prover/z3/blob/master/src/qe/mbp/mbp_arrays.cpp#L426 (or arithmetic)

[NikolajBjorner]

in my example it should replace x[0] by a fresh variable y (or as bailout a constant using the model).
Then it can replace (e y) by another integer variable and it is done with its work on DT+A.

[NikolajBjorner]

@hgvk94 - what do you suggest we do about this?

[hgvk94]

Good point. Making the ADT rule applicable to terms that contain variables as sub terms does fix the issue (on both our examples). Don't see why that wasn't implemented before. Testing it on other examples ...