1 /*++
2 Copyright (c) 2006 Microsoft Corporation and Arie Gurfinkel
3
4 Module Name:
5
6 sem_matcher.cpp
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2008-02-02.
15 Arie Gurfinkel
16
17 Revision History:
18
19 --*/
20 #include "muz/spacer/spacer_sem_matcher.h"
21
22 namespace spacer {
23
sem_matcher(ast_manager & man)24 sem_matcher::sem_matcher(ast_manager &man) : m(man), m_arith(m), m_pinned(m) {}
25
match_var(var * v,expr * e)26 bool sem_matcher::match_var (var *v, expr *e) {
27 expr_offset r;
28 if (m_subst->find(v, 0, r)) {
29 if (!m.are_equal(r.get_expr(), e)) {
30 return false;
31 }
32 }
33 else {
34 m_subst->insert(v, 0, expr_offset(e, 1));
35 }
36 return true;
37 }
operator ()(expr * e1,expr * e2,substitution & s,bool & pos)38 bool sem_matcher::operator()(expr * e1, expr * e2, substitution & s, bool &pos) {
39 reset();
40 m_subst = &s;
41 m_todo.push_back(expr_pair(e1, e2));
42
43 // true on the first run through the loop
44 bool top = true;
45 pos = true;
46 while (!m_todo.empty()) {
47 expr_pair const & p = m_todo.back();
48
49 if (is_var(p.first)) {
50 if (!match_var(to_var(p.first), p.second)) {
51 return false;
52 }
53 m_todo.pop_back();
54 top = false;
55 continue;
56 }
57
58
59 if (is_var(p.second))
60 return false;
61 if (!is_app(p.first))
62 return false;
63 if (!is_app(p.second))
64 return false;
65
66 app * n1 = to_app(p.first);
67 app * n2 = to_app(p.second);
68
69 expr *t = nullptr;
70
71 // strip negation
72 if (top && n1->get_decl() != n2->get_decl()) {
73 if (m.is_not(n1, t) && !m.is_not(n2) && is_app(t) &&
74 to_app(t)->get_decl() == n2->get_decl()) {
75 pos = false;
76 n1 = to_app(e1);
77 }
78 else if (!m.is_not(n1) && m.is_not(n2, t) && is_app(t) &&
79 to_app(t)->get_decl() == n1->get_decl()) {
80 pos = false;
81 n2 = to_app(t);
82 }
83 }
84 top = false;
85
86 if (n1->get_decl() != n2->get_decl()) {
87 expr *e1 = nullptr, *e2 = nullptr;
88 rational val1, val2;
89
90 // x<=y == !(x>y)
91 if (m_arith.is_le(n1) && m.is_not(n2, t) && m_arith.is_gt(t)) {
92 n2 = to_app(t);
93 }
94 else if (m_arith.is_le(n2) && m.is_not(n1, t) && m_arith.is_gt(t)) {
95 n1 = to_app(t);
96 }
97 // x>=y == !(x<y)
98 if (m_arith.is_ge(n1) && m.is_not(n2, t) && m_arith.is_lt(t)) {
99 n2 = to_app(t);
100 }
101 else if (m_arith.is_ge(n2) && m.is_not(n1, t) && m_arith.is_lt(t)) {
102 n1 = to_app(t);
103 }
104 // x+val1 matched to val2, where x is a variable, and
105 // val1, val2 are numerals
106 if (m_arith.is_numeral(n2, val2) && m_arith.is_add(n1, e1, e2) &&
107 m_arith.is_numeral(e2, val1) && is_var(e1)) {
108 val1 = val2 - val1;
109
110 expr_ref num1(m);
111 num1 = m_arith.mk_numeral (val1, val1.is_int());
112 m_pinned.push_back(num1);
113 if (!match_var (to_var(e1), num1)) {
114 return false;
115 }
116
117 m_todo.pop_back();
118 continue;
119 }
120 else {
121 return false;
122 }
123 }
124
125 unsigned num_args1 = n1->get_num_args();
126 if (num_args1 != n2->get_num_args())
127 return false;
128
129 m_todo.pop_back();
130
131 if (num_args1 == 0)
132 continue;
133
134 unsigned j = num_args1;
135 while (j > 0) {
136 --j;
137 m_todo.push_back(expr_pair(n1->get_arg(j), n2->get_arg(j)));
138 }
139 }
140 return true;
141 }
142
reset()143 void sem_matcher::reset() {
144 m_todo.reset();
145 m_pinned.reset();
146 }
147 }
148