Trait

util.analyzers

Z3BoolExprToBDDTranslator

Related Doc: package analyzers

Permalink

trait Z3BoolExprToBDDTranslator extends Z3ExprTranslators

Base trait for translating Z3 SMT Boolean expression to BDD

Self Type
Z3BoolExprToBDDTranslator with BDDFactory
Linear Supertypes
Z3ExprTranslators, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Z3BoolExprToBDDTranslator
  2. Z3ExprTranslators
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Value Members

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

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

    Permalink
    Definition Classes
    Any
  5. def atMostN(kids: List[BoolExpr], n: Int, SMTContext: Context): BoolExpr

    Permalink

    Transform a at most n using the sequential encoding

    Transform a at most n using the sequential encoding

    kids

    the Boolean expressions addressed by the at most

    n

    the maximum number of kids which must be true

    SMTContext

    the Z3 context to create Z3 terms

    returns

    Z3 Boolean expression

    Definition Classes
    Z3ExprTranslators
  6. def boolExprToBdd(expr: BoolExpr, varMap: Map[BoolExpr, BDD], context: SMTContext): BDD

    Permalink

    Transfrom a Boolean expression to a BDD

    Transfrom a Boolean expression to a BDD

    expr

    the Z3 Boolean expression

    varMap

    the BDD for Boolean variable (leaves of the Z3 AST)

    context

    context in which the expression has been built

    returns

    the BDD

  7. def boolExprToPartialBdd(expr: BoolExpr, varMap: Map[BoolExpr, BDD], context: SMTContext, upTo: Int): BDD

    Permalink

    Transform a Boolean expression to a truncated BDD

    Transform a Boolean expression to a truncated BDD

    expr

    the Z3 Boolean expression

    varMap

    the BDD for Boolean variable (leaves of the Z3 AST)

    context

    context in which the expression has been built

    upTo

    the maximum number of positive arc in paths of BDD

    returns

    the BDD

  8. def boolExprToPartialBddRec(expr: BoolExpr, varMap: Map[BoolExpr, BDD], context: Context, remain: Int)(implicit cache: Map[(BoolExpr, Int), BDD]): BDD

    Permalink
  9. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  10. def dnfOf(expr: Expr, vars: List[BoolExpr], context: Context): BoolExpr

    Permalink

    Transform an expression to its dnfFrom

    Transform an expression to its dnfFrom

    expr

    Boolean expression

    vars

    the list of leaves terms

    context

    the context use to build the expression

    returns

    the DNF form

    Definition Classes
    Z3ExprTranslators
  11. final def eq(arg0: AnyRef): Boolean

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

    Permalink
    Definition Classes
    AnyRef → Any
  13. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  14. final def getClass(): Class[_]

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

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

    Permalink
    Definition Classes
    Any
  17. final def ne(arg0: AnyRef): Boolean

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

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

    Permalink
    Definition Classes
    AnyRef
  20. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  21. def toNNF(expr: BoolExpr, vars: List[BoolExpr], context: SMTContext, breakITE: Boolean = false): BoolExpr

    Permalink

    Transform the expression in NNF form

    Transform the expression in NNF form

    expr

    the expression to transform

    vars

    the list of leaves

    context

    the context use to build the expression

    breakITE

    break ite into i.t + \neg i.e

    returns

    the NNF form

    Definition Classes
    Z3ExprTranslators
  22. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  23. def translate(node: BoolExpr, atoms: Map[BoolExpr, Expr]): Expr

    Permalink
    Definition Classes
    Z3ExprTranslators
  24. final def wait(): Unit

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

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

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

Inherited from Z3ExprTranslators

Inherited from AnyRef

Inherited from Any

Ungrouped