RiSE4fun samples for Z3List of built-in samples for the Z3 in RiSE4funen-USrise4fun &copy; 2017 Microsoft Corporationhttp://rise4fun.com//Images/Rise.gifRiSE4fun samples for Z3http://rise4fun.com/Z3/smtc_arithsmtc_arith; This example illustrates basic arithmetic and ; uninterpreted functions (declare-fun x () Int) (declare-fun y () Int) (declare-fun z () Int) (assert (>= (* 2 x) (+ y z))) (declare-fun f (Int) Int) (declare-fun g (Int Int) Int) (assert (< (f x) (g x x))) (assert (> (f y) (g x x))) (check-sat) (get-model) (push) (assert (= x y)) (check-sat) (pop) (exit) http://rise4fun.com/Z3/doc_examplesdoc_examples; This is a basic example that uses comparison ; between integers, push, pop, statistics, and ; retrieves the current assertions (set-option :interactive-mode true) ; enable (get-assertions) command (set-logic QF_LIA) (declare-fun w () Int) (declare-fun x () Int) (declare-fun y () Int) (declare-fun z () Int) (assert (> x y)) (assert (> y z)) (push) (assert (> z x)) (check-sat) (get-info :all-statistics) (pop) (push) (assert (= x w)) (check-sat) (get-assertions) (exit) http://rise4fun.com/Z3/smtc_coresmtc_core; This example illustates extraction ; of unsatisfiable cores (a subset of assertions ; that are mutually unsatisfiable) (set-option :produce-unsat-cores true) (declare-fun p () Bool) (declare-fun q () Bool) (declare-fun r () Bool) (declare-fun s () Bool) ; Z3 will only track assertions that are named. (assert (! (or p q) :named a1)) (assert (! (implies r s) :named a2)) (assert (! (implies s (iff q r)) :named a3)) (assert (! (or r p) :named a4)) (assert (! (or r s) :named a5)) (assert (! (not (and r q)) :named a6)) (assert (! (not (and s p)) :named a7)) (check-sat) (get-unsat-core) http://rise4fun.com/Z3/smtc_datatypessmtc_datatypes; This example illustrates the declaration and ; use of recursive datatypes in Z3. ; List is a builtin datatype defined as in the SMT tutorial at http://www.smtlib.org (declare-fun l1 () (List Int)) (declare-fun l2 () (List Int)) (declare-fun l3 () (List Int)) (declare-fun x () Int) (declare-fun y () Int) (assert (not (= l1 nil))) (assert (not (= l2 nil))) (push) (assert (= (head l1) (head l2))) (assert (= (tail l1) (tail l2))) (push) (assert (not (= l1 l2))) (check-sat) (pop) (check-sat) (eval l1) (eval l2) (pop) (check-sat) (eval l1) (eval l2) (reset) ;; declare a mutually recursive parametric datatype (declare-datatypes (T) ((Tree leaf (node (value T) (children TreeList))) (TreeList nil (cons (car Tree) (cdr TreeList))))) (declare-fun t1 () (Tree Int)) (declare-fun t2 () (Tree Bool)) ;; we must use as to distinguish the leaf (Tree Int) from leaf (Tree Bool) (assert (not (= t1 (as leaf (Tree Int))))) (assert (> (value t1) 20)) (assert (not (is-leaf t2))) (assert (not (value t2))) (check-sat) (get-model) http://rise4fun.com/Z3/strategystrategy; This example illustrates the use of simple strategies for ; solving/simplifying formulas. (declare-fun x () Int) (declare-fun y () Int) (declare-fun a () Bool) (declare-fun b () Bool) (push) (assert (and (= (+ x y) 1) (or (> x 10) (< y 5)))) ; The apply command can be used to preprocess a formula using a given strategy. ; The following strategy just applies the simplifier followed by a simple solver. ; For more information regarding strategies: (help-tactic) (apply (and-then simplify solve-eqs)) (pop) (push) (assert (and (<= 0 x) (<= x 10) (<= 0 y) (<= y 5) (>= (+ (* 3 x) (* 5 y)) 12))) ; simplify and then convert into a 0-1 problem (apply (and-then simplify lia2pb)) ; simplify, convert into 0-1 problem, and then convert into sat ; Remark: pb2bv expects that the right hand side of all inequalities is just a numeral. ; We accomplish that by prodiving the parameter :arith-lhs to the simplifier. (apply (and-then simplify lia2pb (using-params simplify :arith-lhs true) pb2bv)) ; We can use the following strategy to solve the problem (set-option :produce-models true) (check-sat-using (and-then simplify lia2pb (using-params simplify :arith-lhs true) pb2bv bit-blast sat)) (help-tactic) (exit)http://rise4fun.com/Z3/smtc_arrayssmtc_arrays; This example illustrates different uses of the arrays ; supported in Z3. ; This includes Combinatory Array Logic (de Moura & Bjorner, FMCAD 2009). ; (define-sort A () (Array Int Int)) (declare-fun x () Int) (declare-fun y () Int) (declare-fun z () Int) (declare-fun a1 () A) (declare-fun a2 () A) (declare-fun a3 () A) (push) ; illustrate select-store (assert (= (select a1 x) x)) (assert (= (store a1 x y) a1)) (check-sat) (get-model) (assert (not (= x y))) (check-sat) (pop) (define-fun all1_array () A ((as const A) 1)) (simplify (select all1_array x)) (define-sort IntSet () (Array Int Bool)) (declare-fun a () IntSet) (declare-fun b () IntSet) (declare-fun c () IntSet) (push) ; illustrate map (assert (not (= ((_ map and) a b) ((_ map not) ((_ map or) ((_ map not) b) ((_ map not) a)))))) (check-sat) (pop) (push) (assert (and (select ((_ map and) a b) x) (not (select a x)))) (check-sat) (pop) (push) (assert (and (select ((_ map or) a b) x) (not (select a x)))) (check-sat) (get-model) (assert (and (not (select b x)))) (check-sat) ;; unsat, so there is no model. (pop) (push) ; illustrate default (assert (= (default a1) 1)) (assert (not (= a1 ((as const A) 1)))) (check-sat) (get-model) (assert (= (default a2) 1)) (assert (not (= a1 a2))) (check-sat) (get-model) (pop) (exit) http://rise4fun.com/Z3/smtc_bvsmtc_bv; This example illustrates macros and ; bit-vectors. ; The problem is to verify a program that checks ; if a bit-vector represents a power of two or is zero. ; (as at most one bit set) (define-fun is-power-of-two ((x (_ BitVec 32))) Bool (= #x00000000 (bvand x (bvsub x #x00000001)))) (define-fun check-power-of-two ((x (_ BitVec 32)) (sh (_ BitVec 32))) Bool (= x (bvshl #x00000001 sh))) (define-fun check-power-of-two-1 ((x (_ BitVec 32)) (sh (_ BitVec 32))) Bool (let ((sh1 (bvshl sh #x00000001))) (or (check-power-of-two x sh1) (check-power-of-two x (bvadd #x00000001 sh1))))) (define-fun check-power-of-two-2 ((x (_ BitVec 32)) (sh (_ BitVec 32))) Bool (let ((sh1 (bvshl sh #x00000001))) (or (check-power-of-two-1 x sh1) (check-power-of-two-1 x (bvadd #x00000001 sh1))))) (define-fun check-power-of-two-3 ((x (_ BitVec 32)) (sh (_ BitVec 32))) Bool (let ((sh1 (bvshl sh #x00000001))) (or (check-power-of-two-2 x sh1) (check-power-of-two-2 x (bvadd #x00000001 sh1))))) (define-fun check-power-of-two-4 ((x (_ BitVec 32)) (sh (_ BitVec 32))) Bool (let ((sh1 (bvshl sh #x00000001))) (or (check-power-of-two-3 x sh1) (check-power-of-two-3 x (bvadd #x00000001 sh1))))) (define-fun check-power-of-two-5 ((x (_ BitVec 32)) (sh (_ BitVec 32))) Bool (let ((sh1 (bvshl sh #x00000001))) (or (check-power-of-two-4 x sh1) (check-power-of-two-4 x (bvadd #x00000001 sh1))))) (declare-fun x () (_ BitVec 32)) (declare-fun y () (_ BitVec 32)) (declare-fun z () (_ BitVec 32)) (push) (assert (not (implies (is-power-of-two x) (check-power-of-two-5 x #x00000000)))) (check-sat) (get-model) (push) (define-fun is-zero-on-zero () Bool (implies (is-power-of-two x) (not (= #x00000000 x)))) (assert (not is-zero-on-zero)) (check-sat) (get-model) (pop) (define-fun check-power-of-two-6 ((x (_ BitVec 32)) (sh (_ BitVec 32))) Bool (let ((sh1 (bvshl sh #x00000001))) (or (check-power-of-two-5 x sh1) (check-power-of-two-5 x (bvadd #x00000001 sh1))))) (assert (not (implies (is-power-of-two x) (check-power-of-two-6 x #x00000000)))) (check-sat) (pop) http://rise4fun.com/Z3/bit-countbit-count; This is a faulty specification or ; implementation of an efficient bit-counting program. ; Can you correct it? ; nb1 is the specification. ; nb2 is the implementation. (define-fun nb1 ((x (_ BitVec 32))) (_ BitVec 32) (bvadd (ite (= ((_ extract 31 31) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 30 30) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 29 29) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 28 28) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 27 27) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 26 26) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 25 25) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 24 24) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 23 23) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 22 22) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 21 21) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 20 20) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 19 19) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 18 18) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 17 17) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 16 16) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 15 15) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 14 14) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 13 13) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 12 12) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 11 11) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 10 10) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 9 9) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 8 8) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 7 7) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 6 6) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 5 5) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 4 4) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 3 3) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 2 2) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 1 1) x) #b0) #x00000001 #x00000000) (ite (= ((_ extract 0 0) x) #b0) #x00000001 #x00000000))) (declare-fun nX () (_ BitVec 32)) (define-fun nb2 ((x (_ BitVec 32))) (_ BitVec 32) (let ((nc2 x)) (let ((nc2 (bvadd (bvand nc2 #x00005555) (bvand ((_ rotate_right 1) nc2) #x00005555)))) (let ((nc2 (bvadd (bvand nc2 #x00003333) (bvand ((_ rotate_right 1) nc2) #x00003333)))) (let ((nc2 (bvadd (bvand nc2 #x00000077) (bvand ((_ rotate_right 2) nc2) #x00000077)))) (let ((nc2 (bvadd (bvand nc2 #x0000000F) (bvand ((_ rotate_right 4) nc2) #x0000000F)))) nc2)))))) (assert (not (= (nb1 nX) (nb2 nX)))) (check-sat) (get-model)