[SMT-LIB] Question on SMTLIB

[Paulo J. Matos]

On 10/27/06, Leonardo de Moura <leonardo at microsoft.com> wrote:
> Hi Paulo,
>

Hi Leonardo,

> I believe SMT-LIB uses static (aka lexical) variable scope. That is, variables bound in a let are in scope for the body of the let. If this is not the case, then the standard should be modified.

I share your opinion. In fact, by reading the let and flet description
that's what I thought, although it is not explicit.

> In my point of view, your examples are valid SMT-LIB benchmarks. The first one is equivalent to (or (= y 1) (= y 2)), and the second to
> (or (and x y) (and z w)).

Testing latest solvers introduced even more confusion since they don't
seem to conform with the standard.

Thanks for your reply,
Cheers,

Paulo Matos

>
> Cheers,
> Leonardo.
>
>
>
> -----Original Message-----
> From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Paulo J. Matos
> Sent: Friday, October 27, 2006 6:45 AM
> To: SMT-LIB
> Cc: Joao Marques-Silva
> Subject: [SMT-LIB] Question on SMTLIB
>
> Hi all,
>
> While reading the last version of the standard and thinking lisp-wise
> I thought to myself if the let's and flet's of smtlib can introduce
> namespaces, i.e., if variables can shadow each other or we can define
> 2 variables with the same name within different namespaces. The answer
> is not obvious and I can't find a reference to it in the standard.
> Moreover, it seems the solvers do not agree on this:
> (benchmark var-test
>            :logic QF_LIA
>            :extrafuns ((y Int))
>            :formula (or (flet (?x (= y 1)) ?x)
>                                  (flet (?x (= y 2)) ?x)))
>
> Both Mathsat3.3.1 and ario1.1 return parse error, however, yices1.0
> returns sat.
>
> So, what should happen in this case? (from page 13 I would guess this
> is possible)
>
> and more, this is also possible:
> ...
> :formula (flet (?x (and x y)) (or ?x (flet (?x (and z w)) ?x)))
>
> Which mean that each variable definition creates an enclosing namespace, right?
>
> Regards,
> --
> Paulo Jorge Matos - pocm at soton.ac.uk
> http://www.personal.soton.ac.uk/pocm
> PhD Student @ ECS
> University of Southampton, UK
> _______________________________________________
> 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
>


-- 
Paulo Jorge Matos - pocm at soton.ac.uk
http://www.personal.soton.ac.uk/pocm
PhD Student @ ECS
University of Southampton, UK