mathsat_convt Member List

This is the complete list of members for mathsat_convt, including all inherited members.

add_array_constraints_for_solving()	array_iface	inlinevirtual
addr_space_arr_type	smt_solver_baset
addr_space_data	smt_solver_baset
addr_space_sym_num	smt_solver_baset
addr_space_type	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())	smt_solver_baset	virtual
array_api	smt_solver_baset
array_create(const expr2tc &expr)	smt_solver_baset
array_domain_to_width(const type2tc &type)	smt_solver_baset
array_iface(bool _b, bool inf)	array_iface	inline
assert_ast(smt_astt a) override	mathsat_convt	virtual
assert_expr(const expr2tc &e)	smt_solver_baset
ast_vec typedef	smt_solver_baset
begin_step(const expr2tc &guard, const expr2tc &cond)	smt_solver_baset
boolean_sort	smt_solver_baset
bump_addrspace_array(unsigned int idx, const expr2tc &val)	smt_solver_baset
can_init_infinite_arrays	array_iface
cfg	mathsat_convt
check_msat_error(msat_term &r) const	mathsat_convt
convert_addr_of(const expr2tc &expr)	smt_solver_baset
convert_array_index(const expr2tc &expr)	smt_solver_baset	virtual
convert_array_of(smt_astt init_val, unsigned long domain_width) override	mathsat_convt	virtual
convert_array_of_prep(const expr2tc &expr)	smt_solver_baset
convert_array_store(const expr2tc &expr)	smt_solver_baset	virtual
convert_assign(const expr2tc &expr)	smt_solver_baset
convert_ast(const expr2tc &expr)	smt_solver_baset
convert_ast(const expr2tc &expr, const type2tc &type, smt_astt const *args, struct expr_op_convert ops)	smt_solver_baset
convert_ast_node(const expr2tc &expr)	smt_solver_baset
convert_bitcast(const expr2tc &expr)	smt_solver_baset
convert_bitcast_to_fp(const expr2tc &from, const type2tc &to_type)	smt_solver_baset
convert_bitcast_to_struct(const expr2tc &from, const type2tc &to_type)	smt_solver_baset
convert_bswap(const expr2tc &expr)	smt_solver_baset
convert_byte_extract(const expr2tc &expr)	smt_solver_baset
convert_byte_extract_bv_mode(const byte_extract2t &data, expr2tc source, expr2tc offs, unsigned int src_width)	smt_solver_baset
convert_byte_extract_int_mode(const byte_extract2t &data, expr2tc source, expr2tc offs, unsigned int src_width)	smt_solver_baset
convert_byte_update(const expr2tc &expr)	smt_solver_baset
convert_byte_update_bv_mode(const byte_update2t &data)	smt_solver_baset
convert_byte_update_int_mode(const byte_update2t &data)	smt_solver_baset
convert_byte_update_int_mode_expr(const byte_update2t &data, expr2tc source, expr2tc offs, expr2tc update_value, unsigned int src_width)	smt_solver_baset
convert_concat_int_mode(smt_astt left_ast, smt_astt right_ast, const expr2tc &expr)	smt_solver_baset
convert_identifier_pointer(const expr2tc &expr, const std::string &sym, const typet *type)	smt_solver_baset
convert_ieee_arith_2op(const expr2tc &expr)	smt_solver_baset
convert_is_finite(const expr2tc &expr)	smt_solver_baset
convert_is_inf(const expr2tc &expr)	smt_solver_baset
convert_is_nan(const expr2tc &expr)	smt_solver_baset
convert_is_normal(const expr2tc &expr)	smt_solver_baset
convert_member(const expr2tc &expr)	smt_solver_baset
convert_modulus(const modulus2t &m, smt_astt a, smt_astt b)	smt_solver_baset
convert_pointer_arith(const expr2tc &expr, const type2tc &t)	smt_solver_baset
convert_pointer_bitcast(const expr2tc &from, const type2tc &to_type)	smt_solver_baset
convert_popcount(const expr2tc &expr)	smt_solver_baset
convert_ptr_cmp(const expr2tc &expr, const expr2tc &expr2, const expr2tc &templ_expr)	smt_solver_baset
convert_rounding_mode(const expr2tc &expr)	smt_solver_baset
convert_signbit(const expr2tc &expr)	smt_solver_baset
convert_sort(const type2tc &type)	smt_solver_baset
convert_terminal(const expr2tc &expr)	smt_solver_baset
convert_typecast(const expr2tc &expr)	smt_solver_baset
convert_typecast_from_fpbv(const typecast2t &cast)	smt_solver_baset
convert_typecast_from_ptr(const typecast2t &cast)	smt_solver_baset
convert_typecast_to_bool(const typecast2t &cast)	smt_solver_baset
convert_typecast_to_fixedbv_nonint(const expr2tc &cast)	smt_solver_baset
convert_typecast_to_fixedbv_nonint_from_bool(const expr2tc &cast)	smt_solver_baset
convert_typecast_to_fixedbv_nonint_from_bv(const expr2tc &cast)	smt_solver_baset
convert_typecast_to_fixedbv_nonint_from_fixedbv(const expr2tc &cast)	smt_solver_baset
convert_typecast_to_fpbv(const typecast2t &cast)	smt_solver_baset
convert_typecast_to_ints(const typecast2t &cast)	smt_solver_baset
convert_typecast_to_ints_from_bool(const typecast2t &cast)	smt_solver_baset
convert_typecast_to_ints_from_fbv_sint(const typecast2t &cast)	smt_solver_baset
convert_typecast_to_ints_from_unsigned(const typecast2t &cast)	smt_solver_baset
convert_typecast_to_ints_intmode(const typecast2t &cast)	smt_solver_baset
convert_typecast_to_ptr(const typecast2t &cast)	smt_solver_baset
convert_typecast_to_struct(const typecast2t &cast)	smt_solver_baset
create_int_right_shift(expr2tc source, expr2tc shift_amount)	smt_solver_baset
ctx_level	smt_solver_baset
current_valid_objects_sym	smt_solver_baset
dec_solve() override	mathsat_convt	virtual
dec_solve_assuming(const ast_vec &assumptions)	smt_solver_baset	virtual
decode_pointer_repr(const expr2tc &repr, const type2tc &to_type)	smt_solver_baset
decompose_select_chain(const expr2tc &expr, expr2tc &base)	smt_solver_baset
decompose_store_chain(const expr2tc &expr, expr2tc &base)	smt_solver_baset
decompose_stores(const expr2tc &expr, const expr2tc &offset, std::vector< flat_storet > &stores, expr2tc &base)	smt_solver_baset
default_convert_array_of(smt_astt init_val, unsigned long domain_width, smt_solver_baset *ctx)	array_iface
define(const expr2tc &expr)	smt_solver_baset
delete_all_asts()	smt_solver_baset
divide_by_element_size(const expr2tc &diff, const expr2tc &size)	smt_solver_baset
divided_operand_pairs	smt_solver_baset
dump_expr(const expr2tc &expr)	smt_solver_baset
dump_smt() override	mathsat_convt	virtual
encode_pointer_repr(const expr2tc &ptr, const type2tc &to_type)	smt_solver_baset
end_step()	smt_solver_baset
env	mathsat_convt
expand_row_stores(const expr2tc &row, const expr2tc &offset, std::vector< flat_storet > &stores)	smt_solver_baset
finalize_pointer_chain(unsigned int obj_num)	smt_solver_baset
fix_array_idx(const expr2tc &idx, const type2tc &array_type)	smt_solver_baset
flatten_array_type(const type2tc &type)	smt_solver_baset
flatten_count	smt_solver_baset
flattened	smt_solver_baset
forall_defs_	smt_solver_baset
fp_api	smt_solver_baset
fp_convt(smt_solver_baset *_ctx)	fp_convt	explicit
fresh_map	smt_solver_baset
get(const expr2tc &expr)	smt_solver_baset	virtual
get_array(const type2tc &type, smt_astt array)	smt_solver_baset
get_array(const expr2tc &expr)	smt_solver_baset
get_array_elem(smt_astt array, uint64_t index, const type2tc &subtype) override	mathsat_convt	virtual
get_ast_cache	smt_solver_baset
get_bool(smt_astt a) override	mathsat_convt	virtual
get_bv(smt_astt a, bool is_signed) override	mathsat_convt	virtual
get_by_ast(const type2tc &type, smt_astt a)	smt_solver_baset	virtual
get_by_ast(const expr2tc &expr)	smt_solver_baset
get_by_type(const expr2tc &expr)	smt_solver_baset	virtual
get_by_value(const type2tc &type, BigInt value)	smt_solver_baset
get_cur_addrspace_ident()	smt_solver_baset
get_double_eps_rel()	smt_solver_baset
get_double_eps_up()	smt_solver_baset
get_double_inf_sentinel()	smt_solver_baset
get_double_max_normal()	smt_solver_baset
get_double_min_normal()	smt_solver_baset
get_double_min_subnormal()	smt_solver_baset
get_flattened_array_subtype(const type2tc &type)	smt_solver_baset
get_fpbv(smt_astt a) override	mathsat_convt	virtual
get_index(const expr2tc &expr, expr2tc &res)	smt_solver_baset
get_index_value(const expr2tc &expr, expr2tc &res)	smt_solver_baset
get_member_name_field(const type2tc &t, const irep_idt &name) const	smt_solver_baset
get_member_name_field(const type2tc &t, const expr2tc &name) const	smt_solver_baset
get_rational(smt_astt a, BigInt &numerator, BigInt &denominator)	smt_solver_baset	inlinevirtual
get_single_eps_rel()	smt_solver_baset
get_single_eps_up()	smt_solver_baset
get_single_inf_sentinel()	smt_solver_baset
get_single_max_normal()	smt_solver_baset
get_single_min_normal()	smt_solver_baset
get_single_min_subnormal()	smt_solver_baset
get_zero_real()	smt_solver_baset
has_model() const	smt_solver_baset	inlinevirtual
imply_ast(smt_astt a, smt_astt b)	smt_solver_baset
init_addr_space_array()	smt_solver_baset
init_pointer_obj(unsigned int obj_num, const expr2tc &size, const typet *type, bool may_be_freed)	smt_solver_baset
int_encoding	smt_solver_baset
int_shift_op_array	smt_solver_baset
invalid_ptr_ast	smt_solver_baset
invert_ast(smt_astt a)	smt_solver_baset
ir_ieee	smt_solver_baset
ir_ieee_api	smt_solver_baset
l_get(smt_astt a)	smt_solver_baset	virtual
l_get(const expr2tc &expr)	smt_solver_baset
l_get_cache	smt_solver_baset
live_asts	smt_solver_baset
live_asts_sizes	smt_solver_baset
machine_ptr	smt_solver_baset
make_bit_bool(smt_astt a)	smt_solver_baset
make_bool_bit(smt_astt a)	smt_solver_baset
make_n_ary_and(const ast_vec &v)	smt_solver_baset
make_n_ary_or(const ast_vec &v)	smt_solver_baset
mathsat_convt(const namespacet &ns, const optionst &options)	mathsat_convt
max_rebuild_sources	smt_solver_baset	static
mk_add(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_and(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_array_sort(smt_sortt domain, smt_sortt range) override	mathsat_convt	virtual
mk_array_symbol(const std::string &name, const smt_sort *s, smt_sortt array_subtype) override	mathsat_convt
array_iface::mk_array_symbol(const std::string &name, smt_sortt sort, smt_sortt subtype)=0	array_iface	pure virtual
mk_bool_sort() override	mathsat_convt	virtual
mk_bv_sort(std::size_t width) override	mathsat_convt	virtual
mk_bvadd(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvand(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvashr(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvfp_rm_sort() override	mathsat_convt	virtual
mk_bvfp_sort(std::size_t ew, std::size_t sw) override	mathsat_convt	virtual
mk_bvlshr(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvmul(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvneg(smt_astt a) override	mathsat_convt	virtual
mk_bvnot(smt_astt a) override	mathsat_convt	virtual
mk_bvor(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvredand(smt_astt op)	smt_solver_baset
mk_bvredor(smt_astt op)	smt_solver_baset
mk_bvsdiv(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvsge(smt_astt a, smt_astt b)	smt_solver_baset	virtual
mk_bvsgt(smt_astt a, smt_astt b)	smt_solver_baset	virtual
mk_bvshl(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvsle(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvslt(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvsmod(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvsub(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvudiv(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvuge(smt_astt a, smt_astt b)	smt_solver_baset	virtual
mk_bvugt(smt_astt a, smt_astt b)	smt_solver_baset	virtual
mk_bvule(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvult(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvumod(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_bvxor(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_concat(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_div(smt_astt a, smt_astt b)	smt_solver_baset	virtual
mk_eq(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_extract(smt_astt a, unsigned int high, unsigned int low) override	mathsat_convt	virtual
mk_fbv_sort(std::size_t width) override	mathsat_convt	virtual
mk_fpbv_rm_sort() override	mathsat_convt	virtual
mk_fpbv_sort(const unsigned ew, const unsigned sw) override	mathsat_convt	virtual
mk_fresh(smt_sortt s, const std::string &tag, smt_sortt st=nullptr)	smt_solver_baset	virtual
mk_fresh_name(const std::string &tag)	smt_solver_baset
mk_from_bv_to_fp(smt_astt op, smt_sortt to) override	mathsat_convt	virtual
mk_from_fp_to_bv(smt_astt op) override	mathsat_convt	virtual
mk_ge(smt_astt a, smt_astt b)	smt_solver_baset	virtual
mk_gt(smt_astt a, smt_astt b)	smt_solver_baset	virtual
mk_implies(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_int2real(smt_astt a)	smt_solver_baset	virtual
mk_int_bv_sort(std::size_t width)	smt_solver_baset	inline
mk_int_sort() override	mathsat_convt	virtual
mk_isint(smt_astt a)	smt_solver_baset	virtual
mk_ite(smt_astt cond, smt_astt t, smt_astt f) override	mathsat_convt	virtual
mk_le(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_lt(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_mod(smt_astt a, smt_astt b)	smt_solver_baset	virtual
mk_mul(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_neg(smt_astt a) override	mathsat_convt	virtual
mk_neq(smt_astt a, smt_astt b)	smt_solver_baset	virtual
mk_not(smt_astt a) override	mathsat_convt	virtual
mk_or(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_quantifier(bool is_forall, std::vector< smt_astt > lhs, smt_astt rhs)	smt_solver_baset	inlinevirtual
mk_real2int(smt_astt a)	smt_solver_baset	virtual
mk_real_fp_sort(std::size_t ew, std::size_t sw)	smt_solver_baset	inline
mk_real_sort() override	mathsat_convt	virtual
mk_select(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_shl(smt_astt a, smt_astt b)	smt_solver_baset	virtual
mk_sign_ext(smt_astt a, unsigned int topwidth) override	mathsat_convt	virtual
mk_smt_bool(bool val) override	mathsat_convt	virtual
mk_smt_bv(const BigInt &theint, smt_sortt s) override	mathsat_convt	virtual
smt_solver_baset::mk_smt_bv(const BigInt &theint, std::size_t w)	smt_solver_baset	inlinevirtual
mk_smt_fpbv(const ieee_floatt &thereal) override	mathsat_convt	virtual
mk_smt_fpbv_abs(smt_astt op) override	mathsat_convt	virtual
mk_smt_fpbv_add(smt_astt lhs, smt_astt rhs, smt_astt rm) override	mathsat_convt	virtual
mk_smt_fpbv_div(smt_astt lhs, smt_astt rhs, smt_astt rm) override	mathsat_convt	virtual
mk_smt_fpbv_eq(smt_astt lhs, smt_astt rhs) override	mathsat_convt	virtual
mk_smt_fpbv_fma(smt_astt v1, smt_astt v2, smt_astt v3, smt_astt rm) override	mathsat_convt	virtual
mk_smt_fpbv_gt(smt_astt lhs, smt_astt rhs)	fp_convt	virtual
mk_smt_fpbv_gte(smt_astt lhs, smt_astt rhs)	fp_convt	virtual
mk_smt_fpbv_inf(bool sgn, unsigned ew, unsigned sw) override	mathsat_convt	virtual
mk_smt_fpbv_is_inf(smt_astt op) override	mathsat_convt	virtual
mk_smt_fpbv_is_nan(smt_astt op) override	mathsat_convt	virtual
mk_smt_fpbv_is_negative(smt_astt op) override	mathsat_convt	virtual
mk_smt_fpbv_is_normal(smt_astt op) override	mathsat_convt	virtual
mk_smt_fpbv_is_positive(smt_astt op) override	mathsat_convt	virtual
mk_smt_fpbv_is_zero(smt_astt op) override	mathsat_convt	virtual
mk_smt_fpbv_lt(smt_astt lhs, smt_astt rhs) override	mathsat_convt	virtual
mk_smt_fpbv_lte(smt_astt lhs, smt_astt rhs) override	mathsat_convt	virtual
mk_smt_fpbv_mul(smt_astt lhs, smt_astt rhs, smt_astt rm) override	mathsat_convt	virtual
mk_smt_fpbv_nan(bool sgn, unsigned ew, unsigned sw) override	mathsat_convt	virtual
mk_smt_fpbv_neg(smt_astt op) override	mathsat_convt	virtual
mk_smt_fpbv_rem(smt_astt lhs, smt_astt rhs) override	mathsat_convt	virtual
mk_smt_fpbv_rm(ieee_floatt::rounding_modet rm) override	mathsat_convt	virtual
mk_smt_fpbv_sqrt(smt_astt rd, smt_astt rm) override	mathsat_convt	virtual
mk_smt_fpbv_sub(smt_astt lhs, smt_astt rhs, smt_astt rm) override	mathsat_convt	virtual
mk_smt_int(const BigInt &theint) override	mathsat_convt	virtual
mk_smt_nearbyint_from_float(smt_astt from, smt_astt rm) override	mathsat_convt	virtual
mk_smt_real(const std::string &str) override	mathsat_convt	virtual
mk_smt_symbol(const std::string &name, const smt_sort *s) override	mathsat_convt
smt_solver_baset::mk_smt_symbol(const std::string &name, smt_sortt s)=0	smt_solver_baset	pure virtual
mk_smt_typecast_from_fpbv_to_fpbv(smt_astt from, smt_sortt to, smt_astt rm) override	mathsat_convt	virtual
mk_smt_typecast_from_fpbv_to_sbv(smt_astt from, std::size_t width) override	mathsat_convt	virtual
mk_smt_typecast_from_fpbv_to_ubv(smt_astt from, std::size_t width) override	mathsat_convt	virtual
mk_smt_typecast_sbv_to_fpbv(smt_astt from, smt_sortt to, smt_astt rm) override	mathsat_convt	virtual
mk_smt_typecast_ubv_to_fpbv(smt_astt from, smt_sortt to, smt_astt rm) override	mathsat_convt	virtual
mk_smt_uninterpreted_function(const std::string &name, const std::vector< smt_astt > &args, smt_sortt rangesort) override	mathsat_convt	virtual
mk_store(smt_astt a, smt_astt b, smt_astt c) override	mathsat_convt	virtual
mk_sub(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_subnormal_flush(smt_astt r, const floatbv_type2t &fbv_type, const expr2tc &rounding_mode)	smt_solver_baset
mk_truncated_div(const type2tc &type, smt_astt a, smt_astt b)	smt_solver_baset
mk_truncated_rem(const type2tc &type, smt_astt a, smt_astt b)	smt_solver_baset
mk_xor(smt_astt a, smt_astt b) override	mathsat_convt	virtual
mk_zero_ext(smt_astt a, unsigned int topwidth) override	mathsat_convt	virtual
new_solver_ast(typename the_solver_ast::solver_ast_type ast, smt_sortt sort)	smt_solver_baset	inline
note_assignment(const expr2tc &lhs, const expr2tc &rhs)	smt_solver_baset
note_division_operands(const expr2tc &expr, std::unordered_set< const expr2t * > &seen)	smt_solver_baset
ns	smt_solver_baset
null_ptr_ast	smt_solver_baset
options	smt_solver_baset
overflow_arith(const expr2tc &expr)	smt_solver_baset	virtual
overflow_cast(const expr2tc &expr)	smt_solver_baset	virtual
overflow_neg(const expr2tc &expr)	smt_solver_baset	virtual
pointer_array_of(const expr2tc &init_val, unsigned long array_width)	smt_solver_baset
pointer_logic	smt_solver_baset
pointer_repr_applies(const type2tc &ptr_type, const type2tc &bv_type)	smt_solver_baset
pointer_struct	smt_solver_baset
pop_array_ctx()	array_iface	inlinevirtual
pop_ctx() override	mathsat_convt	virtual
pre_solve()	smt_solver_baset
print_model() override	mathsat_convt	virtual
ptr_flatten_history	smt_solver_baset
ptr_flow	smt_solver_baset
ptr_foo_inited	smt_solver_baset
push_array_ctx()	array_iface	inlinevirtual
push_ctx() override	mathsat_convt	virtual
quantifier_counter	smt_solver_baset
ra_api	smt_solver_baset
record_flattened_pointer(smt_astt address, smt_astt pointer)	smt_solver_baset
renumber_map	smt_solver_baset
renumber_mapt typedef	smt_solver_baset
renumber_symbol_address(const expr2tc &guard, const expr2tc &addr_symbol, const expr2tc &new_size)	smt_solver_baset
rewrite_ptrs_to_structs(type2tc &type)	smt_solver_baset
round_fixedbv_to_int(smt_astt a, unsigned int width, unsigned int towidth)	smt_solver_baset
round_int_to_fp(smt_astt int_val, const floatbv_type2t &fbv_type, unsigned int source_width)	smt_solver_baset
round_real_to_int(smt_astt a)	smt_solver_baset
set_array_iface(array_iface *iface)	smt_solver_baset
set_fp_conv(fp_convt *iface)	smt_solver_baset
set_ra_conv(ra_apit *iface)	smt_solver_baset
set_tuple_iface(tuple_iface *iface)	smt_solver_baset
smt_cache	smt_solver_baset
smt_cache_mutex	smt_solver_baset
smt_cachet typedef	smt_solver_baset
smt_post_init()	smt_solver_baset
smt_solver_baset(const namespacet &_ns, const optionst &_options)	smt_solver_baset
smt_sort_cachet typedef	smt_solver_baset
solver_text() override	mathsat_convt	virtual
sort_cache	smt_solver_baset
step_assigned	smt_solver_baset
step_flattens	smt_solver_baset
step_guard	smt_solver_baset
step_overwritten	smt_solver_baset
step_sources	smt_solver_baset
supports_assumptions() const	smt_solver_baset	inlinevirtual
supports_bools_in_arrays	array_iface
tuple_api	smt_solver_baset
tuple_array_create_despatch(const expr2tc &expr, smt_sortt domain)	smt_solver_baset
uf_ackermann_counter	smt_solver_baset
uf_ackermann_history	smt_solver_baset
use_fp_api	mathsat_convt
~fp_convt()=default	fp_convt	virtual
~mathsat_convt() override	mathsat_convt
~smt_solver_baset()	smt_solver_baset	virtual