class representing a component alternative for the SMT based analysis
Analysis of the alternatives for a given design space
Created by kdelmas on 04/11/16.
Trait for encoding structure function as a BDD
Class for a classic BDD Factory (variable are integer and BDD are JavaBDD)
Created by kdelmas on 27/09/17.
base trait for BDD factories
Trait for order computation
Case class encoding a partial function over component traces
Case class encoding a partial function over component traces
the type of return values
the function from component trace to value
the default value
class representing a component for component analysis by SMT-based approach
Created by kdelmas on 08/04/16.
Base trait for available cut computation modes
Base trait for available DSE resolution methods
Base type for literals in prime implicants, in terms of DSL identifiers.
Created by kevin on 15/02/17.
Extractor from parameter node
Extractor from parameter node
the type of the node
the type of parameter
the type of the kids
Extractor from parameter node
Extractor from parameter node
the type of the node
the type of edge label
the type of parameter
the type of kids
Extractor from parameter node
Extractor from parameter node
the node type
the parameter type
compute the BDD of the trigger function of each possible trace of the component
compute the cardinality of BDD trigger functions of the component
Base trait for node factory based on hashConsing
Base trait for node factory based on hashConsing
the type of the nodes
Factory for node containing list of kids
Factory for node containing list of kids
the type of simplified node
the type of the nodes
the type of the parameter
the type of kids
Hashcode computation for leaf node
Hashcode computation for leaf node
the type of reduced nodes
the type of the nodes
the type of edge labels
the type of the parameter
the type of the kids
the type of the collection gathering kids
Factory for nodes containing only a parameter
Factory for nodes containing only a parameter
the type of the nodes
the type of parameter
Generic BDD factory over the type of BDD variables
Generic BDD factory over the type of BDD variables
the type of variable labelled on BDD nodes
Base trait for MDD factory
Base trait for MDD factory
Variable type
collection type for values
values type
terminal type
variables' domain type
Case class encoding Set of Sets and ensuring that any element cannot be contained in another one
Case class encoding Set of Sets and ensuring that any element cannot be contained in another one
the element type, must be subtype of Set
the type of Set elements
initial set
Case class representing infinite numeric (classic number plus infinity)
Case class representing infinite numeric (classic number plus infinity)
the type of the values
Base trait used to defined Numeric implicit objects
Base trait used to defined Numeric implicit objects
the type of the values
Base trait for representing infinite values
BDDFactory where variables labelled on BDD node are InstBoolIdent
Translates the structure function of a system represented by a z3 expression to a SAT-solver friendly formula in DIMACS or OPB format for prime implicant enumeration using external solvers.
Legality analysis based on SMT problem solving
MDD factory class
MDD factory class
Variable type
collection type for values
values type
terminal type
variables' domain type
Printer trait should be mixed with a factory
Printer trait should be mixed with a factory
the type representing node variables
the collection types of values associated to a variable
the type of variables possible values
Interval approximation of numeric values
Interval approximation of numeric values
the type of the value
Created by kdelmas on 16/11/16.
A negative literal.
Translates the structure function of a system represented by a z3 expression to a SAT-solver friendly formula in DIMACS or OPB format for prime implicant enumeration using external solvers.
Case class encoding the structure function of a system
Case class encoding the structure function of a system
the boolean expression of the structure function
the mapping of KCR events to Z3 varaibles
the SMT evaluation context
Base trait for analysis of the structure function
Trait fot cutsets computation on phi
Trait fot cutsets computation on phi
the collection to store cutsets
Trait for BDD based cutsets enumeration on phi
Trait for SAT based enumeration of cutsets
Trait for SMT resolution based cutsets enumeration
Trait for Pseudo-Boolean based cutsets computation
A positive literal.
compute the SMT expression (c in1..inn e1..ek)=(o1..om) where flows and events are bounded variables
Trait for additional analysis of the DSE problem solution
Case clas for subsitution analysis with pure SMT exploration (ie without the interpreter)
Case class encoding substitution variables
Case class encoding substitution variables
the targeted instance
the corresponding Z3 variable
the sort of the Z3 varaible
Class for enumrating prime implicants of a structure function.
Class for timeout task
Class for timeout task
the type of returned result
Created by kdelmas on 22/02/17.
compute the SMT expression (exists e1..ek (c in1..inn e1..ek)=(o1..om)) in traceFieldExpr where flows are given as bounded variables referred in traceFieldVars
Base trait for translating Z3 SMT Boolean expression to BDD
Created by kdelmas on 04/11/16.
Cut computation based on BDD analysis
Factory for node containing list of kids
Factory for node containing parameter and a map of kids
Factory for nodes containing only a parameter
HIPHOPS based DSE resolution method
Cut enumeration based on HIPHOPS external tool
Useful conversion from infinity to infinite numeric
Particular type of infinite numeric
Cut computation based on Iterative SAT method
Cut computation based on Iterative SMT method
Created by kdelmas on 04/11/16.
Object representing negative infinity
Cut enumeration based on Pseudo-Boolean solving
Object representing positive infinity
SMT based resolution method
Cut enumeration based on XFTA external tool
Cut enumeration based on XSAP external tool
Created by rdelmas on 07/06/16.
Created by rdelmas on 07/06/16.
A translation function from z3 expressions to FormulaLike
base trait for BDD factories
the type of variable labelled on BDD nodes
the BDD representation which must be a subtype of JavaBDD type