Trait/Object

util.stack.immutable

AssertionStack

Related Docs: object AssertionStack | package immutable

Permalink

sealed trait AssertionStack[BoolExpr] extends AnyRef

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.

Self Type
AssertionStack[BoolExpr]
Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. AssertionStack
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Abstract Value Members

  1. abstract val bottom: List[List[(BoolExpr, Boolean)]]

    Permalink

    The bottom of the stack.

  2. abstract val size: Int

    Permalink

    Number of levels of the stack.

  3. abstract val solverProxy: StackSolverProxy[BoolExpr]

    Permalink

    The statefull solver proxy on which this stack operates.

  4. abstract val top: List[(BoolExpr, Boolean)]

    Permalink

    The top level of the stack.

Concrete Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. def ::(a: BoolExpr, keep: Boolean = false): AssertionStack[BoolExpr]

    Permalink

    Prepends an item to the current top level.

  4. def :::(as: List[(BoolExpr, Boolean)]): AssertionStack[BoolExpr]

    Permalink

    Prepends a list of items to the current top level.

  5. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  6. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  7. def biFoldLeft[B1, B2](zero1: B1, zero2: B2)(f1: (B1, (BoolExpr, Boolean)) ⇒ B1, f2: (B2, B1) ⇒ B2): B2

    Permalink

    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.

  8. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  9. def containsNotKeep: Boolean

    Permalink

    Returns true iff the stack contains some element for which the keep flag is false.

  10. def containsToKeep: Boolean

    Permalink

    Returns true iff the stack contains some element for which the keep flag is true.

  11. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  12. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  13. def exists(p: (BoolExpr, Boolean) ⇒ Boolean): Boolean

    Permalink

    True iff some element of some level of the stack satisfies predicate p.

  14. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  15. def findLevelFromBottom(p: (List[(BoolExpr, Boolean)]) ⇒ Boolean): Option[(List[(BoolExpr, Boolean)], Int)]

    Permalink

    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.

  16. def findLevelFromTop(p: (List[(BoolExpr, Boolean)]) ⇒ Boolean): Option[(List[(BoolExpr, Boolean)], Int)]

    Permalink

    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.

  17. def flatMapH[B](f: ((BoolExpr, Boolean)) ⇒ GenTraversableOnce[B]): List[List[B]]

    Permalink

    Horizontally flatMap:s a function, level per level, returning list of results (one result per level).

  18. def foldLeftH[B](zero: B)(f: (B, (BoolExpr, Boolean)) ⇒ B): List[B]

    Permalink

    Horizontally foldLeft:s each level of the stack with a given function, returns a list of result (one result per level).

  19. def forall(p: (BoolExpr, Boolean) ⇒ Boolean): Boolean

    Permalink

    True iff all elements of all levels of the stack satisfy predicate p.

  20. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  21. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  22. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  23. def levelWhere(p: (List[(BoolExpr, Boolean)]) ⇒ Boolean): Int

    Permalink

    Returns true the index of the first stack level from the top where the predicate is true.

  24. def mapH[B](f: ((BoolExpr, Boolean)) ⇒ B): List[List[B]]

    Permalink

    Horizontally map:s a function, level per level, returning list of results (one result per level).

  25. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  26. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  27. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  28. def pop(n: Int): AssertionStack[BoolExpr]

    Permalink

    Pops n levels of the stack, throw exception if n larger than size-1.

  29. def push: AssertionStack[BoolExpr]

    Permalink

    Adds a new empty level on the stack.

  30. def reset: AssertionStack[BoolExpr]

    Permalink

    Pops the whole stack down to size 1, all things to keep will end up in the first level.

  31. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  32. def toString(): String

    Permalink
    Definition Classes
    AssertionStack → AnyRef → Any
  33. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  34. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  35. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped