dreal4
dreal4 copied to clipboard
Boolean `define-fun` functions don't work
On dReal v4.21.06.1:
(set-logic QF_NRA)
(declare-fun a () Real)
(define-fun eqfn ((x Real) (y Real)) Bool (= x y))
(assert (eqfn a 1.0))
(assert (eqfn a 2.0))
(check-sat)
(get-model)
(exit)
returns satisfiable.
It seems like all define-fun functions that return a Bool don't work correctly.
More things I noticed that might be relevant:
- Certain trivial functions appear to work fine. So, it's not all functions that return Bool.
- Everything appears to work fine if you smuggle the value of the Bool as a Real, e.g.
(define-fun eqfn ((x Real) (y Real)) Real (ite (= x y) 1.0 0.0))and replacing call sites with(= 1.0 (eqfun ...)).