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