Can't get models for constants of nested datatypes with booleans

[ajalab]

We have a constant x, which is a tuple of two booleans wrapped by Option.

;; ex1.smt2
(get-info :version)

; A tuple of two booleans
; data Tuple = tuple { first :: Bool, second :: Bool }
(declare-datatypes
  ((Tuple 0))
  ((Tuple (tuple
    (first  Bool)
    (second Bool)
))))


; Option type of a tuple
; data Option = none | some { value :: Tuple }}
(declare-datatypes ((Option 0)) ((Option (none) (some (value Tuple)))))

; x :: Option is a constant
(declare-fun x () Option)

; Assertion 1. x has some value
(assert ((_ is (some (Tuple) Option)) x))

; Assertion 2. first (value x) == true
(assert (first (value x)))

(check-sat)
(get-model)

(echo "(first (value x)) = ")
(eval (first (value x)))

I expected that constant x will be like some { value: tuple { first: true, second: <any value> } }. Z3 reports that this formula can be satisfied, however, the satisfying values are hidden by the datatype name Tuple and we cannot get them by using eval command.

$ z3 ex1.smt2
(:version "4.8.1")
sat
(model 
  (define-fun x () Option
    (some Tuple))
)
(first (value x)) = 
(first Tuple)

I think this behavior should be an issue because adding a dummy Int field which is irrelevant to the assertions solves the problem.

;; ex2.smt2
(get-info :version)

; A tuple of two booleans and one integer
; data Tuple = tuple { first :: Bool, second :: Bool, third :: Int }
(declare-datatypes
  ((Tuple 0))
  ((Tuple (tuple
    (first  Bool)
    (second Bool)
    (third  Int)  ; new field
))))

; same as ex1.smt2 ...

$ z3 ex2.smt2
(:version "4.8.1")
sat
(model 
  (define-fun x () Option
    (some (tuple true false 0)))
)
(first (value x)) = 
true

Otherwise using another syntax of declare-datatypes also solves the problem (but it's not a standard SMT-LIB2 format?).

;; ex3.smt2
(get-info :version)

; A tuple of two booleans
; data Tuple = tuple { first :: Bool, second :: Bool }
(declare-datatypes
  () ; ((Tuple 0))
  ((Tuple (tuple
    (first  Bool)
    (second Bool)
))))

; same as ex1.smt2 ...

$ z3 ex3.smt2
(:version "4.8.1")
sat
(model 
  (define-fun x () Option
    (some (tuple true false)))
)
(first (value x)) = 
true

https://gist.github.com/ajalab/98706e47ddc52c7043ded268b9f72193

[NikolajBjorner]

The SMTLIB2.6 grammar for datatypes is a bit different from how you use it. Z3 ends up believing you have a 0-ary constructor Tuple. Try instead:

;; ex1.smt2
(get-info :version)

; A tuple of two booleans
; data Tuple = tuple { first :: Bool, second :: Bool }
(declare-datatypes
((Tuple 0))
(((tup
(first Bool)
(second Bool)))))

; Option type of a tuple
; data Option = none | some { value :: Tuple }}
(declare-datatypes ((Opt 0)) (((none) (some (value Tuple)))))

See also the examples in
http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

[ajalab]

I misunderstood the syntax. Thanks for your comments.

Actually the first SMT2 code was generated by using C API. I was confused because in the C code the solver correctly derived the model but SMT2 code generated by Z3_solver_to_string didn't. There may be something wrong with my implementation so I'll check it carefully.

[NikolajBjorner]

That explains, Z3 produced the incorrect syntax. This is now fixed.