The bottom of the stack.
Number of levels of the stack.
The statefull solver proxy on which this stack operates.
The top level of the stack.
Prepends an item to the current top level.
Prepends a list of items to the current top level.
Folds each level of the stack with the given zero1 and f1 yielding a list containing one result per level, which is then folded using zero2 and f2.
Returns true iff the stack contains some element for which the keep flag is false.
Returns true iff the stack contains some element for which the keep flag is true.
True iff some element of some level of the stack satisfies predicate p.
Returns the first level from the bottom of the stack which satisfies the given predicate together with the integer representing its depth from the bottom of the stack, None if not found.
Returns the first level from the top which satisfies the given predicate together with the integer representing its depth from the top of the stack, None if not found.
Horizontally flatMap:s a function, level per level, returning list of results (one result per level).
Horizontally foldLeft:s each level of the stack with a given function, returns a list of result (one result per level).
True iff all elements of all levels of the stack satisfy predicate p.
Returns true the index of the first stack level from the top where the predicate is true.
Horizontally map:s a function, level per level, returning list of results (one result per level).
Pops n levels of the stack, throw exception if n larger than size-1.
Adds a new empty level on the stack.
Pops the whole stack down to size 1, all things to keep will end up in the first level.
An immutable stack of lists of items of type BoolExpr, each item paired with a boolean value indicating if we want the item to stay in the stack when popping the stack. Embeds a proxy to a statefull SMT solver, and enforces the item keeping mechanism on the proxy.