cprover
Loading...
Searching...
No Matches
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
11class BigInt;
13
15class smt_termt : protected irept, private smt_sortt::storert<smt_termt>
16{
17public:
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
46protected:
48};
49
50template <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
59template <typename derivedt>
61{
62 return static_cast<irept &&>(std::move(term));
63}
64
65template <typename derivedt>
67{
68 return static_cast<const smt_termt &>(irep);
69}
70
72{
73public:
74 explicit smt_bool_literal_termt(bool value);
75 bool value() const;
76};
77
81{
82public:
95 irep_idt identifier() const;
96};
97
99{
100public:
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{
116private:
122 std::vector<smt_termt> arguments);
123
124public:
126 std::vector<std::reference_wrapper<const smt_termt>> arguments() const;
127
128 template <typename functiont>
130 {
131 private:
132 functiont function;
133
134 public:
135 template <typename... function_type_argument_typest>
140
141 template <typename... argument_typest>
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{
156public:
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
ait()
Definition ai.h:567
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
mp_integer value() const
Definition smt_terms.cpp:98
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
std::vector< std::reference_wrapper< const smt_termt > > arguments() const
Stores identifiers in unescaped and unquoted form.
Definition smt_terms.h:81
irep_idt identifier() const
Definition smt_terms.cpp:72
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
smt_termt()=delete
bool operator!=(const smt_termt &) const
Definition smt_terms.cpp:30
STL namespace.
Data structure for smt sorts.