adds context variables to the knowledge base

[ivg]

Context variables are regular state variables and are introduced to enable stateful analyses. They are not stored in the knowledge base nor they are persistent. They are also not involved in the fixed point computation. At the same time, the data type of a stateful variable is not required to have the domain structure or even be ordered. Anything could be stored in the state.

Many analyses require a regular, non-monotonic and unordered, state. A good example, is an optimization analysis or a variable desugaring analysis that will come in one of the next pull requests. We may also find it useful and much more efficient to store some state of the analysis, like the current target or theory, in the context, rather than in the knowledge base or in the temporal promise.

Previously, if we needed to implement a stateful analysis we have to wrap the knowledge monad into the state monad, e.g., this is what we are doing in the Primus interpreter. It is however a little bit tedious and comes with some performance penalty. Essentially since it is superfluous, as the knowledge monad is already having the state. Another option to add an arbitrary state to the analysis is to cheat with the domain ordering and implement a timed data structure with the chain structure (i.e., where a more recent version is considered to have more informational content than the previous, despite the actual content). This approach is rather artificial and again comes with some unnecessary performance cost.