[SMT-LIB] Question on SMTLIB

[Leonardo de Moura]

Hi Paulo,

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.
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)).

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