#include <z3_conv.h>

Inheritance diagram for z3_convt:

Public Member Functions
	z3_convt (const namespacet &ns, const optionst &options)
	~z3_convt () override
void	push_ctx () override
	Push one context on the SMT assertion stack.
void	pop_ctx () override
	Pop one context on the SMT assertion stack.
smt_resultt	dec_solve () override
	Solve the formula given to the solver.
smt_resultt	dec_solve_assuming (const ast_vec &assumptions) override
	Solve with each boolean ast in `assumptions` held true for this query only.
bool	supports_assumptions () const override
tvt	get_bool (smt_astt a) override
	Extract the assignment to a boolean variable from the SMT solver's model.
BigInt	get_bv (smt_astt a, bool is_signed) override
	Extract the assignment to a bitvector from the SMT solver's model.
ieee_floatt	get_fpbv (smt_astt a) override
	Extract the assignment to a floating-point from the SMT solvers model.
bool	get_rational (smt_astt a, BigInt &numerator, BigInt &denominator) override
	Extract the assignment to a rational/real value from the SMT solvers model.
expr2tc	get_array_elem (smt_astt array, uint64_t index, const type2tc &subtype) override
	Extract an element from the model of an array, at an explicit index.
z3::expr	mk_tuple_update (const z3::expr &t, unsigned i, const z3::expr &new_val)
z3::expr	mk_tuple_select (const z3::expr &t, unsigned i)
smt_astt	mk_add (smt_astt a, smt_astt b) override
smt_astt	mk_bvadd (smt_astt a, smt_astt b) override
smt_astt	mk_sub (smt_astt a, smt_astt b) override
smt_astt	mk_bvsub (smt_astt a, smt_astt b) override
smt_astt	mk_mul (smt_astt a, smt_astt b) override
smt_astt	mk_bvmul (smt_astt a, smt_astt b) override
smt_astt	mk_mod (smt_astt a, smt_astt b) override
smt_astt	mk_bvsmod (smt_astt a, smt_astt b) override
smt_astt	mk_bvumod (smt_astt a, smt_astt b) override
smt_astt	mk_div (smt_astt a, smt_astt b) override
smt_astt	mk_bvsdiv (smt_astt a, smt_astt b) override
smt_astt	mk_bvudiv (smt_astt a, smt_astt b) override
smt_astt	mk_shl (smt_astt a, smt_astt b) override
smt_astt	mk_bvshl (smt_astt a, smt_astt b) override
smt_astt	mk_bvashr (smt_astt a, smt_astt b) override
smt_astt	mk_bvlshr (smt_astt a, smt_astt b) override
smt_astt	mk_neg (smt_astt a) override
smt_astt	mk_bvneg (smt_astt a) override
smt_astt	mk_bvnot (smt_astt a) override
smt_astt	mk_bvxor (smt_astt a, smt_astt b) override
smt_astt	mk_bvor (smt_astt a, smt_astt b) override
smt_astt	mk_bvand (smt_astt a, smt_astt b) override
smt_astt	mk_implies (smt_astt a, smt_astt b) override
smt_astt	mk_xor (smt_astt a, smt_astt b) override
smt_astt	mk_or (smt_astt a, smt_astt b) override
smt_astt	mk_and (smt_astt a, smt_astt b) override
smt_astt	mk_not (smt_astt a) override
smt_astt	mk_lt (smt_astt a, smt_astt b) override
smt_astt	mk_bvult (smt_astt a, smt_astt b) override
smt_astt	mk_bvslt (smt_astt a, smt_astt b) override
smt_astt	mk_gt (smt_astt a, smt_astt b) override
smt_astt	mk_bvugt (smt_astt a, smt_astt b) override
smt_astt	mk_bvsgt (smt_astt a, smt_astt b) override
smt_astt	mk_le (smt_astt a, smt_astt b) override
smt_astt	mk_bvule (smt_astt a, smt_astt b) override
smt_astt	mk_bvsle (smt_astt a, smt_astt b) override
smt_astt	mk_ge (smt_astt a, smt_astt b) override
smt_astt	mk_bvuge (smt_astt a, smt_astt b) override
smt_astt	mk_bvsge (smt_astt a, smt_astt b) override
smt_astt	mk_eq (smt_astt a, smt_astt b) override
smt_astt	mk_neq (smt_astt a, smt_astt b) override
smt_astt	mk_store (smt_astt a, smt_astt b, smt_astt c) override
smt_astt	mk_select (smt_astt a, smt_astt b) override
smt_astt	mk_real2int (smt_astt a) override
smt_astt	mk_int2real (smt_astt a) override
smt_astt	mk_isint (smt_astt a) override
smt_astt	overflow_arith (const expr2tc &expr) override
	Detect integer arithmetic overflows.
smt_sortt	mk_bool_sort () override
	Create a bool sort.
smt_sortt	mk_real_sort () override
	Create a real sort.
smt_sortt	mk_int_sort () override
	Create a int sort.
smt_sortt	mk_bv_sort (std::size_t width) override
	Create a bv sort.
smt_sortt	mk_array_sort (smt_sortt domain, smt_sortt range) override
	Create an array sort.
smt_sortt	mk_fbv_sort (std::size_t width) override
	Create a fixed-point sort.
smt_sortt	mk_bvfp_sort (std::size_t ew, std::size_t sw) override
	Create a floating-point sort, using bitvectors.
smt_sortt	mk_bvfp_rm_sort () override
	Create a floating-point rounding mode sort, using bitvectors.
smt_sortt	mk_fpbv_sort (const unsigned ew, const unsigned sw) override
	Create a sort representing a floating-point number.
