z3_utils.cpp File Reference

#include "z3_utils/z3_utils.h"
#include "hal_core/netlist/decorators/boolean_function_net_decorator.h"
#include "hal_core/utilities/log.h"
#include "z3_api.h"
#include "z3_utils/converter/cpp_converter.h"
#include "z3_utils/converter/verilog_converter.h"
#include <sstream>

Include dependency graph for z3_utils.cpp:

Go to the source code of this file.

Namespaces
	hal
	hal::z3_utils

Functions
z3::expr	hal::z3_utils::from_bf (const BooleanFunction &bf, z3::context &ctx, const std::map< std::string, z3::expr > &var2expr={})
Result< z3::expr >	hal::z3_utils::value_from_binary_string (z3::context &ctx, const std::string &bit_string)
Result< BooleanFunction >	hal::z3_utils::to_bf (const z3::expr &e)
std::string	hal::z3_utils::to_smt2 (const z3::expr &e)
std::string	hal::z3_utils::to_cpp (const z3::expr &e)
std::string	hal::z3_utils::to_verilog (const z3::expr &e, const std::map< std::string, bool > &control_mapping={})
	Translates a z3 expression into a verilog network representation. More...
std::set< std::string >	hal::z3_utils::get_variable_names (const z3::expr &e)
	Extracts all variable names from a z3 expression. More...
std::set< u32 >	hal::z3_utils::extract_net_ids (const z3::expr &e)
	Extracts all net IDs from the variables of a z3 expression. More...
std::set< u32 >	hal::z3_utils::extract_net_ids (const std::set< std::string > &variable_names)
	Extracts all net IDs from a set of variables. More...
z3::expr	hal::z3_utils::get_expr_in_ctx (const z3::expr &e, z3::context &ctx)
	Translates the expr to another context. More...