#include </home/runner/work/hal/hal/plugins/z3_utils/include/z3_utils/converter/converter.h>

Inheritance diagram for hal::z3_utils::Converter:

Collaboration diagram for hal::z3_utils::Converter:

Public Types
enum	Operation { bvand , bvnot , bvor , bvxor , NONE }

Public Member Functions
std::string	convert_z3_expr_to_func (const z3::expr &e) const

Protected Member Functions
virtual std::string	build_operand (const std::string &operand) const =0

virtual std::string	build_operation (const Operation &operation, const std::vector< std::string > &operands) const =0

virtual std::string	generate_assignment (const std::string &l) const =0

virtual std::string	generate_initialization (const std::vector< std::string > &input_vars) const =0

virtual std::string	construct_function (const std::string &assignments, const std::string &initalization, const std::vector< std::string > &input_vars) const =0

std::string	integer_with_leading_zeros (const u32 i, const u32 total_length) const

std::string	replace_all (const std::string &str, const std::string &from, const std::string &to) const

std::string	operation_to_string (const Operation &op) const

bool	does_line_contain_assignment (const std::string &l) const

std::string	extract_lhs (const std::string &l) const

std::map< u32, u32 >	extract_paranthesis_pairs (const std::string &l) const

bool	contains_one_operation (const std::string &l) const

std::map< std::string, std::string >	extract_sub_exrepssions (const std::string &l) const

Operation	extract_operation (const std::string &se) const

std::vector< std::string >	extract_operands (const std::string &se) const

std::map< std::string, std::string >	translate_sub_expressions (const std::map< std::string, std::string > &se) const

std::string	merge_sub_expressions (const std::map< std::string, std::string > &translated_sub_expressions) const

std::string	generate_function (const std::vector< std::string > &assignments, std::vector< std::string > &input_vars) const

Protected Attributes
std::vector< Operation >	m_operations = {Converter::bvand, Converter::bvnot, Converter::bvor, Converter::bvxor}

Detailed Description

The base class for the converters that translate a Boolean function given in SMT-LIB notation into another language.

Definition at line 41 of file converter.h.

Member Enumeration Documentation

◆ Operation

enum hal::z3_utils::Converter::Operation

The bit-vector operations that the converters can translate.

Enumerator
bvand	Bitwise AND.
bvnot	Bitwise NOT.
bvor	Bitwise OR.
bvxor	Bitwise XOR.
NONE	No operation, returned when no known operation could be extracted.

Definition at line 47 of file converter.h.

Member Function Documentation

◆ build_operand()

virtual std::string hal::z3_utils::Converter::build_operand ( const std::string & operand ) const

protectedpure virtual

Translate a single operand into the target language.

Parameters

[in] operand - The operand in SMT-LIB notation.

Returns: The operand in the target language.

◆ build_operation()

virtual std::string hal::z3_utils::Converter::build_operation	(	const Operation &	operation,
		const std::vector< std::string > &	operands
	)		const

protectedpure virtual

Translate a single operation and its operands into the target language.

Parameters

[in]	operation	- The operation to translate.
[in]	operands	- The operands of the operation, already translated.

Returns: The operation in the target language.

Referenced by translate_sub_expressions().

◆ construct_function()

virtual std::string hal::z3_utils::Converter::construct_function	(	const std::string &	assignments,
		const std::string &	initalization,
		const std::vector< std::string > &	input_vars
	)		const

protectedpure virtual

Assemble the complete function of the target language from its parts.

Parameters

[in]	assignments	- The translated assignments that make up the body.
[in]	initalization	- The translated initialization code.
[in]	input_vars	- The input variables of the function.

Returns: The complete function in the target language.

Referenced by convert_z3_expr_to_func().

◆ contains_one_operation()

bool hal::z3_utils::Converter::contains_one_operation ( const std::string & l ) const

protected

Check whether the given line consists of exactly one operation, i.e., whether it needs no further splitting.

