the class for parsing invariant More...

#include <chc_inv_in.h>

Inheritance diagram for ilang::smt::SmtlibInvariantParser:

Public Types
typedef std::function < std::string(const std::string &)>	verilog_internal_name_lookup_fn_t
	a function to map state name (internal name reference to verilog signal)

typedef std::map< std::string, SmtTermInfoVerilog >	term_container_t
	the type of container to hold the terms

typedef std::map< std::string, SmtTermInfoVerilog >	quantifier_temp_def_t
	then we need stack for forall infos

typedef std::vector < quantifier_temp_def_t >	quantifier_def_stack_t
	and the stack

typedef std::map< std::string, var_type >	sort_container_t
	the sort container

typedef std::map< std::string, SmtTermInfoVerilog >	local_vars_t
	the container of temporary variables

typedef std::map< std::string, std::string >	local_vars_lookup_t
	search_string to local var name

typedef std::map< std::string, int >	free_vars_t
	the container of all the free variables

Public Member Functions
	SmtlibInvariantParser (YosysSmtParser *yosys_smt_info, bool _flatten_datatype, bool _flatten_hierarchy, const std::set< std::string > &_inv_pred_name, const std::string &dut_instance_name, bool discourageOutOfScopeVariable=true)

	SmtlibInvariantParser (const SmtlibInvariantParser &)=delete
	no copy constructor

SmtlibInvariantParser &	operator= (const SmtlibInvariantParser &)=delete
	no assignment

virtual bool	ParseInvResultFromFile (const std::string &fname) override

virtual void	ParseSmtResultFromString (const std::string &text) override

std::string	GetFinalTranslateResult () const override
	get the translate result

const local_vars_t &	GetLocalVarDefs () const
	get the local variable definitions

const free_vars_t &	GetFreeVarDefs () const
	get the free variable definitions

bool	in_bad_state (void) const
	check if this module is in a bad state

virtual SmtTermInfoVlgPtr	push_quantifier_scope ()
	call back function to handle (forall

virtual SmtTermInfoVlgPtr	pop_quantifier_scope ()
	call back function to handle ) of forall

virtual void	declare_function (const std::string &name, var_type *sort)
	declare function (useful for Grain)

virtual var_type *	make_sort (const std::string &name, const std::vector< int > &)
	call back function to create a sort

virtual void	declare_quantified_variable (const std::string &name, var_type *sort)
	call back function to create a temporary (quantified variable)

virtual SmtTermInfoVlgPtr	mk_function (const std::string &name, var_type *sort, const std::vector< int > &idx, const std::vector< SmtTermInfoVlgPtr > &args)

virtual SmtTermInfoVlgPtr	mk_number (const std::string &rep, int width, int base)
	call back function to make a number term

virtual SmtTermInfoVlgPtr	search_quantified_var_stack (const std::string &name)
	find if a certain var is a quantified variable

virtual void	assert_formula (SmtTermInfoVlgPtr result)
	this function receives the final assert result

