[YICES-HELP] Modeling recursive datatype definitions with uninterpreted types

[Bruno Dutertre]

Avik Chaudhuri wrote:
> Hello,
> 
> I am trying to model the following recursive Expression language in 
> Yices, to interface with a symbolic execution engine for a larger 
> language. I want to test equality/inequality between Expressions as well 
> as get out models when necessary.
> 
> (define-type Expression
>  (datatype
>    (integer ic::int)
>    (hash ac::(-> int Expression))
>    null
>  )
> )
> 
> Since Yices does not allow such a recursive definition, I am using the 
> following weaker definition instead.
> 
> (define-type UExpression)
> 
> (define-type Expression
>  (datatype
>    (integer ic::int)
>    (hash ac::(-> int UExpression))
>    null
>  )
> )
> 
> As long as I do not use strict typechecking (using -tc), I get correct 
> answers for problems such as the following, where Expressions appear 
> consistently where UExpressions are expected.
> 
> (define basehash::(-> int UExpression))
> 
> (define x::Expression (hash (update (update basehash (0) null) (1) 
> (integer 0))))
> (define y::Expression (hash (update (update (hc x) (1) (integer 0)) (0) 
> null)))
> 
> ;; (assert (/= x y))
> ;; result: unsat
> 
> (assert (= x y))
> 
> (define z::Expression (hash (update (hc y) (2) x)))
> 
> (assert (= x z))
> ;; result: a suitable model for basehash
> 
> (check)
> 
> ====
> 
> My question is, will I ever get unexpected results if I ask such 
> queries? More formally, suppose that I only ever make 
> equality/inequality assertions over Expressions, and I never 
> "instantiate" UExpression with anything other than Expression.
> Am I guaranteed to get reasonable results? Is there any other discipline 
> I need to follow for this to work?
> 

Avik,

It's easy to get circular Expression using this trick, which may or
may not be reasonable. Normal interpretation of recursive data types
would disallow such circular structures. For example, you can try

  (define z::Expression)
  (assert (= z (hash (update (hc y) (2) z)))))
  (check)

and you'll get a model. There may be other risks too (including
segmentation faults and infinite loops), but I can't look into this
in much details, so I'm not really sure. Use at your own risks!

Bruno