RiSE4fun samples for Z3OptList of built-in samples for the Z3Opt in RiSE4funen-USrise4fun © 2017 Microsoft Corporationhttp://rise4fun.com//Images/Rise.gifRiSE4fun samples for Z3Opt- http://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)