HAL  v4.5.0-124-g47ab54673
The Hardware Analyzer - a comprehensive reverse engineering and manipulation framework for gate-level netlists.
hal::BooleanFunction Class Referencefinal

#include <hal_core/netlist/boolean_function.h>

Collaboration diagram for hal::BooleanFunction:
Collaboration graph

Classes

struct  Node
 
struct  NodeType
 

Public Types

enum  Value { ZERO = 0 , ONE = 1 , X = -1 , Z = -2 }
 represents the type of the node More...
 

Public Member Functions

 BooleanFunction ()
 
BooleanFunction operator& (const BooleanFunction &other) const
 
BooleanFunctionoperator&= (const BooleanFunction &other)
 
BooleanFunction operator~ () const
 
BooleanFunction operator| (const BooleanFunction &other) const
 
BooleanFunctionoperator|= (const BooleanFunction &other)
 
BooleanFunction operator^ (const BooleanFunction &other) const
 
BooleanFunctionoperator^= (const BooleanFunction &other)
 
BooleanFunction operator+ (const BooleanFunction &other) const
 
BooleanFunctionoperator+= (const BooleanFunction &other)
 
BooleanFunction operator- (const BooleanFunction &other) const
 
BooleanFunctionoperator-= (const BooleanFunction &other)
 
BooleanFunction operator* (const BooleanFunction &other) const
 
BooleanFunctionoperator*= (const BooleanFunction &other)
 
bool operator== (const BooleanFunction &other) const
 
bool operator!= (const BooleanFunction &other) const
 
bool operator< (const BooleanFunction &other) const
 
bool is_empty () const
 
BooleanFunction clone () const
 
u16 size () const
 
bool is (u16 type) const
 
bool is_variable () const
 
bool has_variable_name (const std::string &variable_name) const
 
Result< std::string > get_variable_name () const
 
bool is_constant () const
 
bool has_constant_value (const std::vector< Value > &value) const
 
bool has_constant_value (u64 value) const
 
Result< std::vector< Value > > get_constant_value () const
 
Result< u64get_constant_value_u64 () const
 
bool is_index () const
 
bool has_index_value (u16 index) const
 
Result< u16get_index_value () const
 
const BooleanFunction::Nodeget_top_level_node () const
 
u32 length () const
 
const std::vector< BooleanFunction::Node > & get_nodes () const
 
std::vector< BooleanFunctionget_parameters () const
 
std::set< std::string > get_variable_names () const
 
std::string to_string (std::function< Result< std::string >(const BooleanFunction::Node &node, std::vector< std::string > &&operands)> &&printer=default_printer) const
 
BooleanFunction simplify () const
 
BooleanFunction simplify_local () const
 
BooleanFunction substitute (const std::string &old_variable_name, const std::string &new_variable_name) const
 
Result< BooleanFunctionsubstitute (const std::string &variable_name, const BooleanFunction &function) const
 
BooleanFunction substitute (const std::map< std::string, std::string > &substitutions) const
 
Result< BooleanFunctionsubstitute (const std::map< std::string, BooleanFunction > &substitutions) const
 
Result< Valueevaluate (const std::unordered_map< std::string, Value > &inputs) const
 
Result< std::vector< Value > > evaluate (const std::unordered_map< std::string, std::vector< Value >> &inputs) const
 
Result< std::vector< std::vector< Value > > > compute_truth_table (const std::vector< std::string > &ordered_variables={}, bool remove_unknown_variables=false) const
 
Result< std::string > get_truth_table_as_string (const std::vector< std::string > &ordered_variables={}, std::string function_name="", bool remove_unknown_variables=false) const
 
z3::expr to_z3 (z3::context &context, const std::map< std::string, z3::expr > &var2expr={}) const
 

Static Public Member Functions

static std::string to_string (Value value)
 
static Result< std::string > to_string (const std::vector< BooleanFunction::Value > &value, u8 base=2)
 
static Result< u64to_u64 (const std::vector< BooleanFunction::Value > &value)
 
static Result< BooleanFunctionbuild (std::vector< Node > &&nodes)
 
static BooleanFunction Var (const std::string &name, u16 size=1)
 
static BooleanFunction Const (const BooleanFunction::Value &value)
 
static BooleanFunction Const (const std::vector< BooleanFunction::Value > &value)
 
static BooleanFunction Const (u64 value, u16 size)
 
static BooleanFunction Index (u16 index, u16 size)
 