smt_sortt	mk_fpbv_rm_sort () override
	Create a sort representing a floating-point rounding mode.
smt_astt	mk_smt_int (const BigInt &theint) override
	Create an integer smt_ast.
smt_astt	mk_smt_real (const std::string &str) override
	Create a real in a smt_ast.
smt_astt	mk_smt_bv (const BigInt &theint, smt_sortt s) override
	Create a bitvector.
smt_astt	mk_smt_fpbv (const ieee_floatt &thereal) override
	Create a floating point bitvector.
smt_astt	mk_smt_fpbv_nan (bool sgn, unsigned ew, unsigned sw) override
	Create a NaN floating point bitvector.
smt_astt	mk_smt_fpbv_inf (bool sgn, unsigned ew, unsigned sw) override
	Create a (+/-)inf floating point bitvector.
smt_astt	mk_smt_fpbv_rm (ieee_floatt::rounding_modet rm) override
	Create a rounding mode to be used by floating point cast and arith ops.
smt_astt	mk_smt_fpbv_fma (smt_astt v1, smt_astt v2, smt_astt v3, smt_astt rm) override
	Convert the ieee arithmetic fused-multiply add (fma): round((v1 * v2) + v3).
smt_astt	mk_smt_typecast_from_fpbv_to_ubv (smt_astt from, std::size_t width) override
	Typecast from a floating point.
smt_astt	mk_smt_typecast_from_fpbv_to_sbv (smt_astt from, std::size_t width) override
	Typecast from a floating point.
smt_astt	mk_smt_typecast_from_fpbv_to_fpbv (smt_astt from, smt_sortt to, smt_astt rm) override
	Typecast from a floating point.
smt_astt	mk_smt_typecast_ubv_to_fpbv (smt_astt from, smt_sortt to, smt_astt rm) override
	Typecast to a floating point.
smt_astt	mk_smt_typecast_sbv_to_fpbv (smt_astt from, smt_sortt to, smt_astt rm) override
	Typecast to a floating point.
smt_astt	mk_smt_fpbv_add (smt_astt lhs, smt_astt rhs, smt_astt rm) override
	Convert a ieee addition.
smt_astt	mk_smt_fpbv_sub (smt_astt lhs, smt_astt rhs, smt_astt rm) override
	Convert a ieee subtraction.
smt_astt	mk_smt_fpbv_mul (smt_astt lhs, smt_astt rhs, smt_astt rm) override
	Convert a ieee multiplication.
smt_astt	mk_smt_fpbv_div (smt_astt lhs, smt_astt rhs, smt_astt rm) override
	Convert the ieee division.
