Find out optimal implementation similar to STP's push and pop

[Robbepop]

Find out what scopes push & pop in STP are and how to incorporate them into this SMT solver.

Note: STP has a stack of vectors that acts as assertion scope level. Users may wish to add or remove such scopes to add or remove entire groups of assertions that have been added to the removed scope level. The STP scope design is inefficient and should not be taken over to Stevia. Stevia should model this concept with a single vector for the assertions and another vector for entry points to new scope levels.