1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     euf_mam.h
7 
8 Abstract:
9 
10     Matching Abstract Machine
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2007-02-13.
15     Nikolaj Bjorner (nbjorner) 2021-01-22.
16 
17 --*/
18 #pragma once
19 
20 #include "ast/ast.h"
21 #include "ast/euf/euf_egraph.h"
22 #include <functional>
23 
24 namespace euf {
25     class solver;
26 };
27 
28 namespace q {
29 
30     typedef euf::enode enode;
31     typedef euf::egraph egraph;
32     typedef euf::enode_vector enode_vector;
33 
34     class ematch;
35 
36     /**
37        \brief Matching Abstract Machine (MAM)
38     */
39     class mam {
40         friend class mam_impl;
41 
mam()42         mam() {}
43 
44     public:
45 
46         static mam * mk(euf::solver& ctx, ematch& em);
47 
~mam()48         virtual ~mam() {}
49 
50         virtual void add_pattern(quantifier * q, app * mp) = 0;
51 
52         virtual void add_node(enode * n, bool lazy) = 0;
53 
54         virtual void propagate() = 0;
55 
56         virtual bool can_propagate() const = 0;
57 
58         virtual void rematch(bool use_irrelevant = false) = 0;
59 
60         virtual void on_merge(enode * root, enode * other) = 0;
61 
62         virtual void on_match(quantifier * qa, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation) = 0;
63 
64         virtual void reset() = 0;
65 
66         virtual std::ostream& display(std::ostream& out) = 0;
67 
68         virtual bool check_missing_instances() = 0;
69 
70         static void ground_subterms(expr* e, ptr_vector<app>& ground);
71 
72     };
73 };
74 
75