Example of extracting model in z3-rkt, for now...

z3-model.rkt

#lang typed/racket

(require z3/ffi
         z3/smt)

;; Example of how to use Z3-Model in current Racket Z3 library.
;; The common pattern in extracting data with the low-level Z3 library is
;; - querying how many things are there
;; - getting the ith "key" and "value"
;; Some functions used in the following example:
;; - model-get-num-consts, model-get-const-decl, model-get-const-interp
;; - model-get-num-funcs, model-get-func-decl, model-get-func-interp
;; - func-interp-get-num-entries, func-interp-get-entry
;; - func-entry-get-num-args, func-entry-get-arg

(with-new-context
  (declare-const a Int/s)
  (declare-const b Int/s)
  (declare-fun f (Int/s) Int/s)
  (assert! (>=/s a 4))
  (assert! (<=/s a 4))
  (assert! (>/s b a))
  (assert! (>/s (f a) b))
  (assert! (>/s (f b) a))
  (define m (check-sat/model))

  (cond
    [(z3-model? m)

     (define ctx (get-context))
     
     ;; Extract and print constants
     (printf "Constants:~n")
     (for ([i (model-get-num-consts ctx m)])
       (define decl   (model-get-const-decl   ctx m i   ))
       (define interp (model-get-const-interp ctx m decl))
       (printf "  * ~a: ~a~n" (func-decl->string ctx decl) (ast->string ctx interp)))

     ;; Extract and print functions
     (printf "Functions:~n")
     (for ([i (model-get-num-funcs ctx m)])
       (define decl (model-get-func-decl ctx m i))
       
       (with-func-interp ([interp (model-get-func-interp ctx m decl)])
         (printf "  * ~a:~n" (func-decl->string ctx decl))
         ;; print each function entry
         (for ([i (func-interp-get-num-entries ctx interp)])
           (with-func-entry ([entry (func-interp-get-entry ctx interp i)])
             (printf "    | ")
             (for ([i (func-entry-get-num-args ctx entry)])
               (printf "~a " (ast->string ctx (func-entry-get-arg ctx entry i))))
             (printf "-> ~a~n" (ast->string ctx (func-entry-get-value ctx entry)))))
         ;; don't forget the "else" entry
         (printf "    | _ -> ~a~n" (ast->string ctx (func-interp-get-else ctx interp)))))]
    [else (printf "No model: ~a~n" m)])
  )

;; ==>
;; Constants:
;;   * (declare-fun b () Int): 5
;;   * (declare-fun a () Int): 4
;; Functions:
;;   * (declare-fun f (Int) Int):
;;     | 4 -> 6
;;     | 5 -> 5
;;     | _ -> 6

;; Z3 convention: except for Z3-Ast, when any other type has `inc-ref!` and `dec-ref!`
;; functions, it is mandatory to bracket your usage with them.
;; You'll get a seg fault otherwise.

(define-syntax-rule (with-func-interp ([interp mk-interp]) e ...)
  (let ([interp mk-interp])
    (func-interp-inc-ref! (get-context) interp)
    (begin0 (let () e ...)
      (func-interp-dec-ref! (get-context) interp))))

(define-syntax-rule (with-func-entry ([entry mk-entry]) e ...)
  (let ([entry mk-entry])
    (func-entry-inc-ref! (get-context) entry)
    (begin0 (let () e ...)
      (func-entry-dec-ref! (get-context) entry))))