sequential_symbolic_execution.h File Reference

This file contains the declarations for functions to perform sequential symbolic execution using z3. More...

#include "hal_core/netlist/boolean_function.h"
#include "hal_core/utilities/result.h"
#include "z3_utils/z3_utils.h"
#include <map>
#include <vector>

Include dependency graph for sequential_symbolic_execution.h:

Go to the source code of this file.

Namespaces
	hal
	hal::sse

Functions
Result< z3::expr >	hal::sse::get_value_at_z3 (Net *net, const u32 time_index, const std::vector< bool > &subgraph_gates_byte_map, const std::vector< std::map< u32, bool >> &known_inputs, const std::map< PinGroup< ModulePin > *, BooleanFunction > &word_level_calculations, const bool substitute_endpoints, z3::context &ctx)
	Get the Z3 expression representing the value of a net at a specific time index. More...
Result< std::vector< z3::expr > >	hal::sse::get_word_values_at_z3 (const std::vector< std::vector< Net * >> &words, const std::vector< u32 > &time_indices, const std::vector< bool > &subgraph_gates_byte_map, const std::vector< std::map< u32, bool >> &known_inputs, const std::map< PinGroup< ModulePin > *, BooleanFunction > &word_level_calculations, const bool substitute_endpoints, z3::context &ctx)
	Get the Z3 expressions representing the values of multiple nets as words at specific time indices. More...
Result< std::vector< z3::expr > >	hal::sse::get_word_values_at_z3 (const std::vector< std::pair< Module *, PinGroup< ModulePin > * >> &words, const std::vector< u32 > &time_indices, const std::vector< bool > &subgraph_gates_byte_map, const std::vector< std::map< u32, bool >> &known_inputs, const std::map< PinGroup< ModulePin > *, BooleanFunction > &word_level_calculations, const bool substitute_endpoints, z3::context &ctx)
	Get the Z3 expressions representing the values of pin groups as words at specific time indices. More...

Detailed Description

This file contains the declarations for functions to perform sequential symbolic execution using z3.

Definition in file sequential_symbolic_execution.h.