Trait

analyzers

SMTTranslation

Related Doc: package analyzers

Permalink

trait SMTTranslation extends ConfigurationAnalyzer with Z3ExprTranslators

Trait for KCR translation to SMT

Self Type
SMTTranslation with Parsing
Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SMTTranslation
  2. Z3ExprTranslators
  3. ConfigurationAnalyzer
  4. Analyser
  5. AnyRef
  6. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. class OrderedCompInstIdent extends Ordered[(ConfigurationAnalyzer.this)#OrderedCompInstIdent]

    Permalink

    Class encoding instance identifiers which can be ordered

    Class encoding instance identifiers which can be ordered

    Definition Classes
    ConfigurationAnalyzer
  2. class OrderedCompTrace extends Ordered[(ConfigurationAnalyzer.this)#OrderedCompTrace]

    Permalink

    Class encoding of component traces which can be ordered

    Class encoding of component traces which can be ordered

    Definition Classes
    ConfigurationAnalyzer
  3. class OrderedSymbol extends Ordered[(ConfigurationAnalyzer.this)#OrderedSymbol]

    Permalink

    Class encoding scala Symbol that can be compared

    Class encoding scala Symbol that can be compared

    Definition Classes
    ConfigurationAnalyzer

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. object OrderedCompInstIdent

    Permalink

    Companion object for ordered instance identifiers

    Companion object for ordered instance identifiers

    Definition Classes
    ConfigurationAnalyzer
  5. object OrderedCompTrace

    Permalink

    Companion object of component traces

    Companion object of component traces

    Definition Classes
    ConfigurationAnalyzer
  6. object OrderedSymbol

    Permalink

    Companion object for ordered symbols

    Companion object for ordered symbols

    Definition Classes
    ConfigurationAnalyzer
  7. lazy val _DSLContext: ImmutableCache

    Permalink
  8. lazy val _SMTContext: SMTContext

    Permalink
  9. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  10. 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
  11. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  12. implicit object compBasicFlow extends Ordering[BasicFlowIdent]

    Permalink

    Order over flow identifiers

    Order over flow identifiers

    Definition Classes
    ConfigurationAnalyzer
  13. implicit object compFlowConst extends Ordering[FlowConst]

    Permalink

    Order over constants

    Order over constants

    Definition Classes
    ConfigurationAnalyzer
  14. implicit object compOrder extends Ordering[CompInstanceIdent]

    Permalink

    Order over instance identifiers in a system component

    Order over instance identifiers in a system component

    Definition Classes
    ConfigurationAnalyzer
  15. 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
  16. final def eq(arg0: AnyRef): Boolean

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

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  20. def getCompTranslation(comp: ComponentDeclaration): Component

    Permalink

    Get the SMT translation of a KCR component

    Get the SMT translation of a KCR component

    comp

    AST node of the component declaration

    returns

    component case class containing mapping from KCR flows ident to SMT translation

  21. def hashCode(): Int

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

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

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

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

    Permalink
    Definition Classes
    AnyRef
  26. lazy val phi: Phi

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

    Permalink
    Definition Classes
    AnyRef
  28. 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
  29. implicit def toOSymb(s: Symbol): (SMTTranslation.this)#OrderedSymbol

    Permalink

    implicit transformation from Symbol to Ordered Symbol

    implicit transformation from Symbol to Ordered Symbol

    s

    Scala Symbol

    returns

    ordered symbol

    Definition Classes
    ConfigurationAnalyzer
  30. def toString(): String

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

    Permalink
    Definition Classes
    Z3ExprTranslators
  32. val translationSMTProfiler: Profiler[Unit, Unit]

    Permalink
  33. lazy val translator: DSLSMTTranslator

    Permalink
  34. final def wait(): Unit

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

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

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

Inherited from Z3ExprTranslators

Inherited from ConfigurationAnalyzer

Inherited from Analyser

Inherited from AnyRef

Inherited from Any

Ungrouped