1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
/*++
Copyright (c) 2006 Microsoft Corporation and Arie Gurfinkel
Module Name:
sem_matcher.h
Abstract:
Semantic matcher
Author:
Leonardo de Moura (leonardo) 2008-02-02.
Arie Gurfinkel
Revision History:
--*/
#pragma once
#include "ast/substitution/substitution.h"
#include "ast/arith_decl_plugin.h"
#include "util/hashtable.h"
namespace spacer {
/**
\brief Functor for matching expressions.
*/
class sem_matcher {
typedef std::pair<expr *, expr *> expr_pair;
typedef pair_hash<obj_ptr_hash<expr>, obj_ptr_hash<expr> > expr_pair_hash;
typedef hashtable<expr_pair, expr_pair_hash, default_eq<expr_pair> > cache;
ast_manager &m;
arith_util m_arith;
expr_ref_vector m_pinned;
substitution * m_subst;
svector<expr_pair> m_todo;
bool match_var(var *v, expr *e);
public:
sem_matcher(ast_manager &man);
void reset();
/**
\brief Return true if e2 is an instance of e1.
In case of success (result is true), it will store the substitution that makes e1 equals to e2 into s.
Sets pos to true if the match is positive and to false if it is negative (i.e., e1 equals !e2)
For example:
1) e1 = f(g(x), x), e2 = f(g(h(a)), h(a))
The result is true, and s will contain x -> h(a)
2) e1 = f(a, x) e2 = f(x, a)
The result is false.
3) e1 = f(x, x) e2 = f(y, a)
The result is false
4) e1 = f(x, y) e2 = f(h(z), a)
The result is true, and s contains x->h(z) and y->a
*/
bool operator()(expr * e1, expr * e2, substitution & s, bool &pos);
};
}