Trait

util.analyzers

Z3ExprTranslators

Related Doc: package analyzers

Permalink

trait Z3ExprTranslators extends AnyRef

Created by kdelmas on 04/11/16.

Linear Supertypes
AnyRef, Any
Known Subclasses
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Z3ExprTranslators
  2. AnyRef
  3. 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

  6. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  7. 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

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

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

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

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

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

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

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

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

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

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

    Permalink
    Definition Classes
    AnyRef
  18. 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

  19. def toString(): String

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

    Permalink
  21. final def wait(): Unit

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

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

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

Inherited from AnyRef

Inherited from Any

Ungrouped