1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 tst_ast.cpp
7
8 Abstract:
9
10 Test AST module
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2006-09-29.
15
16 Revision History:
17
18 --*/
19 #include "ast/ast.h"
20
tst1()21 static void tst1() {
22 ast_manager m;
23
24 family_id fid = m.get_basic_family_id();
25
26 sort_ref b(m.mk_bool_sort(), m);
27 expr_ref a(m.mk_const(symbol("a"), b.get()), m);
28 expr_ref c(m.mk_const(symbol("c"), b.get()), m);
29 expr_ref i1(m.mk_app(fid, OP_AND, a.get(), c.get()), m);
30 expr_ref i2(m.mk_app(fid, OP_AND, a.get(), c.get()), m);
31 expr_ref i3(m.mk_app(fid, OP_OR, a.get(), c.get()), m);
32 ENSURE(i1.get() == i2.get());
33 ENSURE(i1.get() != i3.get());
34
35 // TODO use smart pointers to track references
36 // ast_manager m;
37 // ast_ref<numeral_ast> n1(m.mk_numeral(rational(2,3)), m);
38 // ast_ref<numeral_ast> n2(m.mk_numeral(rational(2,3)), m);
39 // ENSURE(n1 == n2);
40 // ast_ref<numeral_ast> n3(m.mk_numeral(rational(1,2)), m);
41 // ENSURE(n1 != n3);
42 // ast_ref<var_ast> v1 (m.mk_var(1), m);
43 // ast_ref<var_ast> v2 (m.mk_var(2), m);
44 // ast_ref<var_ast> v3 (m.mk_var(1), m);
45 // ENSURE(v1 != v2);
46 // ENSURE(v1 == v3);
47 // TRACE("ast", tout << "resetting v1\n";);
48 // v1.reset();
49 // TRACE("ast", tout << "overwriting v3\n";);
50 // v3 = v2;
51
52 // ast_ref<type_decl_ast> t1(m.mk_type_decl(symbol("int"), 0), m);
53 // ast_ref<type_ast> i(m.mk_type(t1.get(), 0, 0), m);
54
55 // ast_ref<const_decl_ast> foo_decl(m.mk_const_decl(symbol("foo"), i.get(), i.get()), m);
56 // ast_ref<const_decl_ast> x_decl(m.mk_const_decl(symbol("x"), i.get()), m);
57
58 // ast_ref<const_ast> x(m.mk_const(x_decl.get()), m);
59 // ast_ref<const_ast> foo_x(m.mk_const(foo_decl.get(), x.get()), m);
60 // ast_ref<const_ast> foo_foo_x(m.mk_const(foo_decl.get(), foo_x.get()), m);
61 // ast_ref<const_ast> foo_foo_x2(m.mk_const(foo_decl.get(), m.mk_const(foo_decl.get(), m.mk_const(x_decl.get()))), m);
62 // ENSURE(foo_foo_x2 == foo_foo_x);
63 }
64
tst2()65 static void tst2() {
66 // ast_manager m;
67 // ast_vector<ast> m_nodes(m);
68
69 // m_nodes.push_back(m.mk_var(1));
70 // m_nodes.push_back(m.mk_numeral(rational(1,2)));
71 // m_nodes.push_back(m.mk_var(2));
72 // m_nodes[1] = m.mk_var(3);
73 // ENSURE(m_nodes[1]->kind() == AST_VAR);
74 // ENSURE(m_nodes.get(1)->kind() == AST_VAR);
75 // m_nodes.pop_back();
76 // ENSURE(m_nodes.size() == 2);
77 // ENSURE(!m_nodes.empty());
78 // m_nodes.set(1, m.mk_var(4));
79 // ENSURE(&(m_nodes.get_manager()) == &m);
80 }
81
tst3()82 static void tst3() {
83 // ast_manager m;
84 // ast_ref<> n(m.mk_var(1), m);
85 // n = m.mk_var(1);
86 // TRACE("ast", tout << n->get_id() << "\n";);
87 }
88
tst4()89 static void tst4() {
90 // ast_manager m;
91 // ast_ref<> n1(m.mk_var(1), m);
92 // ast_ref<> n2(m.mk_var(2), m);
93 // ast_ref<> n3(m.mk_var(3), m);
94 // weak_memoize<int> wm1;
95 // #ifdef Z3DEBUG
96 // int r;
97 // #endif
98 // ENSURE(!wm1.find(n1, r));
99 // wm1.insert(n2, 10);
100 // ENSURE(!wm1.find(n1, r));
101 // ENSURE(wm1.find(n2, r) && r == 10);
102 // wm1.insert(n2, 20);
103 // ENSURE(!wm1.find(n1, r));
104 // ENSURE(wm1.find(n2, r) && r == 20);
105 // wm1.insert(n1, 0);
106 // ENSURE(wm1.find(n1, r) && r == 0);
107 // ENSURE(wm1.find(n2, r) && r == 20);
108 }
109
tst5()110 static void tst5() {
111 ast_manager m;
112 sort_ref b(m.mk_bool_sort(), m);
113 expr_ref a1(m.mk_const(symbol("a1"), b.get()), m);
114 expr_ref a2(m.mk_const(symbol("a2"), b.get()), m);
115 expr_array arr1;
116 expr_array arr2;
117 expr_array arr3;
118 m.push_back(arr1, a1);
119 m.push_back(arr1, a2);
120 m.pop_back(arr1, arr2);
121 m.set(arr2, 0, a2, arr3);
122 ENSURE(m.size(arr1) == 2);
123 ENSURE(m.size(arr2) == 1);
124 ENSURE(m.size(arr3) == 1);
125 ENSURE(m.get(arr1, 0) == a1);
126 ENSURE(m.get(arr1, 1) == a2);
127 ENSURE(m.get(arr2, 0) == a1);
128 ENSURE(m.get(arr3, 0) == a2);
129 m.del(arr1);
130 m.del(arr2);
131 m.del(arr3);
132 }
133
134
135 struct foo {
136 unsigned m_id;
137 unsigned short m_ref_count;
138 unsigned char m_kind;
139 unsigned char m_arity;
140 bool m_val1:1;
141 bool m_val2:1;
142 };
143
tst_ast()144 void tst_ast() {
145 TRACE("ast",
146 tout << "sizeof(ast): " << sizeof(ast) << "\n";
147 tout << "sizeof(expr): " << sizeof(expr) << "\n";
148 tout << "sizeof(app): " << sizeof(app) << "\n";
149 );
150 TRACE("ast", tout << "sizeof(foo): " << sizeof(foo) << "\n";);
151 tst1();
152 tst2();
153 tst3();
154 tst4();
155 tst5();
156 }
157
158