Skip to content

Instantly share code, notes, and snippets.

# slavchev/level38.smt Created Dec 27, 2017

 ;; 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)
to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.