As I was using Floats and Reals in the same .smt2 file, I noticed that this would often lead to the result being "unknown". I have seen this mentioned here but as some time has passed since this answer I wanted to ask if maybe I'm simply not using the correct settings (e.g. Should I maybe be passing a tactic as parameter in the check-sat line? Or narrowing down set-logic?)
Here is an example that exhibits the behavior:
(set-logic ALL)
(set-option :produce-models true)
(set-info :smt-lib-version 2.6)
(set-info :status unknown)
(define-sort FPN () (_ FloatingPoint 8 24))
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun x0 () FPN)
(declare-fun y0 () FPN)
(declare-fun z0 () FPN)
(declare-fun x1 () FPN)
(declare-fun y1 () FPN)
(declare-fun z1 () FPN)
(define-fun fun ( (x FPN) (y FPN) (z FPN) (arg0 Real) (arg1 Real) (arg2 Real)) FPN (fp.add RNE
(fp.add RNE (fp.mul RNE ((_ to_fp 8 24) RNE arg0) x)
(fp.mul RNE ((_ to_fp 8 24) RNE arg1) y))
(fp.mul RNE ((_ to_fp 8 24) RNE arg2) z)) )
(assert (fp.eq x0 ((_ to_fp 8 24) RNE 1)))
(assert (fp.eq y0 ((_ to_fp 8 24) RNE 0)))
(assert (fp.eq z0 ((_ to_fp 8 24) RNE 0)))
(assert (fp.eq x1 ((_ to_fp 8 24) RNE 0)))
(assert (fp.eq y1 ((_ to_fp 8 24) RNE 0)))
(assert (fp.eq z1 ((_ to_fp 8 24) RNE 0)))
(assert
(fp.gt (fun x0 y0 z0 a b c) (fun x1 y1 z1 a b c))
)
(check-sat)
(get-info :reason-unknown)
(get-model)
(exit)
Thank you so much for any responses!
I'm afraid not much has changed since then. Mixing floats and reals like this creates really difficult problems for SMT solvers to deal with. You can file specific cases at the z3 issue tracker (https://github.com/Z3Prover/z3/issues) to alert the developers, alas I doubt there'll be much of an improvement any time soon.
Note that it's always a good idea to try other solvers as well. CVC5 and MathSAT both support floats and reals together. Unfortunately, when I call mathsat on your problem it errors out with a syntax error (I think it's a bug in mathsat itself), but CVC5 does indeed find the following model:
(
(define-fun a () Real (/ 1 4294967296))
(define-fun b () Real (- 1.0))
(define-fun c () Real (- 1.0))
(define-fun x0 () (_ FloatingPoint 8 24) (fp #b0 #b01111111 #b00000000000000000000000))
(define-fun y0 () (_ FloatingPoint 8 24) (fp #b0 #b00000000 #b00000000000000000000000))
(define-fun z0 () (_ FloatingPoint 8 24) (fp #b0 #b00000000 #b00000000000000000000000))
(define-fun x1 () (_ FloatingPoint 8 24) (fp #b0 #b00000000 #b00000000000000000000000))
(define-fun y1 () (_ FloatingPoint 8 24) (fp #b0 #b00000000 #b00000000000000000000000))
(define-fun z1 () (_ FloatingPoint 8 24) (fp #b0 #b00000000 #b00000000000000000000000))
)
I haven't checked if the model is actually valid, but it's good news that CVC5 can handle this problem out-of-the-box (and quickly too.)