1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 ast_lt.cpp
7
8 Abstract:
9
10 Total order on ASTs that does not depend on the internal ids.
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2011-04-08
15
16 Revision History:
17
18 --*/
19 #include "ast/ast.h"
20
21 #define check_symbol(S1,S2) if (S1 != S2) return lt(S1,S2)
22 #define check_value(V1,V2) if (V1 != V2) return V1 < V2
23 #define check_bool(B1,B2) if (B1 != B2) return !B1 && B2
24 #define check_ptr(P1,P2) if (!P1 && P2) return true; if (P1 && !P2) return false
25 #define check_ast(T1,T2) if (T1 != T2) { n1 = T1; n2 = T2; goto start; }
26
27 #define check_parameter(p1, p2) { \
28 check_value(p1.get_kind(), p2.get_kind()); \
29 switch (p1.get_kind()) { \
30 case parameter::PARAM_INT: \
31 check_value(p1.get_int(), p2.get_int()); \
32 break; \
33 case parameter::PARAM_AST: \
34 check_ast(p1.get_ast(), p2.get_ast()); \
35 break; \
36 case parameter::PARAM_SYMBOL: \
37 check_symbol(p1.get_symbol(), p2.get_symbol()); \
38 break; \
39 case parameter::PARAM_RATIONAL: \
40 check_value(p1.get_rational(), p2.get_rational()); \
41 break; \
42 case parameter::PARAM_DOUBLE: \
43 check_value(p1.get_double(), p2.get_double()); \
44 break; \
45 case parameter::PARAM_EXTERNAL: \
46 check_value(p1.get_ext_id(), p2.get_ext_id()); \
47 break; \
48 default: \
49 UNREACHABLE(); \
50 break; \
51 } \
52 }
53
lt(ast * n1,ast * n2)54 bool lt(ast * n1, ast * n2) {
55 unsigned num;
56 start:
57 if (n1 == n2)
58 return false;
59 check_value(n1->get_kind(), n2->get_kind());
60 switch(n1->get_kind()) {
61 case AST_SORT:
62 check_symbol(to_sort(n1)->get_name(), to_sort(n2)->get_name());
63 check_value(to_sort(n1)->get_num_parameters(), to_sort(n2)->get_num_parameters());
64 num = to_sort(n1)->get_num_parameters();
65 SASSERT(num > 0);
66 for (unsigned i = 0; i < num; i++) {
67 parameter p1 = to_sort(n1)->get_parameter(i);
68 parameter p2 = to_sort(n2)->get_parameter(i);
69 check_parameter(p1, p2);
70 }
71 UNREACHABLE();
72 return false;
73 case AST_FUNC_DECL:
74 check_symbol(to_func_decl(n1)->get_name(), to_func_decl(n2)->get_name());
75 check_value(to_func_decl(n1)->get_arity(), to_func_decl(n2)->get_arity());
76 check_value(to_func_decl(n1)->get_num_parameters(), to_func_decl(n2)->get_num_parameters());
77 num = to_func_decl(n1)->get_num_parameters();
78 for (unsigned i = 0; i < num; i++) {
79 parameter p1 = to_func_decl(n1)->get_parameter(i);
80 parameter p2 = to_func_decl(n2)->get_parameter(i);
81 check_parameter(p1, p2);
82 }
83 num = to_func_decl(n1)->get_arity();
84 for (unsigned i = 0; i < num; i++) {
85 ast * d1 = to_func_decl(n1)->get_domain(i);
86 ast * d2 = to_func_decl(n2)->get_domain(i);
87 check_ast(d1, d2);
88 }
89 n1 = to_func_decl(n1)->get_range();
90 n2 = to_func_decl(n2)->get_range();
91 goto start;
92 case AST_APP:
93 check_value(to_app(n1)->get_num_args(), to_app(n2)->get_num_args());
94 check_value(to_app(n1)->get_depth(), to_app(n2)->get_depth());
95 check_ast(to_app(n1)->get_decl(), to_app(n2)->get_decl());
96 num = to_app(n1)->get_num_args();
97 for (unsigned i = 0; i < num; i++) {
98 expr * arg1 = to_app(n1)->get_arg(i);
99 expr * arg2 = to_app(n2)->get_arg(i);
100 check_ast(arg1, arg2);
101 }
102 UNREACHABLE();
103 return false;
104 case AST_QUANTIFIER:
105 check_value(to_quantifier(n1)->get_kind(), to_quantifier(n2)->get_kind());
106 check_value(to_quantifier(n1)->get_num_decls(), to_quantifier(n2)->get_num_decls());
107 check_value(to_quantifier(n1)->get_num_patterns(), to_quantifier(n2)->get_num_patterns());
108 check_value(to_quantifier(n1)->get_num_no_patterns(), to_quantifier(n2)->get_num_no_patterns());
109 check_value(to_quantifier(n1)->get_weight(), to_quantifier(n2)->get_weight());
110 num = to_quantifier(n1)->get_num_decls();
111 for (unsigned i = 0; i < num; i++) {
112 check_symbol(to_quantifier(n1)->get_decl_name(i), to_quantifier(n2)->get_decl_name(i));
113 check_ast(to_quantifier(n1)->get_decl_sort(i), to_quantifier(n2)->get_decl_sort(i));
114 }
115 num = to_quantifier(n1)->get_num_patterns();
116 for (unsigned i = 0; i < num; i++) {
117 check_ast(to_quantifier(n1)->get_pattern(i), to_quantifier(n2)->get_pattern(i));
118 }
119 num = to_quantifier(n1)->get_num_no_patterns();
120 for (unsigned i = 0; i < num; i++) {
121 check_ast(to_quantifier(n1)->get_no_pattern(i), to_quantifier(n2)->get_no_pattern(i));
122 }
123 n1 = to_quantifier(n1)->get_expr();
124 n2 = to_quantifier(n2)->get_expr();
125 goto start;
126 case AST_VAR:
127 check_value(to_var(n1)->get_idx(), to_var(n2)->get_idx());
128 n1 = to_var(n1)->get_sort();
129 n2 = to_var(n2)->get_sort();
130 goto start;
131 default:
132 UNREACHABLE();
133 return false;
134 }
135 }
136
is_sorted(unsigned num,expr * const * ns)137 bool is_sorted(unsigned num, expr * const * ns) {
138 for (unsigned i = 1; i < num; i++) {
139 ast * prev = ns[i-1];
140 ast * curr = ns[i];
141 if (lt(curr, prev))
142 return false;
143 }
144 return true;
145 }
146
lex_lt(unsigned num,ast * const * n1,ast * const * n2)147 bool lex_lt(unsigned num, ast * const * n1, ast * const * n2) {
148 for (unsigned i = 0; i < num; i ++) {
149 if (n1[i] == n2[i])
150 continue;
151 return lt(n1[i], n2[i]);
152 }
153 return false;
154 }
155