smt_solver.h

Go to the documentation of this file.

#ifndef _ESBMC_PROP_SMT_SMT_SOLVER_H_
#define _ESBMC_PROP_SMT_SMT_SOLVER_H_
 
#include <optional>
#include <boost/multi_index/hashed_index.hpp>
#include <boost/multi_index/member.hpp>
#include <boost/multi_index/ordered_index.hpp>
#include <boost/multi_index_container.hpp>
#include <memory>
#include <mutex>
#include <set>
#include <utility>
#include <unordered_map>
#include <unordered_set>
#include <solvers/prop/literal.h>
#include <solvers/prop/pointer_logic.h>
#include <solvers/smt/smt_result.h>
#include <irep2/irep2_utils.h>
#include <util/message/message.h>
#include <util/symtab/namespace.h>
#include <util/base/threeval.h>

 
// Forward dec.
class fp_convt;
class ir_ieee_convt;
class smt_solver_baset;

expr2tc byte_update_bit_offset(const byte_update2t &data);

bool lowest_address_high();

unsigned flattened_position(unsigned offset, unsigned width, unsigned total);

expr2tc union_member_bits(const expr2tc &bits, unsigned width);

expr2tc union_bits_with_member(
  const expr2tc &rest,
  const expr2tc &member,
  unsigned bits);

expr2tc union_bits_of_member(const expr2tc &member, unsigned bits);
class ra_apit;
 
#include <solvers/smt/smt_array.h>
#include <solvers/smt/tuple/smt_tuple.h>
#include <solvers/smt/fp/fp_conv.h>

class smt_solver_baset
{
public:
  typedef std::vector<smt_astt> ast_vec;
 
  template <typename the_solver_ast>
  smt_astt
  new_solver_ast(typename the_solver_ast::solver_ast_type ast, smt_sortt sort)
  {
    return new the_solver_ast(this, ast, sort);
  }

  smt_solver_baset(const namespacet &_ns, const optionst &_options);
 
  virtual ~smt_solver_baset();

  void smt_post_init();
 
  // The API that we provide to the rest of the world:

  virtual void push_ctx();
  virtual void pop_ctx();

  virtual bool has_model() const
  {
    return true;
  }

  smt_astt convert_ast(const expr2tc &expr);

  smt_astt convert_ast_node(const expr2tc &expr);

  smt_astt convert_ieee_arith_2op(const expr2tc &expr);

  smt_astt convert_ast(
    const expr2tc &expr,
    const type2tc &type,
    smt_astt const *args,
    struct expr_op_convert ops);
 
  smt_astt convert_assign(const expr2tc &expr);
  void define(const expr2tc &expr);

