shelling out to z3 from clojure 1.12

z3.clj

;; rdfs:seeAlso <https://microsoft.github.io/z3guide/docs/logic/Lambdas>
(require '[clojure.edn :as edn])
(require '[clojure.java.process :as proc])
(require '[clojure.java.io :as io])

;; TODO: this can be simplified with a clojure macro (load-z3 forms...) 

(let [input  (java.io.File/createTempFile "input" ".z3")]
       
  (doseq [form '[(declare-const a Int)
                 (declare-const b Int)
                 (declare-const c Int)
                 (simplify (select (lambda ((x Int) (y Int) (z Int)) (+ x (* z y))) a b c))]]
    (spit input (pr-str form) :append true))
       
  (edn/read-string (proc/exec {:in (proc/from-file input)} "z3" "-in")))
  
;;=>
(+ a (* b c))

(let [input (java.io.File/createTempFile "input" ".z3")]
       
  (doseq [form '[(declare-const m (Array Int Int))
                 (declare-const m1 (Array Int Int))
                 (declare-const z Int)
                 (define-fun memset ((lo Int) (hi Int) (y Int) (m (Array Int Int))) 
                   (Array Int Int) 
                   (lambda ((x Int)) (if (and (<= lo x) (<= x hi)) y (m x))))
                 (assert (= m1 (memset 1 700 z m)))
                 (assert (not (= (select m1 6) z)))
                 (check-sat)]]
    (spit input (pr-str form) :append true))
       
  (edn/read-string (proc/exec {:in (proc/from-file input)} "z3" "-in")))

;;=>
unsat

(let [input (java.io.File/createTempFile "input" ".z3")]
       
  (doseq [form '[(define-funs-rec 
                   ((ping ((x Int) (y Bool)) Int)
                    (pong ((a Int) (b Bool)) Int))

                   ((if y (pong (+ x 1) (not y)) (- x 1))
                    (if b (ping (- a 1) (not b)) a)))

                 (declare-const x Int)
                 (assert (> x 0))
                 (assert (> (ping x true) x))
                 (check-sat)
                 (get-model)]]
     (spit input (pr-str form) :append true))
       
 (edn/read-string (proc/exec {:in (proc/from-file input)} "z3" "-in")))

;;=>
sat

(let [input (java.io.File/createTempFile "input" ".z3")
           output (java.io.File/createTempFile "output" ".txt")]
       
       (doseq [form '[(set-option :smt.mbqi true)
                      (declare-fun f (Int Int) Int)
                      (declare-const a Int)
                      (declare-const b Int)

                      (assert (forall ((x Int)) (= (f x x) (+ x a))))

                      (assert (< (f a b) a))
                      (assert (< a 0))
                      (check-sat)
                      (get-model)

                      (eval (f (+ a 10) 20))]]
         (spit input (pr-str form) :append true))
       
       (proc/exec {:in (proc/from-file input)
                   :out (proc/to-file output)}
                  "z3" "-in")

       (with-open [r (java.io.PushbackReader. (io/reader output))]
         (into [] (take-while some?) (repeatedly #(edn/read {:eof nil} r)))))

;;=>
[sat
 ((define-fun b () Int 0)
  (define-fun a () Int (- 1))
  (define-fun
   f
   ((x!0 Int) (x!1 Int))
   Int
   (ite (and (= x!0 (- 1)) (= x!1 0)) (- 2) (+ (- 1) x!0))))
 8]