1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 model_converter.h
7
8 Abstract:
9
10 Abstract interface for converting models.
11
12 Author:
13
14 Leonardo (leonardo) 2011-04-21
15
16 Notes:
17
18 --*/
19 #include "tactic/model_converter.h"
20 #include "model/model_v2_pp.h"
21 #include "ast/ast_smt2_pp.h"
22
23 /*
24 * Add or overwrite value in model.
25 */
display_add(std::ostream & out,ast_manager & m,func_decl * f,expr * e) const26 void model_converter::display_add(std::ostream& out, ast_manager& m, func_decl* f, expr* e) const {
27 VERIFY(e);
28 smt2_pp_environment_dbg env(m);
29 smt2_pp_environment* _env = m_env ? m_env : &env;
30 VERIFY(f->get_range() == e->get_sort());
31 ast_smt2_pp(out, f, e, *_env, params_ref(), 0, "model-add") << "\n";
32 }
33
34 /*
35 * A value is removed from the model.
36 */
display_del(std::ostream & out,func_decl * f) const37 void model_converter::display_del(std::ostream& out, func_decl* f) const {
38 if (m_env) {
39 ast_smt2_pp(out << "(model-del ", f->get_name(), f->is_skolem(), *m_env) << ")\n";
40 }
41 else {
42 out << "(model-del " << f->get_name() << ")\n";
43 }
44 }
45
set_env(ast_pp_util * visitor)46 void model_converter::set_env(ast_pp_util* visitor) {
47 if (visitor) {
48 m_env = &visitor->env();
49 }
50 else {
51 m_env = nullptr;
52 }
53 }
54
55
display_add(std::ostream & out,ast_manager & m)56 void model_converter::display_add(std::ostream& out, ast_manager& m) {
57 // default printer for converter that adds entries
58 model_ref mdl = alloc(model, m);
59 (*this)(mdl);
60 for (unsigned i = 0, sz = mdl->get_num_constants(); i < sz; ++i) {
61 func_decl* f = mdl->get_constant(i);
62 display_add(out, m, f, mdl->get_const_interp(f));
63 }
64 for (unsigned i = 0, sz = mdl->get_num_functions(); i < sz; ++i) {
65 func_decl* f = mdl->get_function(i);
66 func_interp* fi = mdl->get_func_interp(f);
67 display_add(out, m, f, fi->get_interp());
68 }
69 }
70
71
72 class concat_model_converter : public concat_converter<model_converter> {
73 public:
concat_model_converter(model_converter * mc1,model_converter * mc2)74 concat_model_converter(model_converter * mc1, model_converter * mc2): concat_converter<model_converter>(mc1, mc2) {
75 VERIFY(m_c1 && m_c2);
76 }
77
operator ()(model_ref & m)78 void operator()(model_ref & m) override {
79 this->m_c2->operator()(m);
80 this->m_c1->operator()(m);
81 }
82
operator ()(expr_ref & fml)83 void operator()(expr_ref & fml) override {
84 this->m_c2->operator()(fml);
85 this->m_c1->operator()(fml);
86 }
87
operator ()(labels_vec & r)88 void operator()(labels_vec & r) override {
89 this->m_c2->operator()(r);
90 this->m_c1->operator()(r);
91 }
92
get_units(obj_map<expr,bool> & fmls)93 void get_units(obj_map<expr, bool>& fmls) override {
94 m_c2->get_units(fmls);
95 m_c1->get_units(fmls);
96 }
97
get_name() const98 char const * get_name() const override { return "concat-model-converter"; }
99
translate(ast_translation & translator)100 model_converter * translate(ast_translation & translator) override {
101 return this->translate_core<concat_model_converter>(translator);
102 }
103
set_env(ast_pp_util * visitor)104 void set_env(ast_pp_util* visitor) override {
105 this->m_c1->set_env(visitor);
106 this->m_c2->set_env(visitor);
107 }
108 };
109
concat(model_converter * mc1,model_converter * mc2)110 model_converter * concat(model_converter * mc1, model_converter * mc2) {
111 if (mc1 == nullptr)
112 return mc2;
113 if (mc2 == nullptr)
114 return mc1;
115 return alloc(concat_model_converter, mc1, mc2);
116 }
117
118
119 class model2mc : public model_converter {
120 model_ref m_model;
121 labels_vec m_labels;
122 public:
model2mc(model * m)123 model2mc(model * m):m_model(m) {}
124
model2mc(model * m,labels_vec const & r)125 model2mc(model * m, labels_vec const & r):m_model(m), m_labels(r) {}
126
~model2mc()127 ~model2mc() override {}
128
operator ()(model_ref & m)129 void operator()(model_ref & m) override {
130 if (!m || !m_model) {
131 m = m_model;
132 return;
133 }
134 m->copy_const_interps(*m_model.get());
135 m->copy_func_interps(*m_model.get());
136 m->copy_usort_interps(*m_model.get());
137 }
138
operator ()(labels_vec & r)139 void operator()(labels_vec & r) override {
140 r.append(m_labels.size(), m_labels.data());
141 }
142
operator ()(expr_ref & fml)143 void operator()(expr_ref& fml) override {
144 model::scoped_model_completion _scm(m_model, false);
145 fml = (*m_model)(fml);
146 }
147
get_units(obj_map<expr,bool> & fmls)148 void get_units(obj_map<expr, bool>& fmls) override {
149 // no-op
150 }
151
cancel()152 void cancel() override {
153 }
154
display(std::ostream & out)155 void display(std::ostream & out) override {
156 out << "(rmodel->model-converter-wrapper\n";
157 model_v2_pp(out, *m_model);
158 out << ")\n";
159 }
160
translate(ast_translation & translator)161 model_converter * translate(ast_translation & translator) override {
162 model * m = m_model->translate(translator);
163 return alloc(model2mc, m, m_labels);
164 }
165
166 };
167
model2model_converter(model * m)168 model_converter * model2model_converter(model * m) {
169 if (!m) return nullptr;
170 return alloc(model2mc, m);
171 }
172
model_and_labels2model_converter(model * m,labels_vec const & r)173 model_converter * model_and_labels2model_converter(model * m, labels_vec const & r) {
174 if (!m) return nullptr;
175 return alloc(model2mc, m, r);
176 }
177
model_converter2model(ast_manager & mng,model_converter * mc,model_ref & m)178 void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m) {
179 if (mc) {
180 m = alloc(model, mng);
181 (*mc)(m);
182 }
183 }
184
apply(model_converter_ref & mc,model_ref & m)185 void apply(model_converter_ref & mc, model_ref & m) {
186 if (mc) {
187 (*mc)(m);
188 }
189 }
190
191