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

[Levent Erkok]

I think the point is that such queries should be rejected by compliant
solvers. Or, contrapositively, any solver not rejecting such a query is
non-compliant with the standard. This follows from the core theory
definition in
http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf,
page 30; which requires equality to receive the same "sort" for its
arguments.

This is not a mere academic interest: At least in my use case the SMT
solver sits at the very end of an already bloated tool chain that generates
bunch of verification-conditions, rewrites them, modifies it in a variety
of ways, and finally ships it off to the solver. If I introduce a bug
somewhere in that tool-chain (quite likely) and thus generate such invalid
queries, I'd very much like the SMT-solver to simply reject my query
instead of silently accepting it and doing something with it. I consider
this a very important, yet oft-overlooked problem, which could have
implications on the adoption of SMT-solvers in the industry.

-Levent.


On Wed, Jul 16, 2014 at 6:23 PM, Andrew Gacek <andrew.gacek at gmail.com>
wrote:

> 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
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>