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