#include <bitblast_conv.h>

Inheritance diagram for bitblast_convt:

Public Types
enum	shiftt { LEFT , LRIGHT , ARIGHT }
Public Types inherited from smt_solver_baset
typedef std::vector< smt_astt >	ast_vec
	Shorthand for a vector of smt_ast's.
typedef boost::multi_index_container< smt_cache_entryt, boost::multi_index::indexed_by< boost::multi_index::hashed_unique< BOOST_MULTI_INDEX_MEMBER(smt_cache_entryt, const expr2tc, val)>, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(smt_cache_entryt, unsigned int, level), std::greater< unsigned int > > > >	smt_cachet
typedef std::unordered_map< type2tc, smt_sortt, type2_hash >	smt_sort_cachet
typedef std::map< std::string, smt_astt >	renumber_mapt

Public Member Functions
	bitblast_convt (bool int_encoding, const namespacet &_ns, sat_iface *sat_api)
	~bitblast_convt ()
virtual smt_astt	mk_func_app (const smt_sort ressort, smt_func_kind f, const smt_ast const *args, unsigned int num)
virtual smt_sort *	mk_sort (smt_sort_kind k,...)
virtual smt_ast *	mk_smt_int (const BigInt &intval)
	Create an integer smt_ast.
virtual smt_ast *	mk_smt_real (const std::string &value)
	Create a real in a smt_ast.
virtual smt_ast *	mk_smt_bvint (const BigInt &inval, bool sign, unsigned int w)
virtual smt_ast *	mk_smt_bool (bool boolval)
	Create a boolean.
