declare-datatypes syntax

declare-datatypes.z3

; z3 supports two types of syntax for declare-datatypes -- z3's own one and smt-lib 2.6 one

; smt-lib 2.6 syntax
 (declare-datatypes (
    (Pair 2)                            ; datatype
  )
  (
    (par (T1 T2) (
      (nil)                             ; constructor 1
      (mk-pair (first T1) (second T2))  ; constructor 2
    ))
  ))

; Z3 syntax
;(declare-datatypes (T1 T2) (
;   (Pair                               ; datatype
;     (nil)                             ; constructor 1
;     (mk-pair (first T1) (second T2))  ; constructor 2
;   )
;))


(declare-const p (Pair Int Int))
(declare-const q (Pair Int Bool))
(simplify (mk-pair 1 2))
(simplify (as nil (Pair Int Int)) )