1 /*++ 2 Copyright (c) 2017 Microsoft Corporation 3 4 Module Name: 5 6 generic_model_converter.h 7 8 Abstract: 9 10 Generic model converter that hides and adds entries. 11 It subsumes filter_model_converter and extension_model_converter. 12 13 Author: 14 15 Nikolaj Bjorner (nbjorner) 2017-10-29 16 17 Notes: 18 19 --*/ 20 #pragma once 21 22 #include "tactic/model_converter.h" 23 24 class generic_model_converter : public model_converter { 25 enum instruction { HIDE, ADD }; 26 struct entry { 27 func_decl_ref m_f; 28 expr_ref m_def; 29 instruction m_instruction; entryentry30 entry(func_decl* f, expr* d, ast_manager& m, instruction i): 31 m_f(f, m), m_def(d, m), m_instruction(i) {} 32 }; 33 ast_manager& m; 34 std::string m_orig; 35 vector<entry> m_entries; 36 obj_map<func_decl, unsigned> m_first_idx; 37 38 expr_ref simplify_def(entry const& e); 39 40 public: generic_model_converter(ast_manager & m,char const * orig)41 generic_model_converter(ast_manager & m, char const* orig) : m(m), m_orig(orig) {} 42 43 ~generic_model_converter() override; 44 hide(expr * e)45 void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); } 46 hide(func_decl * f)47 void hide(func_decl * f) { m_entries.push_back(entry(f, nullptr, m, HIDE)); } 48 49 void add(func_decl * d, expr* e); 50 add(expr * d,expr * e)51 void add(expr * d, expr* e) { SASSERT(is_app(d) && to_app(d)->get_num_args() == 0); add(to_app(d)->get_decl(), e); } 52 operator()53 void operator()(labels_vec & labels) override {} 54 55 void operator()(model_ref & md) override; 56 operator()57 void operator()(expr_ref& fml) override { UNREACHABLE(); } 58 cancel()59 void cancel() override {} 60 61 void display(std::ostream & out) override; 62 translate(ast_translation & translator)63 model_converter * translate(ast_translation & translator) override { return copy(translator); } 64 65 generic_model_converter* copy(ast_translation & translator); 66 67 void set_env(ast_pp_util* visitor) override; 68 69 void get_units(obj_map<expr, bool>& units) override; 70 }; 71 72 typedef ref<generic_model_converter> generic_model_converter_ref; 73 74