Trait

analyzers

CircuitGraphExporter

Related Doc: package analyzers

Permalink

trait CircuitGraphExporter extends Exporter with Z3ExprTranslators

Trait for Circuit Graph exportation

Self Type
CircuitGraphExporter with Parsing with SMTTranslation
Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. CircuitGraphExporter
  2. Z3ExprTranslators
  3. Exporter
  4. ConfigurationAnalyzer
  5. Analyser
  6. AnyRef
  7. 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. final def asInstanceOf[T0]: T0

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

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

    Permalink

    Order over flow identifiers

    Order over flow identifiers

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

    Permalink

    Order over constants

    Order over constants

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  16. def exportToCG(file: File): Unit

    Permalink

    Translate structure function to circuit graph

    Translate structure function to circuit graph

    file

    destination file

  17. def finalize(): Unit

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

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

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

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

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

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

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

    Permalink
    Definition Classes
    AnyRef
  25. 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
  26. implicit def toOSymb(s: Symbol): (CircuitGraphExporter.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
  27. def toString(): String

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

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

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

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

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

Inherited from Z3ExprTranslators

Inherited from Exporter

Inherited from ConfigurationAnalyzer

Inherited from Analyser

Inherited from AnyRef

Inherited from Any

Ungrouped