[YICES-HELP] logic definiton in yices v1

[Bruno Dutertre]

André Scholz wrote:
> Hello,
> 
> why does
> 
> prompt> yices -smt test.smt
> 
> answer "sat" on the following file. More specific, why can i specify a variable 
> to be Real, when i am using the logic of linear "integer" arithmetic? I can 
> even omit the :logic line without Yices complaining. Does Yices infer which 
> logic is needed for the given input?
> 
> The file "test.smt" contains:
> 
> (benchmark Test
> 
> :logic QF_LIA
> :extrafuns ( (v_1 Real) )
> :formula
> (and
>     (< 0 v_1)
>     (< v_1 1)
> )
> )
> 
> Kind regards,
> André
> 
> P.S.: I am not a member of this list. Please add me to the CC. Thank you.
> 
> 

André,

Yices is quite permissive when processing SMT files and it accepts
more than what the standard strictly requires.

It makes limited  use of the :logic flag to determine whether the logic
requires more than arithmetic, whether it has integers, whether it
includes quantifiers, etc. This is used to determine which solver to
use and to set some heuristics.

So there's limited cross checking: if you specify :logic QF_LIA,
Yices will use simplex as the solver and assume that nothing
else than linear arithmetic is required. It won't accept formulas
with uninterpreted functions, for example. Besides that, it will
take anything that the Simplex solver can process (even if not
strictly part of the QF_LIA logic).

Bruno