neurosym_convt Class Reference

Backend for NeuroSym, a neural-guided SMT solver (a GAN proposes candidate models, with a Z3 fallback preserving soundness and completeness). More...

#include <neurosym_conv.h>

Inheritance diagram for neurosym_convt:

Public Member Functions
	neurosym_convt (const namespacet &ns, const optionst &options)
	~neurosym_convt () override
smt_resultt	dec_solve () override
	Solve the formula given to the solver.
const std::string	solver_text () override
	Solver name fetcher.
std::string	dump_smt () override
	Method to dump the SMT formula.
bool	has_model () const override
	Whether a satisfiable result can be turned into a model.
tvt	get_bool (smt_astt a) override
	Extract the assignment to a boolean variable from the SMT solver's model.
tvt	l_get (smt_astt a) override
	Fetch the value of a boolean sorted smt_ast.
BigInt	get_bv (smt_astt a, bool is_signed) override
	Extract the assignment to a bitvector from the SMT solver's model.
Public Member Functions inherited from smtlib_convt
	smtlib_convt (const namespacet &_ns, const optionst &options)
	smtlib_convt (const namespacet &_ns, const optionst &options, const std::string &solver_prog, const std::string &output_path, const std::string &logic="")
	~smtlib_convt () override
smt_resultt	dec_solve () override
	Solve the formula given to the solver.
void	emit_check_sat ()
smt_resultt	read_check_sat_response ()
const std::string	solver_text () override
	Solver name fetcher.
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_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
void	assert_ast (smt_astt a) override
	Assert the truth of an ast.
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_fbv_sort (std::size_t width) override
	Create a fixed-point sort.
smt_sortt	mk_array_sort (smt_sortt domain, smt_sortt range) override
	Create an array 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_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_bool (bool val) override
	Create a boolean.
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_astt	mk_array_symbol (const std::string &name, const smt_sort *s, smt_sortt array_subtype) override
smt_sort *	mk_struct_sort (const type2tc &type)
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	convert_array_of (smt_astt init_val, unsigned long domain_width) override
	Create an array with a single initializer.
sexpr	get_value (smt_astt a) const
bool	has_model () const override
	get_value() reads from the interactive pipe, so without it the solver can still answer sat/unsat but no model can be recovered.
tvt	get_bool (smt_astt a) override
	Extract the assignment to a boolean variable from the SMT solver's model.
tvt	l_get (smt_astt a) override
	Fetch the value of a boolean sorted smt_ast.
BigInt	get_bv (smt_astt a, bool is_signed) override
	Extract the assignment to a bitvector from the SMT solver's model.
expr2tc	get_array_elem (smt_astt array, uint64_t index, const type2tc &type) override
	Extract an element from the model of an array, at an explicit index.
std::string	sort_to_string (const smt_sort *s) const
unsigned int	emit_terminal_ast (const smtlib_smt_ast *a, std::string &output) const
unsigned int	emit_ast (const smtlib_smt_ast *ast, std::string &output, std::unordered_map< const smtlib_smt_ast *, std::string > &temp_symbols) const
void	emit_ast (const smtlib_smt_ast *ast) const
void	push_ctx () override
	Push one context on the SMT assertion stack.
void	pop_ctx () override
	Pop one context on the SMT assertion stack.
std::string	dump_smt () override
	Method to dump the SMT formula.
template<typename... Ts>
void	emit (const Ts &...) const
void	flush () const
template<typename... Ts>
void	emit (const Ts &...ts) const
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 ()
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 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)
tvt	l_get (const expr2tc &expr)
	Fetch the value of a boolean expression from the current model.
virtual smt_astt	mk_neq (smt_astt a, smt_astt b)
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.
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_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 void	print_model ()
	Method to print the SMT model.
virtual smt_astt	convert_array_index (const expr2tc &expr)
	High level index expression conversion.
virtual smt_astt	convert_array_store (const expr2tc &expr)
	Partner method to convert_array_index, for stores.
virtual smt_astt	mk_fresh (smt_sortt s, const std::string &tag, smt_sortt st=nullptr)
	Create a free variable with the given sort, and a unique name, with the prefix given in 'tag'.
std::string	mk_fresh_name (const std::string &tag)
	Create a previously un-used variable name with the prefix given in tag.
void	renumber_symbol_address (const expr2tc &guard, const expr2tc &addr_symbol, const expr2tc &new_size)
smt_sortt	convert_sort (const type2tc &type)
	Convert a type2tc into an smt_sort.
smt_astt	convert_terminal (const expr2tc &expr)
	Convert a terminal expression into an SMT AST.
smt_astt	convert_pointer_arith (const expr2tc &expr, const type2tc &t)
	Flatten pointer arithmetic.
smt_astt	divide_by_element_size (const expr2tc &diff, const expr2tc &size)
	The quotient of a signed byte difference by an element size, truncated toward zero.
smt_astt	convert_ptr_cmp (const expr2tc &expr, const expr2tc &expr2, const expr2tc &templ_expr)
	Compare two pointers.
smt_astt	convert_addr_of (const expr2tc &expr)
	Take the address of some kind of expression.
smt_astt	convert_member (const expr2tc &expr)
	Handle union/struct based corner cases for member2tc expressions.
smt_astt	convert_identifier_pointer (const expr2tc &expr, const std::string &sym, const typet *type)
	Convert an identifier to a pointer.
smt_astt	init_pointer_obj (unsigned int obj_num, const expr2tc &size, const typet *type, bool may_be_freed)
smt_astt	convert_is_nan (const expr2tc &expr)
	Checks for equality with NaN representation.
smt_astt	convert_is_inf (const expr2tc &expr)
	Checks for equality with inf representation.
smt_astt	convert_is_normal (const expr2tc &expr)
	Checks for equality with normal representation.
smt_astt	convert_is_finite (const expr2tc &expr)
	Checks for equality with finite representation.
smt_astt	convert_signbit (const expr2tc &expr)
	Converts signbit representation.
smt_astt	convert_popcount (const expr2tc &expr)
	Converts popcount representation.
smt_astt	convert_bswap (const expr2tc &expr)
	Converts bswap representation.
smt_astt	convert_rounding_mode (const expr2tc &expr)
	Converts rounding mode for ieee fp operations.
smt_astt	convert_byte_extract (const expr2tc &expr)
	Convert a byte_extract2tc, pulling a byte from the byte representation of some piece of data.
smt_astt	convert_byte_extract_int_mode (const byte_extract2t &data, expr2tc source, expr2tc offs, unsigned int src_width)
smt_astt	convert_byte_extract_bv_mode (const byte_extract2t &data, expr2tc source, expr2tc offs, unsigned int src_width)
expr2tc	create_int_right_shift (expr2tc source, expr2tc shift_amount)
smt_astt	convert_byte_update (const expr2tc &expr)
	Convert a byte_update2tc, inserting a byte into the byte representation of some piece of data.
smt_astt	convert_byte_update_int_mode (const byte_update2t &data)
	Convert a byte_update2tc in integer arithmetic mode, handling both constant and non-constant offsets with proper type preservation.
expr2tc	convert_byte_update_int_mode_expr (const byte_update2t &data, expr2tc source, expr2tc offs, expr2tc update_value, unsigned int src_width)
	Convert a byte_update2tc with offset in integer mode, using conditional expressions for all possible byte positions.
smt_astt	convert_byte_update_bv_mode (const byte_update2t &data)
	Convert a byte_update2tc using bitvector operations, preserving the original bitvector-based implementation.
smt_astt	convert_bitcast (const expr2tc &expr)
	Convert a bitcast2tc, converting an expr to its bit representation.
smt_astt	convert_pointer_bitcast (const expr2tc &from, const type2tc &to_type)
	The pointer, floating-point and struct legs of convert_bitcast, split out so the dispatcher stays readable.