  void dump_expr(const expr2tc &expr);
 
  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);

  smt_astt imply_ast(smt_astt a, smt_astt b);

  virtual void assert_ast(smt_astt a) = 0;

  virtual smt_resultt dec_solve() = 0;

  virtual smt_resultt dec_solve_assuming(const ast_vec &assumptions);
  virtual bool supports_assumptions() const
  {
    return false;
  }
 
  void pre_solve();

  virtual expr2tc get_by_type(const expr2tc &expr);

  virtual expr2tc get_by_ast(const type2tc &type, smt_astt a);

  expr2tc get_by_ast(const expr2tc &expr);

  expr2tc get_by_value(const type2tc &type, BigInt value);

  virtual bool get_rational(smt_astt a, BigInt &numerator, BigInt &denominator)
  {
    // Default implementation returns false - solver-specific implementations
    // should override this
    (void)a;
    (void)numerator;
    (void)denominator;
    return false;
  }

  std::optional<expr2tc> get_index_value(const expr2tc &expr, expr2tc &res);
  std::optional<expr2tc> get_index(const expr2tc &expr, expr2tc &res);
 
  virtual expr2tc get(const expr2tc &expr);

  virtual const std::string solver_text() = 0;

  virtual tvt l_get(smt_astt a);

  tvt l_get(const expr2tc &expr);


 
  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)
  {
    (void)is_forall;
    (void)lhs;
    (void)rhs;
    abort();
  }
 
  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)
  {
    if (int_encoding)
      return mk_int_sort();
 
    if (width == 0)
      width = 1;
 
    return mk_bv_sort(width);
  }

  smt_sortt mk_real_fp_sort(std::size_t ew, std::size_t sw)
  {
    if (int_encoding)
      return mk_real_sort();
 
    if (config.ansi_c.use_fixed_for_float)
      return mk_fbv_sort(ew + sw);
 
    return fp_api->mk_fpbv_sort(ew, sw);
  }

  virtual smt_sortt mk_bool_sort();

  virtual smt_sortt mk_real_sort();

  virtual smt_sortt mk_int_sort();

  virtual smt_sortt mk_bv_sort(std::size_t width);

  virtual smt_sortt mk_fbv_sort(std::size_t width);

  virtual smt_sortt mk_bvfp_sort(std::size_t ew, std::size_t sw);

  virtual smt_sortt mk_bvfp_rm_sort();

  virtual smt_sortt mk_array_sort(smt_sortt domain, smt_sortt range);

  virtual smt_astt mk_smt_int(const BigInt &theint) = 0;

  virtual smt_astt mk_smt_real(const std::string &str) = 0;
 
  // Returns SMT AST representing real zero
  smt_astt get_zero_real();
  // Returns SMT AST representing double precision minimum normal value
  // (2^-1022)
  smt_astt get_double_min_normal();
  // Returns SMT AST representing double precision minimum subnormal value
  // (2^-1074)
  smt_astt get_double_min_subnormal();
  // Returns SMT AST representing double precision maximum normal value
  // (~1.7976931348623157e+308)
  smt_astt get_double_max_normal();
  // Returns SMT AST representing single precision minimum normal value (2^-126)
  smt_astt get_single_min_normal();
  // Returns SMT AST representing single precision minimum subnormal value
  // (2^-149)
  smt_astt get_single_min_subnormal();
  // Returns SMT AST representing single precision maximum normal value
  // (~3.4028234663852886e+38)
  smt_astt get_single_max_normal();
  // Under --ir-ieee, returns real zero when r lies in the region that
  // rounds to zero under the selected rounding mode; otherwise returns r
  // unchanged. This models only the zero/nonzero underflow boundary:
  // signed zero and subnormal-grid quantization are not represented.
  // Returns r unchanged for unsupported float formats.
  smt_astt mk_subnormal_flush(
    smt_astt r,
    const floatbv_type2t &fbv_type,
    const expr2tc &rounding_mode);
 
  // Returns SMT AST for the integer-encoding sentinel for double +∞:
  // max_normal+1
  smt_astt get_double_inf_sentinel();
  // Returns SMT AST for the integer-encoding sentinel for single +∞:
  // max_normal+1
  smt_astt get_single_inf_sentinel();
  // Returns SMT AST for the double precision relative error bound under
  // round-to-nearest: half machine epsilon = 2^-53 ~ 1.11e-16
  smt_astt get_double_eps_rel();
  // Returns SMT AST for the single precision relative error bound under
  // round-to-nearest: half machine epsilon = 2^-24 ~ 5.96e-08
  smt_astt get_single_eps_rel();
  // Returns SMT AST for the double precision directional error bound under
  // round-toward-+inf: full machine epsilon = 2^-52 ~ 2.22e-16
  smt_astt get_double_eps_up();
  // Returns SMT AST for the single precision directional error bound under
  // round-toward-+inf: full machine epsilon = 2^-23 ~ 1.19e-07
  smt_astt get_single_eps_up();

  virtual smt_astt mk_smt_bv(const BigInt &theint, std::size_t w)
  {
    return mk_smt_bv(theint, mk_int_bv_sort(w));
  }

  virtual smt_astt mk_smt_bv(const BigInt &theint, smt_sortt s) = 0;

  virtual smt_astt mk_smt_bool(bool val) = 0;

  virtual smt_astt mk_smt_symbol(const std::string &name, smt_sortt s) = 0;

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

  virtual smt_astt
  mk_extract(smt_astt a, unsigned int high, unsigned int low) = 0;

  virtual smt_astt mk_sign_ext(smt_astt a, unsigned int topwidth) = 0;

  virtual smt_astt mk_zero_ext(smt_astt a, unsigned int topwidth) = 0;

  virtual smt_astt mk_concat(smt_astt a, smt_astt b) = 0;

  virtual smt_astt mk_ite(smt_astt cond, smt_astt t, smt_astt f) = 0;

  virtual tvt get_bool(smt_astt a) = 0;

  virtual BigInt get_bv(smt_astt a, bool is_signed) = 0;

  smt_astt mk_bvredor(smt_astt op);

  smt_astt mk_bvredand(smt_astt op);



  virtual smt_astt overflow_arith(const expr2tc &expr);

  virtual smt_astt overflow_cast(const expr2tc &expr);

  virtual smt_astt overflow_neg(const expr2tc &expr);

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

  virtual std::string dump_smt();

  virtual void print_model();



  virtual smt_astt convert_array_index(const expr2tc &expr);

  virtual smt_astt convert_array_store(const expr2tc &expr);



  virtual smt_astt
  mk_fresh(smt_sortt s, const std::string &tag, smt_sortt st = nullptr);
  std::string mk_fresh_name(const std::string &tag);
 
  void renumber_symbol_address(
    const expr2tc &guard,
    const expr2tc &addr_symbol,
    const expr2tc &new_size);

  smt_sortt convert_sort(const type2tc &type);
  smt_astt convert_terminal(const expr2tc &expr);

  smt_astt convert_pointer_arith(const expr2tc &expr, const type2tc &t);
  smt_astt divide_by_element_size(const expr2tc &diff, const expr2tc &size);
  smt_astt convert_ptr_cmp(
    const expr2tc &expr,
    const expr2tc &expr2,
    const expr2tc &templ_expr);
  smt_astt convert_addr_of(const expr2tc &expr);
  smt_astt convert_member(const expr2tc &expr);
  smt_astt convert_identifier_pointer(
    const expr2tc &expr,
    const std::string &sym,
    const typet *type);

  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);
  smt_astt convert_is_inf(const expr2tc &expr);
  smt_astt convert_is_normal(const expr2tc &expr);
  smt_astt convert_is_finite(const expr2tc &expr);
  smt_astt convert_signbit(const expr2tc &expr);
  smt_astt convert_popcount(const expr2tc &expr);
  smt_astt convert_bswap(const expr2tc &expr);
  smt_astt convert_rounding_mode(const expr2tc &expr);
  smt_astt convert_byte_extract(const expr2tc &expr);
  /* Integer mode byte extraction helper functions */
  smt_astt convert_byte_extract_int_mode(
    const byte_extract2t &data,
    expr2tc source,
    expr2tc offs,
    unsigned int src_width);
  /* Bit-vector mode byte extraction helper functions */
  smt_astt convert_byte_extract_bv_mode(
    const byte_extract2t &data,
    expr2tc source,
    expr2tc offs,
    unsigned int src_width);
  /* Helper function for integer arithmetic right shift simulation */
  expr2tc create_int_right_shift(expr2tc source, expr2tc shift_amount);
  smt_astt convert_byte_update(const expr2tc &expr);
  smt_astt convert_byte_update_int_mode(const byte_update2t &data);
  expr2tc convert_byte_update_int_mode_expr(
    const byte_update2t &data,
    expr2tc source,
    expr2tc offs,
    expr2tc update_value,
    unsigned int src_width);
  smt_astt convert_byte_update_bv_mode(const byte_update2t &data);
  smt_astt convert_bitcast(const expr2tc &expr);
  smt_astt convert_pointer_bitcast(const expr2tc &from, const type2tc &to_type);
  smt_astt convert_bitcast_to_fp(const expr2tc &from, const type2tc &to_type);
  smt_astt
  convert_bitcast_to_struct(const expr2tc &from, const type2tc &to_type);
  smt_astt encode_pointer_repr(const expr2tc &ptr, const type2tc &to_type);
  smt_astt decode_pointer_repr(const expr2tc &repr, const type2tc &to_type);
  bool pointer_repr_applies(const type2tc &ptr_type, const type2tc &bv_type);
  void assert_expr(const expr2tc &e);
  void note_division_operands(
    const expr2tc &expr,
    std::unordered_set<const expr2t *> &seen);
  smt_astt convert_modulus(const modulus2t &m, smt_astt a, smt_astt b);
  smt_astt mk_truncated_div(const type2tc &type, smt_astt a, smt_astt b);
  smt_astt mk_truncated_rem(const type2tc &type, smt_astt a, smt_astt b);
  smt_astt array_create(const expr2tc &expr);

  void init_addr_space_array();
  void set_tuple_iface(tuple_iface *iface);
  void set_array_iface(array_iface *iface);
  void set_fp_conv(fp_convt *iface);
  void set_ra_conv(ra_apit *iface);
 
  void bump_addrspace_array(unsigned int idx, const expr2tc &val);
  std::string get_cur_addrspace_ident();

  std::set<std::pair<expr2tc, expr2tc>> divided_operand_pairs;
  void finalize_pointer_chain(unsigned int obj_num);

  smt_astt convert_typecast_to_bool(const typecast2t &cast);
  smt_astt convert_typecast_to_fixedbv_nonint(const expr2tc &cast);
  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);
  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);
  smt_astt convert_typecast_from_ptr(const typecast2t &cast);
  smt_astt convert_typecast_to_struct(const typecast2t &cast);
  smt_astt convert_typecast(const expr2tc &expr);
  smt_astt convert_typecast_to_fpbv(const typecast2t &cast);
  smt_astt convert_typecast_from_fpbv(const typecast2t &cast);
  smt_astt round_real_to_int(smt_astt a);
  smt_astt
  round_fixedbv_to_int(smt_astt a, unsigned int width, unsigned int towidth);
  smt_astt round_int_to_fp(
    smt_astt int_val,
    const floatbv_type2t &fbv_type,
    unsigned int source_width);

  smt_astt tuple_array_create_despatch(const expr2tc &expr, smt_sortt domain);

  smt_astt make_bool_bit(smt_astt a);
  smt_astt make_bit_bool(smt_astt a);

  expr2tc fix_array_idx(const expr2tc &idx, const type2tc &array_type);
  type2tc flatten_array_type(const type2tc &type);
  type2tc get_flattened_array_subtype(const type2tc &type);
  expr2tc array_domain_to_width(const type2tc &type);

  void rewrite_ptrs_to_structs(type2tc &type);

  expr2tc decompose_select_chain(const expr2tc &expr, expr2tc &base);
  expr2tc decompose_store_chain(const expr2tc &expr, expr2tc &base);

  struct flat_storet
  {
    expr2tc index;
    expr2tc value;
  };

  void expand_row_stores(
    const expr2tc &row,
    const expr2tc &offset,
    std::vector<flat_storet> &stores);

  bool decompose_stores(
    const expr2tc &expr,
    const expr2tc &offset,
    std::vector<flat_storet> &stores,
    expr2tc &base);

  smt_astt convert_array_of_prep(const expr2tc &expr);
  smt_astt pointer_array_of(const expr2tc &init_val, unsigned long array_width);
 
  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;
 
  // Ours:
  expr2tc get_array(const type2tc &type, smt_astt array);
  expr2tc get_array(const expr2tc &expr);
 
  void delete_all_asts();

 
  // Types
 
  // Type for (optional) AST cache
 
  struct smt_cache_entryt
  {
    const expr2tc val;
    smt_astt ast;
    unsigned int level;
  };
 
  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;
 
  // Members
  unsigned int ctx_level;

  smt_cachet smt_cache;
  std::mutex smt_cache_mutex;
  smt_sort_cachet sort_cache;

  std::unordered_map<smt_astt, tvt> l_get_cache;
  std::unordered_map<smt_astt, std::pair<type2tc, expr2tc>> get_ast_cache;
  std::list<pointer_logict> pointer_logic;
  type2tc pointer_struct;
  type2tc machine_ptr;
  smt_sortt boolean_sort;
  bool int_encoding;
  bool ir_ieee;
  const namespacet &ns;
  /* Options contain all the parameters set by the user to run ESBMC */
  const optionst &options;
 
  bool ptr_foo_inited;
 
  smt_astt null_ptr_ast;
  smt_astt invalid_ptr_ast;

  size_t quantifier_counter = 0;

  struct uf_ackermann_entry
  {
    std::vector<smt_astt> args;
    smt_astt result;
    unsigned int level;
  };

  std::unordered_map<std::string, std::vector<uf_ackermann_entry>>
    uf_ackermann_history;
  size_t uf_ackermann_counter = 0;

  struct ptr_flatten_entry
  {
    smt_astt address;
    smt_astt pointer;
    smt_astt guard;
    unsigned int level;
    size_t id;
  };

  std::vector<ptr_flatten_entry> ptr_flatten_history;
  static constexpr size_t max_rebuild_sources = 32;
  std::unordered_map<expr2tc, ptr_flatten_entry, irep2_hash> flattened;
  void record_flattened_pointer(smt_astt address, smt_astt pointer);

  smt_astt step_guard = nullptr;
  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;
  void begin_step(const expr2tc &guard, const expr2tc &cond);
  void note_assignment(const expr2tc &lhs, const expr2tc &rhs);
  void end_step();

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

  std::map<std::string, unsigned int> fresh_map;

  std::list<unsigned int> addr_space_sym_num;
  type2tc addr_space_type;
  type2tc addr_space_arr_type;
  std::list<std::map<unsigned, bool>> addr_space_data;

  expr2tc current_valid_objects_sym;
 
  // XXX - push-pop will break here.
  typedef std::map<std::string, smt_astt> renumber_mapt;
  std::vector<renumber_mapt> renumber_map;

  std::vector<smt_astt> live_asts;
  std::vector<unsigned int> live_asts_sizes;
 
  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;
 
  // Workaround for integer shifts. This is an array of the powers of two,
  // up to 2^64.
  smt_astt int_shift_op_array;
 
