2

In SMT-LIB:

(declare-fun y () Real)
(declare-fun x () Real)
(assert (= 0.0 x))
(assert (= y (/ 1.0 x)))
(check-sat)

Should this model be SAT or UNSAT?

agentp
  • 6,849
  • 2
  • 19
  • 37
Douglas B. Staple
  • 10,510
  • 8
  • 31
  • 58

1 Answers1

1

In SMT-LIB 2.0 and 2.5, all functions are total, so this example is SAT in SMT-LIB. Both Z3 and CVC4 do indeed return SAT for the example in the question.

I found this counter-intuitive. I think it would be mathematically more well justified to say that y=1/x, x=0 is unsatisfiable in the reals. In Mathematica, the equivalent code returns an empty list, indicating that no solution exists, i.e., FindInstance[Element[x, Reals] && Element[y, Reals] && x == 0 && y == 1/x, {x, y}] returns {}

Nonetheless, / is defined this way in SMT-LIB. So as far as Z3 or CVC4 are concerned, this problem is SAT.

Douglas B. Staple
  • 10,510
  • 8
  • 31
  • 58
  • 2
    Yes, that's how SMT defines those operators/functions. A recurring theme that always has exactly 50% supporters and 50% opponents :) – Christoph Wintersteiger Jun 29 '16 at 19:16
  • Thanks a lot Christoph. I ran into this trying to figure out whether or not `(and (= y (^ x 0.5)) (< x 0.0))` should be SAT or UNSAT. For consistency with the rest of SMT, I guess this sqrt example should also be SAT. Now I just need to figure out how to get Z3 to actually give SAT for this sqrt example. – Douglas B. Staple Jun 29 '16 at 19:26