virtual void	define_function (const std::string &func_name, const std::vector< SmtTermInfoVlgPtr > &args, var_type *ret_type, SmtTermInfoVlgPtr func_body)
	this function receives the final result

	DECLARE_OPERATOR (true)

	DECLARE_OPERATOR (false)

	DECLARE_OPERATOR (and)

	DECLARE_OPERATOR (or)

	DECLARE_OPERATOR (not)

	DECLARE_OPERATOR (implies)

	DECLARE_OPERATOR (eq)

	DECLARE_OPERATOR (ite)

	DECLARE_OPERATOR (xor)

	DECLARE_OPERATOR (nand)

	DECLARE_OPERATOR (concat)

	DECLARE_OPERATOR (bvnot)

	DECLARE_OPERATOR (bvand)

	DECLARE_OPERATOR (bvnand)

	DECLARE_OPERATOR (bvor)

	DECLARE_OPERATOR (bvnor)

	DECLARE_OPERATOR (bvxor)

	DECLARE_OPERATOR (bvxnor)

	DECLARE_OPERATOR (bvult)

	DECLARE_OPERATOR (bvslt)

	DECLARE_OPERATOR (bvule)

	DECLARE_OPERATOR (bvsle)

	DECLARE_OPERATOR (bvugt)

	DECLARE_OPERATOR (bvsgt)

	DECLARE_OPERATOR (bvuge)

	DECLARE_OPERATOR (bvsge)

	DECLARE_OPERATOR (bvcomp)

	DECLARE_OPERATOR (bvneg)

	DECLARE_OPERATOR (bvadd)

	DECLARE_OPERATOR (bvsub)

	DECLARE_OPERATOR (bvmul)

	DECLARE_OPERATOR (bvudiv)

	DECLARE_OPERATOR (bvsdiv)

	DECLARE_OPERATOR (bvsmod)

	DECLARE_OPERATOR (bvurem)

	DECLARE_OPERATOR (bvsrem)

	DECLARE_OPERATOR (bvshl)

	DECLARE_OPERATOR (bvlshr)

	DECLARE_OPERATOR (bvashr)

	DECLARE_OPERATOR (extract)

	DECLARE_OPERATOR (bit2bool)

	DECLARE_OPERATOR (repeat)

	DECLARE_OPERATOR (zero_extend)

	DECLARE_OPERATOR (sign_extend)

	DECLARE_OPERATOR (rotate_left)

	DECLARE_OPERATOR (rotate_right)

Public Member Functions inherited from ilang::smt::SmtlibInvariantParserBase
	SmtlibInvariantParserBase (const SmtlibInvariantParserBase &)=delete
	no copy constructor

SmtlibInvariantParserBase &	operator= (const SmtlibInvariantParserBase &)=delete
	no assignment

std::string	GetRawSmtString () const
	get the local variable definitions More...

Protected Member Functions
bool	bad_state_return (void)
	If it is bad state, return true and display a message.

Protected Attributes
smtlib2_abstract_parser_wrapper *	parser_wrapper
	the parser interface

term_container_t	term_container
	the term container

sort_container_t	sort_container
	we will allocate in this container

quantifier_def_stack_t	quantifier_def_stack
	the temporary def stacks

unsigned	mask
	sentry – probably no use

const std::set< std::string >	inv_pred_name
	a collection of functions that should be treated as inv predicates

std::vector< unsigned >	quantifier_var_def_idx_stack
	the quantifier declare index (order)

local_vars_t	local_vars
	to hold the local variables

local_vars_lookup_t	local_vars_lookup
	to hold map for search string -> local variables

free_vars_t	free_vars
	to hold the free variables

std::string	final_translate_result
	the final translated result

const std::string	dut_verilog_instance_name
	we need to store the right vlog instance name

YosysSmtParser *	design_smt_info_ptr
	a pointer to get the knowlege of the context

const bool	datatype_flattened
	whether we are on a design w. datatype flattened

const bool	hierarchy_flattened
	whether we are on a design w. hierarchy flattened

const bool	no_outside_var_refer
	discourage out-of-scope variable referall

bool	_bad_state
	bad state

Protected Attributes inherited from ilang::smt::SmtlibInvariantParserBase
std::string	raw_string

Additional Inherited Members
Static Public Member Functions inherited from ilang::smt::SmtlibInvariantParserBase
static void	set_new_local_ctr (unsigned cnt)
	set the counter to a new val when loading

static void	parse_local_var_name_to_set_counter (const std::string &name)
	parse the names to set the new counters

static unsigned	get_local_ctr ()
	to check the value of this counter

Static Protected Member Functions inherited from ilang::smt::SmtlibInvariantParserBase
static std::string	get_a_new_local_var_name ()
	a counter to get local variable name

Static Protected Attributes inherited from ilang::smt::SmtlibInvariantParserBase
static unsigned	local_var_idx
	the idx to it

Detailed Description

the class for parsing invariant

Member Function Documentation

virtual SmtTermInfoVlgPtr ilang::smt::SmtlibInvariantParser::mk_function	(	const std::string &	name,
		var_type *	sort,
		const std::vector< int > &	idx,
		const std::vector< SmtTermInfoVlgPtr > &	args
	)

virtual

call back function to apply an uninterpreted function fall-through case if it is not an defined op, if failed, return NULL

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

chc_inv_in.h

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Function Documentation