to parse an smt file this will only work on the yosys's generated smt and not on the assembled CHC More...

Public Types
typedef std::map< std::string, state_var_t * >	variable_idx_t

Public Member Functions
	YosysSmtParser (const std::string &buf)

void	BreakDatatypes ()
	Process (replace and add)

void	AddNoChangeStateUpdateFunction ()
	Add the no change function.

std::string	Export ()
	Export to string.

const smt_file &	GetRawSmtAst () const
	Get the unflattened datatype.

const std::vector< std::string > &	get_module_def_orders () const
	return a reference to module def order

const std::vector< state_var_t > &	get_module_flatten_dt (const std::string &mod_name) const
	return a module's flatten datatypes

const variable_idx_t &	get_var_idx () const
	return the top module's variable index

bool	is_state_name (const std::string &state_name) const
	check if a name is a state

Static Public Member Functions
static void	convert_flatten_datatype_to_arg_vec (const std::vector< state_var_t > &, std::vector< arg_t > &, const std::string &suffix)
	convert a flatten_datatype to function arg

static void	convert_datatype_to_type_vec (const std::vector< state_var_t > &all_flattened_state_var, std::vector< var_type > &args)
	convert a flatten_datatype to function type decl

static std::string	st_name_add_suffix (const std::string &stname, const std::string &suffix)
	add a suffix (for next state)

static std::string	st_name_add_prefix (const std::string &stname, const std::string &prefix)
	add a prefix (for state name)

static std::vector< std::string >	str_to_list (const std::string &in)
	extract list from a space seped text

Protected Member Functions
void	construct_flatten_dataype ()
	construct flatten_datatype (hierarchically)

void	replace_all_function_arg_body ()
	replace function body and argument

void	add_no_change_function ()
	add the no-change-function (hierarchically)

void	create_variable_idx ()
	create the variable indices

std::string	replace_a_body (const std::string &current_module, const std::map< std::string, state_var_t > &current_mod_state_var_idx, const std::vector< std::string > &arg_def, const std::set< std::string > &defined_func, const std::string &body_text)
	replace : handle a func_body

void	replace_a_func (std::shared_ptr< func_def_t > fn, const std::string &current_module, const std::map< std::string, state_var_t > &current_mod_state_var_idx, const std::set< std::string > &defined_func)
	replace : handle a func (arg) and invoke the body repl part

Protected Attributes
smt_file	smt_ast
	the internal smt-ast

datatypes_t	flatten_datatype
	the datatype defs without datatypes

variable_idx_t	variable_idx
	the variable indices — only top level

Detailed Description

to parse an smt file this will only work on the yosys's generated smt and not on the assembled CHC

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

Public Types