CODEWITHSUNDEEP
z3smt
paubo147
paubo147

Reputation: 778

Exclusive datatypes in z3 (follow up)

I declared an exclusive datatype in z3 as well as a constant and a little assertion:

(declare-datatypes () ((IntOrBool (bpart (b Bool)) (ipart (i Int)))))
(declare-fun iob () (IntOrBool))    
(assert (= true (b iob)))

I get the expected result (bpart true), but with 

(assert (= 1 (i iob)))

z3 reports (bpart false). Does z3 ignore the assertion I gave? If he treats the datatype as a non-exclusive one, how can I force z3 to return an ipart as result?

Upvotes: 1

Views: 80

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8369

The functions "b" and "I" are accessors. They can have arbitrary interpretations when applied to a constructor that does not match. So Z3 finds a model where iob is set to (bpart false) and (i (bpart false)) is interpreted as 1. You could force the right constructor by asserting instead:

 (assert (= (bpart true) iob))

or

(assert (= (ipart 1) iob))

Upvotes: 1

Related Questions