1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 macro_manager.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2010-04-05. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "util/obj_hashtable.h" 22 #include "ast/ast_util.h" 23 #include "ast/justified_expr.h" 24 #include "ast/recurse_expr.h" 25 #include "ast/func_decl_dependencies.h" 26 #include "ast/macros/macro_util.h" 27 28 /** 29 \brief Macros are universally quantified formulas of the form: 30 (forall X (= (f X) T[X])) 31 (forall X (iff (f X) T[X])) 32 where T[X] does not contain X. 33 34 This class is responsible for storing macros and expanding them. 35 It has support for backtracking and tagging declarations in an expression as forbidded for being macros. 36 */ 37 class macro_manager { 38 ast_manager & m; 39 macro_util m_util; 40 41 obj_map<func_decl, quantifier *> m_decl2macro; // func-decl -> quantifier 42 obj_map<func_decl, proof *> m_decl2macro_pr; // func-decl -> quantifier_proof 43 obj_map<func_decl, expr_dependency *> m_decl2macro_dep; // func-decl -> unsat core dependency 44 func_decl_ref_vector m_decls; 45 quantifier_ref_vector m_macros; 46 proof_ref_vector m_macro_prs; 47 expr_dependency_ref_vector m_macro_deps; 48 obj_hashtable<func_decl> m_forbidden_set; 49 func_decl_ref_vector m_forbidden; 50 struct scope { 51 unsigned m_decls_lim; 52 unsigned m_forbidden_lim; 53 }; 54 svector<scope> m_scopes; 55 56 func_decl_dependencies m_deps; 57 58 void restore_decls(unsigned old_sz); 59 void restore_forbidden(unsigned old_sz); 60 61 struct macro_expander_cfg; 62 struct macro_expander_rw; 63 64 public: 65 macro_manager(ast_manager & m); 66 ~macro_manager(); 67 void copy_to(macro_manager& dst); get_manager()68 ast_manager & get_manager() const { return m; } get_util()69 macro_util & get_util() { return m_util; } 70 bool insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep = nullptr); has_macros()71 bool has_macros() const { return !m_macros.empty(); } 72 void push_scope(); 73 void pop_scope(unsigned num_scopes); 74 void reset(); 75 void mark_forbidden(unsigned n, expr * const * exprs); 76 void mark_forbidden(unsigned n, justified_expr const * exprs); mark_forbidden(expr * e)77 void mark_forbidden(expr * e) { mark_forbidden(1, &e); } is_forbidden(func_decl * d)78 bool is_forbidden(func_decl * d) const { return m_forbidden_set.contains(d); } get_forbidden_set()79 obj_hashtable<func_decl> const & get_forbidden_set() const { return m_forbidden_set; } 80 void display(std::ostream & out); contains(func_decl * d)81 bool contains(func_decl* d) const { return m_decls.contains(d); } get_num_macros()82 unsigned get_num_macros() const { return m_decls.size(); } get_first_macro_last_level()83 unsigned get_first_macro_last_level() const { return m_scopes.empty() ? 0 : m_scopes.back().m_decls_lim; } get_macro_func_decl(unsigned i)84 func_decl * get_macro_func_decl(unsigned i) const { return m_decls.get(i); } 85 func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const; get_macro_quantifier(func_decl * f)86 quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = nullptr; m_decl2macro.find(f, q); return q; } 87 void get_head_def(quantifier * q, func_decl * d, app * & head, expr_ref & def, bool& revert) const; 88 void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep); 89 90 91 }; 92 93 94