Parameters

[in] l - The line to check.

Returns: true if the line contains exactly one operation, false otherwise.

Definition at line 122 of file converter.cpp.

References log_debug, m_operations, operation_to_string(), and start_index.

Referenced by extract_sub_exrepssions().

◆ convert_z3_expr_to_func()

std::string hal::z3_utils::Converter::convert_z3_expr_to_func ( const z3::expr & e ) const

This base function prases and splits up the smt representation of a wrapped z3 expression and converts it into another representation depending on the child class that overrides the virtual methods.

Parameters

[in] e - z3 expression that is converted.

Returns: The converted expression as a string.

Definition at line 294 of file converter.cpp.

References construct_function(), does_line_contain_assignment(), generate_assignment(), generate_initialization(), hal::z3_utils::get_variable_names(), log_debug, hal::z3_utils::to_smt2(), and hal::utils::to_vector().

◆ does_line_contain_assignment()

bool hal::z3_utils::Converter::does_line_contain_assignment ( const std::string & l ) const

protected

Check whether the given line of the SMT-LIB representation holds an assignment.

Parameters

[in] l - The line to check.

Returns: true if the line holds an assignment, false otherwise.

Definition at line 70 of file converter.cpp.

Referenced by convert_z3_expr_to_func().

◆ extract_lhs()

std::string hal::z3_utils::Converter::extract_lhs ( const std::string & l ) const

protected

Get the variable that is assigned to in the given line.

Parameters

[in] l - The line holding the assignment.

Returns: The name of the assigned variable.

Definition at line 75 of file converter.cpp.

References start_index.

◆ extract_operands()

std::vector< std::string > hal::z3_utils::Converter::extract_operands ( const std::string & se ) const

protected

Get the operands that the given sub-expression applies its operation to.

Parameters

[in] se - The sub-expression.

Returns: The operands.

Definition at line 235 of file converter.cpp.

Referenced by translate_sub_expressions().

◆ extract_operation()

Converter::Operation hal::z3_utils::Converter::extract_operation ( const std::string & se ) const

protected

Get the operation that the given sub-expression applies.

Parameters

[in] se - The sub-expression.

Returns: The operation, Converter::NONE if no known operation was found.

Definition at line 220 of file converter.cpp.

References log_error, m_operations, NONE, and operation_to_string().

Referenced by translate_sub_expressions().

◆ extract_paranthesis_pairs()

std::map< u32, u32 > hal::z3_utils::Converter::extract_paranthesis_pairs ( const std::string & l ) const

protected

Get the matching parenthesis for every opening parenthesis of the given line.

Parameters

[in] l - The line to analyze.

Returns: A map from the position of each opening parenthesis to the position of its counterpart.

Definition at line 83 of file converter.cpp.

References log_debug, and start_index.

Referenced by extract_sub_exrepssions().

◆ extract_sub_exrepssions()

std::map< std::string, std::string > hal::z3_utils::Converter::extract_sub_exrepssions ( const std::string & l ) const

protected

Split the given line into the sub-expressions that it is composed of.

Parameters

[in] l - The line to split.

Returns: A map from a placeholder to the sub-expression that it stands for.

Definition at line 147 of file converter.cpp.

References contains_one_operation(), extract_paranthesis_pairs(), integer_with_leading_zeros(), log_debug, and replace_all().

◆ generate_assignment()

virtual std::string hal::z3_utils::Converter::generate_assignment ( const std::string & l ) const

protectedpure virtual

Translate a single assignment of the SMT-LIB representation into the target language.

Parameters

[in] l - The line holding the assignment.

Returns: The assignment in the target language.

Referenced by convert_z3_expr_to_func().

◆ generate_function()

std::string hal::z3_utils::Converter::generate_function	(	const std::vector< std::string > &	assignments,
		std::vector< std::string > &	input_vars
	)		const

protected

Translate all assignments into the target language and assemble them into a complete function.

