[SMT-LIB] Question on SMTLIB

[Paulo J. Matos]

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