dreal4 icon indicating copy to clipboard operation
dreal4 copied to clipboard

Boolean `define-fun` functions don't work

Open percontation opened this issue 1 year ago • 1 comments

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.

percontation avatar Jul 24 '24 02:07 percontation

More things I noticed that might be relevant:

  1. Certain trivial functions appear to work fine. So, it's not all functions that return Bool.
  2. 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 ...)).

percontation avatar Jul 24 '24 02:07 percontation