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

__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__¶: Initialize self. See help(type(self)) for accurate signature.

__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

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

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

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

size¶

The bit-size of the node.

Type:	int

type¶

The type of the node.

Type:	int

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¶

__init__¶: Initialize self. See help(type(self)) for accurate signature.

__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>¶

__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

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

__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

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]

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

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

top_level_node¶

The top-level node of the Boolean function.

Warning: fails if the Boolean function is empty.

Type:	hal_py.BooleanFunction.Node

variable_names¶

The set of variable names used by the Boolean function.

Type:	set[str]