Language and parser for static properties

[ondrej33]

To process "generic" static properties given by a formula, we need some sort of language/format for them. For now, the goal is to make an initial testable version, that is:

1. come up with some simple syntax covering first-order logic (it might be worth it to check some solver tools for syntax ideas)
2. implement a parser for the language (on backend)

The format should be user-friendly, and the parser should give readable error messages. The processing should also be easily modifiable. Later, we might enrich the language with some predefined "patterns", or something else.

[ondrej33]

A few notes after some initial discussion

• At first, we will only consider quantification over Boolean variables. In future, we might add quantifying over whole Boolean states (vectors) if that seems necessary.
• We will not allow free variables in the formulas (that could cause some ambiguity in how they are interpreted). This can also change later.
• Lastly, when writing formulas, the users should be provided with some "readable" version of the syntax (clickable quantifier symbols and such) so that they do not need to remember the actual syntax.