cprover
smt_terms.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
5 
7 #include <util/irep.h>
8 
9 #include <functional>
10 
11 class BigInt;
12 using mp_integer = BigInt;
13 
15 class smt_termt : protected irept, private smt_sortt::storert<smt_termt>
16 {
17 public:
18  // smt_termt does not support the notion of an empty / null state. Use
19  // optionalt<smt_termt> instead if an empty term is required.
20  smt_termt() = delete;
21 
22  using irept::pretty;
23 
24  bool operator==(const smt_termt &) const;
25  bool operator!=(const smt_termt &) const;
26 
27  const smt_sortt &get_sort() const;
28 
31 
37  template <typename derivedt>
38  class storert
39  {
40  protected:
42  static irept upcast(smt_termt term);
43  static const smt_termt &downcast(const irept &);
44  };
45 
46 protected:
47  smt_termt(irep_idt id, smt_sortt sort);
48 };
49 
50 template <typename derivedt>
52 {
53  static_assert(
54  std::is_base_of<irept, derivedt>::value &&
55  std::is_base_of<storert<derivedt>, derivedt>::value,
56  "Only irept based classes need to upcast smt_termt to store it.");
57 }
58 
59 template <typename derivedt>
61 {
62  return static_cast<irept &&>(std::move(term));
63 }
64 
65 template <typename derivedt>
67 {
68  return static_cast<const smt_termt &>(irep);
69 }
70 
72 {
73 public:
74  explicit smt_bool_literal_termt(bool value);
75  bool value() const;
76 };
77 
81 {
82 public:
95  irep_idt identifier() const;
96 };
97 
99 {
100 public:
102  smt_bit_vector_constant_termt(const mp_integer &value, std::size_t bit_width);
103  mp_integer value() const;
104 
105  // This deliberately hides smt_termt::get_sort, because bit_vector terms
106  // always have bit_vector sorts. The same sort data is returned for both
107  // functions either way. Therefore this hiding is benign if the kind of sort
108  // is not important and useful for avoiding casts if the term is a known
109  // smt_bit_vector_constant_termt at compile time and the `bit_width()` is
110  // needed.
111  const smt_bit_vector_sortt &get_sort() const;
112 };
113 
115 {
116 private:
122  std::vector<smt_termt> arguments);
123 
124 public:
126  std::vector<std::reference_wrapper<const smt_termt>> arguments() const;
127 
128  template <typename functiont>
129  class factoryt
130  {
131  private:
132  functiont function;
133 
134  public:
135  template <typename... function_type_argument_typest>
136  explicit factoryt(function_type_argument_typest &&... arguments)
137  : function{std::forward<function_type_argument_typest>(arguments)...}
138  {
139  }
140 
141  template <typename... argument_typest>
143  operator()(argument_typest &&... arguments) const
144  {
145  function.validate(arguments...);
146  auto return_sort = function.return_sort(arguments...);
148  smt_identifier_termt{function.identifier(), std::move(return_sort)},
149  {std::forward<argument_typest>(arguments)...}};
150  }
151  };
152 };
153 
155 {
156 public:
157 #define TERM_ID(the_id) virtual void visit(const smt_##the_id##_termt &) = 0;
158 #include "smt_terms.def"
159 #undef TERM_ID
160 };
161 
162 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const smt_bit_vector_sortt & get_sort() const
Definition: smt_terms.cpp:103
smt_bit_vector_constant_termt(const mp_integer &value, smt_bit_vector_sortt)
Definition: smt_terms.cpp:77
mp_integer value() const
Definition: smt_terms.cpp:98
smt_bool_literal_termt(bool value)
Definition: smt_terms.cpp:40
bool value() const
Definition: smt_terms.cpp:46
smt_function_application_termt operator()(argument_typest &&... arguments) const
Definition: smt_terms.h:143
factoryt(function_type_argument_typest &&... arguments)
Definition: smt_terms.h:136
const smt_identifier_termt & function_identifier() const
Definition: smt_terms.cpp:124
smt_function_application_termt(smt_identifier_termt function_identifier, std::vector< smt_termt > arguments)
Unchecked construction of function application terms.
Definition: smt_terms.cpp:110
std::vector< std::reference_wrapper< const smt_termt > > arguments() const
Definition: smt_terms.cpp:130
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:81
irep_idt identifier() const
Definition: smt_terms.cpp:72
smt_identifier_termt(irep_idt identifier, smt_sortt sort)
Constructs an identifier term with the given identifier and sort.
Definition: smt_terms.cpp:59
Class for adding the ability to up and down cast smt_sortt to and from irept.
Definition: smt_sorts.h:39
Class for adding the ability to up and down cast smt_termt to and from irept.
Definition: smt_terms.h:39
static irept upcast(smt_termt term)
Definition: smt_terms.h:60
static const smt_termt & downcast(const irept &)
Definition: smt_terms.h:66
const smt_sortt & get_sort() const
Definition: smt_terms.cpp:35
bool operator==(const smt_termt &) const
Definition: smt_terms.cpp:25
void accept(smt_term_const_downcast_visitort &) const
Definition: smt_terms.cpp:150
smt_termt()=delete
bool operator!=(const smt_termt &) const
Definition: smt_terms.cpp:30
Data structure for smt sorts.
BigInt mp_integer
Definition: smt_terms.h:12