smt_astt	mk_smt_fpbv_rem (smt_astt lhs, smt_astt rhs) override
	Convert the ieee remainder (SMT-LIB fp.rem, C's remainder()).
smt_astt	mk_smt_nearbyint_from_float (smt_astt from, smt_astt rm) override
	Calculate the nearby int from a floating point, considering the rounding mode.
smt_astt	mk_smt_fpbv_sqrt (smt_astt rd, smt_astt rm) override
	Convert the ieee arithmetic square-root (sqrt).
smt_astt	mk_smt_fpbv_eq (smt_astt lhs, smt_astt rhs) override
	Convert an ieee equality.
smt_astt	mk_smt_fpbv_gt (smt_astt lhs, smt_astt rhs) override
	Convert an ieee greater than.
smt_astt	mk_smt_fpbv_lt (smt_astt lhs, smt_astt rhs) override
	Convert an ieee less than.
smt_astt	mk_smt_fpbv_gte (smt_astt lhs, smt_astt rhs) override
	Convert an ieee greater than or equal.
smt_astt	mk_smt_fpbv_lte (smt_astt lhs, smt_astt rhs) override
	Convert an ieee less than or equal.
smt_astt	mk_smt_fpbv_is_nan (smt_astt op) override
	Convert an ieee is_nan operation.
smt_astt	mk_smt_fpbv_is_inf (smt_astt op) override
	Convert an ieee is_inf operation.
smt_astt	mk_smt_fpbv_is_normal (smt_astt op) override
	Convert an ieee is_normal operation.
smt_astt	mk_smt_fpbv_is_zero (smt_astt op) override
	Convert an ieee is_zero operation.
smt_astt	mk_smt_fpbv_is_negative (smt_astt op) override
	Convert an ieee is_neg operation.
smt_astt	mk_smt_fpbv_is_positive (smt_astt op) override
	Convert an ieee is_pos operation.
smt_astt	mk_smt_fpbv_abs (smt_astt op) override
	Convert an ieee abs operation.
smt_astt	mk_smt_fpbv_neg (smt_astt op) override
	Convert an ieee negation operation.
smt_astt	mk_from_bv_to_fp (smt_astt op, smt_sortt to) override
	Convert BV to FP.
smt_astt	mk_from_fp_to_bv (smt_astt op) override
	Convert FP to BV.
smt_astt	mk_smt_bool (bool val) override
	Create a boolean.
smt_astt	mk_array_symbol (const std::string &name, const smt_sort *s, smt_sortt array_subtype) override
smt_astt	mk_smt_symbol (const std::string &name, const smt_sort *s) override
smt_astt	mk_smt_uninterpreted_function (const std::string &name, const std::vector< smt_astt > &args, smt_sortt rangesort) override
	Apply an uninterpreted function.
smt_sortt	mk_struct_sort (const type2tc &type) override
	Create a sort representing a struct.
smt_astt	mk_extract (smt_astt a, unsigned int high, unsigned int low) override
	Create an 'extract' func app.
smt_astt	mk_sign_ext (smt_astt a, unsigned int topwidth) override
	Given a signed, upwards cast, extends the sign of the given AST to the desired length.
smt_astt	mk_zero_ext (smt_astt a, unsigned int topwidth) override
	Identical to mk_sign_ext, but extends AST with zeros.
smt_astt	mk_concat (smt_astt a, smt_astt b) override
	Concatenate two smt expressions.
smt_astt	mk_ite (smt_astt cond, smt_astt t, smt_astt f) override
	Create an ite operation.
smt_astt	tuple_create (const expr2tc &structdef) override
	Create a new tuple from a struct definition.
smt_astt	tuple_fresh (const smt_sort *s, std::string name="") override
expr2tc	tuple_get (const expr2tc &expr) override
	Extract the assignment to a tuple-typed symbol from the SMT solvers model.
expr2tc	tuple_get (const type2tc &type, smt_astt sym) override
expr2tc	tuple_get_array_elem (smt_astt array, uint64_t index, const type2tc &subtype) override
smt_astt	tuple_array_create (const type2tc &array_type, smt_astt input_args, bool const_array, const smt_sort domain) override
smt_astt	mk_tuple_symbol (const std::string &name, smt_sortt s) override
	Convert a symbol to a tuple_smt_ast.
smt_astt	mk_tuple_array_symbol (const expr2tc &expr) override
	Like mk_tuple_symbol, but for arrays.
smt_astt	tuple_array_of (const expr2tc &init, unsigned long domain_width) override
	Create a potentially /large/ array of tuples.
smt_astt	convert_array_of (smt_astt init_val, unsigned long domain_width) override
	Create an array with a single initializer.
void	assert_ast (smt_astt a) override
	Assert the truth of an ast.
const std::string	solver_text () override
	Solver name fetcher.
std::string	dump_smt () override
	Method to dump the SMT formula.
void	print_model () override
	Method to print the SMT model.
smt_astt	mk_quantifier (bool is_forall, std::vector< smt_astt > lhs, smt_astt rhs) override
virtual void	output_smt ()
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 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.
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.
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 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.
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.
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_symbol (const std::string &name, smt_sortt s)=0
	Create a symbol / variable.
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_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 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 Member Functions inherited from tuple_iface
virtual smt_astt	tuple_fresh (smt_sortt s, std::string name="")=0
	Create a fresh tuple, with freely valued fields.
virtual smt_astt	tuple_array_create (const type2tc &array_type, smt_astt *inputargs, bool const_array, smt_sortt domain)=0
virtual void	add_tuple_constraints_for_solving ()
virtual void	push_tuple_ctx ()
virtual void	pop_tuple_ctx ()
virtual	~tuple_iface ()=default
Public Member Functions inherited from array_iface
	array_iface (bool _b, bool inf)
virtual smt_astt	mk_array_symbol (const std::string &name, smt_sortt sort, smt_sortt subtype)=0
smt_astt	default_convert_array_of (smt_astt init_val, unsigned long domain_width, smt_solver_baset *ctx)
virtual void	add_array_constraints_for_solving ()
virtual void	push_array_ctx ()
virtual void	pop_array_ctx ()
Public Member Functions inherited from fp_convt
	fp_convt (smt_solver_baset *_ctx)
virtual	~fp_convt ()=default

Public Attributes
z3::context	z3_ctx
z3::solver	solver
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.
Public Attributes inherited from array_iface
bool	supports_bools_in_arrays
bool	can_init_infinite_arrays

Additional Inherited Members
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
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().

Constructor & Destructor Documentation

◆ z3_convt()

z3_convt::z3_convt	(	const namespacet &	ns,
		const optionst &	options )

◆ ~z3_convt()

z3_convt::~z3_convt ( )

override

Member Function Documentation

◆ assert_ast()

void z3_convt::assert_ast ( smt_astt a )

overridevirtual

Assert the truth of an ast.

Equivalent to the 'assert' directive in the SMTLIB language, this informs the solver that in the satisfying assignment it attempts to produce, the formula corresponding to the smt_ast argument must evaluate to true.

Parameters

a	A handle to the formula that must be true.

Implements smt_solver_baset.

◆ convert_array_of()

smt_astt z3_convt::convert_array_of	(	smt_astt	init_val,
		unsigned long	domain_width )

overridevirtual

Create an array with a single initializer.

This may be a small, fixed size array, or it may be a nondeterministically sized array with a word-sized domain. Default implementation is to repeatedly store into the array for as many elements as necessary; subclassing class should override if it has a more efficient method. Nondeterministically sized memory with an initializer is very rare; the only real users of this are fixed-sized (but large) static arrays that are zero initialized, or some infinite-domain modelling arrays used in ESBMC.

Parameters

init_val	The value to initialize each element with.
domain_width	The size of the array to create, in domain bits.

Returns: An AST representing the created constant array.

Implements array_iface.

◆ dec_solve()

smt_resultt z3_convt::dec_solve ( )

overridevirtual

Solve the formula given to the solver.

The solver will attempt to produce a satisfying assignment for all of the variables / symbols used in the formula, where all the asserted sub-formula are true. Results are either unsat (the formula is inconsistent), sat (an assignment exists), or that an error occurred.

Returns: Result code of the call to the solver.

Implements smt_solver_baset.

◆ dec_solve_assuming()

smt_resultt z3_convt::dec_solve_assuming ( const ast_vec & assumptions )

overridevirtual

Solve with each boolean ast in assumptions held true for this query only.

Backends without support abort; check supports_assumptions().

Reimplemented from smt_solver_baset.

◆ dump_smt()

std::string z3_convt::dump_smt ( )

overridevirtual

Method to dump the SMT formula.

Reimplemented from smt_solver_baset.

◆ get_array_elem()

expr2tc z3_convt::get_array_elem	(	smt_astt	a,
		uint64_t	idx,
		const type2tc &	subtype )

overridevirtual

Extract an element from the model of an array, at an explicit index.

Parameters

array	AST representing the array we are extracting from
index	The index of the element we wish to expect
subtype	The type of the element we are extracting, i.e., array range

Returns: Expression representation of the element

Implements array_iface.

◆ get_bool()

tvt z3_convt::get_bool ( smt_astt a )

overridevirtual

Extract the assignment to a boolean variable from the SMT solver's model.

Parameters

a	The AST whose value we wish to know.

Returns: a's value, or tvt::TV_UNKNOWN when the solver cannot reduce it to a ground boolean. That is an expected outcome for terms that still contain a quantifier: callers must not invent a value for it.

Implements smt_solver_baset.

◆ get_bv()

BigInt z3_convt::get_bv	(	smt_astt	a,
		bool	is_signed )

overridevirtual

Extract the assignment to a bitvector from the SMT solver's model.

Parameters

a	The AST whose value we wish to know.
is_signed	whether the bitvector is signed

Returns: Expression representation of a's value

Implements smt_solver_baset.

◆ get_fpbv()

ieee_floatt z3_convt::get_fpbv ( smt_astt a )

overridevirtual

Extract the assignment to a floating-point from the SMT solvers model.

Parameters

a	the AST whos value we wish to know.

Returns: the ieee floating-point

Reimplemented from fp_convt.

◆ get_rational()

bool z3_convt::get_rational	(	smt_astt	a,
		BigInt &	numerator,
		BigInt &	denominator )

overridevirtual

Extract the assignment to a rational/real value from the SMT solvers model.

Used in integer/real arithmetic mode to get floating point values.

Parameters

a	The AST whose value we wish to know.
numerator	Output parameter for the numerator of the rational.
denominator	Output parameter for the denominator of the rational.

Returns: True if the rational value was successfully extracted, false otherwise.

Reimplemented from smt_solver_baset.

◆ mk_add()

smt_astt z3_convt::mk_add	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_and()

smt_astt z3_convt::mk_and	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_array_sort()

smt_sortt z3_convt::mk_array_sort	(	smt_sortt	domain,
		smt_sortt	range )

overridevirtual

Create an array sort.

Reimplemented from smt_solver_baset.

◆ mk_array_symbol()

smt_astt z3_convt::mk_array_symbol	(	const std::string &	name,
		const smt_sort *	s,
		smt_sortt	array_subtype )

override

◆ mk_bool_sort()

smt_sortt z3_convt::mk_bool_sort ( )

overridevirtual

Create a bool sort.

Reimplemented from smt_solver_baset.

◆ mk_bv_sort()

smt_sortt z3_convt::mk_bv_sort ( std::size_t width )

overridevirtual

Create a bv sort.

Reimplemented from smt_solver_baset.

◆ mk_bvadd()

smt_astt z3_convt::mk_bvadd	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvand()

smt_astt z3_convt::mk_bvand	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvashr()

smt_astt z3_convt::mk_bvashr	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvfp_rm_sort()

smt_sortt z3_convt::mk_bvfp_rm_sort ( )

overridevirtual

Create a floating-point rounding mode sort, using bitvectors.

Reimplemented from smt_solver_baset.

◆ mk_bvfp_sort()

smt_sortt z3_convt::mk_bvfp_sort	(	std::size_t	ew,
		std::size_t	sw )

overridevirtual

Create a floating-point sort, using bitvectors.

Reimplemented from smt_solver_baset.

◆ mk_bvlshr()

smt_astt z3_convt::mk_bvlshr	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvmul()

smt_astt z3_convt::mk_bvmul	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvneg()

smt_astt z3_convt::mk_bvneg ( smt_astt a )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvnot()

smt_astt z3_convt::mk_bvnot ( smt_astt a )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvor()

smt_astt z3_convt::mk_bvor	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvsdiv()

smt_astt z3_convt::mk_bvsdiv	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvsge()

smt_astt z3_convt::mk_bvsge	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvsgt()

smt_astt z3_convt::mk_bvsgt	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvshl()

smt_astt z3_convt::mk_bvshl	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvsle()

smt_astt z3_convt::mk_bvsle	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvslt()

smt_astt z3_convt::mk_bvslt	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvsmod()

smt_astt z3_convt::mk_bvsmod	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvsub()

smt_astt z3_convt::mk_bvsub	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvudiv()

smt_astt z3_convt::mk_bvudiv	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvuge()

smt_astt z3_convt::mk_bvuge	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvugt()

smt_astt z3_convt::mk_bvugt	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvule()

smt_astt z3_convt::mk_bvule	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvult()

smt_astt z3_convt::mk_bvult	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvumod()

smt_astt z3_convt::mk_bvumod	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_bvxor()

smt_astt z3_convt::mk_bvxor	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_concat()

smt_astt z3_convt::mk_concat	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Concatenate two smt expressions.

Parameters

a	the first part of the concatenation
b	the second part of the concatenation

Returns: the concatenation of a and b

Implements smt_solver_baset.

◆ mk_div()

smt_astt z3_convt::mk_div	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_eq()

smt_astt z3_convt::mk_eq	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_extract()

smt_astt z3_convt::mk_extract	(	smt_astt	a,
		unsigned int	high,
		unsigned int	low )

overridevirtual

Create an 'extract' func app.

Since we can't currently encode integer constants as function arguments without serious faff, this can't be performed via the medium of mk_func_app. Hence, this api call.

Parameters

a	The source piece of ast to extract a value from.
high	The topmost bit to select from the source, down to low.
low	The lowest bit to select from the source.

Implements smt_solver_baset.

◆ mk_fbv_sort()

smt_sortt z3_convt::mk_fbv_sort ( std::size_t width )

overridevirtual

Create a fixed-point sort.

Reimplemented from smt_solver_baset.

◆ mk_fpbv_rm_sort()

smt_sortt z3_convt::mk_fpbv_rm_sort ( )

overridevirtual

Create a sort representing a floating-point rounding mode.

Returns: The floating-point rounding mode representation of the type, wrapped in an smt_sort.

Reimplemented from fp_convt.

◆ mk_fpbv_sort()

smt_sortt z3_convt::mk_fpbv_sort	(	const unsigned	ew,
		const unsigned	sw )

overridevirtual

Create a sort representing a floating-point number.

Parameters

ew	Exponent width, in bits, of the bitvector to create.
sw	Significand width, in bits, of the bitvector to create.

Returns: The floating-point representation of the type, wrapped in an smt_sort.

Reimplemented from fp_convt.

◆ mk_from_bv_to_fp()

smt_astt z3_convt::mk_from_bv_to_fp	(	smt_astt	op,
		smt_sortt	to )

overridevirtual

Convert BV to FP.

Parameters

op	the bitvector
to	the floating-point type

Reimplemented from fp_convt.

◆ mk_from_fp_to_bv()

smt_astt z3_convt::mk_from_fp_to_bv ( smt_astt op )

overridevirtual

Convert FP to BV.

Parameters

op	the floating-point

Reimplemented from fp_convt.

◆ mk_ge()

smt_astt z3_convt::mk_ge	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_gt()

smt_astt z3_convt::mk_gt	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_implies()

smt_astt z3_convt::mk_implies	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_int2real()

smt_astt z3_convt::mk_int2real ( smt_astt a )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_int_sort()

smt_sortt z3_convt::mk_int_sort ( )

overridevirtual

Create a int sort.

Reimplemented from smt_solver_baset.

◆ mk_isint()

smt_astt z3_convt::mk_isint ( smt_astt a )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_ite()

smt_astt z3_convt::mk_ite	(	smt_astt	cond,
		smt_astt	t,
		smt_astt	f )

overridevirtual

Create an ite operation.

Parameters

cond	the ite condition
t	the true case
f	the false case

Returns: an ite expression

Implements smt_solver_baset.

◆ mk_le()

smt_astt z3_convt::mk_le	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_lt()

smt_astt z3_convt::mk_lt	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_mod()

smt_astt z3_convt::mk_mod	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_mul()

smt_astt z3_convt::mk_mul	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_neg()

smt_astt z3_convt::mk_neg ( smt_astt a )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_neq()

smt_astt z3_convt::mk_neq	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_not()

smt_astt z3_convt::mk_not ( smt_astt a )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_or()

smt_astt z3_convt::mk_or	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_quantifier()

smt_astt z3_convt::mk_quantifier	(	bool	is_forall,
		std::vector< smt_astt >	lhs,
		smt_astt	rhs )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_real2int()

smt_astt z3_convt::mk_real2int ( smt_astt a )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_real_sort()

smt_sortt z3_convt::mk_real_sort ( )

overridevirtual

Create a real sort.

Reimplemented from smt_solver_baset.

◆ mk_select()

smt_astt z3_convt::mk_select	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_shl()

smt_astt z3_convt::mk_shl	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_sign_ext()

smt_astt z3_convt::mk_sign_ext	(	smt_astt	a,
		unsigned int	topwidth )

overridevirtual

Given a signed, upwards cast, extends the sign of the given AST to the desired length.

Parameters

a	The bitvector to upcast.
topwidth	The number of bits to extend the input by

Returns: A bitvector with topwidth more bits, of the appropriate sign.

Implements smt_solver_baset.

◆ mk_smt_bool()

smt_astt z3_convt::mk_smt_bool ( bool val )

overridevirtual

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_bv()

smt_astt z3_convt::mk_smt_bv	(	const BigInt &	theint,
		smt_sortt	s )

overridevirtual

Create a bitvector.

Parameters

s	the sort.
theint	Integer representation of the bitvector. Any excess bits in the stored integer should be ignored.

Returns: The newly created terminal smt_ast of this bitvector.

Implements smt_solver_baset.

◆ mk_smt_fpbv()

smt_astt z3_convt::mk_smt_fpbv ( const ieee_floatt & thereal )

overridevirtual

Create a floating point bitvector.

Parameters

thereal	the floating-point number
ew	Exponent width, in bits, of the bitvector to create.
sw	Significand width, in bits, of the bitvector to create.

Returns: The newly created terminal smt_ast of this bitvector.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_abs()

smt_astt z3_convt::mk_smt_fpbv_abs ( smt_astt op )

overridevirtual

Convert an ieee abs operation.

Parameters

op	the operand

Returns: The newly created fp.abs smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_add()

smt_astt z3_convt::mk_smt_fpbv_add	(	smt_astt	lhs,
		smt_astt	rhs,
		smt_astt	rm )

overridevirtual

Convert a ieee addition.

Parameters

lhs	left hand side of the addition
rhs	right hand side of the addition
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_div()

smt_astt z3_convt::mk_smt_fpbv_div	(	smt_astt	lhs,
		smt_astt	rhs,
		smt_astt	rm )

overridevirtual

Convert the ieee division.

Parameters

lhs	left hand side of the division
rhs	right hand side of the division
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_eq()

smt_astt z3_convt::mk_smt_fpbv_eq	(	smt_astt	lhs,
		smt_astt	rhs )

overridevirtual

Convert an ieee equality.

Parameters

lhs	left hand side
rhs	right hand side

Returns: The newly created fp.eq smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_fma()

smt_astt z3_convt::mk_smt_fpbv_fma	(	smt_astt	v1,
		smt_astt	v2,
		smt_astt	v3,
		smt_astt	rm )

overridevirtual

Convert the ieee arithmetic fused-multiply add (fma): round((v1 * v2) + v3).

Parameters

v1	in the equation
v2	in the equation
v3	in the equation
rm	the rounding mode

Returns: The newly created fma smt_ast

Reimplemented from fp_convt.

◆ mk_smt_fpbv_gt()

smt_astt z3_convt::mk_smt_fpbv_gt	(	smt_astt	lhs,
		smt_astt	rhs )

overridevirtual

Convert an ieee greater than.

Parameters

lhs	left hand side
rhs	right hand side

Returns: The newly created fp.gt smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_gte()

smt_astt z3_convt::mk_smt_fpbv_gte	(	smt_astt	lhs,
		smt_astt	rhs )

overridevirtual

Convert an ieee greater than or equal.

Parameters

lhs	left hand side
rhs	right hand side

Returns: The newly created fp.gt smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_inf()

smt_astt z3_convt::mk_smt_fpbv_inf	(	bool	sgn,
		unsigned	ew,
		unsigned	sw )

overridevirtual

Create a (+/-)inf floating point bitvector.

Parameters

sgn	Whether this bitvector is negative or positive.
ew	Exponent width, in bits, of the bitvector to create.
sw	Significand width, in bits, of the bitvector to create.

Returns: The newly created terminal smt_ast of this bitvector.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_is_inf()

smt_astt z3_convt::mk_smt_fpbv_is_inf ( smt_astt op )

overridevirtual

Convert an ieee is_inf operation.

Parameters

op	the operand

Returns: The newly created fp.isInfinite smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_is_nan()

smt_astt z3_convt::mk_smt_fpbv_is_nan ( smt_astt op )

overridevirtual

Convert an ieee is_nan operation.

Parameters

op	the operand

Returns: The newly created fp.isNaN smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_is_negative()

smt_astt z3_convt::mk_smt_fpbv_is_negative ( smt_astt op )

overridevirtual

Convert an ieee is_neg operation.

Parameters

op	the operand

Returns: The newly created fp.isNegative smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_is_normal()

smt_astt z3_convt::mk_smt_fpbv_is_normal ( smt_astt op )

overridevirtual

Convert an ieee is_normal operation.

Parameters

op	the operand

Returns: The newly created fp.isNormal smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_is_positive()

smt_astt z3_convt::mk_smt_fpbv_is_positive ( smt_astt op )

overridevirtual

Convert an ieee is_pos operation.

Parameters

op	the operand

Returns: The newly created fp.isPositive smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_is_zero()

smt_astt z3_convt::mk_smt_fpbv_is_zero ( smt_astt op )

overridevirtual

Convert an ieee is_zero operation.

Parameters

op	the operand

Returns: The newly created fp.isZero smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_lt()

smt_astt z3_convt::mk_smt_fpbv_lt	(	smt_astt	lhs,
		smt_astt	rhs )

overridevirtual

Convert an ieee less than.

Parameters

lhs	left hand side
rhs	right hand side

Returns: The newly created fp.lt smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_lte()

smt_astt z3_convt::mk_smt_fpbv_lte	(	smt_astt	lhs,
		smt_astt	rhs )

overridevirtual

Convert an ieee less than or equal.

Parameters

lhs	left hand side
rhs	right hand side

Returns: The newly created fp.lt smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_mul()

smt_astt z3_convt::mk_smt_fpbv_mul	(	smt_astt	lhs,
		smt_astt	rhs,
		smt_astt	rm )

overridevirtual

Convert a ieee multiplication.

Parameters

lhs	left hand side of the multiplication
rhs	right hand side of the multiplication
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_nan()

smt_astt z3_convt::mk_smt_fpbv_nan	(	bool	sgn,
		unsigned	ew,
		unsigned	sw )

overridevirtual

Create a NaN floating point bitvector.

Parameters

ew	Exponent width, in bits, of the bitvector to create.
sw	Significand width, in bits, of the bitvector to create.

Returns: The newly created terminal smt_ast of this bitvector.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_neg()

smt_astt z3_convt::mk_smt_fpbv_neg ( smt_astt op )

overridevirtual

Convert an ieee negation operation.

Parameters

op	the operand

Returns: The newly created fp.neg smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_rem()

smt_astt z3_convt::mk_smt_fpbv_rem	(	smt_astt	lhs,
		smt_astt	rhs )

overridevirtual

Convert the ieee remainder (SMT-LIB fp.rem, C's remainder()).

The operation is exact, so it takes no rounding mode.

Parameters

lhs	left hand side of the remainder
rhs	right hand side of the remainder

Returns: The newly created fp.rem smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_rm()

smt_astt z3_convt::mk_smt_fpbv_rm ( ieee_floatt::rounding_modet rm )

overridevirtual

Create a rounding mode to be used by floating point cast and arith ops.

Parameters

rm	the kind of rounding mode

Returns: The newly created rounding mode smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_fpbv_sqrt()

smt_astt z3_convt::mk_smt_fpbv_sqrt	(	smt_astt	rd,
		smt_astt	rm )

overridevirtual

Convert the ieee arithmetic square-root (sqrt).

Parameters

op	the sqrt radicand
rm	the rounding mode

Returns: The newly created sqrt smt_ast

Reimplemented from fp_convt.

◆ mk_smt_fpbv_sub()

smt_astt z3_convt::mk_smt_fpbv_sub	(	smt_astt	lhs,
		smt_astt	rhs,
		smt_astt	rm )

overridevirtual

Convert a ieee subtraction.

Parameters

lhs	left hand side of the subtraction
rhs	right hand side of the subtraction
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_int()

smt_astt z3_convt::mk_smt_int ( const BigInt & theint )

overridevirtual

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_nearbyint_from_float()

smt_astt z3_convt::mk_smt_nearbyint_from_float	(	smt_astt	from,
		smt_astt	rm )

overridevirtual

Calculate the nearby int from a floating point, considering the rounding mode.

Parameters

from	the floating-point
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_real()

smt_astt z3_convt::mk_smt_real ( const std::string & str )

overridevirtual

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 z3_convt::mk_smt_symbol	(	const std::string &	name,
		const smt_sort *	s )

override

◆ mk_smt_typecast_from_fpbv_to_fpbv()

smt_astt z3_convt::mk_smt_typecast_from_fpbv_to_fpbv	(	smt_astt	from,
		smt_sortt	to,
		smt_astt	rm )

overridevirtual

Typecast from a floating point.

Parameters

from	the floating point being casted to floating-point
to	the floating-point resulting type
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_typecast_from_fpbv_to_sbv()

smt_astt z3_convt::mk_smt_typecast_from_fpbv_to_sbv	(	smt_astt	from,
		std::size_t	width )

overridevirtual

Typecast from a floating point.

Parameters

from	the floating point being casted to signed bitvector
to	the signed bitvector resulting type

Returns: The newly created cast smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_typecast_from_fpbv_to_ubv()

smt_astt z3_convt::mk_smt_typecast_from_fpbv_to_ubv	(	smt_astt	from,
		std::size_t	width )

overridevirtual

Typecast from a floating point.

Parameters

from	the floating point being casted to unsigned bitvector
to	the unsigned bitvector resulting type

Returns: The newly created cast smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_typecast_sbv_to_fpbv()

smt_astt z3_convt::mk_smt_typecast_sbv_to_fpbv	(	smt_astt	from,
		smt_sortt	to,
		smt_astt	rm )

overridevirtual

Typecast to a floating point.

Parameters

from	the signed bitvector being casted to a floating-point
cast	the floating-point resulting type
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_typecast_ubv_to_fpbv()

smt_astt z3_convt::mk_smt_typecast_ubv_to_fpbv	(	smt_astt	from,
		smt_sortt	to,
		smt_astt	rm )

overridevirtual

Typecast to a floating point.

Parameters

from	the unsigned bitvector being casted to a floating-point
cast	the floating-point resulting type
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented from fp_convt.

◆ mk_smt_uninterpreted_function()

smt_astt z3_convt::mk_smt_uninterpreted_function	(	const std::string &	name,
		const std::vector< smt_astt > &	args,
		smt_sortt	rangesort )

overridevirtual

Apply an uninterpreted function.

Declares (or reuses) a solver function symbol named name whose domain is the sorts of args and whose range is rangesort, then applies it to args. Every application sharing name resolves to the same declaration, so the solver enforces functional congruence (equal arguments imply an equal result) natively.

The default implementation Ackermannises the application (a fresh symbol plus congruence assumptions against earlier applications of the same name) for backends without native uninterpreted-function support. Solvers that expose UFs override this to declare and apply them directly.

Parameters

name	Stable (mangled) name of the function symbol.
args	The already-converted argument asts.
rangesort	The sort of the function's result.

Returns: The ast denoting name(args).

Reimplemented from smt_solver_baset.

◆ mk_store()

smt_astt z3_convt::mk_store	(	smt_astt	a,
		smt_astt	b,
		smt_astt	c )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_struct_sort()

smt_sortt z3_convt::mk_struct_sort ( const type2tc & type )

overridevirtual

Create a sort representing a struct.

i.e., a tuple. Ideally this should actually be part of the overridden tuple api, but due to history it isn't yet. If solvers don't support tuples, implement this to abort.

Parameters

type	The struct type to create a tuple representation of.

Returns: The tuple representation of the type, wrapped in an smt_sort.

Implements tuple_iface.

◆ mk_sub()

smt_astt z3_convt::mk_sub	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_tuple_array_symbol()

smt_astt z3_convt::mk_tuple_array_symbol ( const expr2tc & expr )

overridevirtual

Like mk_tuple_symbol, but for arrays.

Implements tuple_iface.

◆ mk_tuple_select()

z3::expr z3_convt::mk_tuple_select	(	const z3::expr &	t,
		unsigned	i )

◆ mk_tuple_symbol()

smt_astt z3_convt::mk_tuple_symbol	(	const std::string &	name,
		smt_sortt	s )

overridevirtual

Convert a symbol to a tuple_smt_ast.

Implements tuple_iface.

◆ mk_tuple_update()

z3::expr z3_convt::mk_tuple_update	(	const z3::expr &	t,
		unsigned	i,
		const z3::expr &	new_val )

◆ mk_xor()

smt_astt z3_convt::mk_xor	(	smt_astt	a,
		smt_astt	b )

overridevirtual

Reimplemented from smt_solver_baset.

◆ mk_zero_ext()

smt_astt z3_convt::mk_zero_ext	(	smt_astt	a,
		unsigned int	topwidth )

overridevirtual

Identical to mk_sign_ext, but extends AST with zeros.

Implements smt_solver_baset.

◆ output_smt()

void z3_convt::output_smt ( )

virtual

◆ overflow_arith()

smt_astt z3_convt::overflow_arith ( const expr2tc & expr )

overridevirtual

Detect integer arithmetic overflows.

Takes an expression that is one of add / sub / mul / div / modulus / shl, and evaluates whether its operation applied to its operands will result in an integer overflow or underflow.

Parameters

expr	Expression to test for arithmetic overflows in.

Returns: Boolean valued AST representing whether an overflow occurs.

Reimplemented from smt_solver_baset.

◆ pop_ctx()

void z3_convt::pop_ctx ( )

overridevirtual

Pop one context on the SMT assertion stack.

Reimplemented from smt_solver_baset.

◆ print_model()

void z3_convt::print_model ( )

overridevirtual

Method to print the SMT model.

Reimplemented from smt_solver_baset.

◆ push_ctx()

void z3_convt::push_ctx ( )

overridevirtual

Push one context on the SMT assertion stack.

Reimplemented from smt_solver_baset.

◆ solver_text()

const std::string z3_convt::solver_text ( )

inlineoverridevirtual

Solver name fetcher.

Returns a string naming the solver being used, and potentially it's version, if available.

Returns: The name of the solver this smt_solver_baset uses.

Implements smt_solver_baset.

◆ supports_assumptions()

bool z3_convt::supports_assumptions ( ) const

inlineoverridevirtual

Reimplemented from smt_solver_baset.

◆ tuple_array_create()

smt_astt z3_convt::tuple_array_create	(	const type2tc &	array_type,
		smt_astt *	input_args,
		bool	const_array,
		const smt_sort *	domain )

override

◆ tuple_array_of()

smt_astt z3_convt::tuple_array_of	(	const expr2tc &	init_value,
		unsigned long	domain_width )

overridevirtual

Create a potentially /large/ array of tuples.

This is called when we encounter an array_of operation, with a very large array size, of tuple sort.

Parameters

Expression	of tuple value to populate this array with.
domain_width	The size of array to create, in domain bits.

Returns: An AST representing an array of the tuple value, init_value.

Implements tuple_iface.

◆ tuple_create()

smt_astt z3_convt::tuple_create ( const expr2tc & structdef )

overridevirtual

Create a new tuple from a struct definition.

Parameters

structdef A constant_struct2tc, describing all the members of the tuple to create.

Returns: AST representing the created tuple

Implements tuple_iface.

◆ tuple_fresh()

smt_astt z3_convt::tuple_fresh	(	const smt_sort *	s,
		std::string	name = "" )

override

◆ tuple_get() [1/2]

expr2tc z3_convt::tuple_get ( const expr2tc & expr )

overridevirtual

Extract the assignment to a tuple-typed symbol from the SMT solvers model.

Implements tuple_iface.

◆ tuple_get() [2/2]

expr2tc z3_convt::tuple_get	(	const type2tc &	type,
		smt_astt	sym )

overridevirtual

Implements tuple_iface.

◆ tuple_get_array_elem()

expr2tc z3_convt::tuple_get_array_elem	(	smt_astt	array,
		uint64_t	index,
		const type2tc &	subtype )

overridevirtual

Implements tuple_iface.

Member Data Documentation

◆ solver

z3::solver z3_convt::solver

◆ z3_ctx

z3::context z3_convt::z3_ctx

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

src/solvers/z3/z3_conv.h
src/solvers/z3/z3_conv.cpp

Public Member Functions

Public Attributes

Additional Inherited Members

Constructor & Destructor Documentation

◆ z3_convt()

◆ ~z3_convt()

Member Function Documentation

◆ assert_ast()

◆ convert_array_of()

◆ dec_solve()

◆ dec_solve_assuming()

◆ dump_smt()

◆ get_array_elem()

◆ get_bool()

◆ get_bv()

◆ get_fpbv()

◆ get_rational()

◆ mk_add()

◆ mk_and()

◆ mk_array_sort()

◆ mk_array_symbol()

◆ mk_bool_sort()

◆ mk_bv_sort()

◆ mk_bvadd()

◆ mk_bvand()

◆ mk_bvashr()

◆ mk_bvfp_rm_sort()

◆ mk_bvfp_sort()

◆ mk_bvlshr()

◆ mk_bvmul()

◆ mk_bvneg()

◆ mk_bvnot()

◆ mk_bvor()

◆ mk_bvsdiv()

◆ mk_bvsge()

◆ mk_bvsgt()

◆ mk_bvshl()

◆ mk_bvsle()

◆ mk_bvslt()

◆ mk_bvsmod()

◆ mk_bvsub()

◆ mk_bvudiv()

◆ mk_bvuge()

◆ mk_bvugt()

◆ mk_bvule()

◆ mk_bvult()

◆ mk_bvumod()

◆ mk_bvxor()

◆ mk_concat()

◆ mk_div()

◆ mk_eq()

◆ mk_extract()

◆ mk_fbv_sort()

◆ mk_fpbv_rm_sort()

◆ mk_fpbv_sort()

◆ mk_from_bv_to_fp()

◆ mk_from_fp_to_bv()

◆ mk_ge()

◆ mk_gt()

◆ mk_implies()

◆ mk_int2real()

◆ mk_int_sort()

◆ mk_isint()

◆ mk_ite()

◆ mk_le()

◆ mk_lt()

◆ mk_mod()

◆ mk_mul()

◆ mk_neg()

◆ mk_neq()

◆ mk_not()

◆ mk_or()

◆ mk_quantifier()

◆ mk_real2int()

◆ mk_real_sort()

◆ mk_select()

◆ mk_shl()

◆ mk_sign_ext()

◆ mk_smt_bool()

◆ mk_smt_bv()