Module node 

Btor2 standard nodes.

The type structure for nodes was chosen so that the nodes that have common fields are combined. For example, Init and Next both specify an assignment to a state at some point in time. They have the same fields as well, so they are subtypes of Temporal.

Structs

Const

Constant node.

Drain

Drain node. Encompasses “bad”, “constraint”, “fair”, and “output”.

Justice

Justice node.

Source

Source node type. Encompasses “input”, “one”, “ones”, and “zero”.

State

State node.

Temporal

Temporal node. Encompasses “init” and “next”.

Enums

ConstType

Constant type.

DrainType

Drain node type. Encompasses “bad”, “constraint”, “fair”, and “output”.

Node

Btor2 node.

SourceType

Source node type.Encompasses “input”, “one”, “ones”, and “zero”.

TemporalType

Temporal node type. Encompasses “init” and “next”.