1 #include "ast/rewriter/value_sweep.h"
2 #include "ast/reg_decl_plugins.h"
3 #include "ast/ast_pp.h"
4 #include "ast/seq_decl_plugin.h"
5 #include "ast/array_decl_plugin.h"
6
tst_value_sweep()7 void tst_value_sweep() {
8 ast_manager m;
9 reg_decl_plugins(m);
10 datatype_util dt(m);
11 arith_util a(m);
12 array_util ar(m);
13 seq_util seq(m);
14 sort_ref int_sort(a.mk_int(), m);
15 func_decl_ref cons(m), is_cons(m), head(m), tail(m), nil(m), is_nil(m);
16
17 sort_ref ilist = dt.mk_list_datatype(int_sort, symbol("ilist"),
18 cons, is_cons, head, tail, nil, is_nil);
19
20 expr_ref n(m.mk_const("n", int_sort), m);
21 expr_ref v1(m.mk_const("v1", ilist), m);
22 expr_ref v2(m.mk_const("v2", ilist), m);
23 std::cout << cons << "\n";
24 expr_ref v3(m.mk_app(cons.get(), n, v1), m);
25 expr_ref_vector terms(m);
26 terms.push_back(v1).push_back(v2).push_back(v3);
27 vector<expr_ref_vector> values;
28 value_sweep ws(m);
29 ws.set_range(30);
30 ws(terms, values);
31 for (auto const& vec : values) {
32 for (expr* v : vec) {
33 std::cout << mk_pp(v, m) << "\n";
34 }
35 std::cout << "\n";
36 }
37 }
38