Skip to content

Commit 505f45c

Browse files
Class for smt2 asts and functions for creating ASTs
This is to represent the structure of the smt2 instance generated by smt2_conv. This will allow separation between the structure and the printing of these instances. The structure is not used in this commit but will ultimately be used by convert_expr.
1 parent e3f7deb commit 505f45c

File tree

2 files changed

+360
-0
lines changed

2 files changed

+360
-0
lines changed

src/solvers/smt2/smt2_ast.cpp

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
/*******************************************************************\
2+
3+
Module: SMT2 solver
4+
5+
Author: Romain Brenguier, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include <util/make_unique.h>
10+
#include "smt2_ast.h"
11+
12+
std::unique_ptr<smt2_ast_symbolt> smt2_ast_symbolt::make(std::string symbol)
13+
{
14+
return util_make_unique<smt2_ast_symbolt>(std::move(symbol));
15+
}
16+
17+
void print(std::shared_ptr<smt2_astt> ast, std::ostream &stream)
18+
{
19+
smt2_astt::visitort print_visitor;
20+
print_visitor.data = [&stream](const std::unique_ptr<smt2_ast_leaft> &data){
21+
data->print(stream);
22+
};
23+
print_visitor.first_child = [&stream](){
24+
stream << "(";
25+
};
26+
print_visitor.next_sibling = [&stream](){
27+
stream << " ";
28+
};
29+
print_visitor.parent = [&stream](){
30+
stream << ")";
31+
};
32+
33+
smt2_astt::dfs(ast, print_visitor);
34+
}
35+
36+
std::shared_ptr<smt2_astt> detail::make_tree(
37+
std::string &&symbol)
38+
{
39+
return smt2_astt::make_leaf(smt2_ast_symbolt::make(std::move(symbol)));
40+
}
41+
42+
std::shared_ptr<smt2_astt> detail::make_tree(
43+
std::unique_ptr<smt2_ast_leaft> leaf)
44+
{
45+
return smt2_astt::make_leaf(std::move(leaf));
46+
}
47+
48+
std::shared_ptr<treet<smt2_ast_leaft>> detail::make_tree(
49+
std::shared_ptr<smt2_astt> tree)
50+
{
51+
return tree;
52+
}
53+
54+
std::unique_ptr<smt2_ast_leaft> smt2_ast_intt::make(mp_integer value)
55+
{
56+
return util_make_unique<smt2_ast_intt>(value);
57+
}
58+
59+
std::shared_ptr<treet<smt2_ast_leaft>> smt2_ast_index(
60+
std::shared_ptr<treet<smt2_ast_leaft>> array,
61+
std::shared_ptr<treet<smt2_ast_leaft>> index)
62+
{
63+
return smt2_ast_node(std::move(array), ".", std::move(index));
64+
}
65+
66+
std::shared_ptr<treet<smt2_ast_leaft>> smt2_not(
67+
std::shared_ptr<treet<smt2_ast_leaft>> ast)
68+
{
69+
return smt2_ast_node("not", std::move(ast));
70+
}
71+
72+
std::shared_ptr<treet<smt2_ast_leaft>> smt2_zero_extend(
73+
const mp_integer &width)
74+
{
75+
return smt2_ast_node("_", "zero_extend", smt2_ast_intt::make(width));
76+
}
77+
78+
std::shared_ptr<treet<smt2_ast_leaft>> smt2_extract(
79+
const mp_integer &width, const mp_integer &offset)
80+
{
81+
return smt2_ast_node(
82+
"_", "extract", smt2_ast_intt::make(width), smt2_ast_intt::make(offset));
83+
}
84+
85+
std::shared_ptr<smt2_astt> smt2_bv(
86+
const mp_integer &index, const mp_integer &width)
87+
{
88+
const std::string bv = "bv" + integer2string(index);
89+
return smt2_ast_node("_", bv, smt2_ast_leaf(width));
90+
}

src/solvers/smt2/smt2_ast.h

Lines changed: 270 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,270 @@
1+
/*******************************************************************\
2+
3+
Module: SMT2 solver
4+
5+
Author: Romain Brenguier, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file Abstract Syntax Tree for SMT2
10+
11+
#ifndef CPROVER_SOLVERS_SMT2_SMT2_AST_H
12+
#define CPROVER_SOLVERS_SMT2_SMT2_AST_H
13+
14+
#include <memory>
15+
#include <util/mp_arith.h>
16+
#include <vector>
17+
#include <util/invariant.h>
18+
#include <util/arith_tools.h>
19+
20+
/// Left-child right-sibling tree
21+
/// https://en.wikipedia.org/wiki/Left-child_right-sibling_binary_tree
22+
template<typename datat>
23+
class treet
24+
{
25+
public:
26+
static std::shared_ptr<treet<datat>> make_node(
27+
std::vector<std::shared_ptr<treet<datat>>> &&children)
28+
{
29+
auto result = std::make_shared<treet<datat>>();
30+
if(children.empty())
31+
return result;
32+
children.back()->parent = result;
33+
for(std::size_t i = children.size() - 1; i != 0; --i)
34+
children[i - 1]->next_sibling = std::move(children[i]);
35+
result->first_child = std::move(children[0]);
36+
return result;
37+
}
38+
39+
static std::shared_ptr<treet<datat>> make_leaf(
40+
std::unique_ptr<datat> leaf)
41+
{
42+
auto result = std::make_shared<treet<datat>>();
43+
result->data = std::move(leaf);
44+
return result;
45+
}
46+
47+
/// Make \p child a child of \p tree. \p child is modified so that parent
48+
/// points to tree. \p child should not have parent before this function is
49+
/// called.
50+
static void add_child(
51+
std::shared_ptr<treet<datat>> tree,
52+
std::shared_ptr<treet<datat>> child)
53+
{
54+
PRECONDITION(tree != nullptr);
55+
PRECONDITION(child->parent.lock() == nullptr);
56+
child->parent = tree;
57+
if(tree->first_child == nullptr)
58+
{
59+
tree->first_child = child;
60+
return;
61+
}
62+
auto last_visited_child = tree->first_child;
63+
while(last_visited_child->next_sibling != nullptr)
64+
last_visited_child = last_visited_child->next_sibling;
65+
last_visited_child->next_sibling = child;
66+
}
67+
68+
/// Type of visitor used for dfs
69+
///
70+
/// A visitor has to provide functions \c first_child, \c next_sibling,
71+
/// \c parent, and \c data which are invoked at the relevant points of the
72+
/// exploration.
73+
struct visitort
74+
{
75+
std::function<void(const std::unique_ptr<datat> &)> data;
76+
std::function<void(void)> first_child;
77+
std::function<void(void)> next_sibling;
78+
std::function<void(void)> parent;
79+
};
80+
81+
/// This is not recursive in order to avoid stack overflow
82+
/// \param ast: pointer to the root node of a tree
83+
/// \param v: visitor
84+
static void dfs(std::shared_ptr<treet<datat>> ast, visitort v)
85+
{
86+
PRECONDITION(ast->parent.lock() == nullptr);
87+
while(true)
88+
{
89+
if(ast->data != nullptr)
90+
v.data(ast->data);
91+
if(ast->first_child != nullptr)
92+
{
93+
v.first_child();
94+
ast = ast->first_child;
95+
}
96+
else
97+
{
98+
while(ast->next_sibling == nullptr)
99+
{
100+
ast = ast->parent.lock();
101+
if(ast == nullptr)
102+
return;
103+
v.parent();
104+
}
105+
106+
v.next_sibling();
107+
ast = ast->next_sibling;
108+
}
109+
}
110+
}
111+
112+
private:
113+
std::unique_ptr<datat> data = nullptr;
114+
/// Null if the node has no children
115+
std::shared_ptr<treet<datat>> first_child = nullptr;
116+
/// Null if the node is the last sibling
117+
std::shared_ptr<treet<datat>> next_sibling = nullptr;
118+
/// Set if the node has no next sibling, and it is not the root
119+
std::weak_ptr<treet<datat>> parent = {};
120+
};
121+
122+
class smt2_ast_leaft
123+
{
124+
public:
125+
virtual void print(std::ostream &stream) const = 0;
126+
};
127+
128+
class smt2_ast_symbolt : public smt2_ast_leaft
129+
{
130+
public:
131+
smt2_ast_symbolt(std::string symbol) : symbol(std::move(symbol)) {}
132+
133+
void print(std::ostream &stream) const override
134+
{
135+
stream << symbol;
136+
}
137+
138+
static std::unique_ptr<smt2_ast_symbolt> make(std::string symbol);
139+
140+
private:
141+
std::string symbol;
142+
};
143+
144+
class smt2_ast_intt : public smt2_ast_leaft
145+
{
146+
public:
147+
smt2_ast_intt(mp_integer value) : value(std::move(value)) {}
148+
149+
void print(std::ostream &stream) const override
150+
{
151+
stream << value;
152+
}
153+
154+
static std::unique_ptr<smt2_ast_leaft> make(mp_integer value);
155+
156+
template<typename T, typename std::enable_if<std::is_integral<T>::value>::type>
157+
static std::unique_ptr<smt2_ast_leaft> make(T value)
158+
{
159+
return make(numeric_cast_v<mp_integer>(value));
160+
}
161+
162+
private:
163+
mp_integer value;
164+
};
165+
166+
using smt2_astt = treet<smt2_ast_leaft>;
167+
168+
void print(std::shared_ptr<smt2_astt> ast, std::ostream &stream);
169+
170+
namespace detail
171+
{
172+
std::shared_ptr<smt2_astt> make_tree(std::shared_ptr<smt2_astt> ast);
173+
174+
std::shared_ptr<smt2_astt> make_tree(std::string &&symbol);
175+
176+
std::shared_ptr<smt2_astt> make_tree(std::unique_ptr<smt2_ast_leaft> leaf);
177+
178+
inline void fill_vector(std::vector<std::shared_ptr<smt2_astt>> &out) {}
179+
180+
/// Add a sequence of ASTs or strings
181+
template <typename FirstType, typename... Args>
182+
void fill_vector(
183+
std::vector<std::shared_ptr<smt2_astt>> &out,
184+
FirstType first,
185+
Args &&... args)
186+
{
187+
out.push_back(make_tree(std::move(first)));
188+
fill_vector(out, std::forward<Args>(args)...);
189+
}
190+
}
191+
192+
/// Make a node with no data and with children given by \p args.
193+
template <typename... Args>
194+
std::shared_ptr<smt2_astt> smt2_ast_node(Args &&... args)
195+
{
196+
std::vector<std::shared_ptr<smt2_astt>> vector;
197+
detail::fill_vector(vector, std::forward<Args>(args)...);
198+
return smt2_astt::make_node(std::move(vector));
199+
}
200+
201+
inline
202+
std::shared_ptr<smt2_astt> smt2_ast_symbol_leaf(std::string s)
203+
{
204+
return smt2_astt::make_leaf(smt2_ast_symbolt::make(s));
205+
}
206+
207+
inline
208+
std::shared_ptr<smt2_astt> smt2_ast_leaf(mp_integer i)
209+
{
210+
return smt2_astt::make_leaf(smt2_ast_intt::make(i));
211+
}
212+
213+
template<typename conditiont, typename true_caset, typename false_caset>
214+
std::shared_ptr<smt2_astt> smt2_ite(
215+
conditiont condition, true_caset true_case, false_caset false_case)
216+
{
217+
return smt2_ast_node(
218+
"ite", std::move(condition), std::move(true_case), std::move(false_case));
219+
}
220+
221+
template<typename leftt, typename rightt>
222+
std::shared_ptr<treet<smt2_ast_leaft>> smt2_eq(leftt left, rightt right)
223+
{
224+
return smt2_ast_node("=", std::move(left), std::move(right));
225+
}
226+
227+
std::shared_ptr<treet<smt2_ast_leaft>> smt2_not(
228+
std::shared_ptr<treet<smt2_ast_leaft>> ast);
229+
230+
smt2_astt smt2_eq(smt2_astt left, smt2_astt right);
231+
232+
inline
233+
std::shared_ptr<smt2_astt> smt2_let(
234+
std::vector<std::pair<std::shared_ptr<smt2_astt>, std::shared_ptr<smt2_astt>>>
235+
symbol_value_pairs,
236+
std::shared_ptr<smt2_astt> expr)
237+
{
238+
std::vector<std::shared_ptr<smt2_astt>> bindings;
239+
for(const auto &pair : symbol_value_pairs)
240+
{
241+
bindings.push_back(
242+
smt2_ast_node(std::move(pair.first), std::move(pair.second)));
243+
}
244+
return smt2_ast_node(
245+
"let", smt2_astt::make_node(std::move(bindings)), std::move(expr));
246+
}
247+
248+
template<typename opt>
249+
std::shared_ptr<smt2_astt> smt2_sign_extend(opt op)
250+
{
251+
return smt2_ast_node("_", "sign_extend", std::move(op));
252+
}
253+
254+
std::shared_ptr<smt2_astt> smt2_zero_extend(
255+
const mp_integer &width);
256+
257+
std::shared_ptr<smt2_astt> smt2_extract(
258+
const mp_integer &width, const mp_integer &offset);
259+
260+
std::shared_ptr<smt2_astt> smt2_bv(
261+
const mp_integer &index, const mp_integer &width);
262+
263+
template <typename arrayt, typename indext>
264+
std::shared_ptr<treet<smt2_ast_leaft>> smt2_ast_index(
265+
arrayt array, indext index)
266+
{
267+
return smt2_ast_node(std::move(array), ".", std::move(index));
268+
}
269+
270+
#endif // CPROVER_SOLVERS_SMT2_SMT2_AST_H

0 commit comments

Comments
 (0)