Give full support for nested quantification

[miquelramirez]

I do not understand this comment:

https://github.com/aig-upf/fs-private/blob/bfws-v1.0-beta2/src/languages/fstrips/formulae.cxx#L189

does that mean that formulae with nested quantifiers aren't being evaluated correctly? Or just it is not very efficiently implemented?

[gfrances]

Good point. It only means that nested quantifiers were not supported up until now, and that this assert needs to go away soon!

[gfrances]

With the current refactorings of the frontend (I fixed a couple of bugs to this respect yesterday, see e.g. here, but this is still untested), the nested quantified formulas should be guaranteed to have all different variable Ids (i.e. variable names) wherever it makes sense.

The Binding class, however, is very naive and was implemented having simple use cases with a single existential quantifier in mind (perhaps with more than one quantified variable, but only one existential quantifier). Looking at it, it's probably buggy for more than one nested quantifier, so we'll need to refactor it a bit at the same time . The reason is that when I want to interpret an inner quantifier and have already some binding for variables from some outer quantification, then this inner quantifier might have a single variable with ID, say, 3, but the Binding object I'm creating now will have size only one.

In any case, and nevermind if the above is not clear enough, we'll need to have an operation that extends a given binding to support new variables.

OTOH, the naive, recursive implementation of the interpretation of a quantified formula, both universal and existential, is way too inefficient, and should be refactored as well. But perhaps that should be dealt with later and in a separate issue, once that the restriction is lifted.