RiSE4fun samples for Z3OptList of built-in samples for the Z3Opt in RiSE4funen-USrise4fun &copy; 2017 Microsoft Corporationhttp://rise4fun.com//Images/Rise.gifRiSE4fun samples for Z3Opthttp://rise4fun.com/Z3Opt/opt.lexopt.lex(declare-const x Int) (declare-const y Int) (declare-const z Int) (assert (< x z)) (assert (< y z)) (assert (< z 5)) (assert (not (= x y))) (maximize x) (maximize y) (check-sat) (get-model) http://rise4fun.com/Z3Opt/opt.paretoopt.pareto(declare-const x Int) (declare-const y Int) (assert (>= 5 x)) (assert (>= x 0)) (assert (>= 4 y)) (assert (>= y 0)) (minimize x) (maximize (+ x y)) (minimize y) (set-option :opt.priority pareto) (check-sat) http://rise4fun.com/Z3Opt/opt.boxopt.box(declare-const x Real) (declare-const y Real) (assert (>= 5 (- x y))) (assert (>= x 0)) (assert (>= 4 y)) (assert (> y 0)) (minimize x) (maximize (+ x y)) (minimize y) (maximize y) (set-option :opt.priority box) (check-sat) http://rise4fun.com/Z3Opt/opt.dlopt.dl(set-option :smt.arith.solver 1) ; enables difference logic solver for sparse constraints (set-option :smt.arith.solver 3) ; enables difference logic solver for dense constraints (declare-const x Int) (declare-const y Int) (assert (>= 10 x)) (assert (>= x (+ y 7))) (maximize (+ x y)) (check-sat) http://rise4fun.com/Z3Opt/opt.pbopt.pb(declare-const p_0_0 Int) (declare-const p_0_1 Int) (declare-const p_0_2 Int) (declare-const p_0_3 Int) (declare-const p_0_4 Int) (declare-const p_1_0 Int) (declare-const p_1_1 Int) (declare-const p_1_2 Int) (declare-const p_1_3 Int) (declare-const p_1_4 Int) (declare-const p_2_0 Int) (declare-const p_2_1 Int) (declare-const p_2_2 Int) (declare-const p_2_3 Int) (declare-const p_2_4 Int) (declare-const p_3_0 Int) (declare-const p_3_1 Int) (declare-const p_3_2 Int) (declare-const p_3_3 Int) (declare-const p_3_4 Int) (assert (and (<= 0 p_0_0) (<= p_0_0 1))) (assert (and (<= 0 p_0_1) (<= p_0_1 1))) (assert (and (<= 0 p_0_2) (<= p_0_2 1))) (assert (and (<= 0 p_0_3) (<= p_0_3 1))) (assert (and (<= 0 p_0_4) (<= p_0_4 1))) (assert (and (<= 0 p_1_0) (<= p_1_0 1))) (assert (and (<= 0 p_1_1) (<= p_1_1 1))) (assert (and (<= 0 p_1_2) (<= p_1_2 1))) (assert (and (<= 0 p_1_3) (<= p_1_3 1))) (assert (and (<= 0 p_1_4) (<= p_1_4 1))) (assert (and (<= 0 p_2_0) (<= p_2_0 1))) (assert (and (<= 0 p_2_1) (<= p_2_1 1))) (assert (and (<= 0 p_2_2) (<= p_2_2 1))) (assert (and (<= 0 p_2_3) (<= p_2_3 1))) (assert (and (<= 0 p_2_4) (<= p_2_4 1))) (assert (and (<= 0 p_3_0) (<= p_3_0 1))) (assert (and (<= 0 p_3_1) (<= p_3_1 1))) (assert (and (<= 0 p_3_2) (<= p_3_2 1))) (assert (and (<= 0 p_3_3) (<= p_3_3 1))) (assert (and (<= 0 p_3_4) (<= p_3_4 1))) (assert (>= 1 (+ p_0_0 p_0_1 p_0_2 p_0_3 p_0_4))) (assert (<= 1 (+ p_0_0 p_0_1 p_0_2 p_0_3 p_0_4))) (assert (>= 1 (+ p_1_0 p_1_1 p_1_2 p_1_3 p_1_4))) (assert (<= 1 (+ p_1_0 p_1_1 p_1_2 p_1_3 p_1_4))) (assert (>= 1 (+ p_2_0 p_2_1 p_2_2 p_2_3 p_2_4))) (assert (<= 1 (+ p_2_0 p_2_1 p_2_2 p_2_3 p_2_4))) (assert (>= 1 (+ p_3_0 p_3_1 p_3_2 p_3_3 p_3_4))) (assert (<= 1 (+ p_3_0 p_3_1 p_3_2 p_3_3 p_3_4))) (assert (>= 1 (+ p_0_0 p_1_0 p_2_0 p_3_0))) (assert (>= 1 (+ p_0_1 p_1_1 p_2_1 p_3_1))) (assert (>= 1 (+ p_0_2 p_1_2 p_2_2 p_3_2))) (assert (>= 1 (+ p_0_3 p_1_3 p_2_3 p_3_3))) (assert (>= 1 (+ p_0_4 p_1_4 p_2_4 p_3_4))) (minimize (+ p_0_0 p_1_1 p_2_2 p_3_3)) (check-sat) (get-model)