We're trying to build a solver for a weighted mean function. The code is written in SMT2Lib, and ran by CVC5 or Z3.
However, after adding an assert that indicates the non-negativity of the denominator, the code does not terminate. ("(assert (> tau0_max 0))")
Are there any alternatives to the parameters or the way we can declare the functions differently in order to approach this problem?
(Ints are not suitable to our problem. We'd like to use Rationals, but instead use Reals as they're offered by SMT2Lib).
(set-option :produce-assignments true)
(set-option :produce-models true)
(set-option :produce-proofs true)
(set-logic ALL)
;define data points x_0 x_1 x_2
(declare-fun x (Int) Real)
(declare-fun n () Int)
(define-fun sqr ((x Real)) Real (* x x))
(define-fun max ((x Real) (y Real)) Real (ite (> x y) x y))
;(define-fun c0 ((i Int)) Real 1.0)
(define-fun miu () Real (/ (+ (x 0) (+ (x 1) (+ (x 2) (+ (x 3) (+ (x 4) (+ (x 5) (+ (x 6) (+ (x 7) (+ (x 8) (+ (x 9) (x 10))))))))))) 11.0))
(define-fun miu_c0 () Real (/ (+ (x 0) (+ (x 1) (+ (x 2) (+ (x 3) (+ (x 4) (+ (x 5) (+ (x 6) (+ (x 7) (+ (x 8) (+ (x 9) (+ (x 10) (x 11)))))))))))) 12.0))
(define-fun tau0 ((i Int)) Real (sqr (- (x i) miu_c0)))
(define-fun tau0_max () Real (max (tau0 0) (max (tau0 1) (max (tau0 2) (max (tau0 3) (max (tau0 4) (max (tau0 5) (max (tau0 6) (max (tau0 7) (max (tau0 8) (max (tau0 9) (max (tau0 10) (tau0 11)))))))))))))
**(assert (> tau0_max 0))**
(define-fun c1 ((i Int)) Real (- 1.0 (/ (tau0 i) tau0_max)))
(define-fun miu_c1 () Real (/ (+ (* (c1 0) (x 0)) (+ (* (c1 1) (x 1)) (+ (* (c1 2) (x 2)) (+ (* (c1 3) (x 3)) (+ (* (c1 4) (x 4)) (+ (* (c1 5) (x 5)) (+ (* (c1 6) (x 6)) (+ (* (c1 7) (x 7)) (+ (* (c1 8) (x 8)) (+ (* (c1 9) (x 9)) (+ (* (c1 10) (x 10)) (* (c1 11) (x 11))))))))))))) 12.0))
(define-fun tau1 ((i Int)) Real (sqr (- (x i) miu_c1)))
(define-fun tau1_max () Real (max (tau1 0) (max (tau1 1) (max (tau1 2) (max (tau1 3) (max (tau1 4) (max (tau1 5) (max (tau1 6) (max (tau1 7) (max (tau1 8) (max (tau1 9) (max (tau1 10) (tau1 11)))))))))))))
(define-fun c2 ((i Int)) Real (* (c1 i) (- 1.0 (/ (tau1 i) tau1_max))))
(assert (= (c2 0) 1.0))
(check-sat)
(get-model)