;; https://iobservable.net/blog/2017/12/27/playing-with-z3-theorem-prover/ | |
;; https://rise4fun.com/Z3/E8DL | |
(define-fun Mul5 ((x Int)) Int (* x 5)) | |
(define-fun Sub6 ((x Int)) Int (- x 6)) | |
(define-fun Append4 ((x Int)) Int | |
(ite (< x 0) (- (* x 10) 4) (+ (* x 10) 4)) | |
) | |
(declare-fun s1Mul5 () Int) | |
(declare-fun s1Sub6 () Int) | |
(declare-fun s1Append4 () Int) | |
(assert (and (<= 0 s1Mul5) (<= s1Mul5 1))) | |
(assert (and (<= 0 s1Sub6) (<= s1Sub6 1))) | |
(assert (and (<= 0 s1Append4) (<= s1Append4 1))) | |
(assert (= 1 (+ s1Mul5 s1Sub6 s1Append4))) | |
(declare-fun s2Mul5 () Int) | |
(declare-fun s2Sub6 () Int) | |
(declare-fun s2Append4 () Int) | |
(assert (and (<= 0 s2Mul5) (<= s2Mul5 1))) | |
(assert (and (<= 0 s2Sub6) (<= s2Sub6 1))) | |
(assert (and (<= 0 s2Append4) (<= s2Append4 1))) | |
(assert (= 1 (+ s2Mul5 s2Sub6 s2Append4))) | |
(declare-fun s3Mul5 () Int) | |
(declare-fun s3Sub6 () Int) | |
(declare-fun s3Append4 () Int) | |
(assert (and (<= 0 s3Mul5) (<= s3Mul5 1))) | |
(assert (and (<= 0 s3Sub6) (<= s3Sub6 1))) | |
(assert (and (<= 0 s3Append4) (<= s3Append4 1))) | |
(assert (= 1 (+ s3Mul5 s3Sub6 s3Append4))) | |
(declare-fun s4Mul5 () Int) | |
(declare-fun s4Sub6 () Int) | |
(declare-fun s4Append4 () Int) | |
(assert (and (<= 0 s4Mul5) (<= s4Mul5 1))) | |
(assert (and (<= 0 s4Sub6) (<= s4Sub6 1))) | |
(assert (and (<= 0 s4Append4) (<= s4Append4 1))) | |
(assert (= 1 (+ s4Mul5 s4Sub6 s4Append4))) | |
(define-fun Step1 ((x Int)) Int | |
(+ (* s1Mul5 (Mul5 x)) (* s1Sub6 (Sub6 x)) (* s1Append4 (Append4 x))) | |
) | |
(define-fun Step2 ((x Int)) Int | |
(+ (* s2Mul5 (Mul5 x)) (* s2Sub6 (Sub6 x)) (* s2Append4 (Append4 x))) | |
) | |
(define-fun Step3 ((x Int)) Int | |
(+ (* s3Mul5 (Mul5 x)) (* s3Sub6 (Sub6 x)) (* s3Append4 (Append4 x))) | |
) | |
(define-fun Step4 ((x Int)) Int | |
(+ (* s4Mul5 (Mul5 x)) (* s4Sub6 (Sub6 x)) (* s4Append4 (Append4 x))) | |
) | |
(define-fun Level38 ((x Int)) Int | |
(Step4 (Step3 (Step2 (Step1 x)))) | |
) | |
;; 1) Append4 => 4 | |
;; 2) Sub6 => -2 | |
;; 3) Append4 => -24 | |
;; 4) Mul5 => -120 | |
(assert (= (Level38 0) -120)) | |
(check-sat) | |
(get-model) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment