smt_solver_baset Class Reference

The base SMT-conversion class/interface. More...

#include <smt_solver.h>

Inheritance diagram for smt_solver_baset:

Classes
struct	flat_storet
	One element update an array with denotes, as an index into the array's flattened form and the value stored there. More...
struct	smt_cache_entryt
struct	uf_ackermann_entry
	One recorded uninterpreted-function application in the Ackermannisation fallback: the argument asts, the fresh result ast, and the context level at which it was created (so it can be pruned on the matching pop, since pop_ctx deletes the asts made since the push). More...
struct	ptr_flatten_entry
	One pointer flattened to its machine representation by a bitcast. More...

Public Types
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
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 ()
External API to smt_solver_baset.
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.
Internal conversion API between smt_solver_baset and solver
converter
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.
virtual smt_astt	mk_smt_int (const BigInt &theint)=0
	Create an integer smt_ast.
virtual smt_astt	mk_smt_real (const std::string &str)=0
	Create a real in a smt_ast.
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_bool (bool val)=0
	Create a boolean.
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.
Integer overflow solver-converter API.
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.
Array operations solver-converter API.
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.

Public Attributes
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

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

Internal foo.
std::set< std::pair< expr2tc, expr2tc > >	divided_operand_pairs
	Operand pairs of every division seen by note_division_operands.
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 ()

Detailed Description

The base SMT-conversion class/interface.

smt_solver_baset handles a number of decisions that must be made when deconstructing ESBMC expressions down into SMT representation. See smt_conv.h for more high level documentation of this.

The basic flow is thus: a class that can create SMT formula in some solver subclasses smt_solver_baset, implementing abstract methods, in particular mk_func_app. The rest of ESBMC then calls convert with an expression, and this class deconstructs it into a series of applications, as documented by the smt_func_kind enumeration. These are then created via mk_func_app or some more specific method calls. Boolean sorted ASTs are then asserted into the solver context.

The exact lifetime of smt asts here is currently undefined, unfortunately, although smt_solver_baset posesses a cache, so they generally have a reference in there. This will probably be fixed in the future.

In theory this class supports pushing and popping of solver contexts, although of course that depends too on the subclass supporting it. However, this hasn't really been tested since everything here was rewritten from The Old Way, so don't trust it.

While mk_func_app is supposed to be the primary interface to making SMT function applications, in some cases we want to introduce some abstractions, and this becomes unweildy. Thus, tuple and array operations are performed via virtual function calls. By default, array operations are then passed through to mk_func_app, while tuples are decomposed into sets of variables which are then created through mk_func_app. If this isn't what a solver wants to happen, it can override this and handle that itself. The idea is that, in the manner of metaSMT, you can then compose a series of subclasses that perform the desired amount of flattening, and then work from there. (Some of this is still WIP though).

NB: the whole smt_asts-are-const situation needs to be resolved too.

See also

smt_conv.h

smt_func_kind

Member Typedef Documentation

ast_vec

typedef std::vector<smt_astt> smt_solver_baset::ast_vec

Shorthand for a vector of smt_ast's.

renumber_mapt

typedef std::map<std::string, smt_astt> smt_solver_baset::renumber_mapt

smt_cachet

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_solver_baset::smt_cachet

smt_sort_cachet

typedef std::unordered_map<type2tc, smt_sortt, type2_hash> smt_solver_baset::smt_sort_cachet

Constructor & Destructor Documentation

smt_solver_baset()

smt_solver_baset::smt_solver_baset	(	const namespacet &	_ns,
		const optionst &	_options )

Primary constructor.

After construction, smt_post_init must be called before the object is used as a solver converter.

Parameters

_ns	Namespace for looking up the type of certain symbols.
_options	Provide all the needed parameters to configure the solver.

~smt_solver_baset()

smt_solver_baset::~smt_solver_baset ( )

virtualdefault

Member Function Documentation

apply_ieee754_semantics()

smt_astt smt_solver_baset::apply_ieee754_semantics ( smt_astt real_result, const floatbv_type2t & fbv_type, smt_astt operand_zero_check = nullptr, const expr2tc & rounding_mode = expr2tc() )

virtual

Applies IEEE 754 floating-point semantics to a real arithmetic result.

Handles overflow, underflow, and subnormal number behaviors that are missing when using integer/real encoding for floating-point operations. Supports both IEEE 754 single precision (32-bit: 8 exponent, 23 fraction) and double precision (64-bit: 11 exponent, 52 fraction) formats. For double precision: overflow to ±1.798e+308, underflow below 4.941e-324, subnormal range [4.941e-324, 2.225e-308). For single precision: overflow to ±3.403e+38, underflow below 1.401e-45, subnormal range [1.401e-45, 1.175e-38). Other formats return the original result unchanged. Under –ir-ieee, when rounding_mode is a concrete round-to-nearest constant (ROUND_TO_EVEN == 0), a tight symmetric epsilon enclosure is asserted. For symbolic or directed rounding modes the function falls back to a weak unconstrained enclosure (sound but imprecise); tight directed bounds are deferred to a future PR.

Parameters

real_result	The result of exact real arithmetic operation
fbv_type	The floating-point type information (exponent/fraction bits)
operand_zero_check	Optional boolean AST for special zero handling (e.g., multiplication where either operand is zero should yield zero regardless of the other operand, even if it would cause underflow)
rounding_mode	The rounding mode expr2tc from the IR operation node; typically a constant_int2t or the __ESBMC_rounding_mode symbol.

Returns

SMT AST representing the result with IEEE 754 semantics applied

array_create()

smt_astt smt_solver_baset::array_create

(

const expr2tc &

expr

)

Convert constant_array2tc's and constant_array_of2tc's.

array_domain_to_width()

expr2tc smt_solver_baset::array_domain_to_width

(

const type2tc &

type

)

Fetch the number of elements in an array (the domain).

assert_ast()

virtual void smt_solver_baset::assert_ast ( smt_astt a )

pure virtual

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.

Implemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

assert_expr()

void smt_solver_baset::assert_expr

(

const expr2tc &

e

)

Convert the given expr to AST, then assert that AST.

begin_step()

void smt_solver_baset::begin_step	(	const expr2tc &	guard,
		const expr2tc &	cond )

bump_addrspace_array()

void smt_solver_baset::bump_addrspace_array	(	unsigned int	idx,
		const expr2tc &	val )

convert_addr_of()

smt_astt smt_solver_baset::convert_addr_of

(

const expr2tc &

expr

)

Take the address of some kind of expression.

This will abort if the given expression isn't based on some symbol in some way. (i.e., you can't take the address of an addition, but you can take the address of a member of a struct, for example).

convert_array_index()

smt_astt smt_solver_baset::convert_array_index ( const expr2tc & expr )

virtual

High level index expression conversion.

Deals with several annoying corner cases that must be addressed, such as flattening multidimensional arrays into one domain sort, or turning bool arrays into bit arrays. XXX, why is this virtual?

Parameters

expr	An index2tc expression to convert to an SMT AST.

Returns

An AST representing the index operation in the expression.

convert_array_of_prep()

smt_astt smt_solver_baset::convert_array_of_prep

(

const expr2tc &

expr

)

Prepare an array_of expression by flattening its dimensions, if it has more than one.

convert_array_store()

smt_astt smt_solver_baset::convert_array_store ( const expr2tc & expr )

virtual

Partner method to convert_array_index, for stores.

XXX, why is this virtual?

Parameters

expr	with2tc operation to convert to SMT.

Returns

AST representing the result of evaluating expr.

convert_assign()

smt_astt smt_solver_baset::convert_assign

(

const expr2tc &

expr

)

convert_ast() [1/2]

smt_astt smt_solver_baset::convert_ast

(

const expr2tc &

expr

)

Main interface to SMT conversion.

Takes one expression, and converts it into the underlying SMT solver, returning a single smt_ast that represents the converted expressions value. The lifetime of the returned pointer is currently undefined.

Parameters

expr	The expression to convert into the SMT solver

Returns

The resulting handle to the SMT value.

convert_ast() [2/2]

smt_astt smt_solver_baset::convert_ast	(	const expr2tc &	expr,
		const type2tc &	type,
		smt_astt const *	args,
		struct expr_op_convert	ops )

Interface to specifig SMT conversion.

Takes one expression, and converts it into the underlying SMT solver, depending on the type of the expression.

Parameters

expr	The expression to convert into the SMT solver
type	The expression's type
args	The expression's args
ops	The operations for each sort type

Returns

The resulting handle to the SMT value.

convert_ast_node()

smt_astt smt_solver_baset::convert_ast_node

(

const expr2tc &

expr

)

Convert a single node, assuming its operands are already in the cache.

This is the per-node body of the conversion; convert_ast() drives it with an explicit-stack post-order walk so that deeply left-nested associative chains (e.g. a huge disjunction) don't recurse one C++ frame per level and overflow the stack. The operand walk inside this body therefore hits the cache instead of recursing.

convert_bitcast()

smt_astt smt_solver_baset::convert_bitcast

(

const expr2tc &

expr

)

Convert a bitcast2tc, converting an expr to its bit representation.

convert_bitcast_to_fp()

smt_astt smt_solver_baset::convert_bitcast_to_fp	(	const expr2tc &	from,
		const type2tc &	to_type )

Read a floating-point value from the bits of from.

Null when those bits are not in a form this can take apart.

convert_bitcast_to_struct()

smt_astt smt_solver_baset::convert_bitcast_to_struct	(	const expr2tc &	from,
		const type2tc &	to_type )

Rebuild a struct from the bits of from, member by member.

Null when those bits are not in a form this can take apart.

convert_bswap()

smt_astt smt_solver_baset::convert_bswap

(

const expr2tc &

expr

)

Converts bswap representation.

convert_byte_extract()

smt_astt smt_solver_baset::convert_byte_extract

(

const expr2tc &

expr

)

Convert a byte_extract2tc, pulling a byte from the byte representation of some piece of data.

convert_byte_extract_bv_mode()

smt_astt smt_solver_baset::convert_byte_extract_bv_mode	(	const byte_extract2t &	data,
		expr2tc	source,
		expr2tc	offs,
		unsigned int	src_width )

convert_byte_extract_int_mode()

smt_astt smt_solver_baset::convert_byte_extract_int_mode	(	const byte_extract2t &	data,
		expr2tc	source,
		expr2tc	offs,
		unsigned int	src_width )

convert_byte_update()

smt_astt smt_solver_baset::convert_byte_update

(

const expr2tc &

expr

)

Convert a byte_update2tc, inserting a byte into the byte representation of some piece of data.

convert_byte_update_bv_mode()

smt_astt smt_solver_baset::convert_byte_update_bv_mode

(

const byte_update2t &

data

)

Convert a byte_update2tc using bitvector operations, preserving the original bitvector-based implementation.

convert_byte_update_int_mode()

smt_astt smt_solver_baset::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.

convert_byte_update_int_mode_expr()

expr2tc smt_solver_baset::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.

convert_concat_int_mode()

smt_astt smt_solver_baset::convert_concat_int_mode	(	smt_astt	left_ast,
		smt_astt	right_ast,
		const expr2tc &	expr )

convert_identifier_pointer()

smt_astt smt_solver_baset::convert_identifier_pointer	(	const expr2tc &	expr,
		const std::string &	sym,
		const typet *	type )

Convert an identifier to a pointer.

When given the name of a variable that we want to take the address of, this inspects our current tracking of addresses / variables, and returns a pointer for the given symbol. If it hasn't had its address taken before, it performs any computations or address space juggling required to make a new pointer.

Parameters

expr	The symbol2tc expression of this symbol.
sym	The textual representation of this symbol.
type	Optionally a pointer to the type of the symbol in the context.

Returns

A pointer-typed AST representing the address of this symbol.

convert_ieee_arith_2op()

smt_astt smt_solver_baset::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.

convert_is_finite()

smt_astt smt_solver_baset::convert_is_finite

(

const expr2tc &

expr

)

Checks for equality with finite representation.

convert_is_inf()

smt_astt smt_solver_baset::convert_is_inf

(

const expr2tc &

expr

)

Checks for equality with inf representation.

convert_is_nan()

smt_astt smt_solver_baset::convert_is_nan

(

const expr2tc &

expr

)

Checks for equality with NaN representation.

convert_is_normal()

smt_astt smt_solver_baset::convert_is_normal

(

const expr2tc &

expr

)

Checks for equality with normal representation.

convert_member()

smt_astt smt_solver_baset::convert_member

(

const expr2tc &

expr

)

Handle union/struct based corner cases for member2tc expressions.

convert_modulus()

smt_astt smt_solver_baset::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.

Encode a remainder: compositional as a - (a / b) * b when the formula also divides the same operands, the rem primitive otherwise.

convert_pointer_arith()

smt_astt smt_solver_baset::convert_pointer_arith	(	const expr2tc &	expr,
		const type2tc &	t )

Flatten pointer arithmetic.

When faced with an addition or subtraction between a pointer and some integer or other pointer, perform whatever multiplications or casting is required to honor the C semantics of pointer arith.

convert_pointer_bitcast()

smt_astt smt_solver_baset::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.

The pointer leg of convert_bitcast.

Each returns null when it does not apply.

Null when neither side is a pointer whose representation this pair can carry.

convert_popcount()

smt_astt smt_solver_baset::convert_popcount

(

const expr2tc &

expr

)

Converts popcount representation.

convert_ptr_cmp()

smt_astt smt_solver_baset::convert_ptr_cmp	(	const expr2tc &	expr,
		const expr2tc &	expr2,
		const expr2tc &	templ_expr )

Compare two pointers.

This attempts to optimize cases where we can avoid comparing the integer representation of a pointer, as that's hugely inefficient sometimes (and gets bitblasted).

Parameters

expr	First pointer to compare
expr2	Second pointer to compare
templ_expr	The comparision expression – this method will look at the kind of comparison being performed, and make an appropriate decision.

Returns

Boolean valued AST as appropriate to the requested comparision

convert_rounding_mode()

smt_astt smt_solver_baset::convert_rounding_mode

(

const expr2tc &

expr

)

Converts rounding mode for ieee fp operations.

convert_signbit()

smt_astt smt_solver_baset::convert_signbit

(

const expr2tc &

expr

)

Converts signbit representation.

convert_sort()

smt_sortt smt_solver_baset::convert_sort

(

const type2tc &

type

)

Convert a type2tc into an smt_sort.

This dispatches control to the appropriate method in the subclassing solver converter for type conversion

convert_terminal()

smt_astt smt_solver_baset::convert_terminal

(

const expr2tc &

expr

)

Convert a terminal expression into an SMT AST.

This dispatches control to the appropriate method in the subclassing solver converter for the terminal conversion

convert_typecast()

smt_astt smt_solver_baset::convert_typecast

(

const expr2tc &

expr

)

Despatch a typecast expression to a more specific typecast method.

convert_typecast_from_fpbv()

smt_astt smt_solver_baset::convert_typecast_from_fpbv

(

const typecast2t &

cast

)

Typecast from a floatbv.

convert_typecast_from_ptr()

smt_astt smt_solver_baset::convert_typecast_from_ptr

(

const typecast2t &

cast

)

Typecast a pointer to an integer.

convert_typecast_to_bool()

smt_astt smt_solver_baset::convert_typecast_to_bool

(

const typecast2t &

cast

)

Typecast data to bools.

convert_typecast_to_fixedbv_nonint()

smt_astt smt_solver_baset::convert_typecast_to_fixedbv_nonint

(

const expr2tc &

cast

)

Typecast to a fixedbv in bitvector mode.

convert_typecast_to_fixedbv_nonint_from_bool()

smt_astt smt_solver_baset::convert_typecast_to_fixedbv_nonint_from_bool

(

const expr2tc &

cast

)

convert_typecast_to_fixedbv_nonint_from_bv()

smt_astt smt_solver_baset::convert_typecast_to_fixedbv_nonint_from_bv

(

const expr2tc &

cast

)

convert_typecast_to_fixedbv_nonint_from_fixedbv()

smt_astt smt_solver_baset::convert_typecast_to_fixedbv_nonint_from_fixedbv

(

const expr2tc &

cast

)

convert_typecast_to_fpbv()

smt_astt smt_solver_baset::convert_typecast_to_fpbv

(

const typecast2t &

cast

)

Typecast to a floatbv.

convert_typecast_to_ints()

smt_astt smt_solver_baset::convert_typecast_to_ints

(

const typecast2t &

cast

)

Typecast anything to an integer (but not pointers).

convert_typecast_to_ints_from_bool()

smt_astt smt_solver_baset::convert_typecast_to_ints_from_bool

(

const typecast2t &

cast

)

convert_typecast_to_ints_from_fbv_sint()

smt_astt smt_solver_baset::convert_typecast_to_ints_from_fbv_sint

(

const typecast2t &

cast

)

convert_typecast_to_ints_from_unsigned()

smt_astt smt_solver_baset::convert_typecast_to_ints_from_unsigned

(

const typecast2t &

cast

)

convert_typecast_to_ints_intmode()

smt_astt smt_solver_baset::convert_typecast_to_ints_intmode

(

const typecast2t &

cast

)

convert_typecast_to_ptr()

smt_astt smt_solver_baset::convert_typecast_to_ptr

(

const typecast2t &

cast

)

Typecast something (i.e.

an integer) to a pointer

convert_typecast_to_struct()

smt_astt smt_solver_baset::convert_typecast_to_struct

(

const typecast2t &

cast

)

Typecast structs to other structs.

create_int_right_shift()

expr2tc smt_solver_baset::create_int_right_shift	(	expr2tc	source,
		expr2tc	shift_amount )

dec_solve()

virtual smt_resultt smt_solver_baset::dec_solve ( )

pure virtual

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.

Implemented in bitwuzla_convt, bitwuzllob_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, minisat_convt, neurosym_convt, smtlib_convt, yices_convt, and z3_convt.

dec_solve_assuming()

smt_resultt smt_solver_baset::dec_solve_assuming ( const ast_vec & assumptions )

virtual

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

Backends without support abort; check supports_assumptions().

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, yices_convt, and z3_convt.

decode_pointer_repr()

smt_astt smt_solver_baset::decode_pointer_repr	(	const expr2tc &	repr,
		const type2tc &	to_type )

decompose_select_chain()

expr2tc smt_solver_baset::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.

Works in conjunction with flatten_array_type.

decompose_store_chain()

expr2tc smt_solver_baset::decompose_store_chain	(	const expr2tc &	expr,
		expr2tc &	base )

Like decompose_select_chain, but for multidimensional stores.

decompose_stores()

bool smt_solver_baset::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.

Unlike decompose_store_chain(), keeps every store a row carries.

define()

void smt_solver_baset::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.

Falls back to convert_assign for aggregates or a symbol that was already converted.

delete_all_asts()

void smt_solver_baset::delete_all_asts

(

)

divide_by_element_size()

smt_astt smt_solver_baset::divide_by_element_size	(	const expr2tc &	diff,
		const expr2tc &	size )

The quotient of a signed byte difference by an element size, truncated toward zero.

A size of 2^k is an arithmetic shift of the difference, biased by 2^k - 1 when negative since the shift rounds toward -inf; k < width - 1 keeps the divisor positive when read signed.

dump_expr()

void smt_solver_baset::dump_expr

(

const expr2tc &

expr

)

Convert expr and dump the resulting SMT AST in SMT format.

Used by –ssa-smt-trace so callers outside the solver layer can request the dump without ever touching smt_astt.

dump_smt()

std::string smt_solver_baset::dump_smt ( )

virtual

Method to dump the SMT formula.

Reimplemented in bitwuzla_convt, bitwuzllob_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, neurosym_convt, smtlib_convt, and z3_convt.

encode_pointer_repr()

smt_astt smt_solver_baset::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.

end_step()

void smt_solver_baset::end_step

(

)

expand_row_stores()

void smt_solver_baset::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.

Requires the row's stride to be a compile-time constant, which both call sites establish.

finalize_pointer_chain()

void smt_solver_baset::finalize_pointer_chain

(

unsigned int

obj_num

)

Create and assert address space constraints on the given object ID number.

Essentially, this asserts that all the objects to date don't overlap with /this/ one.

fix_array_idx()

expr2tc smt_solver_baset::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.

flatten_array_type()

type2tc smt_solver_baset::flatten_array_type

(

const type2tc &

type

)

For a multi-dimensional array, convert the type into a single dimension array.

This works by concatenating the domain widths together into one large domain.

get()

expr2tc smt_solver_baset::get ( const expr2tc & expr )

virtual

get_array() [1/2]

expr2tc smt_solver_baset::get_array

(

const expr2tc &

expr

)

get_array() [2/2]

expr2tc smt_solver_baset::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.

get_bool()

virtual tvt smt_solver_baset::get_bool ( smt_astt a )

pure virtual

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.

Implemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, neurosym_convt, smtlib_convt, yices_convt, and z3_convt.

get_bv()

virtual BigInt smt_solver_baset::get_bv ( smt_astt a, bool is_signed )

pure virtual

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

Implemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, neurosym_convt, smtlib_convt, yices_convt, and z3_convt.

get_by_ast() [1/2]

expr2tc smt_solver_baset::get_by_ast

(

const expr2tc &

expr

)

Resolve expr's model value through its converted AST.

Unlike get_by_type, the struct/pointer case goes through the AST-based tuple getter, so expr need not be a symbol (it may be a member / index access). Lets external callers fetch aggregate values without ever naming smt_astt.

get_by_ast() [2/2]

expr2tc smt_solver_baset::get_by_ast ( const type2tc & type, smt_astt a )

virtual

Get the satisfying assignment using the ast.

Parameters

a	Variable to get the value of.
type	The variable type.

Returns

Explicit assigned value of expr in the solver. May be nil, in which case the solver did not assign a value to it for some reason.

get_by_type()

expr2tc smt_solver_baset::get_by_type ( const expr2tc & expr )

virtual

Get the satisfying assignment using the type.

Parameters

expr	Variable to get the value of. Must be a symbol expression.

Returns

Explicit assigned value of expr in the solver. May be nil, in which case the solver did not assign a value to it for some reason.

get_by_value()

expr2tc smt_solver_baset::get_by_value	(	const type2tc &	type,
		BigInt	value )

Builds the bitvector based on the value retrieved from the solver.

Parameters

type	the type (fixedbv or (un)signedbv),
value	the value retrieved from the solver.

Returns

Expression representation of a's value

get_cur_addrspace_ident()

std::string smt_solver_baset::get_cur_addrspace_ident

(

)

Get the symbol name for the current address-allocation record array.

get_double_eps_rel()

smt_astt smt_solver_baset::get_double_eps_rel

(

)

get_double_eps_up()

smt_astt smt_solver_baset::get_double_eps_up

(

)

get_double_inf_sentinel()

smt_astt smt_solver_baset::get_double_inf_sentinel

(

)

get_double_max_normal()

smt_astt smt_solver_baset::get_double_max_normal

(

)

get_double_min_normal()

smt_astt smt_solver_baset::get_double_min_normal

(

)

get_double_min_subnormal()

smt_astt smt_solver_baset::get_double_min_subnormal

(

)

get_flattened_array_subtype()

type2tc smt_solver_baset::get_flattened_array_subtype

(

const type2tc &

type

)

Get the base subtype of an array, delving through any intermediate multidimensional arrays.

get_index()

std::optional< expr2tc > smt_solver_baset::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.

get_index_value()

std::optional< expr2tc > smt_solver_baset::get_index_value	(	const expr2tc &	expr,
		expr2tc &	res )

Fetch a satisfying assignment from the solver.

If a previous call to dec_solve returned satisfiable, then the solver has a set of assignments to symbols / variables used in the formula. This method retrieves the value of a symbol, and formats it into an ESBMC expression.

Parameters

expr	Variable to get the value of. Must be a symbol expression.

Returns

Explicit assigned value of expr in the solver. May be nil, in which case the solver did not assign a value to it for some reason. get()'s index_id case: read one element out of the solver's array model rather than materialising the whole array. Nullopt where the case falls through to get()'s generic tail.

get_member_name_field() [1/2]

unsigned int smt_solver_baset::get_member_name_field	(	const type2tc &	t,
		const expr2tc &	name ) const

get_member_name_field() [2/2]

unsigned int smt_solver_baset::get_member_name_field	(	const type2tc &	t,
		const irep_idt &	name ) const

get_rational()

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

inlinevirtual

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 in z3_convt.

get_single_eps_rel()

smt_astt smt_solver_baset::get_single_eps_rel

(

)

get_single_eps_up()

smt_astt smt_solver_baset::get_single_eps_up

(

)

get_single_inf_sentinel()

smt_astt smt_solver_baset::get_single_inf_sentinel

(

)

get_single_max_normal()

smt_astt smt_solver_baset::get_single_max_normal

(

)

get_single_min_normal()

smt_astt smt_solver_baset::get_single_min_normal

(

)

get_single_min_subnormal()

smt_astt smt_solver_baset::get_single_min_subnormal

(

)

get_zero_real()

smt_astt smt_solver_baset::get_zero_real

(

)

has_model()

virtual bool smt_solver_baset::has_model ( ) const

inlinevirtual

Whether a satisfiable result can be turned into a model.

False for the subprocess SMT-LIB backends with no interactive model solver attached: they answer sat/unsat, but get() and l_get() have nothing to read.

Reimplemented in neurosym_convt, and smtlib_convt.

imply_ast()

smt_astt smt_solver_baset::imply_ast	(	smt_astt	a,
		smt_astt	b )

Create an ipmlication between two smt_ast's.

Parameters

a	The ast that implies the truth of the other. Boolean.
b	The ast whos truth is implied. Boolean.

Returns

The resulting piece of AST.

init_addr_space_array()

void smt_solver_baset::init_addr_space_array

(

)

Initialize tracking data for the address space records.

This also sets up the symbols / addresses of 'NULL', '0', and the invalid pointer

init_pointer_obj()

smt_astt smt_solver_baset::init_pointer_obj	(	unsigned int	obj_num,
		const expr2tc &	size,
		const typet *	type,
		bool	may_be_freed )

Parameters

may_be_freed

The object is heap-allocated: once freed it stops keeping later objects off its addresses.

invert_ast()

smt_astt smt_solver_baset::invert_ast

(

smt_astt

a

)

Create the inverse of an smt_ast.

Equivalent to a 'not' operation.

Parameters

a	The ast to invert. Must be boolean sorted.

Returns

The inverted piece of AST.

l_get() [1/2]

tvt smt_solver_baset::l_get

(

const expr2tc &

expr

)

Fetch the value of a boolean expression from the current model.

l_get() [2/2]

tvt smt_solver_baset::l_get ( smt_astt a )

virtual

Fetch the value of a boolean sorted smt_ast.

(The 'l' is for literal, and is historic). Returns a three valued result, of true, false, or unassigned.

Parameters

a	The boolean sorted ast to fetch the value of.

Returns

A three-valued return val, of the assignment to a.

Reimplemented in neurosym_convt, and smtlib_convt.

make_bit_bool()

smt_astt smt_solver_baset::make_bit_bool

(

smt_astt

a

)

Convert a bitvector with one bit to a boolean.

make_bool_bit()

smt_astt smt_solver_baset::make_bool_bit

(

smt_astt

a

)

Convert a boolean to a bitvector with one bit.

make_n_ary_and()

smt_astt smt_solver_baset::make_n_ary_and

(

const ast_vec &

v

)

make_n_ary_or()

smt_astt smt_solver_baset::make_n_ary_or

(

const ast_vec &

v

)

mk_add()

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

virtual

Reimplemented in cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_and()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_array_sort()

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

virtual

Create an array sort.

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bool_sort()

smt_sortt smt_solver_baset::mk_bool_sort ( )

virtual

Create a bool sort.

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bv_sort()

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

virtual

Create a bv sort.

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvadd()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvand()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvashr()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvfp_rm_sort()

smt_sortt smt_solver_baset::mk_bvfp_rm_sort ( )

virtual

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

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvfp_sort()

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

virtual

Create a floating-point sort, using bitvectors.

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvlshr()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvmul()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvneg()

smt_astt smt_solver_baset::mk_bvneg ( smt_astt a )

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvnot()

smt_astt smt_solver_baset::mk_bvnot ( smt_astt a )

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvor()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvredand()

smt_astt smt_solver_baset::mk_bvredand

(

smt_astt

op

)

Reduction and: equals bit1 iff all bits are 1.

Parameters

op	the expr to be reduced

Returns

reduced op

mk_bvredor()

smt_astt smt_solver_baset::mk_bvredor

(

smt_astt

op

)

Reduction or: equals bit0 iff all bits are 0.

Parameters

op	the expr to be reduced

Returns

reduced op

mk_bvsdiv()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvsge()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvsgt()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvshl()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvsle()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvslt()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvsmod()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvsub()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvudiv()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvuge()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvugt()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvule()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvult()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvumod()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_bvxor()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_concat()

virtual smt_astt smt_solver_baset::mk_concat ( smt_astt a, smt_astt b )

pure virtual

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

Implemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_div()

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

virtual

Reimplemented in cvc5_convt, cvc_convt, smtlib_convt, yices_convt, and z3_convt.

mk_eq()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_extract()

virtual smt_astt smt_solver_baset::mk_extract ( smt_astt a, unsigned int high, unsigned int low )

pure virtual

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.

Implemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_fbv_sort()

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

virtual

Create a fixed-point sort.

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_fresh()

smt_astt smt_solver_baset::mk_fresh ( smt_sortt s, const std::string & tag, smt_sortt st = nullptr )

virtual

Create a free variable with the given sort, and a unique name, with the prefix given in 'tag'.

mk_fresh_name()

std::string smt_solver_baset::mk_fresh_name

(

const std::string &

tag

)

Create a previously un-used variable name with the prefix given in tag.

mk_ge()

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

virtual

Reimplemented in cvc5_convt, cvc_convt, smtlib_convt, yices_convt, and z3_convt.

mk_gt()

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

virtual

Reimplemented in cvc5_convt, cvc_convt, smtlib_convt, yices_convt, and z3_convt.

mk_implies()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_int2real()

smt_astt smt_solver_baset::mk_int2real ( smt_astt a )

virtual

Reimplemented in cvc5_convt, cvc_convt, smtlib_convt, and z3_convt.

mk_int_bv_sort()

smt_sortt smt_solver_baset::mk_int_bv_sort ( std::size_t width )

inline

Create an integer or SBV/UBV sort.

mk_int_sort()

smt_sortt smt_solver_baset::mk_int_sort ( )

virtual

Create a int sort.

Reimplemented in cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_isint()

smt_astt smt_solver_baset::mk_isint ( smt_astt a )

virtual

Reimplemented in cvc5_convt, cvc_convt, smtlib_convt, yices_convt, and z3_convt.

mk_ite()

virtual smt_astt smt_solver_baset::mk_ite ( smt_astt cond, smt_astt t, smt_astt f )

pure virtual

Create an ite operation.

Parameters

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

Returns

an ite expression

Implemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_le()

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

virtual

Reimplemented in cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_lt()

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

virtual

Reimplemented in cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_mod()

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

virtual

Reimplemented in cvc5_convt, cvc_convt, smtlib_convt, yices_convt, and z3_convt.

mk_mul()

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

virtual

Reimplemented in cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_neg()

smt_astt smt_solver_baset::mk_neg ( smt_astt a )

virtual

Reimplemented in cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_neq()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, yices_convt, and z3_convt.

mk_not()

smt_astt smt_solver_baset::mk_not ( smt_astt a )

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_or()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_quantifier()

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

inlinevirtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, and z3_convt.

mk_real2int()

smt_astt smt_solver_baset::mk_real2int ( smt_astt a )

virtual

Reimplemented in cvc5_convt, cvc_convt, smtlib_convt, and z3_convt.

mk_real_fp_sort()

smt_sortt smt_solver_baset::mk_real_fp_sort ( std::size_t ew, std::size_t sw )

inline

Create an real or floating-point/fixed-point sort.

mk_real_sort()

smt_sortt smt_solver_baset::mk_real_sort ( )

virtual

Create a real sort.

Reimplemented in cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_select()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_shl()

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

virtual

Reimplemented in cvc5_convt, cvc_convt, smtlib_convt, yices_convt, and z3_convt.

mk_sign_ext()

virtual smt_astt smt_solver_baset::mk_sign_ext ( smt_astt a, unsigned int topwidth )

pure virtual

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.

Implemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_smt_bool()

virtual smt_astt smt_solver_baset::mk_smt_bool ( bool val )

pure virtual

Create a boolean.

Parameters

val	Whether to create a true or false boolean.

Returns

The newly created terminal smt_ast of this boolean.

Implemented in bitblast_convt, bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_smt_bv() [1/2]

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

pure virtual

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.

Implemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_smt_bv() [2/2]

virtual smt_astt smt_solver_baset::mk_smt_bv ( const BigInt & theint, std::size_t w )

inlinevirtual

Create a bitvector.

Parameters

theint	Integer representation of the bitvector. Any excess bits in the stored integer should be ignored.
w	Width, in bits, of the bitvector to create.

Returns

The newly created terminal smt_ast of this bitvector.

mk_smt_int()

virtual smt_astt smt_solver_baset::mk_smt_int ( const BigInt & theint )

pure 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.

Implemented in bitblast_convt, bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_smt_real()

virtual smt_astt smt_solver_baset::mk_smt_real ( const std::string & str )

pure 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.

Implemented in bitblast_convt, bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_smt_symbol()

virtual smt_astt smt_solver_baset::mk_smt_symbol ( const std::string & name, smt_sortt s )

pure virtual

Create a symbol / variable.

These correspond to renamed SSA variables in the SSA program, although any other names can be used too, so long as they don't conflict with anything else.

Parameters

name	Textual name of the symbol to create.
s	The sort of the symbol we're creating.
The	newly created terminal smt_ast of this symbol.

mk_smt_uninterpreted_function()

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

virtual

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 in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_store()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_sub()

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

virtual

Reimplemented in cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_subnormal_flush()

smt_astt smt_solver_baset::mk_subnormal_flush	(	smt_astt	r,
		const floatbv_type2t &	fbv_type,
		const expr2tc &	rounding_mode )

mk_truncated_div()

smt_astt smt_solver_baset::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).

mk_truncated_rem()

smt_astt smt_solver_baset::mk_truncated_rem	(	const type2tc &	type,
		smt_astt	a,
		smt_astt	b )

mk_xor()

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

virtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

mk_zero_ext()

virtual smt_astt smt_solver_baset::mk_zero_ext ( smt_astt a, unsigned int topwidth )

pure virtual

Identical to mk_sign_ext, but extends AST with zeros.

Implemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

new_solver_ast()

template<typename the_solver_ast>

smt_astt smt_solver_baset::new_solver_ast ( typename the_solver_ast::solver_ast_type ast, smt_sortt sort )

inline

note_assignment()

void smt_solver_baset::note_assignment	(	const expr2tc &	lhs,
		const expr2tc &	rhs )

note_division_operands()

void smt_solver_baset::note_division_operands	(	const expr2tc &	expr,
		std::unordered_set< const expr2t * > &	seen )

Record every division's operand pair in expr, recursively.

convert_modulus lowers a remainder compositionally only when its operands appear here; unconditional lowering costs 3-5x on rem-heavy proofs.

overflow_arith()

smt_astt smt_solver_baset::overflow_arith ( const expr2tc & expr )

virtual

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 in bitwuzla_convt, boolector_convt, and z3_convt.

overflow_cast()

smt_astt smt_solver_baset::overflow_cast ( const expr2tc & expr )

virtual

Detect integer overflows in a cast.

Takes a typecast2tc as an argument, and if it causes a decrease in integer width, then encodes a test that the dropped bits are never significant / used.

Parameters

expr	Cast to test for dropped / overflowed data in.

Returns

Boolean valued AST representing whether an overflow occurs.

overflow_neg()

smt_astt smt_solver_baset::overflow_neg ( const expr2tc & expr )

virtual

Detects integer overflows in negation.

This only tests for the case where MIN_INT is being negated, in which case there is no positive representation of that number, and an overflow occurs. Evaluates to true if that can occur in the operand.

Parameters

expr	A neg2tc to test for overflows in.

Returns

Boolean valued AST representing whether an overflow occurs.

pointer_array_of()

smt_astt smt_solver_baset::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.

pointer_repr_applies()

bool smt_solver_baset::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.

pop_ctx()

void smt_solver_baset::pop_ctx ( )

virtual

Pop one context on the SMT assertion stack.

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

pre_solve()

void smt_solver_baset::pre_solve

(

)

print_model()

void smt_solver_baset::print_model ( )

virtual

Method to print the SMT model.

Reimplemented in bitwuzla_convt, boolector_convt, mathsat_convt, yices_convt, and z3_convt.

push_ctx()

void smt_solver_baset::push_ctx ( )

virtual

Push one context on the SMT assertion stack.

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, smtlib_convt, yices_convt, and z3_convt.

record_flattened_pointer()

void smt_solver_baset::record_flattened_pointer	(	smt_astt	address,
		smt_astt	pointer )

renumber_symbol_address()

void smt_solver_baset::renumber_symbol_address	(	const expr2tc &	guard,
		const expr2tc &	addr_symbol,
		const expr2tc &	new_size )

rewrite_ptrs_to_structs()

void smt_solver_baset::rewrite_ptrs_to_structs

(

type2tc &

type

)

For the given type, replace all instances of a pointer type with the struct representation of it.

round_fixedbv_to_int()

smt_astt smt_solver_baset::round_fixedbv_to_int	(	smt_astt	a,
		unsigned int	width,
		unsigned int	towidth )

Round a fixedbv to an integer.

round_int_to_fp()

smt_astt smt_solver_baset::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.

Used for int->fp casts under –ir-ieee. source_width is the bit-width of the source integer type.

round_real_to_int()

smt_astt smt_solver_baset::round_real_to_int

(

smt_astt

a

)

Round a real to an integer; not straightforward at all.

set_array_iface()

void smt_solver_baset::set_array_iface

(

array_iface *

iface

)

Stores handle for the array interface.

set_fp_conv()

void smt_solver_baset::set_fp_conv

(

fp_convt *

iface

)

Stores handle for the floating-point interface.

set_ra_conv()

void smt_solver_baset::set_ra_conv

(

ra_apit *

iface

)

Stores handle for the real-arithmetic/enclosure interface.

set_tuple_iface()

void smt_solver_baset::set_tuple_iface

(

tuple_iface *

iface

)

Stores handle for the tuple interface.

smt_post_init()

void smt_solver_baset::smt_post_init

(

)

Post-constructor setup method.

We must create various pieces of memory model data for tracking, however can't do it from the constructor because the solver converter itself won't have been initialized itself at that point. So, once it's ready, the solver converter should call this from it's constructor.

solver_text()

virtual const std::string smt_solver_baset::solver_text ( )

pure virtual

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.

Implemented in bitwuzla_convt, bitwuzllob_convt, boolector_convt, cvc5_convt, cvc_convt, mathsat_convt, minisat_convt, neurosym_convt, smtlib_convt, yices_convt, and z3_convt.

supports_assumptions()

virtual bool smt_solver_baset::supports_assumptions ( ) const

inlinevirtual

Reimplemented in bitwuzla_convt, boolector_convt, cvc5_convt, yices_convt, and z3_convt.

tuple_array_create_despatch()

smt_astt smt_solver_baset::tuple_array_create_despatch	(	const expr2tc &	expr,
		smt_sortt	domain )

Prep call for creating a tuple array.

Member Data Documentation

addr_space_arr_type

type2tc smt_solver_baset::addr_space_arr_type

Type of the array of address space allocation records.

addr_space_data

std::list<std::map<unsigned, bool> > smt_solver_baset::addr_space_data

The objects given an address so far, each mapped to whether it is a heap object that may be freed.

In a list to support pushing and popping.

addr_space_sym_num

std::list<unsigned int> smt_solver_baset::addr_space_sym_num

Integer recording how many times the address space allocation record array has been modified.

Essentially, this is like the SSA variable number, for an array we build / modify at conversion time. In a list so that we can support push/pop operations.

addr_space_type

type2tc smt_solver_baset::addr_space_type

Type of the address space allocation records.

Currently a start address integer and an end address integer.

array_api

array_iface* smt_solver_baset::array_api

boolean_sort

smt_sortt smt_solver_baset::boolean_sort

Sort for booleans.

For fast access.

ctx_level

unsigned int smt_solver_baset::ctx_level

Number of un-popped context pushes encountered so far.

current_valid_objects_sym

expr2tc smt_solver_baset::current_valid_objects_sym

Holds the __ESBMC_alloc symbol convert_terminal() was last invoked with.

divided_operand_pairs

std::set<std::pair<expr2tc, expr2tc> > smt_solver_baset::divided_operand_pairs