Parameters

[in]	assignments	- The assignments of the SMT-LIB representation.
[in,out]	input_vars	- The input variables of the function, filled by this function.

Returns: The complete function in the target language.

◆ generate_initialization()

virtual std::string hal::z3_utils::Converter::generate_initialization ( const std::vector< std::string > & input_vars ) const

protectedpure virtual

Generate the code that reads the input variables before the translated function is evaluated.

Parameters

[in] input_vars - The input variables of the function.

Returns: The initialization code in the target language.

Referenced by convert_z3_expr_to_func().

◆ integer_with_leading_zeros()

std::string hal::z3_utils::Converter::integer_with_leading_zeros	(	const u32	i,
		const u32	total_length
	)		const

protected

Convert an integer into a string of the given length, padded with leading zeros.

Parameters

[in]	i	- The integer to convert.
[in]	total_length	- The length of the resulting string.

Returns: The padded string.

Definition at line 16 of file converter.cpp.

Referenced by extract_sub_exrepssions().

◆ merge_sub_expressions()

std::string hal::z3_utils::Converter::merge_sub_expressions ( const std::map< std::string, std::string > & translated_sub_expressions ) const

protected

Substitute the translated sub-expressions back into one another to form a single expression.

Parameters

[in] translated_sub_expressions - A map from each placeholder to the translated sub-expression.

Returns: The merged expression.

Definition at line 271 of file converter.cpp.

References replace_all().

◆ operation_to_string()

std::string hal::z3_utils::Converter::operation_to_string ( const Operation & op ) const

protected

Get the SMT-LIB name of an operation.

Parameters

[in] op - The operation.

Returns: The name of the operation.

Definition at line 43 of file converter.cpp.

References bvand, bvnot, bvor, bvxor, and log_error.

Referenced by contains_one_operation(), and extract_operation().

◆ replace_all()

std::string hal::z3_utils::Converter::replace_all	(	const std::string &	str,
		const std::string &	from,
		const std::string &	to
	)		const

protected

Replace every occurrence of a substring within a string.

Parameters

[in]	str	- The string to operate on.
[in]	from	- The substring to replace.
[in]	to	- The replacement.

Returns: The resulting string.

Definition at line 23 of file converter.cpp.

References start_index, and hal::core_strings::to().

Referenced by extract_sub_exrepssions(), and merge_sub_expressions().

◆ translate_sub_expressions()

std::map< std::string, std::string > hal::z3_utils::Converter::translate_sub_expressions ( const std::map< std::string, std::string > & se ) const

protected

Translate every sub-expression into the target language.

Parameters

[in] se - A map from a placeholder to the sub-expression that it stands for.

Returns: A map from each placeholder to the translated sub-expression.

Definition at line 256 of file converter.cpp.

References build_operation(), extract_operands(), and extract_operation().

Member Data Documentation

◆ m_operations

std::vector<Operation> hal::z3_utils::Converter::m_operations = {Converter::bvand, Converter::bvnot, Converter::bvor, Converter::bvxor}

protected

The operations that the converter supports.

Definition at line 224 of file converter.h.

Referenced by contains_one_operation(), and extract_operation().

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

plugins/z3_utils/include/z3_utils/converter/converter.h
plugins/z3_utils/src/converter/converter.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ Operation

Member Function Documentation

◆ build_operand()

◆ build_operation()

◆ construct_function()

◆ contains_one_operation()

◆ convert_z3_expr_to_func()

◆ does_line_contain_assignment()

◆ extract_lhs()

◆ extract_operands()

◆ extract_operation()

◆ extract_paranthesis_pairs()

◆ extract_sub_exrepssions()

◆ generate_assignment()

◆ generate_function()

◆ generate_initialization()

◆ integer_with_leading_zeros()

◆ merge_sub_expressions()

◆ operation_to_string()

◆ replace_all()

◆ translate_sub_expressions()

Member Data Documentation

◆ m_operations