Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-10 15:28:57 -0800 (Thu, 10 Mar 2005)
Revision: 6884
Log message:
*******************************************************************
* WARNING: This breaks binary compatibility for .cmoz/.prlb files *
*******************************************************************
This commit increases the separation between the first-order variables and the
meta-variables:
- The free variables computation will no longer include the SO variables in
the free variables list.
- The rewriter should handle correctly the case of a FO variable and a SO
variable (even a 0-arity one) sharing the same name (the rewriter now will
consider the two completely unrelated).
- When applying rules and cond. rewrites, the refiner will give the rewriter
the set of all the meta-vars in the sequent, so that the rewriter can avoid
creating new binding that would clash with meta-vars (this is only needed to
avoid user confusion on I/O, the semantics does not depend on this).