Unexpected reference to k!0 and k!1 in model.

[LeventErkok]

For this benchmark:

(set-option :produce-models true)
(set-logic ALL)

(declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
                                    ((mkSBVTuple2 (proj_1_SBVTuple2 T1)
                                                  (proj_2_SBVTuple2 T2))))))

(define-fun s1 () (SBVTuple2 (Array Bool Bool) (Array Bool Bool))
		  (mkSBVTuple2 ((as const (Array Bool Bool)) false)
		               ((as const (Array Bool Bool)) false)))

(declare-fun s0 () (SBVTuple2 (Array Bool Bool) (Array Bool Bool)))

(define-fun s2 () Bool (distinct s0 s1))

(assert s2)

(check-sat)
(get-value (s0))

z3 reports:

sat
((s0 (mkSBVTuple2 (_ as-array k!1) (_ as-array k!0))))

which has references to k!0 and k!1 that seems to be left stray from substitution. (Originally reported by Joshua Moerman on SBV.)

[NikolajBjorner]

this is now addressed in current master.

[LeventErkok]

Thanks! Works just fine indeed.

[Jaxan]

I have a larger program where the issue remains. So it is not completely fixed. (I cannot re-open this issue.) I have tried to make a smaller test-case, but it's very hard because each change has a big impact on the models. SMT code:

(declare-datatypes () ((State S1 S2 S3 S4)))
(declare-datatypes (T) ((Pair (mk-pair (first T) (second T)))))
(declare-datatypes () ((Aut (mk (states (Set State)) (init (Set State)) (final (Set State)) (delta (Set (Pair State))) ))))

(define-fun acc0 ((x State) (aut Aut)) Bool (select (final aut) x))
(define-fun acc1 ((x State) (aut Aut)) Bool (exists ((y State)) (and (select (states aut) y) (select (delta aut) (mk-pair x y)) (acc0 y aut))))

(define-fun accept0 ((aut Aut)) Bool (exists ((x State)) (and (select (states aut) x) (select (init aut) x) (acc0 x aut))))
(define-fun accept1 ((aut Aut)) Bool (exists ((x State)) (and (select (states aut) x) (select (init aut) x) (acc1 x aut))))

(define-fun equiv1 ((a1 Aut) (a2 Aut)) Bool (and (= (accept0 a1) (accept0 a2)) (= (accept1 a1) (accept1 a2))))

(declare-const m Aut)
(define-const m1 Aut (mk ((as const (Set State)) false) ((as const (Set State)) false) ((as const (Set State)) false) ((as const (Set (Pair State))) false) ))
(define-const m2 Aut (mk (lambda ((x!1 State)) (or (= x!1 S2) (= x!1 S3))) (lambda ((x!1 State)) (= x!1 S2)) (store ((as const (Set State)) true) S1 false) (lambda ((x!1 (Pair State))) (= x!1 (mk-pair S2 S2)))))
(assert (not (equiv1 m m1)))

(check-sat) ; without this, the next check-sat gives "unknown"
(get-model) ; without this, the next get-model gives something else

(assert (not (equiv1 m m2)))

(check-sat)
(get-model) ; This model is bugged

Unexpected output:

(model 
  (define-fun m () Aut
    (let ((a!1 (lambda ((x!1 State))
             (or (= (ite (= x!1 S4) S4 S1) S1) (= (ite (= x!1 S4) S4 S1) S4)))))
  (mk a!1
      (_ as-array k!34)
      (_ as-array k!33)
      ((as const (Set (Pair State))) true))))
  (define-fun k!34 ((x!0 State)) Bool
    (or (= (ite (= x!0 S4) S4 S1) S3) (= (ite (= x!0 S4) S4 S1) S4)))
  (define-fun k!33 ((x!0 State)) Bool
    (or (= (ite (= x!0 S4) S4 S1) S1) (= (ite (= x!0 S4) S4 S1) S3)))
)

You see that the definition of m refers to k!34 and k!33. When I use (get-value (m)) instead of (get-model), those definitions are not even shown.

Sorry that I was not able to make a smaller test-case.

This is tested on HEAD (git commit 35fa24a).

[NikolajBjorner]

In this case, the definition of k!33 and k!34 are accessible in the model.
It would be nicer for sure to inline also these, but generally it isn't done because in-lining could be too expensive. So the general scheme is to rely on the model where shared definitions are accessible.

[Jaxan]

I see; that makes sense. However, in the case of (get-value (m)), I think that it should always be inlined. (SBV requires this as well.)

Thanks for the reply!

[LeventErkok]

@NikolajBjorner

I understand the need for avoiding expensive inlining, but that makes upstream tooling rather difficult. I'm curious if there might be a compromise. You already have these two settings:

(set-option :pp.max_depth      4294967295)
(set-option :pp.min_alias_size 4294967295)

They control how much inlining the pretty-printer does. Perhaps you can provide a similar setting with a low default value to avoid costs but allow end-users to avoid these issues? In fact, why not just use these settings directly for the inlining as well? (I just tried, makes no difference on this example.)

[LeventErkok]

Just tried (set-option :model.inline_def true) on this example, and works perfectly! Thanks for quickly addressing this Nikolaj.

[Jaxan]

I can confirm, the patch works. Thanks a lot!