static Result< BooleanFunctionAnd (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionOr (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionNot (BooleanFunction &&p0, u16 size)
 
static Result< BooleanFunctionXor (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionAdd (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionSub (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionMul (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionSdiv (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionUdiv (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionSrem (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionUrem (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionSlice (BooleanFunction &&p0, BooleanFunction &&p1, BooleanFunction &&p2, u16 size)
 
static Result< BooleanFunctionConcat (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionZext (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionSext (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionShl (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionLshr (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionAshr (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionRol (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionRor (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionEq (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionSle (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionSlt (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionUle (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionUlt (BooleanFunction &&p0, BooleanFunction &&p1, u16 size)
 
static Result< BooleanFunctionIte (BooleanFunction &&p0, BooleanFunction &&p1, BooleanFunction &&p2, u16 size)
 
static Result< BooleanFunctionfrom_string (const std::string &expression)
 

Static Public Attributes

static constexpr u32 MAX_TRUTH_TABLE_VARIABLES = 20
 

Friends

std::ostream & operator<< (std::ostream &os, Value v)
 
std::ostream & operator<< (std::ostream &os, const BooleanFunction &f)
 

Detailed Description

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.

Definition at line 54 of file boolean_function.h.

Member Enumeration Documentation

◆ Value

represents the type of the node

Represents the logic value that a Boolean function operates on.

Enumerator
ZERO 

Represents a logical 0.

ONE 

Represents a logical 1.

Represents an undefined value.

Represents a high-impedance value.

Definition at line 73 of file boolean_function.h.

Constructor & Destructor Documentation

◆ BooleanFunction()

hal::BooleanFunction::BooleanFunction ( )
explicit

Constructs an empty / invalid Boolean function.

Definition at line 249 of file boolean_function.cpp.

Referenced by Add(), And(), Ashr(), build(), clone(), Concat(), Const(), Eq(), get_parameters(), Index(), Ite(), Lshr(), Mul(), Not(), Or(), Rol(), Ror(), Sdiv(), Sext(), Shl(), Sle(), Slice(), Slt(), Srem(), Sub(), substitute(), Udiv(), Ule(), Ult(), Urem(), Var(), Xor(), and Zext().

Member Function Documentation

◆ Add()

Result< BooleanFunction > hal::BooleanFunction::Add ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation.
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 340 of file boolean_function.cpp.

References hal::BooleanFunction::NodeType::Add, BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), and size().

Referenced by hal::boolean_function_init(), hal::module_identification::check_addition(), hal::module_identification::check_addition_offset(), operator+(), and operator+=().

◆ And()

Result< BooleanFunction > hal::BooleanFunction::And ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation.
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 297 of file boolean_function.cpp.

References hal::BooleanFunction::NodeType::And, BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), and size().

Referenced by hal::boolean_function_init(), hal::module_identification::VerifiedCandidate::get_merged_word_level_operation(), operator&(), operator&=(), and hal::netlist_preprocessing::simplify_lut_inits().

◆ Ashr()

Result< BooleanFunction > hal::BooleanFunction::Ashr ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- Boolean function to shift.
[in]p1- Boolean function of type Index encoding the number of bits to shift.
[in]size- Bit-size of the shifted Boolean function.
Returns
Ok() and the shifted Boolean function on success, an error otherwise.

Definition at line 515 of file boolean_function.cpp.

References hal::BooleanFunction::NodeType::Ashr, BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), and size().

Referenced by hal::boolean_function_init().

◆ build()

Result< BooleanFunction > hal::BooleanFunction::build ( std::vector< Node > &&  nodes)
static

Builds and validates a Boolean function from a vector of nodes.

Parameters
[in]nodes- Vector of Boolean function nodes.
Returns
Ok() and the Boolean function on success, an error otherwise.

Definition at line 253 of file boolean_function.cpp.

References BooleanFunction(), and ERR_APPEND.

Referenced by hal::boolean_function_init(), hal::SMT::Model::evaluate(), and hal::BooleanFunctionParser::translate().

◆ clone()

BooleanFunction hal::BooleanFunction::clone ( ) const

Clones the Boolean function.

Returns
The cloned Boolean function.

Definition at line 748 of file boolean_function.cpp.

References BooleanFunction().

Referenced by hal::GateType::add_boolean_function(), hal::boolean_function_init(), hal::GateTypeComponent::create_ff_component(), hal::GateTypeComponent::create_ram_port_component(), hal::FFComponent::get_async_reset_function(), hal::LatchComponent::get_async_reset_function(), hal::FFComponent::get_async_set_function(), hal::LatchComponent::get_async_set_function(), hal::BooleanFunctionDecorator::get_boolean_function_from(), hal::FFComponent::get_clock_function(), hal::LatchComponent::get_data_in_function(), hal::LatchComponent::get_enable_function(), hal::module_identification::VerifiedCandidate::get_merged_word_level_operation(), hal::FFComponent::get_next_state_function(), operator&(), operator&=(), operator*(), operator*=(), operator+(), operator+=(), operator-(), operator-=(), operator^(), operator^=(), operator|(), operator|=(), operator~(), hal::SMT::SymbolicState::set(), hal::FFComponent::set_async_reset_function(), hal::LatchComponent::set_async_reset_function(), hal::FFComponent::set_async_set_function(), hal::LatchComponent::set_async_set_function(), hal::FFComponent::set_clock_function(), hal::RAMPortComponent::set_clock_function(), hal::LatchComponent::set_data_in_function(), hal::LatchComponent::set_enable_function(), hal::RAMPortComponent::set_enable_function(), hal::FFComponent::set_next_state_function(), simplify(), simplify_local(), hal::solve_fsm::solve_fsm(), substitute(), hal::BooleanFunctionDecorator::substitute_module_pins(), hal::BooleanFunctionDecorator::substitute_power_ground_nets(), and hal::BooleanFunctionDecorator::substitute_power_ground_pins().

◆ compute_truth_table()

Result< std::vector< std::vector< BooleanFunction::Value > > > hal::BooleanFunction::compute_truth_table ( const std::vector< std::string > &  ordered_variables = {},
bool  remove_unknown_variables = false 
) const

◆ Concat()

Result< BooleanFunction > hal::BooleanFunction::Concat ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- First Boolean function (MSBs).
[in]p1- Second Boolean function (LSBs).
[in]size- Bit-size of the concatenated Boolean function, i.e., n + m.
Returns
Ok() and the concatenated Boolean function on success, an error otherwise.

Definition at line 440 of file boolean_function.cpp.

References BooleanFunction(), hal::BooleanFunction::NodeType::Concat, ERR, OK, hal::BooleanFunction::Node::Operation(), and size().

Referenced by hal::boolean_function_init(), hal::module_identification::check_addition_offset(), hal::BooleanFunctionDecorator::get_boolean_function_from(), hal::solve_fsm::solve_fsm(), and hal::solve_fsm::solve_fsm_brute_force().

◆ Const() [1/3]

◆ Const() [2/3]

BooleanFunction hal::BooleanFunction::Const ( const std::vector< BooleanFunction::Value > &  value)
static

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

Parameters
[in]value- The vector of values.
Returns
The Boolean function.

Definition at line 275 of file boolean_function.cpp.

References BooleanFunction(), and hal::BooleanFunction::Node::Constant().

◆ Const() [3/3]

BooleanFunction hal::BooleanFunction::Const ( u64  value,
u16  size 
)
static

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

Parameters
[in]value- The integer value.
[in]size- The bit-size.
Returns
The Boolean function.

Definition at line 280 of file boolean_function.cpp.

References Const(), and size().

◆ Eq()

Result< BooleanFunction > hal::BooleanFunction::Eq ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation (always =1).
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 563 of file boolean_function.cpp.

References BooleanFunction(), hal::BooleanFunction::NodeType::Eq, ERR, OK, hal::BooleanFunction::Node::Operation(), and size().

Referenced by hal::boolean_function_init(), hal::module_identification::VerifiedCandidate::get_merged_word_level_operation(), and hal::solve_fsm::solve_fsm().

◆ evaluate() [1/2]

Result< std::vector< BooleanFunction::Value > > hal::BooleanFunction::evaluate ( const std::unordered_map< std::string, std::vector< Value >> &  inputs) const

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

Parameters
[in]inputs- A map from variable name to a vector of input values.
Returns
Ok() and the resulting value on success, an error otherwise.

Definition at line 1257 of file boolean_function.cpp.

References Const(), ERR, name, OK, size(), to_string(), and Var().

◆ evaluate() [2/2]

Result< BooleanFunction::Value > hal::BooleanFunction::evaluate ( const std::unordered_map< std::string, Value > &  inputs) const

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

Parameters
[in]inputs- A map from variable name to input value.
Returns
Ok() and the resulting value on success, an error otherwise.

Definition at line 1226 of file boolean_function.cpp.

References ERR, name, OK, size(), and to_string().

Referenced by compute_truth_table(), and hal::boolean_influence::get_boolean_influence_with_hal_boolean_function_class().

◆ from_string()

Result< BooleanFunction > hal::BooleanFunction::from_string ( const std::string &  expression)
static

◆ get_constant_value()

Result< std::vector< BooleanFunction::Value > > hal::BooleanFunction::get_constant_value ( ) const

Get the value of the top-level node of the Boolean function of type Constant as a vector of BooleanFunction::Value.

Returns
The constant value on success, an error otherwise.

Definition at line 806 of file boolean_function.cpp.

References ERR, hal::BooleanFunction::Node::get_constant_value(), get_top_level_node(), and is_empty().

◆ get_constant_value_u64()

Result< u64 > hal::BooleanFunction::get_constant_value_u64 ( ) const

Get the 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, an error otherwise.

Definition at line 816 of file boolean_function.cpp.

References ERR, hal::BooleanFunction::Node::get_constant_value_u64(), get_top_level_node(), and is_empty().

◆ get_index_value()

Result< u16 > hal::BooleanFunction::get_index_value ( ) const

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

Returns
The index value on success, an error otherwise.

Definition at line 836 of file boolean_function.cpp.

References ERR, hal::BooleanFunction::Node::get_index_value(), get_top_level_node(), and is_empty().

◆ get_nodes()

const std::vector< BooleanFunction::Node > & hal::BooleanFunction::get_nodes ( ) const

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

Returns
A vector of nodes.

Definition at line 856 of file boolean_function.cpp.

Referenced by hal::boolean_function_init(), hal::SMT::Model::evaluate(), and hal::z3_utils::from_bf().

◆ get_parameters()

std::vector< BooleanFunction > hal::BooleanFunction::get_parameters ( ) const

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

Returns
A vector of Boolean functions.

Developer Note

Instead of iterating the whole Boolean function and decomposing the abstract syntax tree, we simple iterate the Boolean function once and compute the coverage, i.e. how many nodes are covered below the node in the tree, and based on these indices assemble the Boolean function node vector.

Definition at line 861 of file boolean_function.cpp.

References BooleanFunction(), get_top_level_node(), index, and length().

Referenced by hal::boolean_function_init().

◆ get_top_level_node()

const BooleanFunction::Node & hal::BooleanFunction::get_top_level_node ( ) const

Returns the top-level node of the Boolean function.

Warning
Fails if the Boolean function is empty.
Returns
The top-level node.

Definition at line 846 of file boolean_function.cpp.

Referenced by hal::boolean_function_init(), get_constant_value(), get_constant_value_u64(), get_index_value(), get_parameters(), get_variable_name(), has_constant_value(), has_index_value(), has_variable_name(), is(), is_constant(), is_index(), is_variable(), and size().

◆ get_truth_table_as_string()

Result< std::string > hal::BooleanFunction::get_truth_table_as_string ( const std::vector< std::string > &  ordered_variables = {},
std::string  function_name = "",
bool  remove_unknown_variables = false 
) const

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
[in]ordered_variables- A vector describing the order of input variables used to generate the truth table. Defaults to an empty vector.
[in]function_name- The name of the Boolean function to be printed as header of the output columns.
[in]remove_unknown_variables- Set true to remove variables from the truth table that are not present within the Boolean function, false otherwise. Defaults to false.
Returns
Ok() and a string representing the truth table on success, an error otherwise.

Definition at line 1524 of file boolean_function.cpp.

References compute_truth_table(), ERR_APPEND, get_variable_names(), and OK.

◆ get_variable_name()

Result< std::string > hal::BooleanFunction::get_variable_name ( ) const

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

Returns
The variable name on success, an error otherwise.

Definition at line 781 of file boolean_function.cpp.

References ERR, get_top_level_node(), hal::BooleanFunction::Node::get_variable_name(), and is_empty().

Referenced by hal::BooleanFunctionNetDecorator::get_net_from(), hal::BooleanFunctionNetDecorator::get_net_id_from(), hal::netlist_preprocessing::remove_buffers(), and substitute().

◆ get_variable_names()

◆ has_constant_value() [1/2]

bool hal::BooleanFunction::has_constant_value ( const std::vector< Value > &  value) const

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

Parameters
[in]value- The constant value to check for.
Returns
true if the Boolean function is of type Constant and holds the given value, false otherwise.

Definition at line 796 of file boolean_function.cpp.

References get_top_level_node(), hal::BooleanFunction::Node::has_constant_value(), and is_empty().

Referenced by hal::boolean_function_init(), and hal::module_identification::has_constant_value().

◆ has_constant_value() [2/2]

bool hal::BooleanFunction::has_constant_value ( u64  value) const

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

Parameters
[in]value- The constant value to check for.
Returns
true if the Boolean function is of type Constant and holds the given value, false otherwise.

Definition at line 801 of file boolean_function.cpp.

References get_top_level_node(), hal::BooleanFunction::Node::has_constant_value(), and is_empty().

◆ has_index_value()

bool hal::BooleanFunction::has_index_value ( u16  index) const

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

Parameters
[in]index- The index value to check for.
Returns
true if the Boolean function is of type Index and holds the given value, false otherwise.

Definition at line 831 of file boolean_function.cpp.

References get_top_level_node(), hal::BooleanFunction::Node::has_index_value(), and is_empty().

Referenced by hal::boolean_function_init().

◆ has_variable_name()

bool hal::BooleanFunction::has_variable_name ( const std::string &  variable_name) const

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

Parameters
variable_name- The variable name to check for.
Returns
true if the Boolean function is of type Variable and holds the given variable name, false otherwise.

Definition at line 776 of file boolean_function.cpp.

References get_top_level_node(), hal::BooleanFunction::Node::has_variable_name(), and is_empty().

Referenced by hal::boolean_function_init(), and substitute().

◆ Index()

BooleanFunction hal::BooleanFunction::Index ( u16  index,
u16  size 
)
static

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

Parameters
[in]index- The integer value.
[in]size- The bit-size.
Returns
The Boolean function.

Definition at line 292 of file boolean_function.cpp.

References BooleanFunction(), hal::BooleanFunction::Node::Index(), index, and size().

Referenced by hal::boolean_function_init(), hal::BooleanFunctionDecorator::get_boolean_function_from(), and hal::BooleanFunctionDecorator::substitute_module_pins().

◆ is()

bool hal::BooleanFunction::is ( u16  type) const

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

Parameters
[in]type- The type to check for.
Returns
true if the node is of the given type, false otherwise.

Definition at line 766 of file boolean_function.cpp.

References get_top_level_node(), hal::BooleanFunction::Node::is(), and is_empty().

Referenced by hal::boolean_function_init(), hal::BooleanFunction::Node::is_constant(), hal::BooleanFunction::Node::is_index(), and hal::BooleanFunction::Node::is_variable().

◆ is_constant()

bool hal::BooleanFunction::is_constant ( ) const

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.

Definition at line 791 of file boolean_function.cpp.

References get_top_level_node(), hal::BooleanFunction::Node::is_constant(), and is_empty().

Referenced by hal::boolean_function_init(), hal::BooleanFunction::Node::get_constant_value(), hal::BooleanFunction::Node::get_constant_value_u64(), hal::BooleanFunction::Node::has_constant_value(), and hal::BooleanFunction::Node::is_operand().

◆ is_empty()

◆ is_index()

bool hal::BooleanFunction::is_index ( ) const

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.

Definition at line 826 of file boolean_function.cpp.

References get_top_level_node(), is_empty(), and hal::BooleanFunction::Node::is_index().

Referenced by hal::boolean_function_init(), hal::BooleanFunction::Node::get_index_value(), hal::BooleanFunction::Node::has_index_value(), and hal::BooleanFunction::Node::is_operand().

◆ is_variable()

bool hal::BooleanFunction::is_variable ( ) const

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

Returns
true if the top-level node of the Boolean function is of type Variable, false otherwise.

Definition at line 771 of file boolean_function.cpp.

References get_top_level_node(), is_empty(), and hal::BooleanFunction::Node::is_variable().

Referenced by hal::boolean_function_init(), hal::BooleanFunction::Node::get_variable_name(), hal::BooleanFunction::Node::has_variable_name(), hal::BooleanFunction::Node::is_operand(), hal::netlist_preprocessing::remove_buffers(), and hal::SMT::SymbolicState::set().

◆ Ite()

Result< BooleanFunction > hal::BooleanFunction::Ite ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
BooleanFunction &&  p2,
u16  size 
)
static

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
[in]p0- Boolean function condition.
[in]p1- Boolean function for true-case.
[in]p2- Boolean function for false-case.
[in]size- Bit-size of the operation, i.e., size of p1 and p2.
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 618 of file boolean_function.cpp.

References BooleanFunction(), ERR, hal::BooleanFunction::NodeType::Ite, OK, hal::BooleanFunction::Node::Operation(), and size().

Referenced by hal::boolean_function_init(), and hal::module_identification::VerifiedCandidate::get_merged_word_level_operation().

◆ length()

u32 hal::BooleanFunction::length ( ) const

Returns the number of nodes in the Boolean function.

Returns
The number of nodes.

Definition at line 851 of file boolean_function.cpp.

Referenced by hal::boolean_function_init(), and get_parameters().

◆ Lshr()

Result< BooleanFunction > hal::BooleanFunction::Lshr ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- Boolean function to shift.
[in]p1- Boolean function of type Index encoding the number of bits to shift.
[in]size- Bit-size of the shifted Boolean function.
Returns
Ok() and the shifted Boolean function on success, an error otherwise.

Definition at line 499 of file boolean_function.cpp.

References BooleanFunction(), ERR, hal::BooleanFunction::NodeType::Lshr, OK, hal::BooleanFunction::Node::Operation(), and size().

Referenced by hal::boolean_function_init().

◆ Mul()

Result< BooleanFunction > hal::BooleanFunction::Mul ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation.
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 362 of file boolean_function.cpp.

References BooleanFunction(), ERR, hal::BooleanFunction::NodeType::Mul, OK, hal::BooleanFunction::Node::Operation(), and size().

Referenced by hal::boolean_function_init(), operator*(), and operator*=().

◆ Not()

Result< BooleanFunction > hal::BooleanFunction::Not ( BooleanFunction &&  p0,
u16  size 
)
static

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
[in]p0- The Boolean function to negate.
[in]size- Bit-size of the operation.
Returns
Ok() and the negated Boolean function on success, an error otherwise.

Definition at line 319 of file boolean_function.cpp.

References BooleanFunction(), ERR, hal::BooleanFunction::NodeType::Not, OK, hal::BooleanFunction::Node::Operation(), and size().

Referenced by hal::boolean_function_init(), operator~(), and hal::solve_fsm::solve_fsm().

◆ operator!=()

bool hal::BooleanFunction::operator!= ( const BooleanFunction other) const

Checks whether two Boolean functions are unequal.

Parameters
[in]other- The other Boolean function.
Returns
true if the Boolean functions are unequal, false otherwise.

Definition at line 722 of file boolean_function.cpp.

◆ operator&()

BooleanFunction hal::BooleanFunction::operator& ( const BooleanFunction other) const

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.
Parameters
[in]other- The other Boolean function.
Returns
The joined Boolean function.

Definition at line 634 of file boolean_function.cpp.

References And(), clone(), and size().

◆ operator&=()

BooleanFunction & hal::BooleanFunction::operator&= ( const BooleanFunction other)

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.
Parameters
[in]other- The other Boolean function.
Returns
The joined Boolean function.

Definition at line 639 of file boolean_function.cpp.

References And(), clone(), and size().

◆ operator*()

BooleanFunction hal::BooleanFunction::operator* ( const BooleanFunction other) const

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.
Parameters
[in]other- The other Boolean function.
Returns
The joined Boolean function.

Definition at line 694 of file boolean_function.cpp.

References clone(), Mul(), and size().

◆ operator*=()

BooleanFunction & hal::BooleanFunction::operator*= ( const BooleanFunction other)

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.
Parameters
[in]other- The other Boolean function.
Returns
The joined Boolean function.

Definition at line 699 of file boolean_function.cpp.

References clone(), Mul(), and size().

◆ operator+()

BooleanFunction hal::BooleanFunction::operator+ ( const BooleanFunction other) const

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.
Parameters
[in]other- The other Boolean function.
Returns
The joined Boolean function.

Definition at line 672 of file boolean_function.cpp.

References Add(), clone(), and size().

◆ operator+=()

BooleanFunction & hal::BooleanFunction::operator+= ( const BooleanFunction other)

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.
Parameters
[in]other- The other Boolean function.
Returns
The joined Boolean function.

Definition at line 677 of file boolean_function.cpp.

References Add(), clone(), and size().

◆ operator-()

BooleanFunction hal::BooleanFunction::operator- ( const BooleanFunction other) const

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.
Parameters
[in]other- The other Boolean function.
Returns
The joined Boolean function.

Definition at line 683 of file boolean_function.cpp.

References clone(), size(), and Sub().

◆ operator-=()

BooleanFunction & hal::BooleanFunction::operator-= ( const BooleanFunction other)

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.
Parameters
[in]other- The other Boolean function.
Returns
The joined Boolean function.

Definition at line 688 of file boolean_function.cpp.

References clone(), size(), and Sub().

◆ operator<()

bool hal::BooleanFunction::operator< ( const BooleanFunction other) const

Checks whether this Boolean function is 'smaller' than the other Boolean function.

Parameters
[in]other- The other Boolean function.
Returns
true if this Boolean function is 'smaller', false otherwise.

Definition at line 727 of file boolean_function.cpp.

◆ operator==()

bool hal::BooleanFunction::operator== ( const BooleanFunction other) const

Checks whether two Boolean functions are equal.

Parameters
[in]other- The other Boolean function.
Returns
true if the Boolean functions are equal, false otherwise.

Definition at line 705 of file boolean_function.cpp.

◆ operator^()

BooleanFunction hal::BooleanFunction::operator^ ( const BooleanFunction other) const

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.
Parameters
[in]other- The other Boolean function.
Returns
The joined Boolean function.

Definition at line 661 of file boolean_function.cpp.

References clone(), size(), and Xor().

◆ operator^=()

BooleanFunction & hal::BooleanFunction::operator^= ( const BooleanFunction other)

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.
Parameters
[in]other- The other Boolean function.
Returns
The joined Boolean function.

Definition at line 666 of file boolean_function.cpp.

References clone(), size(), and Xor().

◆ operator|()

BooleanFunction hal::BooleanFunction::operator| ( const BooleanFunction other) const

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.
Parameters
[in]other- The other Boolean function.
Returns
The joined Boolean function.

Definition at line 650 of file boolean_function.cpp.

References clone(), Or(), and size().

◆ operator|=()

BooleanFunction & hal::BooleanFunction::operator|= ( const BooleanFunction other)

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.
Parameters
[in]other- The other Boolean function.
Returns
The joined Boolean function.

Definition at line 655 of file boolean_function.cpp.

References clone(), Or(), and size().

◆ operator~()

BooleanFunction hal::BooleanFunction::operator~ ( ) const

Negates the Boolean function.

Returns
The negated Boolean function.

Definition at line 645 of file boolean_function.cpp.

References clone(), Not(), and size().

◆ Or()

Result< BooleanFunction > hal::BooleanFunction::Or ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation.
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 308 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), hal::BooleanFunction::NodeType::Or, and size().

Referenced by hal::boolean_function_init(), operator|(), and operator|=().

◆ Rol()

Result< BooleanFunction > hal::BooleanFunction::Rol ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- Boolean function to rotate.
[in]p1- Boolean function of type Index encoding the number of bits to rotate.
[in]size- Bit-size of the rotated Boolean function.
Returns
Ok() and the rotated Boolean function on success, an error otherwise.

Definition at line 531 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), hal::BooleanFunction::NodeType::Rol, and size().

Referenced by hal::boolean_function_init().

◆ Ror()

Result< BooleanFunction > hal::BooleanFunction::Ror ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- Boolean function to rotate.
[in]p1- Boolean function of type Index encoding the number of bits to rotate.
[in]size- Bit-size of the rotated Boolean function.
Returns
Ok() and the rotated Boolean function on success, an error otherwise.

Definition at line 547 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), hal::BooleanFunction::NodeType::Ror, and size().

Referenced by hal::boolean_function_init().

◆ Sdiv()

Result< BooleanFunction > hal::BooleanFunction::Sdiv ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation.
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 373 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), hal::BooleanFunction::NodeType::Sdiv, and size().

Referenced by hal::boolean_function_init().

◆ Sext()

Result< BooleanFunction > hal::BooleanFunction::Sext ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- Boolean function to extend.
[in]p1- Boolean function of type Index encoding the bit-size of the sign-extended result.
[in]size- Bit-size of the sign-extended Boolean function.
Returns
Ok() and the extended Boolean function on success, an error otherwise.

Definition at line 467 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), hal::BooleanFunction::NodeType::Sext, and size().

Referenced by hal::boolean_function_init(), and hal::BooleanFunctionDecorator::get_boolean_function_from().

◆ Shl()

Result< BooleanFunction > hal::BooleanFunction::Shl ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- Boolean function to shift.
[in]p1- Boolean function of type Index encoding the number of bits to shift.
[in]size- Bit-size of the shifted Boolean function.
Returns
Ok() and the shifted Boolean function on success, an error otherwise.

Definition at line 483 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), hal::BooleanFunction::NodeType::Shl, and size().

Referenced by hal::boolean_function_init().

◆ simplify()

BooleanFunction hal::BooleanFunction::simplify ( ) const

Simplifies the Boolean function.

Returns
The simplified Boolean function.

Definition at line 1112 of file boolean_function.cpp.

References clone(), and hal::Simplification::local_simplification().

Referenced by hal::boolean_function_init(), and hal::netlist_utils::remove_buffers().

◆ simplify_local()

BooleanFunction hal::BooleanFunction::simplify_local ( ) const

Simplifies the Boolean function using only the local simplification.

Returns
The simplified Boolean function.

Definition at line 1121 of file boolean_function.cpp.

References clone(), and hal::Simplification::local_simplification().

Referenced by hal::boolean_function_init(), and hal::netlist_preprocessing::remove_buffers().

◆ size()

◆ Sle()

Result< BooleanFunction > hal::BooleanFunction::Sle ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation (always =1).
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 574 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Sle.

Referenced by hal::boolean_function_init(), and hal::module_identification::check_leq().

◆ Slice()

Result< BooleanFunction > hal::BooleanFunction::Slice ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
BooleanFunction &&  p2,
u16  size 
)
static

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
[in]p0- Boolean function to slice.
[in]p1- Boolean function of type Index encoding start index i.
[in]p2- Boolean function of type Index encoding end index j.
[in]size- Bit-size of the resulting Boolean function slice, i.e., j - i + 1.
Returns
OK() and the Boolean function slice on success, an error otherwise.

Definition at line 417 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Slice.

Referenced by hal::boolean_function_init(), and hal::BooleanFunctionDecorator::substitute_module_pins().

◆ Slt()

Result< BooleanFunction > hal::BooleanFunction::Slt ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation (always =1).
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 585 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Slt.

Referenced by hal::boolean_function_init(), and hal::module_identification::check_leq().

◆ Srem()

Result< BooleanFunction > hal::BooleanFunction::Srem ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation.
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 395 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Srem.

Referenced by hal::boolean_function_init().

◆ Sub()

Result< BooleanFunction > hal::BooleanFunction::Sub ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation.
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 351 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Sub.

Referenced by hal::boolean_function_init(), hal::module_identification::check_sub(), operator-(), and operator-=().

◆ substitute() [1/4]

Result< BooleanFunction > hal::BooleanFunction::substitute ( const std::map< std::string, BooleanFunction > &  substitutions) const

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

Parameters
[in]substitutions- A map from variable names to Boolean functions.
Returns
Ok() and the resulting Boolean function on success, an error otherwise.

Definition at line 1189 of file boolean_function.cpp.

References BooleanFunction(), clone(), ERR, and OK.

◆ substitute() [2/4]

BooleanFunction hal::BooleanFunction::substitute ( const std::map< std::string, std::string > &  substitutions) const

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.

Parameters
[in]substitutions- A map from old variable names to new variable names.
Returns
The resulting Boolean function.

Definition at line 1172 of file boolean_function.cpp.

References clone(), get_variable_name(), and hal::BooleanFunction::Node::Variable().

◆ substitute() [3/4]

BooleanFunction hal::BooleanFunction::substitute ( const std::string &  old_variable_name,
const std::string &  new_variable_name 
) const

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.

Parameters
[in]old_variable_name- The old variable name to substitute.
[in]new_variable_name- The new variable name.
Returns
The resulting Boolean function.

Definition at line 1128 of file boolean_function.cpp.

References clone(), has_variable_name(), size(), and hal::BooleanFunction::Node::Variable().

Referenced by hal::boolean_function_init(), hal::verilator::converter::get_function_for_combinational_gate(), hal::Gate::get_resolved_boolean_function(), hal::netlist_utils::remove_buffers(), hal::solve_fsm::solve_fsm_brute_force(), hal::BooleanFunctionDecorator::substitute_power_ground_nets(), and hal::BooleanFunctionDecorator::substitute_power_ground_pins().

◆ substitute() [4/4]

Result< BooleanFunction > hal::BooleanFunction::substitute ( const std::string &  variable_name,
const BooleanFunction function 
) const

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

Parameters
[in]variable_name- The variable to substitute.
[in]function- The function replace the variable with.
Returns
Ok() and the resulting Boolean function on success, an error otherwise.

Definition at line 1142 of file boolean_function.cpp.

References BooleanFunction(), clone(), ERR, name, OK, and to_string().

◆ to_string() [1/3]

Result< std::string > hal::BooleanFunction::to_string ( const std::vector< BooleanFunction::Value > &  value,
u8  base = 2 
)
static

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

Parameters
[in]value- The value as a bit-vector.
[in]base- 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, an error otherwise.

Definition at line 205 of file boolean_function.cpp.

References ERR.

◆ to_string() [2/3]

std::string hal::BooleanFunction::to_string ( std::function< Result< std::string >(const BooleanFunction::Node &node, std::vector< std::string > &&operands)> &&  printer = default_printer) const

Translates the Boolean function into its string representation.

Parameters
[in]printer- A function a node and its operands as inputs and outputs their string representation. Allows for different grammers to be printed. Defaults to the 'default_printer'.
Returns
The Boolean function as a string.

Definition at line 1018 of file boolean_function.cpp.

References hal::BooleanFunction::Node::get_arity(), log_error, and hal::BooleanFunction::Node::to_string().

◆ to_string() [3/3]

◆ to_u64()

Result< u64 > hal::BooleanFunction::to_u64 ( const std::vector< BooleanFunction::Value > &  value)
static

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

Parameters
[in]value- The value as a bit-vector.
Returns
A 64-bit integer representing the values on success, an error otherwise.

Definition at line 222 of file boolean_function.cpp.

References ERR, OK, and to_string().

Referenced by hal::SMT::ConstantPropagation::Add(), hal::boolean_function_init(), hal::solve_fsm::solve_fsm(), hal::solve_fsm::solve_fsm_brute_force(), and hal::SMT::ConstantPropagation::Sub().

◆ to_z3()

z3::expr hal::BooleanFunction::to_z3 ( z3::context &  context,
const std::map< std::string, z3::expr > &  var2expr = {} 
) const
Deprecated:
DEPRECATED
Translates the Boolean function into the z3 expression representation.
Parameters
[in,out]context- Z3 context to generate expressions.
[in]var2expr- Maps input variables to expression.
Returns
Z3 representation of the Boolean function.

Definition at line 1611 of file boolean_function.cpp.

References hal::BooleanFunction::NodeType::And, hal::BooleanFunction::NodeType::Concat, hal::BooleanFunction::NodeType::Constant, hal::BooleanFunction::NodeType::Index, log_error, hal::BooleanFunction::NodeType::Not, hal::BooleanFunction::NodeType::Or, hal::BooleanFunction::NodeType::Sext, hal::BooleanFunction::NodeType::Slice, hal::BooleanFunction::NodeType::Variable, and hal::BooleanFunction::NodeType::Xor.

◆ Udiv()

Result< BooleanFunction > hal::BooleanFunction::Udiv ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation.
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 384 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Udiv.

Referenced by hal::boolean_function_init().

◆ Ule()

Result< BooleanFunction > hal::BooleanFunction::Ule ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation (always =1).
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 596 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Ule.

Referenced by hal::boolean_function_init(), and hal::module_identification::check_leq().

◆ Ult()

Result< BooleanFunction > hal::BooleanFunction::Ult ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation (always =1).
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 607 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Ult.

Referenced by hal::boolean_function_init(), and hal::module_identification::check_leq().

◆ Urem()

Result< BooleanFunction > hal::BooleanFunction::Urem ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation.
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 406 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Urem.

Referenced by hal::boolean_function_init().

◆ Var()

BooleanFunction hal::BooleanFunction::Var ( const std::string &  name,
u16  size = 1 
)
static

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

Parameters
[in]name- The name of the variable.
[in]size- The bit-size. Defaults to 1.
Returns
The Boolean function.

Definition at line 265 of file boolean_function.cpp.

References BooleanFunction(), name, size(), and hal::BooleanFunction::Node::Variable().

Referenced by hal::boolean_function_init(), evaluate(), hal::BooleanFunctionDecorator::get_boolean_function_from(), hal::BooleanFunctionNetDecorator::get_boolean_variable(), hal::module_identification::VerifiedCandidate::get_merged_word_level_operation(), hal::netlist_preprocessing::simplify_lut_inits(), and hal::BooleanFunctionDecorator::substitute_module_pins().

◆ Xor()

Result< BooleanFunction > hal::BooleanFunction::Xor ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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
[in]p0- First Boolean function.
[in]p1- Second Boolean function.
[in]size- Bit-size of the operation.
Returns
Ok() and the joined Boolean function on success, an error otherwise.

Definition at line 329 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Xor.

Referenced by hal::boolean_function_init(), operator^(), and operator^=().

◆ Zext()

Result< BooleanFunction > hal::BooleanFunction::Zext ( BooleanFunction &&  p0,
BooleanFunction &&  p1,
u16  size 
)
static

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

Parameters
[in]p0- Boolean function to extend.
[in]p1- Boolean function of type Index encoding the bit-size of the zero-extended result.
[in]size- Bit-size of the zero-extended Boolean function.
Returns
Ok() and the extended Boolean function on success, an error otherwise.

Definition at line 451 of file boolean_function.cpp.

References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Zext.

Referenced by hal::boolean_function_init(), and hal::BooleanFunctionDecorator::get_boolean_function_from().

Friends And Related Function Documentation

◆ operator<< [1/2]

std::ostream& operator<< ( std::ostream &  os,
const BooleanFunction f 
)
friend

The ostream operator that forwards to_string of a boolean function.

Parameters
[in]os- the stream to write to.
[in]f- the function.
Returns
A reference to os.

Definition at line 629 of file boolean_function.cpp.

◆ operator<< [2/2]

std::ostream& operator<< ( std::ostream &  os,
BooleanFunction::Value  v 
)
friend

Output stream operator that forwards to_string of a value.

Parameters
[in]os- The stream to write to.
[in]v- The value.
Returns
A reference to output stream.

Definition at line 244 of file boolean_function.cpp.

Member Data Documentation

◆ MAX_TRUTH_TABLE_VARIABLES

constexpr u32 hal::BooleanFunction::MAX_TRUTH_TABLE_VARIABLES = 20
staticconstexpr

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
[in]ordered_variables- A vector describing the order of input variables used to generate the truth table. Defaults to an empty vector.
[in]remove_unknown_variables- Set true to remove variables from the truth table that are not present within the Boolean function, false otherwise. Defaults to false.
Returns
Ok() and a vector of values representing the truth table output on success, an error otherwise. The maximum number of variables a truth table may be computed for. Each additional variable doubles the number of rows, so the limit bounds the runtime as well as the size of the result.

Definition at line 872 of file boolean_function.h.

Referenced by compute_truth_table().


The documentation for this class was generated from the following files: