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