virtual smt_astt	mk_smt_symbol (const std::string &name, const smt_sort *sort)
virtual smt_sort *	mk_struct_sort (const type2tc &t)
virtual smt_ast *	mk_extract (const smt_ast src, unsigned int high, unsigned int low, const smt_sort s)
virtual tvt	l_get (const smt_ast *a)
virtual void	assert_ast (const smt_ast *a)
expr2tc	get_bool (const smt_ast *a)
expr2tc	get_bv (const type2tc &t, const smt_ast *a)
bool	process_clause (const bvt &bv, bvt &dest)
bitblast_smt_ast *	mk_ast_equality (const smt_ast a, const smt_ast b, const smt_sort *ressort)
virtual literalt	land (const bvt &bv)
virtual literalt	lor (const bvt &bv)
void	eliminate_duplicates (const bvt &bv, bvt &dest)
void	bvand (const bvt &bv0, const bvt &bv1, bvt &output)
void	bvor (const bvt &bv0, const bvt &bv1, bvt &output)
void	bvxor (const bvt &bv0, const bvt &bv1, bvt &output)
void	bvnot (const bvt &bv0, bvt &output)
void	full_adder (const bvt &op0, const bvt &op1, bvt &output, literalt carry_in, literalt &carry_out)
literalt	carry (literalt a, literalt b, literalt c)
literalt	carry_out (const bvt &a, const bvt &b, literalt c)
literalt	equal (const bvt &op0, const bvt &op1)
literalt	lt_or_le (bool or_equal, const bvt &bv0, const bvt &bv1, bool is_signed)
void	invert (bvt &bv)
void	barrel_shift (const bvt &op, const shiftt s, const bvt &dist, bvt &out)
void	shift (const bvt &inp, const shiftt &s, unsigned long d, bvt &out)
literalt	unsigned_less_than (const bvt &arg0, const bvt &arg1)
void	unsigned_multiplier (const bvt &op0, const bvt &bv1, bvt &output)
void	signed_multiplier (const bvt &op0, const bvt &bv1, bvt &output)
void	cond_negate (const bvt &vals, bvt &out, literalt cond)
void	negate (const bvt &inp, bvt &oup)
void	incrementer (const bvt &inp, const literalt &carryin, literalt carryout, bvt &oup)
void	signed_divider (const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
void	unsigned_divider (const bvt &op0, const bvt &op1, bvt &res, bvt &rem)
void	unsigned_multiplier_no_overflow (const bvt &op0, const bvt &op1, bvt &r)
void	adder_no_overflow (const bvt &op0, const bvt &op1, bvt &res, bool subtract, bool is_signed)
void	adder_no_overflow (const bvt &op0, const bvt &op1, bvt &res)
bool	is_constant (const bvt &bv)
bitblast_smt_ast *	new_ast (smt_sortt ressort)
Public Member Functions inherited from smt_solver_baset
template<typename the_solver_ast>
smt_astt	new_solver_ast (typename the_solver_ast::solver_ast_type ast, smt_sortt sort)
	smt_solver_baset (const namespacet &_ns, const optionst &_options)
	Primary constructor.
virtual	~smt_solver_baset ()
void	smt_post_init ()
	Post-constructor setup method.
void	record_flattened_pointer (smt_astt address, smt_astt pointer)
void	begin_step (const expr2tc &guard, const expr2tc &cond)
void	note_assignment (const expr2tc &lhs, const expr2tc &rhs)
void	end_step ()
virtual void	push_ctx ()
	Push one context on the SMT assertion stack.
virtual void	pop_ctx ()
	Pop one context on the SMT assertion stack.
virtual bool	has_model () const
	Whether a satisfiable result can be turned into a model.
smt_astt	convert_ast (const expr2tc &expr)
	Main interface to SMT conversion.
smt_astt	convert_ast_node (const expr2tc &expr)
	Convert a single node, assuming its operands are already in the cache.
smt_astt	convert_ieee_arith_2op (const expr2tc &expr)
	Convert one of the two-operand IEEE arithmetic nodes (add/sub/mul/div/ rem), which share an operand layout and differ only in the solver call they end up in.
smt_astt	convert_ast (const expr2tc &expr, const type2tc &type, smt_astt const *args, struct expr_op_convert ops)
	Interface to specifig SMT conversion.
smt_astt	convert_assign (const expr2tc &expr)
void	define (const expr2tc &expr)
	Bind the symbol on the left of an equality to its right-hand side without asserting anything: later conversions of the symbol yield the right-hand side, so only definitions something asserted depends on reach the solver.
void	dump_expr (const expr2tc &expr)
	Convert `expr` and dump the resulting SMT AST in SMT format.
smt_astt	make_n_ary_and (const ast_vec &v)
smt_astt	make_n_ary_or (const ast_vec &v)
smt_astt	invert_ast (smt_astt a)
	Create the inverse of an smt_ast.
smt_astt	imply_ast (smt_astt a, smt_astt b)
	Create an ipmlication between two smt_ast's.
virtual void	assert_ast (smt_astt a)=0
	Assert the truth of an ast.
virtual smt_resultt	dec_solve ()=0
	Solve the formula given to the solver.
virtual smt_resultt	dec_solve_assuming (const ast_vec &assumptions)
	Solve with each boolean ast in `assumptions` held true for this query only.
virtual bool	supports_assumptions () const
void	pre_solve ()
virtual expr2tc	get_by_type (const expr2tc &expr)
	Get the satisfying assignment using the type.
virtual expr2tc	get_by_ast (const type2tc &type, smt_astt a)
	Get the satisfying assignment using the ast.
expr2tc	get_by_ast (const expr2tc &expr)
	Resolve `expr's` model value through its converted AST.
expr2tc	get_by_value (const type2tc &type, BigInt value)
	Builds the bitvector based on the value retrieved from the solver.
virtual bool	get_rational (smt_astt a, BigInt &numerator, BigInt &denominator)
	Extract the assignment to a rational/real value from the SMT solvers model.
std::optional< expr2tc >	get_index_value (const expr2tc &expr, expr2tc &res)
	Fetch a satisfying assignment from the solver.
std::optional< expr2tc >	get_index (const expr2tc &expr, expr2tc &res)
	get_index_value(), returning the element it read from the model, if any, rather than leaving it in `res` for get()'s generic tail.
virtual expr2tc	get (const expr2tc &expr)
virtual const std::string	solver_text ()=0
	Solver name fetcher.
virtual tvt	l_get (smt_astt a)
	Fetch the value of a boolean sorted smt_ast.
tvt	l_get (const expr2tc &expr)
	Fetch the value of a boolean expression from the current model.
virtual smt_astt	mk_add (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvadd (smt_astt a, smt_astt b)
virtual smt_astt	mk_sub (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvsub (smt_astt a, smt_astt b)
virtual smt_astt	mk_mul (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvmul (smt_astt a, smt_astt b)
virtual smt_astt	mk_mod (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvsmod (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvumod (smt_astt a, smt_astt b)
virtual smt_astt	mk_div (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvsdiv (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvudiv (smt_astt a, smt_astt b)
virtual smt_astt	mk_shl (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvshl (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvashr (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvlshr (smt_astt a, smt_astt b)
virtual smt_astt	mk_neg (smt_astt a)
virtual smt_astt	mk_bvneg (smt_astt a)
virtual smt_astt	mk_bvnot (smt_astt a)
virtual smt_astt	mk_bvxor (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvor (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvand (smt_astt a, smt_astt b)
virtual smt_astt	mk_implies (smt_astt a, smt_astt b)
virtual smt_astt	mk_xor (smt_astt a, smt_astt b)
virtual smt_astt	mk_or (smt_astt a, smt_astt b)
virtual smt_astt	mk_and (smt_astt a, smt_astt b)
virtual smt_astt	mk_not (smt_astt a)
virtual smt_astt	mk_lt (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvult (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvslt (smt_astt a, smt_astt b)
virtual smt_astt	mk_gt (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvugt (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvsgt (smt_astt a, smt_astt b)
virtual smt_astt	mk_le (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvule (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvsle (smt_astt a, smt_astt b)
virtual smt_astt	mk_ge (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvuge (smt_astt a, smt_astt b)
virtual smt_astt	mk_bvsge (smt_astt a, smt_astt b)
virtual smt_astt	mk_eq (smt_astt a, smt_astt b)
virtual smt_astt	mk_neq (smt_astt a, smt_astt b)
virtual smt_astt	mk_store (smt_astt a, smt_astt b, smt_astt c)
virtual smt_astt	mk_select (smt_astt a, smt_astt b)
virtual smt_astt	mk_real2int (smt_astt a)
virtual smt_astt	mk_int2real (smt_astt a)
virtual smt_astt	mk_isint (smt_astt a)
virtual smt_astt	mk_quantifier (bool is_forall, std::vector< smt_astt > lhs, smt_astt rhs)
smt_astt	convert_concat_int_mode (smt_astt left_ast, smt_astt right_ast, const expr2tc &expr)
smt_sortt	mk_int_bv_sort (std::size_t width)
	Create an integer or SBV/UBV sort.
smt_sortt	mk_real_fp_sort (std::size_t ew, std::size_t sw)
	Create an real or floating-point/fixed-point sort.
virtual smt_sortt	mk_bool_sort ()
	Create a bool sort.
virtual smt_sortt	mk_real_sort ()
	Create a real sort.
virtual smt_sortt	mk_int_sort ()
	Create a int sort.
virtual smt_sortt	mk_bv_sort (std::size_t width)
	Create a bv sort.
virtual smt_sortt	mk_fbv_sort (std::size_t width)
	Create a fixed-point sort.
virtual smt_sortt	mk_bvfp_sort (std::size_t ew, std::size_t sw)
	Create a floating-point sort, using bitvectors.
virtual smt_sortt	mk_bvfp_rm_sort ()
	Create a floating-point rounding mode sort, using bitvectors.
virtual smt_sortt	mk_array_sort (smt_sortt domain, smt_sortt range)
	Create an array sort.
smt_astt	get_zero_real ()
smt_astt	get_double_min_normal ()
smt_astt	get_double_min_subnormal ()
smt_astt	get_double_max_normal ()
smt_astt	get_single_min_normal ()
smt_astt	get_single_min_subnormal ()
smt_astt	get_single_max_normal ()
smt_astt	mk_subnormal_flush (smt_astt r, const floatbv_type2t &fbv_type, const expr2tc &rounding_mode)
smt_astt	get_double_inf_sentinel ()
smt_astt	get_single_inf_sentinel ()
smt_astt	get_double_eps_rel ()
smt_astt	get_single_eps_rel ()
smt_astt	get_double_eps_up ()
smt_astt	get_single_eps_up ()
virtual smt_astt	mk_smt_bv (const BigInt &theint, std::size_t w)
	Create a bitvector.
virtual smt_astt	mk_smt_bv (const BigInt &theint, smt_sortt s)=0
	Create a bitvector.
virtual smt_astt	mk_smt_symbol (const std::string &name, smt_sortt s)=0
	Create a symbol / variable.
virtual smt_astt	mk_smt_uninterpreted_function (const std::string &name, const std::vector< smt_astt > &args, smt_sortt rangesort)
	Apply an uninterpreted function.
virtual smt_astt	mk_extract (smt_astt a, unsigned int high, unsigned int low)=0
	Create an 'extract' func app.
virtual smt_astt	mk_sign_ext (smt_astt a, unsigned int topwidth)=0
	Given a signed, upwards cast, extends the sign of the given AST to the desired length.
virtual smt_astt	mk_zero_ext (smt_astt a, unsigned int topwidth)=0
	Identical to mk_sign_ext, but extends AST with zeros.
virtual smt_astt	mk_concat (smt_astt a, smt_astt b)=0
	Concatenate two smt expressions.
virtual smt_astt	mk_ite (smt_astt cond, smt_astt t, smt_astt f)=0
	Create an ite operation.
virtual tvt	get_bool (smt_astt a)=0
	Extract the assignment to a boolean variable from the SMT solver's model.
virtual BigInt	get_bv (smt_astt a, bool is_signed)=0
	Extract the assignment to a bitvector from the SMT solver's model.
smt_astt	mk_bvredor (smt_astt op)
	Reduction or: equals bit0 iff all bits are 0.
smt_astt	mk_bvredand (smt_astt op)
	Reduction and: equals bit1 iff all bits are 1.
virtual smt_astt	overflow_arith (const expr2tc &expr)
	Detect integer arithmetic overflows.
virtual smt_astt	overflow_cast (const expr2tc &expr)
	Detect integer overflows in a cast.
virtual smt_astt	overflow_neg (const expr2tc &expr)
	Detects integer overflows in negation.
virtual smt_astt	apply_ieee754_semantics (smt_astt real_result, const floatbv_type2t &fbv_type, smt_astt operand_zero_check=nullptr, const expr2tc &rounding_mode=expr2tc())
	Applies IEEE 754 floating-point semantics to a real arithmetic result.
virtual std::string	dump_smt ()
	Method to dump the SMT formula.
virtual void	print_model ()
	Method to print the SMT model.
virtual smt_astt	convert_array_index (const expr2tc &expr)
	High level index expression conversion.
virtual smt_astt	convert_array_store (const expr2tc &expr)
	Partner method to convert_array_index, for stores.
virtual smt_astt	mk_fresh (smt_sortt s, const std::string &tag, smt_sortt st=nullptr)
	Create a free variable with the given sort, and a unique name, with the prefix given in 'tag'.
std::string	mk_fresh_name (const std::string &tag)
	Create a previously un-used variable name with the prefix given in tag.
void	renumber_symbol_address (const expr2tc &guard, const expr2tc &addr_symbol, const expr2tc &new_size)
smt_sortt	convert_sort (const type2tc &type)
	Convert a type2tc into an smt_sort.
smt_astt	convert_terminal (const expr2tc &expr)
	Convert a terminal expression into an SMT AST.
smt_astt	convert_pointer_arith (const expr2tc &expr, const type2tc &t)
	Flatten pointer arithmetic.
smt_astt	divide_by_element_size (const expr2tc &diff, const expr2tc &size)
	The quotient of a signed byte difference by an element size, truncated toward zero.
smt_astt	convert_ptr_cmp (const expr2tc &expr, const expr2tc &expr2, const expr2tc &templ_expr)
	Compare two pointers.
smt_astt	convert_addr_of (const expr2tc &expr)
	Take the address of some kind of expression.
smt_astt	convert_member (const expr2tc &expr)
	Handle union/struct based corner cases for member2tc expressions.
smt_astt	convert_identifier_pointer (const expr2tc &expr, const std::string &sym, const typet *type)
	Convert an identifier to a pointer.
smt_astt	init_pointer_obj (unsigned int obj_num, const expr2tc &size, const typet *type, bool may_be_freed)
smt_astt	convert_is_nan (const expr2tc &expr)
	Checks for equality with NaN representation.
smt_astt	convert_is_inf (const expr2tc &expr)
	Checks for equality with inf representation.
smt_astt	convert_is_normal (const expr2tc &expr)
	Checks for equality with normal representation.
smt_astt	convert_is_finite (const expr2tc &expr)
	Checks for equality with finite representation.
smt_astt	convert_signbit (const expr2tc &expr)
	Converts signbit representation.
smt_astt	convert_popcount (const expr2tc &expr)
	Converts popcount representation.
smt_astt	convert_bswap (const expr2tc &expr)
	Converts bswap representation.
smt_astt	convert_rounding_mode (const expr2tc &expr)
	Converts rounding mode for ieee fp operations.
smt_astt	convert_byte_extract (const expr2tc &expr)
	Convert a byte_extract2tc, pulling a byte from the byte representation of some piece of data.
smt_astt	convert_byte_extract_int_mode (const byte_extract2t &data, expr2tc source, expr2tc offs, unsigned int src_width)
smt_astt	convert_byte_extract_bv_mode (const byte_extract2t &data, expr2tc source, expr2tc offs, unsigned int src_width)
expr2tc	create_int_right_shift (expr2tc source, expr2tc shift_amount)
smt_astt	convert_byte_update (const expr2tc &expr)
	Convert a byte_update2tc, inserting a byte into the byte representation of some piece of data.
smt_astt	convert_byte_update_int_mode (const byte_update2t &data)
	Convert a byte_update2tc in integer arithmetic mode, handling both constant and non-constant offsets with proper type preservation.
expr2tc	convert_byte_update_int_mode_expr (const byte_update2t &data, expr2tc source, expr2tc offs, expr2tc update_value, unsigned int src_width)
	Convert a byte_update2tc with offset in integer mode, using conditional expressions for all possible byte positions.
smt_astt	convert_byte_update_bv_mode (const byte_update2t &data)
	Convert a byte_update2tc using bitvector operations, preserving the original bitvector-based implementation.
smt_astt	convert_bitcast (const expr2tc &expr)
	Convert a bitcast2tc, converting an expr to its bit representation.
smt_astt	convert_pointer_bitcast (const expr2tc &from, const type2tc &to_type)
	The pointer, floating-point and struct legs of convert_bitcast, split out so the dispatcher stays readable.
smt_astt	convert_bitcast_to_fp (const expr2tc &from, const type2tc &to_type)
	Read a floating-point value from the bits of `from`.
smt_astt	convert_bitcast_to_struct (const expr2tc &from, const type2tc &to_type)
	Rebuild a struct from the bits of `from`, member by member.
smt_astt	encode_pointer_repr (const expr2tc &ptr, const type2tc &to_type)
	Flatten a pointer to the machine representation a bitcast reinterprets, and rebuild it from one; see the comment on the definitions in smt_bitcast.cpp.
smt_astt	decode_pointer_repr (const expr2tc &repr, const type2tc &to_type)
bool	pointer_repr_applies (const type2tc &ptr_type, const type2tc &bv_type)
	True when `ptr_type's` representation occupies `bv_type` exactly, so the bits read back are the bits that were written.
void	assert_expr (const expr2tc &e)
	Convert the given expr to AST, then assert that AST.
void	note_division_operands (const expr2tc &expr, std::unordered_set< const expr2t * > &seen)
	Record every division's operand pair in `expr`, recursively.
smt_astt	convert_modulus (const modulus2t &m, smt_astt a, smt_astt b)
	Encode a remainder: compositional via the matching division when one exists in the formula, the solver's rem primitive otherwise.
smt_astt	mk_truncated_div (const type2tc &type, smt_astt a, smt_astt b)
	C's / and % of signed `type` on Int-sorted operands, from the solver's Euclidean div/mod (#8662).
smt_astt	mk_truncated_rem (const type2tc &type, smt_astt a, smt_astt b)
smt_astt	array_create (const expr2tc &expr)
	Convert constant_array2tc's and constant_array_of2tc's.
void	init_addr_space_array ()
	Initialize tracking data for the address space records.
void	set_tuple_iface (tuple_iface *iface)
	Stores handle for the tuple interface.
void	set_array_iface (array_iface *iface)
	Stores handle for the array interface.
void	set_fp_conv (fp_convt *iface)
	Stores handle for the floating-point interface.
void	set_ra_conv (ra_apit *iface)
	Stores handle for the real-arithmetic/enclosure interface.
void	bump_addrspace_array (unsigned int idx, const expr2tc &val)
std::string	get_cur_addrspace_ident ()
	Get the symbol name for the current address-allocation record array.
void	finalize_pointer_chain (unsigned int obj_num)
	Create and assert address space constraints on the given object ID number.
smt_astt	convert_typecast_to_bool (const typecast2t &cast)
	Typecast data to bools.
smt_astt	convert_typecast_to_fixedbv_nonint (const expr2tc &cast)
	Typecast to a fixedbv in bitvector mode.
smt_astt	convert_typecast_to_fixedbv_nonint_from_bv (const expr2tc &cast)
smt_astt	convert_typecast_to_fixedbv_nonint_from_bool (const expr2tc &cast)
smt_astt	convert_typecast_to_fixedbv_nonint_from_fixedbv (const expr2tc &cast)
smt_astt	convert_typecast_to_ints (const typecast2t &cast)
	Typecast anything to an integer (but not pointers).
smt_astt	convert_typecast_to_ints_intmode (const typecast2t &cast)
smt_astt	convert_typecast_to_ints_from_fbv_sint (const typecast2t &cast)
smt_astt	convert_typecast_to_ints_from_unsigned (const typecast2t &cast)
smt_astt	convert_typecast_to_ints_from_bool (const typecast2t &cast)
smt_astt	convert_typecast_to_ptr (const typecast2t &cast)
	Typecast something (i.e.
smt_astt	convert_typecast_from_ptr (const typecast2t &cast)
	Typecast a pointer to an integer.
smt_astt	convert_typecast_to_struct (const typecast2t &cast)
	Typecast structs to other structs.
smt_astt	convert_typecast (const expr2tc &expr)
	Despatch a typecast expression to a more specific typecast method.
smt_astt	convert_typecast_to_fpbv (const typecast2t &cast)
	Typecast to a floatbv.
smt_astt	convert_typecast_from_fpbv (const typecast2t &cast)
	Typecast from a floatbv.
smt_astt	round_real_to_int (smt_astt a)
	Round a real to an integer; not straightforward at all.
smt_astt	round_fixedbv_to_int (smt_astt a, unsigned int width, unsigned int towidth)
	Round a fixedbv to an integer.
smt_astt	round_int_to_fp (smt_astt int_val, const floatbv_type2t &fbv_type, unsigned int source_width)
	Round an SMT integer to the nearest representable float/double using IEEE 754 round-to-nearest-even.
smt_astt	tuple_array_create_despatch (const expr2tc &expr, smt_sortt domain)
	Prep call for creating a tuple array.
smt_astt	make_bool_bit (smt_astt a)
	Convert a boolean to a bitvector with one bit.
smt_astt	make_bit_bool (smt_astt a)
	Convert a bitvector with one bit to a boolean.
expr2tc	fix_array_idx (const expr2tc &idx, const type2tc &array_type)
	Given an array index, extract the lower n bits of it, where n is the bitwidth of the array domain.
type2tc	flatten_array_type (const type2tc &type)
	For a multi-dimensional array, convert the type into a single dimension array.
type2tc	get_flattened_array_subtype (const type2tc &type)
	Get the base subtype of an array, delving through any intermediate multidimensional arrays.
expr2tc	array_domain_to_width (const type2tc &type)
	Fetch the number of elements in an array (the domain).
void	rewrite_ptrs_to_structs (type2tc &type)
	For the given type, replace all instances of a pointer type with the struct representation of it.
expr2tc	decompose_select_chain (const expr2tc &expr, expr2tc &base)
	When dealing with multi-dimensional arrays, and selecting one element out of several dimensions, reduce it to an expression on a single dimensional array, by concatenating the indexes.
expr2tc	decompose_store_chain (const expr2tc &expr, expr2tc &base)
	Like decompose_select_chain, but for multidimensional stores.
void	expand_row_stores (const expr2tc &row, const expr2tc &offset, std::vector< flat_storet > &stores)
	Name every element of a row being written whole as a store of the corresponding read out of it, at `offset` in the flattened array.
bool	decompose_stores (const expr2tc &expr, const expr2tc &offset, std::vector< flat_storet > &stores, expr2tc &base)
	Decompose an array with into the flat element updates it denotes, oldest first, giving back the array the chain is rooted at.
smt_astt	convert_array_of_prep (const expr2tc &expr)
	Prepare an array_of expression by flattening its dimensions, if it has more than one.
smt_astt	pointer_array_of (const expr2tc &init_val, unsigned long array_width)
	Create an array of pointers; expects the init_val to be null, because there's no other way to initialize a pointer array in C, AFAIK.
unsigned int	get_member_name_field (const type2tc &t, const irep_idt &name) const
unsigned int	get_member_name_field (const type2tc &t, const expr2tc &name) const
expr2tc	get_array (const type2tc &type, smt_astt array)
	Given an array expression, attempt to extract its valuation from the solver model, computing a constant_array2tc by calling get_array_elem.
expr2tc	get_array (const expr2tc &expr)
void	delete_all_asts ()

Public Attributes
sat_iface *	sat_api
Public Attributes inherited from smt_solver_baset
unsigned int	ctx_level
	Number of un-popped context pushes encountered so far.
smt_cachet	smt_cache
	A cache mapping expressions to converted SMT ASTs.
std::mutex	smt_cache_mutex
	A mutex lock for writing to the cache.
smt_sort_cachet	sort_cache
	A cache of converted type2tc's to smt sorts.
std::unordered_map< smt_astt, tvt >	l_get_cache
	Model-value cache for l_get().
std::unordered_map< smt_astt, std::pair< type2tc, expr2tc > >	get_ast_cache
	Model-value cache for get_by_ast(), on the same terms and with the same invalidation as l_get_cache.
std::list< pointer_logict >	pointer_logic
	Pointer_logict object, which contains some code for formatting how pointers are displayed in counter-examples.
type2tc	pointer_struct
	Constant struct representing the implementation of the pointer type – i.e., the struct type that pointers get translated to.
type2tc	machine_ptr
	The type of the machine integer that can store a pointer.
smt_sortt	boolean_sort
	Sort for booleans.
bool	int_encoding
	Whether we are encoding expressions in integer mode or not.
bool	ir_ieee
	Whether –ir-ieee mode is active (integer encoding with IEEE float semantics).
const namespacet &	ns
	A namespace containing all the types in the program.
const optionst &	options
bool	ptr_foo_inited
smt_astt	null_ptr_ast
smt_astt	invalid_ptr_ast
size_t	quantifier_counter = 0
	Counter for generating unique bound-variable names in quantifiers.
std::unordered_map< std::string, std::vector< uf_ackermann_entry > >	uf_ackermann_history
	Per-name history of uninterpreted-function applications, used only by the Ackermannisation fallback in the base mk_smt_uninterpreted_function (for backends without native UF support).
size_t	uf_ackermann_counter = 0
	Counter for the fresh result symbols minted by the Ackermann fallback.
std::vector< ptr_flatten_entry >	ptr_flatten_history
	Every flattened pointer in this context.
std::unordered_map< expr2tc, ptr_flatten_entry, irep2_hash >	flattened
	Each flattening bitcast converted so far, for steps that hit it in the conversion cache.
smt_astt	step_guard = nullptr
	The SSA step being converted: its guard, the flattens its operands may hold (all a rebuild in it reads), those it makes, and the symbol it assigns.
std::set< size_t >	step_sources
std::set< size_t >	step_flattens
std::string	step_assigned
expr2tc	step_overwritten
size_t	flatten_count = 0
std::unordered_map< std::string, std::pair< unsigned int, std::set< size_t > > >	ptr_flow
	The flattens each SSA symbol's value may hold, and the context level it was recorded at.
std::unordered_map< irep_idt, expr2tc, irep_id_hash >	forall_defs_
	Map from SSA symbol name to its forall/exists irep2 expression.
std::map< std::string, unsigned int >	fresh_map
	Mapping of name prefixes to use counts: when we want a fresh new name with a particular prefix, this map stores how many times that prefix has been used, and thus what number should be appended to make the name unique.
std::list< unsigned int >	addr_space_sym_num
	Integer recording how many times the address space allocation record array has been modified.
type2tc	addr_space_type
	Type of the address space allocation records.
type2tc	addr_space_arr_type
	Type of the array of address space allocation records.
std::list< std::map< unsigned, bool > >	addr_space_data
	The objects given an address so far, each mapped to whether it is a heap object that may be freed.
expr2tc	current_valid_objects_sym
	Holds the __ESBMC_alloc symbol convert_terminal() was last invoked with.
std::vector< renumber_mapt >	renumber_map
std::vector< smt_astt >	live_asts
	Lifetime tracking of smt ast's.
std::vector< unsigned int >	live_asts_sizes
	Accounting of live_asts for push/pop.
tuple_iface *	tuple_api
array_iface *	array_api
fp_convt *	fp_api
ra_apit *	ra_api
std::unique_ptr< ir_ieee_convt >	ir_ieee_api
smt_astt	int_shift_op_array
std::set< std::pair< expr2tc, expr2tc > >	divided_operand_pairs
	Operand pairs of every division seen by note_division_operands.

Additional Inherited Members
Static Public Attributes inherited from smt_solver_baset
static constexpr size_t	max_rebuild_sources = 32
	The most flattens one rebuilt pointer is defined over; see decode_pointer_repr().

Member Enumeration Documentation

◆ shiftt

enum bitblast_convt::shiftt

Enumerator
LEFT
LRIGHT
ARIGHT

Constructor & Destructor Documentation

◆ bitblast_convt()

bitblast_convt::bitblast_convt	(	bool	int_encoding,
		const namespacet &	_ns,
		sat_iface *	sat_api )

◆ ~bitblast_convt()

bitblast_convt::~bitblast_convt ( )

Member Function Documentation

◆ adder_no_overflow() [1/2]

void bitblast_convt::adder_no_overflow	(	const bvt &	op0,
		const bvt &	op1,
		bvt &	res )

◆ adder_no_overflow() [2/2]

void bitblast_convt::adder_no_overflow	(	const bvt &	op0,
		const bvt &	op1,
		bvt &	res,
		bool	subtract,
		bool	is_signed )

◆ assert_ast()

void bitblast_convt::assert_ast ( const smt_ast * a )

virtual

◆ barrel_shift()

void bitblast_convt::barrel_shift	(	const bvt &	op,
		const shiftt	s,
		const bvt &	dist,
		bvt &	out )

◆ bvand()

void bitblast_convt::bvand	(	const bvt &	bv0,
		const bvt &	bv1,
		bvt &	output )

◆ bvnot()

void bitblast_convt::bvnot	(	const bvt &	bv0,
		bvt &	output )

◆ bvor()

void bitblast_convt::bvor	(	const bvt &	bv0,
		const bvt &	bv1,
		bvt &	output )

◆ bvxor()

void bitblast_convt::bvxor	(	const bvt &	bv0,
		const bvt &	bv1,
		bvt &	output )

◆ carry()

literalt bitblast_convt::carry	(	literalt	a,
		literalt	b,
		literalt	c )

◆ carry_out()

literalt bitblast_convt::carry_out	(	const bvt &	a,
		const bvt &	b,
		literalt	c )

◆ cond_negate()

void bitblast_convt::cond_negate	(	const bvt &	vals,
		bvt &	out,
		literalt	cond )

◆ eliminate_duplicates()

void bitblast_convt::eliminate_duplicates	(	const bvt &	bv,
		bvt &	dest )

◆ equal()

literalt bitblast_convt::equal	(	const bvt &	op0,
		const bvt &	op1 )

◆ full_adder()

void bitblast_convt::full_adder	(	const bvt &	op0,
		const bvt &	op1,
		bvt &	output,
		literalt	carry_in,
		literalt &	carry_out )

◆ get_bool()

expr2tc bitblast_convt::get_bool ( const smt_ast * a )

◆ get_bv()

expr2tc bitblast_convt::get_bv	(	const type2tc &	t,
		const smt_ast *	a )

◆ incrementer()

void bitblast_convt::incrementer	(	const bvt &	inp,
		const literalt &	carryin,
		literalt	carryout,
		bvt &	oup )

◆ invert()

void bitblast_convt::invert ( bvt & bv )

◆ is_constant()

bool bitblast_convt::is_constant ( const bvt & bv )

◆ l_get()

tvt bitblast_convt::l_get ( const smt_ast * a )

virtual

◆ land()

literalt bitblast_convt::land ( const bvt & bv )

virtual

◆ lor()

literalt bitblast_convt::lor ( const bvt & bv )

virtual

◆ lt_or_le()

literalt bitblast_convt::lt_or_le	(	bool	or_equal,
		const bvt &	bv0,
		const bvt &	bv1,
		bool	is_signed )

◆ mk_ast_equality()

bitblast_smt_ast * bitblast_convt::mk_ast_equality	(	const smt_ast *	a,
		const smt_ast *	b,
		const smt_sort *	ressort )

◆ mk_extract()

smt_ast * bitblast_convt::mk_extract	(	const smt_ast *	src,
		unsigned int	high,
		unsigned int	low,
		const smt_sort *	s )

virtual

◆ mk_func_app()

smt_astt bitblast_convt::mk_func_app	(	const smt_sort *	ressort,
		smt_func_kind	f,
		const smt_ast const	args,
		unsigned int	num )

virtual

◆ mk_smt_bool()

smt_ast * bitblast_convt::mk_smt_bool ( bool val )

virtual

Create a boolean.

Parameters

val	Whether to create a true or false boolean.

Returns: The newly created terminal smt_ast of this boolean.

Implements smt_solver_baset.

◆ mk_smt_bvint()

smt_ast * bitblast_convt::mk_smt_bvint	(	const BigInt &	inval,
		bool	sign,
		unsigned int	w )

virtual

◆ mk_smt_int()

smt_ast * bitblast_convt::mk_smt_int ( const BigInt & theint )

virtual

Create an integer smt_ast.

That is, an integer in QF_AUFLIRA, rather than a bitvector.

Parameters

theint BigInt representation of the number to create.

Returns: The newly created terminal smt_ast of this integer.

Implements smt_solver_baset.

◆ mk_smt_real()

smt_ast * bitblast_convt::mk_smt_real ( const std::string & str )

virtual

Create a real in a smt_ast.

Parameters

str	String representation of the real, to be parsed by the solver. Tends to be one integer divided ('/') by another. After inspecting all other options, there are none that are good, this is a legitimate use of strings.

Returns: An SMT AST representing this real value.

No backend is required to return a distinct smt_ast * per call: a backend that memoises real constants by value (a natural optimisation) is free to hand back the same pointer for repeated calls with the same str. Do not key identity-sensitive metadata (e.g. AST-pointer-keyed side-channel maps) directly on the result of this call unless the value is known to be one this call site exclusively owns; mint a fresh symbol (mk_fresh) and constrain it equal to the desired real value instead.

Implements smt_solver_baset.

◆ mk_smt_symbol()

smt_astt bitblast_convt::mk_smt_symbol	(	const std::string &	name,
		const smt_sort *	sort )

virtual

◆ mk_sort()

smt_sort * bitblast_convt::mk_sort	(	smt_sort_kind	k,
			... )

virtual

◆ mk_struct_sort()

smt_sort * bitblast_convt::mk_struct_sort ( const type2tc & t )

virtual

◆ negate()

void bitblast_convt::negate	(	const bvt &	inp,
		bvt &	oup )

◆ new_ast()

bitblast_smt_ast * bitblast_convt::new_ast ( smt_sortt ressort )

inline

◆ process_clause()

bool bitblast_convt::process_clause	(	const bvt &	bv,
		bvt &	dest )

◆ shift()

void bitblast_convt::shift	(	const bvt &	inp,
		const shiftt &	s,
		unsigned long	d,
		bvt &	out )

◆ signed_divider()

void bitblast_convt::signed_divider	(	const bvt &	op0,
		const bvt &	op1,
		bvt &	res,
		bvt &	rem )

◆ signed_multiplier()

void bitblast_convt::signed_multiplier	(	const bvt &	op0,
		const bvt &	bv1,
		bvt &	output )

◆ unsigned_divider()

void bitblast_convt::unsigned_divider	(	const bvt &	op0,
		const bvt &	op1,
		bvt &	res,
		bvt &	rem )

◆ unsigned_less_than()

literalt bitblast_convt::unsigned_less_than	(	const bvt &	arg0,
		const bvt &	arg1 )

◆ unsigned_multiplier()

void bitblast_convt::unsigned_multiplier	(	const bvt &	op0,
		const bvt &	bv1,
		bvt &	output )

◆ unsigned_multiplier_no_overflow()

void bitblast_convt::unsigned_multiplier_no_overflow	(	const bvt &	op0,
		const bvt &	op1,
		bvt &	r )

Member Data Documentation

◆ sat_api

sat_iface* bitblast_convt::sat_api

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

src/solvers/sat/bitblast_conv.h
src/solvers/sat/bitblast_conv.cpp

Public Types

Public Member Functions

Public Attributes

Additional Inherited Members

Member Enumeration Documentation

◆ shiftt

Constructor & Destructor Documentation

◆ bitblast_convt()

◆ ~bitblast_convt()

Member Function Documentation

◆ adder_no_overflow() [1/2]

◆ adder_no_overflow() [2/2]

◆ assert_ast()

◆ barrel_shift()

◆ bvand()

◆ bvnot()

◆ bvor()

◆ bvxor()

◆ carry()

◆ carry_out()

◆ cond_negate()

◆ eliminate_duplicates()

◆ equal()

◆ full_adder()

◆ get_bool()

◆ get_bv()

◆ incrementer()

◆ invert()

◆ is_constant()

◆ l_get()

◆ land()

◆ lor()

◆ lt_or_le()

◆ mk_ast_equality()

◆ mk_extract()

◆ mk_func_app()

◆ mk_smt_bool()

◆ mk_smt_bvint()

◆ mk_smt_int()

◆ mk_smt_real()

◆ mk_smt_symbol()

◆ mk_sort()

◆ mk_struct_sort()

◆ negate()

◆ new_ast()

◆ process_clause()

◆ shift()

◆ signed_divider()

◆ signed_multiplier()

◆ unsigned_divider()

◆ unsigned_less_than()

◆ unsigned_multiplier()

◆ unsigned_multiplier_no_overflow()

Member Data Documentation

◆ sat_api