Invalid interpretations produced by Spacer

[rodrigo7491]

Hi,

While trying to validate the interpretations generated by Spacer for a number of CHC-comp instances, I believe I found some examples in which invalid interpretations are generated. Below is an explanation of the validation procedure and one example for reproducibility.

For a given satisfiable system of CHCs of form P1(X1) /\ ... /\ Pn(Xn) /\ cons => H(X), implicitly quantified, an SMT instance is generated for each clause in the system. Each SMT instance consists of the interpretations of the predicates generated by Spacer together with the constraints P1(X1) /\ ... /\ Pn(Xn) /\ cons /\ (not H(X)), i.e., body /\ (not head). For the interpretations to be valid all the SMT instances need to be unsatisfiable.

For the chc-LIA-Lin_325 instance, the interpretation generated by Spacer is invalid w.r.t the last CHC of the system. Both Z3 and CVC5 can find a satisfiable assignment for the SMT instance in question, shown below.

(set-logic LIA)

(define-fun main_1 ((x!0 Int) (x!1 Int) (x!2 Int) (x!3 Int)) Bool
    (let ((a!1 (not (>= (+ x!2 (* (- 2) x!3)) (- 1))))
          (a!2 (not (<= (+ x!2 (* (- 2) x!3)) (- 3))))
          (a!3 (not (<= (+ (* 2 x!1) (* (- 1) x!2)) 1)))
          (a!4 (exists ((x!4 Int) (x!5 Int) (x!6 Int))
                 (! (let ((a!1 (not (>= (+ x!2 (* (- 2) x!3)) (- 1))))
                          (a!2 (not (<= (+ x!2 (* (- 2) x!3)) (- 3))))
                          (a!3 (not (<= (+ (* 2 x!1) (* (- 1) x!2)) 1))))
                      (and a!1
                           a!2
                           a!3
                           (= x!6 (+ 1 x!3))
                           (not (= x!5 0))
                           (= x!5 (+ 2 x!2))
                           (not (= x!5 x!4))
                           (<= x!1 x!3)
                           (= x!4 (* 2 x!1))
                           (= x!0 2)))
                    :weight 0))))
      (or (= x!0 0) (and a!1 a!2 a!3) a!4)))

(declare-fun A ()  Int)
(declare-fun B ()  Int)
(declare-fun C ()  Int)
(declare-fun v_3 ()  Int)

(assert
    (and
      (and
        (main_1 v_3 A B C)
        (= 2 v_3)
      )
      (not false)
    )
)

(check-sat)
(exit)

The example shown is for a system of linear CHCs, but this problem also occurs with nonlinear CHCs, e.g., the 8th clause of chc-LIA_361.

Z3 version: 4.12.1 OS: Linux Mint 20.2 and Ubuntu 20.04.1

[hgvk94]

I cannot reproduce the issue. For the instance chc-LIA-Lin_325, when I run z3 without any parameters, I am getting the following model:

(define-fun main_1 ((x!0 Int) (x!1 Int) (x!2 Int) (x!3 Int)) Bool
  (let ((a!1 (not (>= (+ x!2 (* (- 2) x!3)) (- 1))))
        (a!2 (not (<= (+ (* 2 x!1) (* (- 1) x!2)) 1)))
        (a!3 (not (<= (+ x!2 (* (- 2) x!3)) (- 3)))))
    (and (or (not (>= x!0 1)) a!1)
         (not (>= x!0 2))
         (or (not (>= x!0 1)) a!2)
         (or (not (>= x!0 1)) a!3))))

What parameters are you using?

We also have an external model validator which uses z3s python API.

Finally, models are only valid modulo preprocessing. There are simplifications that do not preserve models. See for example issue on ghub

[rodrigo7491]

I'm not using any parameters when running Z3. I built from master to check and it gives me the model you posted, which is different from the one obtained with the 4.12.1 release. Both models have the same issue, however.

Thanks for mentioning #5887 (which links to #5920), I didn't know this was an issue with Z3. For the instances I mentioned, both Eldarica and Golem generate valid models, so I was not expecting Spacer to behave this way.

I'm not using the Python API, so I can't try the external model validator you mentioned now, but I will keep it in mind.

[hgvk94]

This model does satisfy the last CHC because it has the literal (not (>= x!0 2)) .

[rodrigo7491]

The model you posted is indeed valid, apologies for the mistake. The one I got with master is not identical to it actually.

Model from master (62e1ec069853b22bb82090c17dfbcd013dfd5088)

(define-fun main_1 ((x!0 Int) (x!1 Int) (x!2 Int) (x!3 Int)) Bool
    (let ((a!1 (not (>= (+ x!2 (* (- 2) x!3)) (- 1))))
          (a!2 (not (<= (+ x!2 (* (- 2) x!3)) (- 3))))
          (a!3 (not (<= (+ (* 2 x!1) (* (- 1) x!2)) 1)))
          (a!4 (not (= x!2 (+ (- 2) (* 2 x!1))))))
      (or (= x!0 0)
          (and (= x!0 2) a!1 a!2 a!3 (not (= x!2 (- 2))) a!4 (<= x!1 x!3))
          (and a!1 a!2 a!3))))