1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 sexpr.h 7 8 Abstract: 9 10 Generic sexpr 11 12 Author: 13 14 Leonardo (leonardo) 2011-07-28 15 16 Notes: 17 18 --*/ 19 #pragma once 20 21 #include "util/rational.h" 22 #include "util/symbol.h" 23 #include "util/obj_ref.h" 24 #include "util/ref_vector.h" 25 26 class sexpr_manager; 27 28 class sexpr { 29 public: 30 enum class kind_t { 31 COMPOSITE, NUMERAL, BV_NUMERAL, STRING, KEYWORD, SYMBOL 32 }; 33 protected: 34 kind_t m_kind; 35 unsigned m_ref_count; 36 unsigned m_line; 37 unsigned m_pos; 38 sexpr(kind_t k, unsigned line, unsigned pos); 39 void display_atom(std::ostream & out) const; 40 friend class sexpr_manager; 41 public: inc_ref()42 void inc_ref() { m_ref_count++; } get_ref_count()43 unsigned get_ref_count() const { return m_ref_count; } get_line()44 unsigned get_line() const { return m_line; } get_pos()45 unsigned get_pos() const { return m_pos; } get_kind()46 kind_t get_kind() const { return m_kind; } is_composite()47 bool is_composite() const { return get_kind() == kind_t::COMPOSITE; } is_numeral()48 bool is_numeral() const { return get_kind() == kind_t::NUMERAL; } is_bv_numeral()49 bool is_bv_numeral() const { return get_kind() == kind_t::BV_NUMERAL; } is_string()50 bool is_string() const { return get_kind() == kind_t::STRING; } is_keyword()51 bool is_keyword() const { return get_kind() == kind_t::KEYWORD; } is_symbol()52 bool is_symbol() const { return get_kind() == kind_t::SYMBOL; } 53 rational const & get_numeral() const; 54 unsigned get_bv_size() const; 55 symbol get_symbol() const; 56 std::string const & get_string() const; 57 unsigned get_num_children() const; 58 sexpr * get_child(unsigned idx) const; 59 sexpr * const * get_children() const; 60 void display(std::ostream & out) const; 61 }; 62 63 class sexpr_manager { 64 small_object_allocator m_allocator; 65 ptr_vector<sexpr> m_to_delete; 66 void del(sexpr * n); 67 public: 68 sexpr_manager(); 69 sexpr * mk_composite(unsigned num_children, sexpr * const * children, unsigned line = UINT_MAX, unsigned pos = UINT_MAX); 70 sexpr * mk_numeral(rational const & val, unsigned line = UINT_MAX, unsigned pos = UINT_MAX); 71 sexpr * mk_bv_numeral(rational const & val, unsigned bv_size, unsigned line = UINT_MAX, unsigned pos = UINT_MAX); 72 sexpr * mk_string(std::string const & val, unsigned line = UINT_MAX, unsigned pos = UINT_MAX); 73 sexpr * mk_string(char const * val, unsigned line = UINT_MAX, unsigned pos = UINT_MAX); 74 sexpr * mk_keyword(symbol const & val, unsigned line = UINT_MAX, unsigned pos = UINT_MAX); 75 sexpr * mk_symbol(symbol const & val, unsigned line = UINT_MAX, unsigned pos = UINT_MAX); inc_ref(sexpr * n)76 void inc_ref(sexpr * n) { n->inc_ref(); } dec_ref(sexpr * n)77 void dec_ref(sexpr * n) { SASSERT(n->m_ref_count > 0); n->m_ref_count--; if (n->m_ref_count == 0) del(n); } 78 }; 79 80 typedef obj_ref<sexpr, sexpr_manager> sexpr_ref; 81 typedef ref_vector<sexpr, sexpr_manager> sexpr_ref_vector; 82 83