Z3 Solver Optimization for Diablo Three Paragon points

gistfile1.txt

;; Critical Hit Chance 50 + 5 * points
;; Attack Speed: +.2% per point, for a maximum of +10% at 50 points.
;; Cooldown Reduction: +2% per point, for a maximum of +10% reduction at 50 points.
;; Critical Hit Chance, +.10% per point, for a maximum of 5% at 50 points.
;; Critical Hit Damage, +1% per point, for a maximum of 50% at 50 points.

(declare-var chdmgp Int)
(declare-var chcp Int)
(declare-var atksp Int)

(define-fun chdmg () Real (+ (* chdmgp 150.0)))
(define-fun chc () Real (+ (* chcp 0.05) 0.10))
(define-fun atks () Real (+ (* chdmgp 0.05) 0.10))

(define-fun dmg () Real (* atks (* chdmg chc)))

;; Cannot exceed 50 points totally
(assert (<= chdmgp 50))
(assert (<= chcp 50))
(assert (<= atksp 50))

;; Total points must be less than 50
(assert (<= 50 (+ chdmgp (+ atksp chcp))))

(maximize dmg)

(set-option :opt.priority box)
(check-sat)
(get-model)