smt_astt	convert_bitcast_to_fp (const expr2tc &from, const type2tc &to_type)
	Read a floating-point value from the bits of from.
smt_astt	convert_bitcast_to_struct (const expr2tc &from, const type2tc &to_type)
	Rebuild a struct from the bits of from, member by member.
smt_astt	encode_pointer_repr (const expr2tc &ptr, const type2tc &to_type)
	Flatten a pointer to the machine representation a bitcast reinterprets, and rebuild it from one; see the comment on the definitions in smt_bitcast.cpp.
smt_astt	decode_pointer_repr (const expr2tc &repr, const type2tc &to_type)
bool	pointer_repr_applies (const type2tc &ptr_type, const type2tc &bv_type)
	True when ptr_type's representation occupies bv_type exactly, so the bits read back are the bits that were written.
void	assert_expr (const expr2tc &e)
	Convert the given expr to AST, then assert that AST.
void	note_division_operands (const expr2tc &expr, std::unordered_set< const expr2t * > &seen)
	Record every division's operand pair in expr, recursively.
smt_astt	convert_modulus (const modulus2t &m, smt_astt a, smt_astt b)
	Encode a remainder: compositional via the matching division when one exists in the formula, the solver's rem primitive otherwise.
smt_astt	mk_truncated_div (const type2tc &type, smt_astt a, smt_astt b)
	C's / and % of signed type on Int-sorted operands, from the solver's Euclidean div/mod (#8662).
smt_astt	mk_truncated_rem (const type2tc &type, smt_astt a, smt_astt b)
smt_astt	array_create (const expr2tc &expr)
	Convert constant_array2tc's and constant_array_of2tc's.
void	init_addr_space_array ()
	Initialize tracking data for the address space records.
void	set_tuple_iface (tuple_iface *iface)
	Stores handle for the tuple interface.
void	set_array_iface (array_iface *iface)
	Stores handle for the array interface.
void	set_fp_conv (fp_convt *iface)
	Stores handle for the floating-point interface.
void	set_ra_conv (ra_apit *iface)
	Stores handle for the real-arithmetic/enclosure interface.
void	bump_addrspace_array (unsigned int idx, const expr2tc &val)
std::string	get_cur_addrspace_ident ()
	Get the symbol name for the current address-allocation record array.
void	finalize_pointer_chain (unsigned int obj_num)
	Create and assert address space constraints on the given object ID number.
smt_astt	convert_typecast_to_bool (const typecast2t &cast)
	Typecast data to bools.
smt_astt	convert_typecast_to_fixedbv_nonint (const expr2tc &cast)
	Typecast to a fixedbv in bitvector mode.
smt_astt	convert_typecast_to_fixedbv_nonint_from_bv (const expr2tc &cast)
smt_astt	convert_typecast_to_fixedbv_nonint_from_bool (const expr2tc &cast)
smt_astt	convert_typecast_to_fixedbv_nonint_from_fixedbv (const expr2tc &cast)
smt_astt	convert_typecast_to_ints (const typecast2t &cast)
	Typecast anything to an integer (but not pointers).
smt_astt	convert_typecast_to_ints_intmode (const typecast2t &cast)
smt_astt	convert_typecast_to_ints_from_fbv_sint (const typecast2t &cast)
smt_astt	convert_typecast_to_ints_from_unsigned (const typecast2t &cast)
smt_astt	convert_typecast_to_ints_from_bool (const typecast2t &cast)
smt_astt	convert_typecast_to_ptr (const typecast2t &cast)
	Typecast something (i.e.
smt_astt	convert_typecast_from_ptr (const typecast2t &cast)
	Typecast a pointer to an integer.
smt_astt	convert_typecast_to_struct (const typecast2t &cast)
	Typecast structs to other structs.
smt_astt	convert_typecast (const expr2tc &expr)
	Despatch a typecast expression to a more specific typecast method.
smt_astt	convert_typecast_to_fpbv (const typecast2t &cast)
	Typecast to a floatbv.
smt_astt	convert_typecast_from_fpbv (const typecast2t &cast)
	Typecast from a floatbv.
smt_astt	round_real_to_int (smt_astt a)
	Round a real to an integer; not straightforward at all.
smt_astt	round_fixedbv_to_int (smt_astt a, unsigned int width, unsigned int towidth)
	Round a fixedbv to an integer.
smt_astt	round_int_to_fp (smt_astt int_val, const floatbv_type2t &fbv_type, unsigned int source_width)
	Round an SMT integer to the nearest representable float/double using IEEE 754 round-to-nearest-even.
smt_astt	tuple_array_create_despatch (const expr2tc &expr, smt_sortt domain)
	Prep call for creating a tuple array.
smt_astt	make_bool_bit (smt_astt a)
	Convert a boolean to a bitvector with one bit.
smt_astt	make_bit_bool (smt_astt a)
	Convert a bitvector with one bit to a boolean.
expr2tc	fix_array_idx (const expr2tc &idx, const type2tc &array_type)
	Given an array index, extract the lower n bits of it, where n is the bitwidth of the array domain.
type2tc	flatten_array_type (const type2tc &type)
	For a multi-dimensional array, convert the type into a single dimension array.
type2tc	get_flattened_array_subtype (const type2tc &type)
	Get the base subtype of an array, delving through any intermediate multidimensional arrays.
expr2tc	array_domain_to_width (const type2tc &type)
	Fetch the number of elements in an array (the domain).
void	rewrite_ptrs_to_structs (type2tc &type)
	For the given type, replace all instances of a pointer type with the struct representation of it.
expr2tc	decompose_select_chain (const expr2tc &expr, expr2tc &base)
	When dealing with multi-dimensional arrays, and selecting one element out of several dimensions, reduce it to an expression on a single dimensional array, by concatenating the indexes.
expr2tc	decompose_store_chain (const expr2tc &expr, expr2tc &base)
	Like decompose_select_chain, but for multidimensional stores.
void	expand_row_stores (const expr2tc &row, const expr2tc &offset, std::vector< flat_storet > &stores)
	Name every element of a row being written whole as a store of the corresponding read out of it, at offset in the flattened array.
bool	decompose_stores (const expr2tc &expr, const expr2tc &offset, std::vector< flat_storet > &stores, expr2tc &base)
	Decompose an array with into the flat element updates it denotes, oldest first, giving back the array the chain is rooted at.
smt_astt	convert_array_of_prep (const expr2tc &expr)
	Prepare an array_of expression by flattening its dimensions, if it has more than one.
smt_astt	pointer_array_of (const expr2tc &init_val, unsigned long array_width)
	Create an array of pointers; expects the init_val to be null, because there's no other way to initialize a pointer array in C, AFAIK.
unsigned int	get_member_name_field (const type2tc &t, const irep_idt &name) const
unsigned int	get_member_name_field (const type2tc &t, const expr2tc &name) const
expr2tc	get_array (const type2tc &type, smt_astt array)
	Given an array expression, attempt to extract its valuation from the solver model, computing a constant_array2tc by calling get_array_elem.
expr2tc	get_array (const expr2tc &expr)
void	delete_all_asts ()
Public 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
virtual smt_astt	mk_smt_fpbv (const ieee_floatt &thereal)
	Create a floating point bitvector.
virtual smt_sortt	mk_fpbv_sort (const unsigned ew, const unsigned sw)
	Create a sort representing a floating-point number.
virtual smt_sortt	mk_fpbv_rm_sort ()
	Create a sort representing a floating-point rounding mode.
virtual smt_astt	mk_smt_fpbv_nan (bool sgn, unsigned ew, unsigned sw)
	Create a NaN floating point bitvector.
virtual smt_astt	mk_smt_fpbv_inf (bool sgn, unsigned ew, unsigned sw)
	Create a (+/-)inf floating point bitvector.
virtual smt_astt	mk_smt_fpbv_rm (ieee_floatt::rounding_modet rm)
	Create a rounding mode to be used by floating point cast and arith ops.
virtual smt_astt	mk_smt_typecast_from_fpbv_to_ubv (smt_astt from, std::size_t width)
	Typecast from a floating point.
virtual smt_astt	mk_smt_typecast_from_fpbv_to_sbv (smt_astt from, std::size_t width)
	Typecast from a floating point.
virtual smt_astt	mk_smt_typecast_from_fpbv_to_fpbv (smt_astt from, smt_sortt to, smt_astt rm)
	Typecast from a floating point.
virtual smt_astt	mk_smt_typecast_ubv_to_fpbv (smt_astt from, smt_sortt to, smt_astt rm)
	Typecast to a floating point.
virtual smt_astt	mk_smt_typecast_sbv_to_fpbv (smt_astt from, smt_sortt to, smt_astt rm)
	Typecast to a floating point.
virtual smt_astt	mk_smt_nearbyint_from_float (smt_astt from, smt_astt rm)
	Calculate the nearby int from a floating point, considering the rounding mode.
virtual smt_astt	mk_smt_fpbv_add (smt_astt lhs, smt_astt rhs, smt_astt rm)
	Convert a ieee addition.
virtual smt_astt	mk_smt_fpbv_sub (smt_astt lhs, smt_astt rhs, smt_astt rm)
	Convert a ieee subtraction.
virtual smt_astt	mk_smt_fpbv_mul (smt_astt lhs, smt_astt rhs, smt_astt rm)
	Convert a ieee multiplication.
virtual smt_astt	mk_smt_fpbv_div (smt_astt lhs, smt_astt rhs, smt_astt rm)
	Convert the ieee division.
virtual smt_astt	mk_smt_fpbv_rem (smt_astt lhs, smt_astt rhs)
	Convert the ieee remainder (SMT-LIB fp.rem, C's remainder()).
virtual smt_astt	mk_smt_fpbv_sqrt (smt_astt rd, smt_astt rm)
	Convert the ieee arithmetic square-root (sqrt).
virtual smt_astt	mk_smt_fpbv_fma (smt_astt v1, smt_astt v2, smt_astt v3, smt_astt rm)
	Convert the ieee arithmetic fused-multiply add (fma): round((v1 * v2) + v3).
virtual smt_astt	mk_smt_fpbv_eq (smt_astt lhs, smt_astt rhs)
	Convert an ieee equality.
virtual smt_astt	mk_smt_fpbv_gt (smt_astt lhs, smt_astt rhs)
	Convert an ieee greater than.
virtual smt_astt	mk_smt_fpbv_lt (smt_astt lhs, smt_astt rhs)
	Convert an ieee less than.
virtual smt_astt	mk_smt_fpbv_gte (smt_astt lhs, smt_astt rhs)
	Convert an ieee greater than or equal.
virtual smt_astt	mk_smt_fpbv_lte (smt_astt lhs, smt_astt rhs)
	Convert an ieee less than or equal.
virtual smt_astt	mk_smt_fpbv_is_nan (smt_astt op)
	Convert an ieee is_nan operation.
virtual smt_astt	mk_smt_fpbv_is_inf (smt_astt op)
	Convert an ieee is_inf operation.
virtual smt_astt	mk_smt_fpbv_is_normal (smt_astt op)
	Convert an ieee is_normal operation.
virtual smt_astt	mk_smt_fpbv_is_zero (smt_astt op)
	Convert an ieee is_zero operation.
virtual smt_astt	mk_smt_fpbv_is_negative (smt_astt op)
	Convert an ieee is_neg operation.
virtual smt_astt	mk_smt_fpbv_is_positive (smt_astt op)
	Convert an ieee is_pos operation.
virtual smt_astt	mk_smt_fpbv_abs (smt_astt op)
	Convert an ieee abs operation.
virtual smt_astt	mk_smt_fpbv_neg (smt_astt op)
	Convert an ieee negation operation.
virtual ieee_floatt	get_fpbv (smt_astt a)
	Extract the assignment to a floating-point from the SMT solvers model.
virtual smt_astt	mk_from_bv_to_fp (smt_astt op, smt_sortt to)
	Convert BV to FP.
virtual smt_astt	mk_from_fp_to_bv (smt_astt op)
	Convert FP to BV.

Additional Inherited Members
Public Types inherited from smtlib_convt
typedef boost::multi_index_container< symbol_table_rec, boost::multi_index::indexed_by< boost::multi_index::hashed_unique< BOOST_MULTI_INDEX_MEMBER(symbol_table_rec, std::string, ident)>, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(symbol_table_rec, unsigned int, level), std::greater< unsigned int > > > >	symbol_tablet
Public Types inherited from smt_solver_baset
typedef std::vector< smt_astt >	ast_vec
	Shorthand for a vector of smt_ast's.
typedef boost::multi_index_container< smt_cache_entryt, boost::multi_index::indexed_by< boost::multi_index::hashed_unique< BOOST_MULTI_INDEX_MEMBER(smt_cache_entryt, const expr2tc, val)>, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(smt_cache_entryt, unsigned int, level), std::greater< unsigned int > > > >	smt_cachet
typedef std::unordered_map< type2tc, smt_sortt, type2_hash >	smt_sort_cachet
typedef std::map< std::string, smt_astt >	renumber_mapt
Public Attributes inherited from smtlib_convt
struct smtlib_convt::process_emitter	emit_proc
struct smtlib_convt::file_emitter	emit_opt_output
symbol_tablet	symbol_table
std::unordered_map< std::string, unsigned int >	declared_ufs
	Uninterpreted functions already emitted via (declare-fun ...), mapped to the context level at which they were declared, so each function symbol is declared to the solver exactly once per scope and every application shares it (giving native functional congruence).
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
Static Public Attributes inherited from smtlib_convt
static const std::string	temp_prefix
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().

Detailed Description

Backend for NeuroSym, a neural-guided SMT solver (a GAN proposes candidate models, with a Z3 fallback preserving soundness and completeness).

NeuroSym natively parses only the QF_BV and QF_LIA fragments of SMT-LIB2, and this backend drives it as a pure QF_BV solver. NeuroSym runs as a separate program that cannot be linked into another application, so this backend reuses the smtlib backend's SMT-LIB2 serializer to render the formula into a file and runs NeuroSym on it in one-shot batch mode (–neurosym-prog, "%f" is replaced by the file path).

NeuroSym has no native array, floating-point, or tuple support, so the factory leaves those capability interfaces unset and ESBMC's flatteners lower everything to pure QF_BV; the header emitted before the formula is overridden to (set-logic QF_BV) accordingly. Integer/real encoding (–ir) is rejected in solve.cpp because the flattened int-mode logic would be QF_AUFLIRA, which NeuroSym cannot parse.

On a sat verdict NeuroSym prints its own "(model (define-fun NAME () SORT VALUE) ...)" block, which dec_solve() parses into local_model, so a counterexample needs no second solve. Composite queries are evaluated from those leaves; anything unhandled still falls back to –neurosym-model-prog.

Constructor & Destructor Documentation

neurosym_convt()

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

~neurosym_convt()

neurosym_convt::~neurosym_convt ( )

override

Member Function Documentation

dec_solve()

smt_resultt neurosym_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.

dump_smt()

std::string neurosym_convt::dump_smt ( )

overridevirtual

Method to dump the SMT formula.

Reimplemented from smt_solver_baset.

get_bool()

tvt neurosym_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 neurosym_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.

has_model()

bool neurosym_convt::has_model ( ) const

inlineoverridevirtual

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 from smt_solver_baset.

l_get()

tvt neurosym_convt::l_get ( smt_astt a )

overridevirtual

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 from smt_solver_baset.

solver_text()

const std::string neurosym_convt::solver_text ( )

overridevirtual

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.

---

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

• src/solvers/neurosym/neurosym_conv.h
• src/solvers/neurosym/neurosym_conv.cpp