[SMT-LIB] Mixing Integers and Reals in SMT2 formulas

[Andrew Gacek]

Do not rely on the implicit type conversion of any solver. Instead,
use 'to_real' and 'to_int' to do explicit type conversions. Only send
well-typed formulas to the solver. Then the examples from the first
answer are

(set-logic AUFLIRA)
(declare-fun x () Int)
(assert (= (to_real x) 1.5))
(check-sat)
(exit)

(set-logic AUFLIRA)
(declare-fun x () Int)
(assert (= 1.5 (to_real x)))
(check-sat)
(exit)

Both of these return UNSAT in Z3 and CVC4. If instead, you really
wanted to find the model where x = 1 you should have instead used one
of the queries:

(set-option :produce-models true)
(set-logic AUFLIRA)
(declare-fun x () Int)
(assert (= (to_int 1.5) x))
(check-sat)
(get-model)
(exit)

(set-option :produce-models true)
(set-logic AUFLIRA)
(declare-fun x () Int)
(assert (= x (to_int 1.5)))
(check-sat)
(get-model)
(exit)

Both of these return SAT with x = 1 in Z3 and CVC4.

-Andrew


On Wed, Jul 16, 2014 at 8:08 PM, Iguernelala Mohamed
<mohamed.iguernelala at gmail.com> wrote:
> Hi there,
>
> I wanted to draw your attention to this question:
> http://stackoverflow.com/questions/24790381/why-does-0-0-5/
> in case someone has a better answer/opinion.
>
> Regards,
>
> --
> Mohamed Iguernelala.
> Senior R&D Engineer, OCamlPro
> Research Associate, VALS team, LRI.
> http://www.iguer.info
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib