1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 matcher.cpp
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2010-04-16.
15
16 Revision History:
17
18 --*/
19 #ifdef _WINDOWS
20 #include "ast/substitution/matcher.h"
21 #include "ast/ast_pp.h"
22 #include "ast/reg_decl_plugins.h"
23
24
tst_match(ast_manager & m,app * t,app * i)25 void tst_match(ast_manager & m, app * t, app * i) {
26 substitution s(m);
27 s.reserve(2, 10); // reserving a big number of variables to be safe.
28
29 matcher match;
30 std::cout << "Is " << mk_pp(i, m) << " an instance of " << mk_pp(t, m) << "\n";
31 if (match(t, i, s)) {
32 std::cout << "yes\n";
33 s.display(std::cout);
34 }
35 else {
36 std::cout << "no\n";
37 }
38
39 s.reset();
40
41 if (t->get_decl() == i->get_decl()) {
42 // trying to match the arguments of t and i
43 std::cout << "Are the arguments of " << mk_pp(i, m) << " an instance of the arguments of " << mk_pp(t, m) << "\n";
44 unsigned num_args = t->get_num_args();
45 unsigned j;
46 for (j = 0; j < num_args; j++) {
47 if (!match(t->get_arg(j), i->get_arg(j), s))
48 break;
49 }
50 if (j == num_args) {
51 std::cout << "yes\n";
52 s.display(std::cout);
53
54 // create some dummy term to test for applying the substitution.
55 sort_ref S( m.mk_uninterpreted_sort(symbol("S")), m);
56 sort * domain[3] = {S, S, S};
57 func_decl_ref r( m.mk_func_decl(symbol("r"), 3, domain, S), m);
58 expr_ref x1( m.mk_var(0, S), m);
59 expr_ref x2( m.mk_var(1, S), m);
60 expr_ref x3( m.mk_var(2, S), m);
61 app_ref rxyzw( m.mk_app(r, x1.get(), x2.get(), x3.get()), m);
62 expr_ref result(m);
63 unsigned deltas[2] = {0,0};
64 s.apply(2, deltas, expr_offset(rxyzw, 0), result);
65 std::cout << "applying substitution to\n" << mk_pp(rxyzw,m) << "\nresult:\n" << mk_pp(result,m) << "\n";
66 }
67 else {
68 std::cout << "no\n";
69 }
70 }
71
72 std::cout << "\n";
73 }
74
tst1()75 void tst1() {
76 ast_manager m;
77 reg_decl_plugins(m);
78 sort_ref s( m.mk_uninterpreted_sort(symbol("S")), m);
79 func_decl_ref g( m.mk_func_decl(symbol("g"), s, s), m);
80 func_decl_ref h( m.mk_func_decl(symbol("h"), s, s), m);
81 sort * domain[2] = {s, s};
82 func_decl_ref f( m.mk_func_decl(symbol("f"), 2, domain, s), m);
83 app_ref a( m.mk_const(symbol("a"), s), m);
84 app_ref b( m.mk_const(symbol("b"), s), m);
85 expr_ref x( m.mk_var(0, s), m);
86 expr_ref y( m.mk_var(1, s), m);
87 app_ref gx( m.mk_app(g.get(), x.get()), m);
88 app_ref fgx_x( m.mk_app(f, gx.get(), x.get()), m);
89 app_ref ha( m.mk_app(h, a.get()), m);
90 app_ref gha( m.mk_app(g, ha.get()), m);
91 app_ref fgha_ha( m.mk_app(f, gha.get(), ha.get()), m);
92 tst_match(m, fgx_x, fgha_ha);
93
94 app_ref fgha_gha( m.mk_app(f, gha.get(), gha.get()), m);
95 tst_match(m, fgx_x, fgha_gha);
96
97 app_ref fxy( m.mk_app(f, x.get(), y.get()), m);
98 app_ref fyx( m.mk_app(f, y.get(), x.get()), m);
99 tst_match(m, fxy, fyx);
100
101 app_ref fygx( m.mk_app(f, y.get(), gx.get()), m);
102 tst_match(m, fxy, fygx);
103
104 tst_match(m, fygx, fxy);
105
106 }
107
108
109
tst_matcher()110 void tst_matcher() {
111 tst1();
112 }
113 #else
tst_matcher()114 void tst_matcher() {
115 }
116 #endif
117