CBMC
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 
6 #include <util/irep.h>
7 
9 
10 #include "smt_index.h"
11 #include "smt_sorts.h"
12 
13 #include <functional>
14 #include <utility>
15 
16 class BigInt; // IWYU pragma: keep
17 using mp_integer = BigInt;
18 
20 class smt_termt : protected irept, private smt_sortt::storert<smt_termt>
21 {
22 public:
23  // smt_termt does not support the notion of an empty / null state. Use
24  // std::optional<smt_termt> instead if an empty term is required.
25  smt_termt() = delete;
26 
27  using irept::pretty;
28 
29  bool operator==(const smt_termt &) const;
30  bool operator!=(const smt_termt &) const;
31 
32  const smt_sortt &get_sort() const;
33 
36 
42  template <typename derivedt>
43  class storert
44  {
45  protected:
47  static irept upcast(smt_termt term);
48  static const smt_termt &downcast(const irept &);
49  };
50 
51 protected:
52  smt_termt(irep_idt id, smt_sortt sort);
53 };
54 
55 template <typename derivedt>
57 {
58  static_assert(
59  std::is_base_of<irept, derivedt>::value &&
60  std::is_base_of<storert<derivedt>, derivedt>::value,
61  "Only irept based classes need to upcast smt_termt to store it.");
62 }
63 
64 template <typename derivedt>
66 {
67  return static_cast<irept &&>(std::move(term));
68 }
69 
70 template <typename derivedt>
72 {
73  return static_cast<const smt_termt &>(irep);
74 }
75 
77 {
78 public:
79  explicit smt_bool_literal_termt(bool value);
80  bool value() const;
81 };
82 
92  private smt_indext::storert<smt_identifier_termt>
93 {
94 public:
110  smt_sortt sort,
111  std::vector<smt_indext> indices = {});
112  irep_idt identifier() const;
113  std::vector<std::reference_wrapper<const smt_indext>> indices() const;
114 };
115 
117 {
118 public:
120  smt_bit_vector_constant_termt(const mp_integer &value, std::size_t bit_width);
121  mp_integer value() const;
122 
123  // This deliberately hides smt_termt::get_sort, because bit_vector terms
124  // always have bit_vector sorts. The same sort data is returned for both
125  // functions either way. Therefore this hiding is benign if the kind of sort
126  // is not important and useful for avoiding casts if the term is a known
127  // smt_bit_vector_constant_termt at compile time and the `bit_width()` is
128  // needed.
129  const smt_bit_vector_sortt &get_sort() const;
130 };
131 
133 {
134 private:
140  std::vector<smt_termt> arguments);
141 
142  // This is used to detect if \p functiont has an `indicies` member function.
143  // It will resolve to std::true_type if it does or std::false type otherwise.
144  template <class functiont, class = void>
145  struct has_indicest : std::false_type
146  {
147  };
148 
149  template <class functiont>
150  struct has_indicest<
151  functiont,
152  std::void_t<decltype(std::declval<functiont>().indices())>> : std::true_type
153  {
154  };
155 
158  template <class functiont>
159  static std::vector<smt_indext> indices(const functiont &function)
160  {
161  if constexpr(has_indicest<functiont>::value)
162  return function.indices();
163  else
164  return {};
165  }
166 
167 public:
169  std::vector<std::reference_wrapper<const smt_termt>> arguments() const;
170 
171  template <typename functiont>
172  class factoryt
173  {
174  private:
175  functiont function;
176 
177  public:
178  template <typename... function_type_argument_typest>
179  explicit factoryt(function_type_argument_typest &&...arguments) noexcept
180  : function{std::forward<function_type_argument_typest>(arguments)...}
181  {
182  }
183 
184  template <typename... argument_typest>
186  operator()(argument_typest &&...arguments) const
187  {
188  function.validate(arguments...);
189  auto return_sort = function.return_sort(arguments...);
192  function.identifier(), std::move(return_sort), indices(function)},
193  {std::forward<argument_typest>(arguments)...}};
194  }
195 
196  template <typename... argument_typest>
198  validation(argument_typest &&...arguments) const
199  {
200  const auto validation_errors = function.validation_errors(arguments...);
201  if(!validation_errors.empty())
202  return response_or_errort<smt_termt>{validation_errors};
203  auto return_sort = function.return_sort(arguments...);
206  function.identifier(), std::move(return_sort), indices(function)},
207  {std::forward<argument_typest>(arguments)...}}};
208  }
209  };
210 };
211 
213 {
214 public:
216  std::vector<smt_identifier_termt> bound_variables,
218  std::vector<std::reference_wrapper<const smt_identifier_termt>>
219  bound_variables() const;
220  const smt_termt &predicate() const;
221 };
222 
224 {
225 public:
227  std::vector<smt_identifier_termt> bound_variables,
229  std::vector<std::reference_wrapper<const smt_identifier_termt>>
230  bound_variables() const;
231  const smt_termt &predicate() const;
232 };
233 
235 {
236 public:
237 #define TERM_ID(the_id) virtual void visit(const smt_##the_id##_termt &) = 0;
238 #include "smt_terms.def"
239 #undef TERM_ID
240 };
241 
242 #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:38
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:364
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:482
Holds either a valid parsed response or response sub-tree of type.
const smt_bit_vector_sortt & get_sort() const
Definition: smt_terms.cpp:121
smt_bit_vector_constant_termt(const mp_integer &value, smt_bit_vector_sortt)
Definition: smt_terms.cpp:95
mp_integer value() const
Definition: smt_terms.cpp:116
smt_bool_literal_termt(bool value)
Definition: smt_terms.cpp:41
bool value() const
Definition: smt_terms.cpp:47
const smt_termt & predicate() const
Definition: smt_terms.cpp:210
std::vector< std::reference_wrapper< const smt_identifier_termt > > bound_variables() const
Definition: smt_terms.cpp:216
smt_exists_termt(std::vector< smt_identifier_termt > bound_variables, smt_termt predicate)
Definition: smt_terms.cpp:189
smt_forall_termt(std::vector< smt_identifier_termt > bound_variables, smt_termt predicate)
Definition: smt_terms.cpp:155
const smt_termt & predicate() const
Definition: smt_terms.cpp:176
std::vector< std::reference_wrapper< const smt_identifier_termt > > bound_variables() const
Definition: smt_terms.cpp:182
factoryt(function_type_argument_typest &&...arguments) noexcept
Definition: smt_terms.h:179
smt_function_application_termt operator()(argument_typest &&...arguments) const
Definition: smt_terms.h:186
response_or_errort< smt_termt > validation(argument_typest &&...arguments) const
Definition: smt_terms.h:198
static std::vector< smt_indext > indices(const functiont &function)
Returns function.indices() if functiont has an indices member function or returns an empty collection...
Definition: smt_terms.h:159
const smt_identifier_termt & function_identifier() const
Definition: smt_terms.cpp:142
smt_function_application_termt(smt_identifier_termt function_identifier, std::vector< smt_termt > arguments)
Unchecked construction of function application terms.
Definition: smt_terms.cpp:128
std::vector< std::reference_wrapper< const smt_termt > > arguments() const
Definition: smt_terms.cpp:148
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:93
irep_idt identifier() const
Definition: smt_terms.cpp:81
smt_identifier_termt(irep_idt identifier, smt_sortt sort, std::vector< smt_indext > indices={})
Constructs an identifier term with the given identifier and sort.
Definition: smt_terms.cpp:60
std::vector< std::reference_wrapper< const smt_indext > > indices() const
Definition: smt_terms.cpp:87
Class for adding the ability to up and down cast smt_indext to and from irept.
Definition: smt_index.h:37
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:44
static irept upcast(smt_termt term)
Definition: smt_terms.h:65
static const smt_termt & downcast(const irept &)
Definition: smt_terms.h:71
const smt_sortt & get_sort() const
Definition: smt_terms.cpp:36
bool operator==(const smt_termt &) const
Definition: smt_terms.cpp:26
void accept(smt_term_const_downcast_visitort &) const
Definition: smt_terms.cpp:236
smt_termt()=delete
bool operator!=(const smt_termt &) const
Definition: smt_terms.cpp:31
Data structure for smt sorts.
BigInt mp_integer
Definition: smt_terms.h:17