Boolean Function

class hal_py.BooleanFunction

A BooleanFunction represents a symbolic expression (e.g., A & B) in order to abstract the (semantic) functionality of a single netlist gate (or even a complex subcircuit comprising multiple gates) in a formal manner. To this end, the BooleanFunction class is able to construct and display arbitrarily-nested expressions, enable symbolic simplification (e.g., simplify A & 0 to 0), and translate Boolean functions to the SAT / SMT solver domain to use the solve constraint formulas.

static Add(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by applying an ADD operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation.

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static And(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by applying an AND operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation.

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Ashr(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Arithmetically shifts a Boolean function to the right by the specified number of bits.

Parameters

p0 (hal_py.BooleanFunction) – Boolean function to shift.
p1 (hal_py.BooleanFunction) – Boolean function of type Index encoding the number of bits to shift.
size (int) – Bit-size of the shifted Boolean function.

Returns

The shifted Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Concat(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Concatenates two Boolean functions of bit-sizes n and m to form a single Boolean function of bit-size n + m.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function (MSBs).
p1 (hal_py.BooleanFunction) – Second Boolean function (LSBs).
size (int) – Bit-size of the concatenated Boolean function, i.e., n + m.

Returns

The concatenated Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Const(*args, **kwargs)

Overloaded function.

Const(value: hal_py.BooleanFunction.Value) -> hal_py.BooleanFunction

Creates a constant single-bit Boolean function from a value.

param hal_py.BooleanFunction.Value value

The value.

returns

The Boolean function.

rtype

hal_py.BooleanFunction
Const(value: List[hal_py.BooleanFunction.Value]) -> hal_py.BooleanFunction

Creates a constant multi-bit Boolean function from a list of values.

param list[hal_py.BooleanFunction.Value] value

The list of values.

returns

The Boolean function.

rtype

hal_py.BooleanFunction
Const(value: int, size: int) -> hal_py.BooleanFunction

Creates a constant multi-bit Boolean function of the given bit-size from an integer value.

param int value

The integer value.

param int size

The bit-size.

returns

The Boolean function.

rtype

hal_py.BooleanFunction

static Eq(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by an equality check that produces a single-bit result.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation (always =1).

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Index(index: int, size: int) → hal_py.BooleanFunction

Creates an index for a Boolean function of the given bit-size from an integer value.

Parameters

index (int) – The integer value.
size (int) – The bit-size.

Returns

The Boolean function.

Return type

hal_py.BooleanFunction

static Ite(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, p2: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins three Boolean functions by an if-then-else operation with p0 as the condition, p1 as true-case, and p2 as false-case. Requires p1 to be of bit-size 1 and both Boolean functions p1 and p2 to be of the same bit-size. Produces a new Boolean function of the specified bit-size that must be equal to the size of p1 and p2.

Parameters

p0 (hal_py.BooleanFunction) – Boolean function condition.
p1 (hal_py.BooleanFunction) – Boolean function for true-case.
p1 – Boolean function for false-case.
size (int) – Bit-size of the operation, i.e., size of p1 and p2.

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Lshr(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Logically shifts a Boolean function to the right by the specified number of bits.

Parameters

p0 (hal_py.BooleanFunction) – Boolean function to shift.
p1 (hal_py.BooleanFunction) – Boolean function of type Index encoding the number of bits to shift.
size (int) – Bit-size of the shifted Boolean function.

Returns

The shifted Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Mul(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by applying an MUL operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation.

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

class Node

Node refers to an abstract syntax tree node of a Boolean function. A node is an abstract base class for either an operation (e.g., AND, XOR) or an operand (e.g., a signal name variable).

static Constant(value: List[hal_py.BooleanFunction.Value]) → hal_py.BooleanFunction.Node

Constructs a ‘constant’ node.

Parameters: value (list[hal_py.BooleanFunction.Value]) – The constant value of the node.
Returns: The node.
Return type: hal_py.BooleanFunction.Node

static Index(index: int, size: int) → hal_py.BooleanFunction.Node

Constructs an ‘index’ node.

Parameters

value (int) – The index value of the node.
size (int) – The bit-size of the node.

Returns

The node.

Return type

hal_py.BooleanFunction.Node

static Operation(type: int, size: int) → hal_py.BooleanFunction.Node

Constructs an ‘operation’ node.

Parameters

type (int) – The type of the operation.
size (int) – The bit-size of the operation.

Returns

The node.

Return type

hal_py.BooleanFunction.Node

static Variable(variable: str, size: int) → hal_py.BooleanFunction.Node

Constructs a ‘variable’ node.

Parameters

value (int) – The variable name of the node.
size (int) – The bit-size of the node.

Returns

The node.

Return type

hal_py.BooleanFunction.Node

__annotations__ = {}

__eq__(self: hal_py.BooleanFunction.Node, arg0: hal_py.BooleanFunction.Node) → bool

Checks whether two Boolean function nodes are equal.

Returns: True if both Boolean function nodes are equal, False otherwise.
Return type: bool

__hash__ = None

__init__(*args, **kwargs)

__lt__(self: hal_py.BooleanFunction.Node, arg0: hal_py.BooleanFunction.Node) → bool

Checks whether this Boolean function node is ‘smaller’ than the other Boolean function node.

Returns: True if this Boolean function node is ‘smaller’, False otherwise.
Return type: bool

__module__ = 'hal_py'

__ne__(self: hal_py.BooleanFunction.Node, arg0: hal_py.BooleanFunction.Node) → bool

Checks whether two Boolean function nodes are unequal.

Returns: True if both Boolean function nodes are unequal, False otherwise.
Return type: bool

__str__(self: hal_py.BooleanFunction.Node) → str

Translates the Boolean function node into its string representation.

Returns: The Boolean function node as a string.
Return type: str

property arity

The arity of the Boolean function node, i.e., the number of parameters.

Type: int

clone(self: hal_py.BooleanFunction.Node) → hal_py.BooleanFunction.Node

Clones the Boolean function node.

Returns: The cloned Boolean function node.
Return type: hal_py.BooleanFunction.Node

property constant

The (optional) constant value of the node.

Type: list[hal_py.BooleanFunction.Value]

get_arity(self: hal_py.BooleanFunction.Node) → int

Returns the arity of the Boolean function node, i.e., the number of parameters.

Returns: The arity.
Return type: int

static get_arity_of_type(type: int) → int

Returns the arity for a Boolean function node of the given type, i.e., the number of parameters.

Returns: The arity.
Return type: int

get_constant_value(self: hal_py.BooleanFunction.Node) → Optional[List[hal_py.BooleanFunction.Value]]

Get the constant value of the node of type Constant as a list of hal_py.BooleanFunction.Value.

Returns: The constant value on success, None otherwise.
Return type: list[hal_py.BooleanFunction.Value] or None

get_constant_value_u64(self: hal_py.BooleanFunction.Node) → Optional[int]

Get the constant value of the node of type Constant as long as it has a size <= 64-bit.

Returns: The constant value on success, None otherwise.
Return type: int or None

get_index_value(self: hal_py.BooleanFunction.Node) → Optional[int]

Get the index value of node of type Index.

Returns: The index value on success, None otherwise.
Return type: int or None

get_variable_name(self: hal_py.BooleanFunction.Node) → Optional[str]

Get the variable name of node of type Variable.

Returns: The variable name on success, None otherwise.
Return type: str or None

has_constant_value(*args, **kwargs)

Overloaded function.

has_constant_value(self: hal_py.BooleanFunction.Node, value: List[hal_py.BooleanFunction.Value]) -> bool

Checks whether the Boolean function node is of type Constant and holds a specific value.

param list[hal_py.BooleanFunction.Value] value

The value to check for.

returns

True if the Boolean function node is of type Constant and holds the given value, False otherwise.

rtype

bool
has_constant_value(self: hal_py.BooleanFunction.Node, value: int) -> bool

Checks whether the Boolean function node is of type Constant and holds a specific value.

param int value

The value to check for.

returns

True if the Boolean function node is of type Constant and holds the given value, False otherwise.

rtype

bool

has_index_value(self: hal_py.BooleanFunction.Node, value: int) → bool

Checks whether the Boolean function node is of type Index and holds a specific value.

Parameters: value (int) – The value to check for.
Returns: True if the Boolean function node is of type Index and holds the given value, False otherwise.
Return type: bool

has_variable_name(self: hal_py.BooleanFunction.Node, variable_name: str) → bool

Checks whether the Boolean function node is of type Variable and holds a specific variable name.

Parameters: variable_name (str) – The variable name to check for.
Returns: True if the Boolean function node is of type Variable and holds the given variable name, False otherwise.
Return type: bool

property index

The (optional) index value of the node.

Type: int

is(self: hal_py.BooleanFunction.Node, type: int) → bool

Checks whether the Boolean function node is of a specific type.

Parameters: type (int) – The type to check for.
Returns: True if the node is of the given type, False otherwise.
Return type: bool

is_commutative(self: hal_py.BooleanFunction.Node) → bool

Checks whether the Boolean function node is commutative.

Returns: True if the Boolean function node is commutative, False otherwise.
Return type: bool

is_constant(self: hal_py.BooleanFunction.Node) → bool

Checks whether the Boolean function node is of type Constant.

Returns: True if the Boolean function node is of type Constant, False otherwise.
Return type: bool

is_index(self: hal_py.BooleanFunction.Node) → bool

Checks whether the Boolean function node is of type Index.

Returns: True if the Boolean function node is of type Index, False otherwise.
Return type: bool

is_operand(self: hal_py.BooleanFunction.Node) → bool

Checks whether the Boolean function node is an operand node.

Returns: True if the Boolean function node is an operand node, False otherwise.
Return type: bool

is_operation(self: hal_py.BooleanFunction.Node) → bool

Checks whether the Boolean function node is an operation node.

Returns: True if the Boolean function node is an operation node, False otherwise.
Return type: bool

is_variable(self: hal_py.BooleanFunction.Node) → bool

Checks whether the Boolean function node is of type Variable.

Returns: True if the Boolean function node is of type Variable, False otherwise.
Return type: bool

property size

The bit-size of the node.

Type: int

property type

The type of the node.

Type: int

property variable

The (optional) variable name of the node.

Type: str

class NodeType

Holds all node types available in a Boolean function.

Add = 16

And = 0

Ashr = 514

Concat = 256

Constant = 4096

Eq = 1024

Index = 4097

Ite = 1029

Lshr = 513

Mul = 18

Not = 2

Or = 1

Rol = 515

Ror = 516

Sdiv = 19

Sext = 259

Shl = 512

Sle = 1025

Slice = 257

Slt = 1026

Srem = 21

Sub = 17

Udiv = 20

Ule = 1027

Ult = 1028

Urem = 22

Variable = 4098

Xor = 3

Zext = 258

__annotations__ = {}

__init__(*args, **kwargs)

__module__ = 'hal_py'

static Not(p0: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Negates the given Boolean function. Requires the Boolean function to be of the specified bit-size and produces a new Boolean function of the same bit-size.

Parameters

p0 (hal_py.BooleanFunction) – The Boolean function to negate.
size (int) – Bit-size of the operation.

Returns

The negated Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

ONE = <Value.ONE: 1>

static Or(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by applying an OR operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation.

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Rol(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Rotates a Boolean function to the left by the specified number of bits.

Parameters

p0 (hal_py.BooleanFunction) – Boolean function to rotate.
p1 (hal_py.BooleanFunction) – Boolean function of type Index encoding the number of bits to rotate.
size (int) – Bit-size of the rotated Boolean function.

Returns

The rotated Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Ror(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Rotates a Boolean function to the right by the specified number of bits.

Parameters

p0 (hal_py.BooleanFunction) – Boolean function to rotate.
p1 (hal_py.BooleanFunction) – Boolean function of type Index encoding the number of bits to rotate.
size (int) – Bit-size of the rotated Boolean function.

Returns

The rotated Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Sdiv(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by applying an SDIV operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation.

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Sext(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Sign-extends a Boolean function to the specified bit-size.

Parameters

p0 (hal_py.BooleanFunction) – Boolean function to extend.
p1 (hal_py.BooleanFunction) – Boolean function of type Index encoding the bit-size of the sign-extended result.
size (int) – Bit-size of the sign-extended Boolean function.

Returns

The sign-extended Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Shl(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Shifts a Boolean function to the left by the specified number of bits.

Parameters

p0 (hal_py.BooleanFunction) – Boolean function to shift.
p1 (hal_py.BooleanFunction) – Boolean function of type Index encoding the number of bits to shift.
size (int) – Bit-size of the shifted Boolean function.

Returns

The shifted Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Sle(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by a signed less-than-equal check that produces a single-bit result.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation (always =1).

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Slice(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, p2: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Returns the slice [i:j] of a Boolean function specified by a start index i and an end index j beginning at 0. Note that slice [i:j] includes positions i and j as well.

Parameters

p0 (hal_py.BooleanFunction) – Boolean function to slice.
p1 (hal_py.BooleanFunction) – Boolean function of type Index encoding start index i.
p2 (hal_py.BooleanFunction) – Boolean function of type Index encoding end index j.
size (int) – Bit-size of the resulting Boolean function slice, i.e., j - i + 1.

Returns

The Boolean function slice on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Slt(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by a signed less-than check that produces a single-bit result.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation (always =1).

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Srem(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by applying an SREM operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation.

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Sub(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by applying an SUB operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation.

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Udiv(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by applying an UDIV operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation.

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Ule(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by an unsigned less-than-equal check that produces a single-bit result.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation (always =1).

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Ult(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by an unsigned less-than check that produces a single-bit result.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation (always =1).

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

static Urem(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by applying an UREM operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation.

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

class Value

Represents the logic value that a Boolean function operates on.

Members:

ZERO : Represents a logical 0.

ONE : Represents a logical 1.

Z : Represents a high-impedance value.

X : Represents an undefined value.

ONE = <Value.ONE: 1>

X = <Value.X: -1>

Z = <Value.Z: -2>

ZERO = <Value.ZERO: 0>

__annotations__ = {}

__eq__(self: object, other: object) → bool

__getstate__(self: object) → int

__hash__(self: object) → int

__index__(self: hal_py.BooleanFunction.Value) → int

__init__(self: hal_py.BooleanFunction.Value, value: int) → None

__int__(self: hal_py.BooleanFunction.Value) → int

__members__ = {'ONE': <Value.ONE: 1>, 'X': <Value.X: -1>, 'Z': <Value.Z: -2>, 'ZERO': <Value.ZERO: 0>}

__module__ = 'hal_py'

__ne__(self: object, other: object) → bool

__repr__(self: object) → str

__setstate__(self: hal_py.BooleanFunction.Value, state: int) → None

__str__(*args, **kwargs)

Overloaded function.

__str__(self: handle) -> str
__str__(self: hal_py.BooleanFunction.Value) -> str

Translates the Boolean function value into its string representation.

returns

The value as a string.

rtype

str

name()

__str__(*args, **kwargs) Overloaded function.

__str__(self: handle) -> str
__str__(self: hal_py.BooleanFunction.Value) -> str

Translates the Boolean function value into its string representation.

returns

The value as a string.

rtype

str

property value

static Var(name: str, size: int = 1) → hal_py.BooleanFunction

Creates a multi-bit Boolean function of the given bit-size comprising only a variable of the specified name.

Parameters

name (str) – The name of the variable.
size (int) – The bit-size. Defaults to 1.

Returns

The BooleanFunction.

Return type

hal_py.BooleanFunction

X = <Value.X: -1>

static Xor(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Joins two Boolean functions by applying an XOR operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.

Parameters

p0 (hal_py.BooleanFunction) – First Boolean function.
p1 (hal_py.BooleanFunction) – Second Boolean function.
size (int) – Bit-size of the operation.

Returns

The joined Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

Z = <Value.Z: -2>

ZERO = <Value.ZERO: 0>

static Zext(p0: hal_py.BooleanFunction, p1: hal_py.BooleanFunction, size: int) → Optional[hal_py.BooleanFunction]

Zero-extends a Boolean function to the specified bit-size.

Parameters

p0 (hal_py.BooleanFunction) – Boolean function to extend.
p1 (hal_py.BooleanFunction) – Boolean function of type Index encoding the bit-size of the zero-extended result.
size (int) – Bit-size of the zero-extended Boolean function.

Returns

The zero-extended Boolean function on success, None otherwise.

Return type

hal_py.BooleanFunction or None

__add__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → hal_py.BooleanFunction

Joins two Boolean functions by an ADD operation. Requires both Boolean functions to be of the same bit-size.

Warning: fails if the Boolean functions have different bit-sizes.

Returns: The joined Boolean Bunction.
Return type: hal_py.BooleanFunction

__and__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → hal_py.BooleanFunction

Joins two Boolean functions by an AND operation. Requires both Boolean functions to be of the same bit-size.

Warning: fails if the Boolean functions have different bit-sizes.

Returns: The joined Boolean Bunction.
Return type: hal_py.BooleanFunction

__annotations__ = {}

__eq__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → bool

Checks whether two Boolean functions are equal.

Returns: True if both Boolean functions are equal, False otherwise.
Return type: bool

__hash__ = None

__iadd__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → hal_py.BooleanFunction

Joins two Boolean functions by an ADD operation in-place. Requires both Boolean functions to be of the same bit-size.

Warning: fails if the Boolean functions have different bit-sizes.

Returns: The joined Boolean Bunction.
Return type: hal_py.BooleanFunction

__iand__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → hal_py.BooleanFunction

Joins two Boolean functions by an AND operation in-place. Requires both Boolean functions to be of the same bit-size.

Warning: fails if the Boolean functions have different bit-sizes.

Returns: The joined Boolean Bunction.
Return type: hal_py.BooleanFunction

__imul__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → hal_py.BooleanFunction

Joins two Boolean functions by an MUL operation in-place. Requires both Boolean functions to be of the same bit-size.

Warning: fails if the Boolean functions have different bit-sizes.

Returns: The joined Boolean Bunction.
Return type: hal_py.BooleanFunction

__init__(self: hal_py.BooleanFunction) → None: Constructs an empty / invalid Boolean function.

__invert__(self: hal_py.BooleanFunction) → hal_py.BooleanFunction

Negates the Boolean function.

Returns: The negated Boolean function.
Return type: hal_py.BooleanFunction

__ior__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → hal_py.BooleanFunction

Joins two Boolean functions by an OR operation in-place. Requires both Boolean functions to be of the same bit-size.

Warning: fails if the Boolean functions have different bit-sizes.

Returns: The joined Boolean Bunction.
Return type: hal_py.BooleanFunction

__isub__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → hal_py.BooleanFunction

Joins two Boolean functions by an SUB operation in-place. Requires both Boolean functions to be of the same bit-size.

Warning: fails if the Boolean functions have different bit-sizes.

Returns: The joined Boolean Bunction.
Return type: hal_py.BooleanFunction

__ixor__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → hal_py.BooleanFunction

Joins two Boolean functions by an XOR operation in-place. Requires both Boolean functions to be of the same bit-size.

Warning: fails if the Boolean functions have different bit-sizes.

Returns: The joined Boolean Bunction.
Return type: hal_py.BooleanFunction

__lt__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → bool

Checks whether this Boolean function is ‘smaller’ than the other Boolean function.

Returns: True if this Boolean function is ‘smaller’, False otherwise.
Return type: bool

__module__ = 'hal_py'

__mul__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → hal_py.BooleanFunction

Joins two Boolean functions by an MUL operation. Requires both Boolean functions to be of the same bit-size.

**Warning:* fails if the Boolean functions have different bit-sizes.

Returns: The joined Boolean Bunction.
Return type: hal_py.BooleanFunction

__ne__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → bool

Checks whether two Boolean functions are unequal.

Returns: True if both Boolean functions are unequal, False otherwise.
Return type: bool

__or__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → hal_py.BooleanFunction

Joins two Boolean functions by an OR operation. Requires both Boolean functions to be of the same bit-size.

Warning: fails if the Boolean functions have different bit-sizes.

Returns: The joined Boolean Bunction.
Return type: hal_py.BooleanFunction

__str__(self: hal_py.BooleanFunction) → str

Translates the Boolean function into its string representation.

Returns: The Boolean function as a string.
Return type: str

__sub__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → hal_py.BooleanFunction

Joins two Boolean functions by an SUB operation. Requires both Boolean functions to be of the same bit-size.

Warning: fails if the Boolean functions have different bit-sizes.

Returns: The joined Boolean Bunction.
Return type: hal_py.BooleanFunction

__xor__(self: hal_py.BooleanFunction, arg0: hal_py.BooleanFunction) → hal_py.BooleanFunction

Joins two Boolean functions by an XOR operation. Requires both Boolean functions to be of the same bit-size.

Warning: fails if the Boolean functions have different bit-sizes.

Returns: The joined Boolean Bunction.
Return type: hal_py.BooleanFunction

clone(self: hal_py.BooleanFunction) → hal_py.BooleanFunction

Clones the Boolean function.

Returns: The cloned Boolean function.
Return type: hal_py.BooleanFunction

compute_truth_table(self: hal_py.BooleanFunction, ordered_variables: List[str] = [], remove_unknown_variables: bool = False) → Optional[List[List[hal_py.BooleanFunction.Value]]]

Computes the truth table outputs for a Boolean function that comprises <= 10 single-bit variables.

Warning: The generation of the truth table is exponential in the number of parameters.

Parameters

ordered_variables (list[str]) – A list describing the order of input variables used to generate the truth table. Defaults to an empty list.
remove_unknown_variables (bool) – Set True to remove variables from the truth table that are not present within the Boolean function, False otherwise. Defaults to False.

Returns

A list of values representing the truth table output on success, None otherwise.

Return type

list[list[hal_py.BooleanFunction.Value]] or None

evaluate(*args, **kwargs)

Overloaded function.

evaluate(self: hal_py.BooleanFunction, inputs: Dict[str, hal_py.BooleanFunction.Value]) -> Optional[hal_py.BooleanFunction.Value]

Evaluates a Boolean function comprising only single-bit variables using the given input values.

param dict[str,hal_py.BooleanFunction.Value] inputs

A dict from variable name to input value.

returns

The resulting value on success, None otherwise.

rtype

hal_py.BooleanFunction.Value or None
evaluate(self: hal_py.BooleanFunction, inputs: Dict[str, List[hal_py.BooleanFunction.Value]]) -> Optional[List[hal_py.BooleanFunction.Value]]

Evaluates a Boolean function comprising multi-bit variables using the given input values.

param dict[str,list[hal_py.BooleanFunction.Value]] inputs

A dict from variable name to a list of input values.

returns

A vector of values on success, None otherwise.

rtype

list[hal_py.BooleanFunction.Value] or None

static from_string(expression: str) → hal_py.BooleanFunction

Parses a Boolean function from a string expression.

Parameters: expression (str) – Boolean function string.
Returns: The Boolean function on success, an empty Boolean function otherwise.
Return type: hal_py.BooleanFunction

get_constant_value(self: hal_py.BooleanFunction) → Optional[List[hal_py.BooleanFunction.Value]]

Get the constant value of the top-level node of the Boolean function of type Constant as a list of hal_py.BooleanFunction.Value.

Returns: The constant value on success, None otherwise.
Return type: list[hal_py.BooleanFunction.Value] or None

get_constant_value_u64(self: hal_py.BooleanFunction) → Optional[int]

Get the constant value of the top-level node of the Boolean function of type Constant as long as it has a size <= 64-bit.

Returns: The constant value on success, None otherwise.
Return type: int or None

get_index_value(self: hal_py.BooleanFunction) → Optional[int]

Get the index value of the top-level node of the Boolean function of type Index.

Returns: The index value on success, None otherwise.
Return type: int or None

get_length(self: hal_py.BooleanFunction) → int

Returns the number of nodes in the Boolean function.

Returns: The number of nodes.
Return type: int

get_nodes(self: hal_py.BooleanFunction) → List[hal::BooleanFunction::Node]

Returns the reverse polish notation list of the Boolean function nodes.

Returns: A list of nodes.
Return type: list[hal_py.BooleanFunction.Node]

get_parameters(self: hal_py.BooleanFunction) → List[hal_py.BooleanFunction]

Returns the parameter list of the top-level node of the Boolean function.

Returns: A vector of Boolean functions.
Return type: list[hal_py.BooleanFunction]

get_size(self: hal_py.BooleanFunction) → int

Returns the bit-size of the Boolean function.

Returns: The bit-size of the Boolean function.
Return type: int

get_top_level_node(self: hal_py.BooleanFunction) → hal::BooleanFunction::Node

Returns the top-level node of the Boolean function.

Warning: fails if the Boolean function is empty.

Returns: The top-level node.
Return type: hal_py.BooleanFunction.Node

get_truth_table_as_string(self: hal_py.BooleanFunction, ordered_variables: List[str] = [], function_name: str = '', remove_unknown_variables: bool = False) → Optional[str]

Prints the truth table for a Boolean function that comprises <= 10 single-bit variables.

Warning: The generation of the truth table is exponential in the number of parameters.

Parameters

ordered_variables (list[str]) – A list describing the order of input variables used to generate the truth table. Defaults to an empty list.
function_name (str) – The name of the Boolean function to be printed as header of the output columns.
remove_unknown_variables (bool) – Set True to remove variables from the truth table that are not present within the Boolean function, False otherwise. Defaults to False.

Returns

A string representing the truth table on success, None otherwise.

Return type

str or None

get_variable_name(self: hal_py.BooleanFunction) → Optional[str]

Get the variable name of the top-level node of the Boolean function of type Variable.

Returns: The variable name on success, None otherwise.
Return type: str or None

get_variable_names(self: hal_py.BooleanFunction) → Set[str]

Returns the set of variable names used by the Boolean function.

Returns: A set of variable names.
Return type: set[str]

has_constant_value(*args, **kwargs)

Overloaded function.

has_constant_value(self: hal_py.BooleanFunction, arg0: List[hal_py.BooleanFunction.Value]) -> bool

Checks whether the top-level node of the Boolean function is of type Constant and holds a specific value.

param list[hal_py.BooleanFunction.Value] value

The constant value to check for.

returns

True if the top-level node of the Boolean function is of type Constant and holds the given value, False otherwise.

rtype

bool
has_constant_value(self: hal_py.BooleanFunction, arg0: int) -> bool

Checks whether the top-level node of the Boolean function is of type Constant and holds a specific value.

param int value

The constant value to check for.

returns

True if the top-level node of the Boolean function is of type Constant and holds the given value, False otherwise.

rtype

bool

has_index_value(self: hal_py.BooleanFunction, arg0: int) → bool

Checks whether the top-level node of the Boolean function is of type Index and holds a specific value.

Parameters: value (int) – The index value to check for.
Returns: True if the top-level node of the Boolean function is of type Index and holds the given value, False otherwise.
Return type: bool

has_variable_name(self: hal_py.BooleanFunction, arg0: str) → bool

Checks whether the top-level node of the Boolean function is of type Variable and holds a specific variable name.

Parameters: value (int) – The variable name to check for.
Returns: True if the top-level node of the Boolean function is of type Variable and holds the given variable name, False otherwise.
Return type: bool

is(self: hal_py.BooleanFunction, type: int) → bool

Checks whether the top-level node of the Boolean function is of a specific type.

Parameters: type (int) – The type to check for.
Returns: True if the node is of the given type, False otherwise.
Return type: bool

is_constant(self: hal_py.BooleanFunction) → bool

Checks whether the top-level node of the Boolean function is of type Constant.

Returns: True if the top-level node of the Boolean function is of type Constant, False otherwise.
Return type: bool

is_empty(self: hal_py.BooleanFunction) → bool

Checks whether the Boolean function is empty.

Returns: True if the Boolean function is empty, False otherwise.
Return type: bool

is_index(self: hal_py.BooleanFunction) → bool

Checks whether the top-level node of the Boolean function is of type Index.

Returns: True if the top-level node of the Boolean function is of type Index, False otherwise.
Return type: bool

is_variable(self: hal_py.BooleanFunction) → bool

Checks whether the top-level node of the Boolean function is of type Variable and holds a specific variable name.

Returns: True if the top-level node of the Boolean function is of type Variable, False otherwise.
Return type: bool

property length

The number of nodes in the Boolean function.

Type: int

nodes(self: hal_py.BooleanFunction) → List[hal::BooleanFunction::Node]

The reverse polish notation list of the Boolean function nodes.

Type: list[hal_py.BooleanFunction.Node]

property parameters

The parameter list of the top-level node of the Boolean function.

Type: list[hal_py.BooleanFunction]

simplify(self: hal_py.BooleanFunction) → hal_py.BooleanFunction

Simplifies the Boolean function.

Returns: The simplified Boolean function.
Return type: hal_py.BooleanFunction

property size

The bit-size of the Boolean function.

Type: int

substitute(*args, **kwargs)

Overloaded function.

substitute(self: hal_py.BooleanFunction, old_variable_name: str, new_variable_name: str) -> hal_py.BooleanFunction

Substitute a variable name with another one, i.e., renames the variable. The operation is applied to all instances of the variable in the function.

param str old_variable_name

The old variable name to substitute.

param str new_variable_name

The new variable name.

returns

The resulting Boolean function.

rtype

hal_py.BooleanFunction
substitute(self: hal_py.BooleanFunction, variable_name: str, function: hal_py.BooleanFunction) -> Optional[hal_py.BooleanFunction]

Substitute a variable with another Boolean function. The operation is applied to all instances of the variable in the function.

param str variable_name

The variable to substitute.

param hal_py.BooleanFunction function

The function replace the variable with.

returns

The resulting Boolean function on success, None otherwise.

rtype

hal_py.BooleanFunction or None
substitute(self: hal_py.BooleanFunction, substitutions: Dict[str, str]) -> hal_py.BooleanFunction

Substitute multiple variable names with different names at once, i.e., rename the variables. The operation is applied to all instances of the variable in the function.

param dict[str,str] substitutions

A dict from old variable names to new variable names.

returns

The resulting Boolean function.

rtype

hal_py.BooleanFunction
substitute(self: hal_py.BooleanFunction, substitutions: Dict[str, hal_py.BooleanFunction]) -> Optional[hal_py.BooleanFunction]

Substitute multiple variables with other boolean functions at once. The operation is applied to all instances of the variable in the function.

param dict substitutions

A map from the variable names to the function to replace the variable with.

returns

The resulting Boolean function on success, None otherwise.

rtype

hal_py.BooleanFunction or None

static to_string(value: List[hal_py.BooleanFunction.Value], base: int = 2) → Optional[str]

Convert the given bit-vector to its string representation in the given base.

Parameters

value (list[hal_py.BooleanFunction.Value]) – The value as a bit-vector.
base (int) – The base that the values should be converted to. Valid values are 2 (default), 8, 10, and 16.

Returns

A string representing the values in the given base on success, None otherwise.

Return type

str or None

static to_u64(value: List[hal_py.BooleanFunction.Value]) → Optional[int]

Convert the given bit-vector to its unsigned 64-bit integer representation.

Parameters: value (list[hal_py.BooleanFunction.Value]) – The value as a bit-vector.
Returns: A 64-bit integer representing the values on success, None otherwise.
Return type: int or None

property top_level_node

The top-level node of the Boolean function.

Warning: fails if the Boolean function is empty.

Type: hal_py.BooleanFunction.Node

property variable_names

The set of variable names used by the Boolean function.

Type: set[str]