Z3 Java API defining a function -

i need defining function z3 java api. try solve (which working fine z3.exe process):

(declare-fun () real) (declare-fun b () real) (declare-fun c () bool)  (define-fun max2 ((x real) (y real)) real (ite (<= x y) y x))  (assert (and (>= 0.0) (<= 100.0))) (assert (or (= (max2 (+ 100.0 (* (- 1.0) a)) (/ 1.0 1000.0)) 0.0) c (not (= b 0.0))))  (check-sat-using (then simplify bit-blast qfnra)) (get-model) 

the result of smt-file is:

sat (model   (define-fun () real     1.0)   (define-fun c () bool     false)   (define-fun b () real     1.0) ) 

the problem is: there no option, define function java api. in post (equivalent of define-fun in z3 api), noticed use following statement in java api:

(declare-fun max2 (real real) real) (assert (forall ((y real) (x real)) (= (max2 y x) (ite (<= x y) y x)))) 

so replaced (define-fun max2 ((x real) (y real)) real (ite (<= x y) y x)) in smt-file , started z3.exe process again. result following:

unknown (model   (define-fun b () real     0.0) ) 

so, can see, there no satisfiable result more. translating in java, same result unknown.

any ideas, can do?

there no equivalent function definitions because aren't necessary, define-fun macro. equivalent thing in api build expression function , every application of function, substitute argument values input values, e.g., using expr.substitute.

like leo mentioned in post cited, use of quantifiers possible purpose, solver give , return unknown because thinks formula hard solve. can around using macro finder (see cited post), recognize kind of macro.