the invariant object, it needs smt-info to parse More...

#include <inv_obj.h>

Public Types
typedef std::vector< std::string >	inv_vec_t
	the vector of multiple invariants

typedef std::vector < std::tuple< std::string, std::string, int > >	extra_var_def_vec_t
	the vector of extra_var defs exprs

typedef std::map< std::string, int >	extra_free_var_def_vec_t
	the vector of free var defs exprs

typedef std::vector< std::string >	smt_formula_vec_t
	the vector of original smt-formula for datapoint attempt

Public Member Functions
	InvariantObject ()
	empty invariants

void	AddInvariantFromVerilogExpr (const std::string &tag, const std::string &vlg_in)
	copy constructor = default More...

const inv_vec_t &	GetVlgConstraints () const
	generate invariants

const extra_var_def_vec_t &	GetExtraVarDefs () const
	get the vars

const extra_free_var_def_vec_t &	GetExtraFreeVarDefs () const
	get the free vars

const smt_formula_vec_t &	GetSmtFormulae () const
	get the smt formula

void	set_dut_inst_name (const std::string &name)
	called by the target generator?

void	ClearAllInvariants ()
	clear all stored invariants

void	ExportToFile (const std::string &fn, bool export_smt_encoding=true) const
	export invariants to a file

void	ImportFromFile (const std::string &fn)
	import invariants that has been previous exported

void	InsertFromAnotherInvObj (const InvariantObject &r)
	this is to support making candidate invariant as confirmed

size_t	NumInvariant () const
	the number of invariants

void	RemoveInvByIdx (size_t idx)
	remove an invariant by its index

Protected Attributes
std::vector< std::string >	inv_vlg_exprs
	the expressions

extra_var_def_vec_t	inv_extra_vlg_vars
	the extra variables that are needed to ...

extra_free_var_def_vec_t	inv_extra_free_vars
	the extra free variables // there might be repetition // check it

smt_formula_vec_t	smt_formula_vec
	the original smt formula

std::string	dut_inst_name
	the buffered dut instance name

Detailed Description

the invariant object, it needs smt-info to parse

Member Function Documentation

void ilang::InvariantObject::AddInvariantFromVerilogExpr	(	const std::string &	tag,
		const std::string &	vlg_in
	)

copy constructor = default

add invariants from verilog-like output

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