Operand pairs of every division seen by note_division_operands.

flatten_count

size_t smt_solver_baset::flatten_count = 0

flattened

std::unordered_map<expr2tc, ptr_flatten_entry, irep2_hash> smt_solver_baset::flattened

Each flattening bitcast converted so far, for steps that hit it in the conversion cache.

forall_defs_

std::unordered_map<irep_idt, expr2tc, irep_id_hash> smt_solver_baset::forall_defs_

Map from SSA symbol name to its forall/exists irep2 expression.

Populated in convert_assign when a symbol is assigned a quantifier expression; used in convert_ast to inline nested quantifier bodies before substituting the outer bound variable.

fp_api

fp_convt* smt_solver_baset::fp_api

fresh_map

std::map<std::string, unsigned int> smt_solver_baset::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.

get_ast_cache

std::unordered_map<smt_astt, std::pair<type2tc, expr2tc> > smt_solver_baset::get_ast_cache

Model-value cache for get_by_ast(), on the same terms and with the same invalidation as l_get_cache.

The pointer key is safe because pop_ctx clears this map before deleting any smt_ast, so an address cannot be reused while an entry for it survives. The stored type gates reuse rather than keying it: the same bit-vector reads differently as signed or unsigned.

int_encoding

bool smt_solver_baset::int_encoding

Whether we are encoding expressions in integer mode or not.

int_shift_op_array

smt_astt smt_solver_baset::int_shift_op_array

invalid_ptr_ast

smt_astt smt_solver_baset::invalid_ptr_ast

ir_ieee

bool smt_solver_baset::ir_ieee

Whether –ir-ieee mode is active (integer encoding with IEEE float semantics).

ir_ieee_api

std::unique_ptr<ir_ieee_convt> smt_solver_baset::ir_ieee_api

l_get_cache

std::unordered_map<smt_astt, tvt> smt_solver_baset::l_get_cache

Model-value cache for l_get().

Holds the current model's boolean assignments; cleared on every model-changing transition (pre_solve, push_ctx, pop_ctx) so a hit always reflects the latest solve. Keyed by the boolean smt_ast pointer (solver ASTs are hash-consed, so identical pointer ⇒ identical term ⇒ identical model value).

live_asts

std::vector<smt_astt> smt_solver_baset::live_asts

Lifetime tracking of smt ast's.

When a context is pop'd, all the ASTs created in that context are freed.

live_asts_sizes

std::vector<unsigned int> smt_solver_baset::live_asts_sizes

Accounting of live_asts for push/pop.

Records the number of pointers contained when a push occurred. On pop, the live_asts vector is reset back to that point.

machine_ptr

type2tc smt_solver_baset::machine_ptr

The type of the machine integer that can store a pointer.

max_rebuild_sources

size_t smt_solver_baset::max_rebuild_sources = 32

staticconstexpr

The most flattens one rebuilt pointer is defined over; see decode_pointer_repr().

ns

const namespacet& smt_solver_baset::ns

A namespace containing all the types in the program.

Used to resolve the rare case where we're doing some pointer arithmetic and need to have the concrete type of a pointer.

null_ptr_ast

smt_astt smt_solver_baset::null_ptr_ast

options

const optionst& smt_solver_baset::options

pointer_logic

std::list<pointer_logict> smt_solver_baset::pointer_logic

Pointer_logict object, which contains some code for formatting how pointers are displayed in counter-examples.

This is a list so that we can push and pop data when context push/pop operations occur.

pointer_struct

type2tc smt_solver_baset::pointer_struct

Constant struct representing the implementation of the pointer type – i.e., the struct type that pointers get translated to.

ptr_flatten_history

std::vector<ptr_flatten_entry> smt_solver_baset::ptr_flatten_history

Every flattened pointer in this context.

Pruned on pop_ctx like uf_ackermann_history, whose asts have the same lifetime.

ptr_flow

std::unordered_map<std::string, std::pair<unsigned int, std::set<size_t> > > smt_solver_baset::ptr_flow

The flattens each SSA symbol's value may hold, and the context level it was recorded at.

ptr_foo_inited

bool smt_solver_baset::ptr_foo_inited

quantifier_counter

size_t smt_solver_baset::quantifier_counter = 0

Counter for generating unique bound-variable names in quantifiers.

ra_api

ra_apit* smt_solver_baset::ra_api

renumber_map

std::vector<renumber_mapt> smt_solver_baset::renumber_map

smt_cache

smt_cachet smt_solver_baset::smt_cache

A cache mapping expressions to converted SMT ASTs.

smt_cache_mutex

std::mutex smt_solver_baset::smt_cache_mutex

A mutex lock for writing to the cache.

sort_cache

smt_sort_cachet smt_solver_baset::sort_cache

A cache of converted type2tc's to smt sorts.

step_assigned

std::string smt_solver_baset::step_assigned

step_flattens

std::set<size_t> smt_solver_baset::step_flattens

step_guard

smt_astt smt_solver_baset::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.

Null and empty outside a step.

step_overwritten

expr2tc smt_solver_baset::step_overwritten

step_sources

std::set<size_t> smt_solver_baset::step_sources

tuple_api

tuple_iface* smt_solver_baset::tuple_api

uf_ackermann_counter

size_t smt_solver_baset::uf_ackermann_counter = 0

Counter for the fresh result symbols minted by the Ackermann fallback.

uf_ackermann_history

std::unordered_map<std::string, std::vector<uf_ackermann_entry> > smt_solver_baset::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).

A later application of the same name is tied to each earlier one by an (args equal => results equal) assumption.

---

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

• src/solvers/smt/smt_solver.h
• src/solvers/smt/smt_bitcast.cpp
• src/solvers/smt/smt_byteops.cpp
• src/solvers/smt/smt_casts.cpp
• src/solvers/smt/smt_fp_conv.cpp
• src/solvers/smt/smt_memspace.cpp
• src/solvers/smt/smt_overflow.cpp
• src/solvers/smt/smt_solver.cpp