search

dreal / dreal4

Automated Reasoning in Nonlinear Theories of Reals
https://dreal.github.io
Apache License 2.0
151 stars 32 forks source link

Boolean `define-fun` functions don't work #315

Open percontation opened 3 months ago

percontation commented 3 months ago

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 commented 3 months ago

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 ...)).