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