Module libpatron::ir

Re-exports

• pub use value::width_to_words;
• pub use value::Value;
• pub use value::ValueRef;
• pub use value::Word;

Modules

• value

Structs

• ArrayType
• Context
  The actual context implementation.
• ExprMetaData
  A dense hash map to store meta-data related to each expression
• ExprRef
• SerializeMeta
  Meta-data that helps with serialization, no matter if serializing to btor, our custom “human-readable” format or SMTLib.
• SignalInfo
• SignalLabels
• State
• StateRef
• StringRef
• TransitionSystem
• TypeCheckError
• Uses
  Indicates which context an expression is used in.

Enums

• Expr
  Represents a SMT bit-vector or array expression.
• SignalKind
  Represents three fundamental signal kinds that are mutually exclusive:
• Type

Traits

• AddNode
  Add an IR node to the context.
• ExprNodeConstruction
  Convenience methods to construct IR nodes.
• ForEachChild
• GetNode
  Lookup an IR node from the context
• SerializableIrNode
• TypeCheck

Functions

• analyze_for_serialization
• bv_value_fits_width
• cone_of_influence
  Generates a list of all inputs and states that can influence the root expression.
• count_expr_uses
• do_transform
• is_usage_root_signal
  Returns whether a signal is always “used”, i.e. visible to the outside world or not.
• merge_signal_info
• replace_anonymous_inputs_with_zero
  Remove any inputs named _input_[...] and replace their use with a literal zero. This essentially gets rid of all undefined value modelling by yosys.
• simplify_expressions
  Applies simplifications to the expressions used in the system.

Type Aliases

• BVLiteralInt
  This restricts the maximum value that a bit-vector literal can carry.
• UseCountInt
• WidthInt
  This type restricts the maximum width that a bit-vector type is allowed to have in our IR.