Scopes of propositional variables

The SAT-solver could take advantage of the fact, that some of propositional variables have very ephemeral character and from some point they will never occur in newly added clauses. For example, variables that simplifies translation of implication to CNF (those generated by `IncrSAT.Formula.imp_to_cnf`) or variables that appear in local definitions, but don't leak to public interfaces. There are many useful simplifications that can be made with such variables. For instance, with such a variable *p*, we can do the following:
- if it has only negative occurrences — set to to false;
- if it has only positive occurrences — set to true;
- if there is only one positive occurrence, and it has a form *p* ∨ ¬*q* — set to *q*;
- it there is only one negative occurrence, and it has a form ¬*p* ∨ *q* — set to *q*.

We can also perform some simplifications on variables that will never appear positively (or negatively, respectively) in new clauses.

We can detect such variables on-line, by assigning a scope to propositional variable, and lifting it in returned types, when the scope is leaved. Alternative (and probably simpler) solution is to:
- don't care about such variables in a batch mode — we always solve all constraints anyway.
- find non-ephemeral variables by traversing the environment in a REPL mode.