level38.smt

;; 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)