private:
  expr2tc get_by_ast_uncached(const type2tc &type, smt_astt a);
 
  double convert_rational_to_double(
    const BigInt &numerator,
    const BigInt &denominator);
};

type2tc make_array_domain_type(const array_type2t &arr);

unsigned long array_domain_width_or_word_size(const array_type2t &arr);
 
// Define here to enable inlining
inline smt_ast::smt_ast(smt_solver_baset *ctx, smt_sortt s)
  : sort(s), context(ctx)
{
  assert(sort != nullptr);
  ctx->live_asts.push_back(this);
}
 
/* Type for push/pop-aware symbol table cache, required by some solvers */
 
struct symtab_entryt
{
  std::string val;
  smt_astt ast;
  unsigned int level;
 
  symtab_entryt(std::string val, smt_astt ast, unsigned int level)
    : val(std::move(val)), ast(ast), level(level)
  {
  }
};
 
typedef boost::multi_index_container<
  symtab_entryt,
  boost::multi_index::indexed_by<
    boost::multi_index::hashed_unique<
      BOOST_MULTI_INDEX_MEMBER(symtab_entryt, std::string, val)>,
    boost::multi_index::ordered_non_unique<
      BOOST_MULTI_INDEX_MEMBER(symtab_entryt, unsigned int, level),
      std::greater<unsigned int>>>>
  symtabt;
 
#endif /* _ESBMC_PROP_SMT_SMT_SOLVER_H_ */