1 #include <unordered_map>
2 #include "ast/ast_pp_dot.h"
3
4 #include "muz/spacer/spacer_iuc_proof.h"
5 #include "ast/for_each_expr.h"
6 #include "ast/array_decl_plugin.h"
7 #include "ast/proofs/proof_utils.h"
8 #include "muz/spacer/spacer_proof_utils.h"
9 #include "muz/spacer/spacer_util.h"
10 namespace spacer {
11
12 /*
13 * ====================================
14 * init
15 * ====================================
16 */
iuc_proof(ast_manager & m,proof * pr,const expr_set & core_lits)17 iuc_proof::iuc_proof(ast_manager& m, proof* pr, const expr_set& core_lits) :
18 m(m), m_pr(pr,m) {
19 for (auto lit : core_lits) m_core_lits.insert(lit);
20 // init A-marks and B-marks
21 collect_core_symbols();
22 compute_marks();
23 }
24
iuc_proof(ast_manager & m,proof * pr,const expr_ref_vector & core_lits)25 iuc_proof::iuc_proof(ast_manager& m, proof* pr, const expr_ref_vector& core_lits) :
26 m(m), m_pr(pr,m) {
27 for (auto lit : core_lits) m_core_lits.insert(lit);
28 // init A-marks and B-marks
29 collect_core_symbols();
30 compute_marks();
31 }
32 /*
33 * ====================================
34 * methods for computing symbol colors
35 * ====================================
36 */
37 class collect_pure_proc {
38 func_decl_set& m_symbs;
39 public:
collect_pure_proc(func_decl_set & s)40 collect_pure_proc(func_decl_set& s):m_symbs(s) {}
41
operator ()(app * a)42 void operator()(app* a) {
43 if (a->get_family_id() == null_family_id) {
44 m_symbs.insert(a->get_decl());
45 }
46 }
operator ()(var *)47 void operator()(var*) {}
operator ()(quantifier *)48 void operator()(quantifier*) {}
49 };
50
collect_core_symbols()51 void iuc_proof::collect_core_symbols()
52 {
53 expr_mark visited;
54 collect_pure_proc proc(m_core_symbols);
55 for (auto lit : m_core_lits)
56 for_each_expr(proc, visited, lit);
57 }
58
59 class is_pure_expr_proc {
60 func_decl_set const& m_symbs;
61 array_util m_au;
62 public:
63 struct non_pure {};
64
is_pure_expr_proc(func_decl_set const & s,ast_manager & m)65 is_pure_expr_proc(func_decl_set const& s, ast_manager& m):
66 m_symbs(s),
67 m_au (m)
68 {}
69
operator ()(app * a)70 void operator()(app* a) {
71 if (a->get_family_id() == null_family_id) {
72 if (!m_symbs.contains(a->get_decl())) {
73 throw non_pure();
74 }
75 }
76 else if (a->get_family_id () == m_au.get_family_id () &&
77 a->is_app_of (a->get_family_id (), OP_ARRAY_EXT)) {
78 throw non_pure();
79 }
80 }
operator ()(var *)81 void operator()(var*) {}
operator ()(quantifier *)82 void operator()(quantifier*) {}
83 };
84
is_core_pure(expr * e) const85 bool iuc_proof::is_core_pure(expr* e) const
86 {
87 is_pure_expr_proc proc(m_core_symbols, m);
88 try {
89 for_each_expr(proc, e);
90 }
91 catch (const is_pure_expr_proc::non_pure &)
92 {return false;}
93
94 return true;
95 }
96
compute_marks()97 void iuc_proof::compute_marks()
98 {
99 proof_post_order it(m_pr, m);
100 while (it.hasNext())
101 {
102 proof* cur = it.next();
103 if (m.get_num_parents(cur) == 0)
104 {
105 switch(cur->get_decl_kind())
106 {
107 case PR_ASSERTED:
108 if (m_core_lits.contains(m.get_fact(cur)))
109 m_b_mark.mark(cur, true);
110 else
111 m_a_mark.mark(cur, true);
112 break;
113 case PR_HYPOTHESIS:
114 m_h_mark.mark(cur, true);
115 break;
116 default:
117 break;
118 }
119 }
120 else
121 {
122 // collect from parents whether derivation of current node
123 // contains A-axioms, B-axioms and hypothesis
124 bool need_to_mark_a = false;
125 bool need_to_mark_b = false;
126 bool need_to_mark_h = false;
127
128 for (unsigned i = 0; i < m.get_num_parents(cur); ++i)
129 {
130 SASSERT(m.is_proof(cur->get_arg(i)));
131 proof* premise = to_app(cur->get_arg(i));
132
133 need_to_mark_a |= m_a_mark.is_marked(premise);
134 need_to_mark_b |= m_b_mark.is_marked(premise);
135 need_to_mark_h |= m_h_mark.is_marked(premise);
136 }
137
138 // if current node is application of a lemma, then all
139 // active hypotheses are removed
140 if (cur->get_decl_kind() == PR_LEMMA) need_to_mark_h = false;
141
142 // save results
143 m_a_mark.mark(cur, need_to_mark_a);
144 m_b_mark.mark(cur, need_to_mark_b);
145 m_h_mark.mark(cur, need_to_mark_h);
146 }
147 }
148 }
149
150 /*
151 * ====================================
152 * statistics
153 * ====================================
154 */
155
156 // debug method
dump_farkas_stats()157 void iuc_proof::dump_farkas_stats()
158 {
159 unsigned fl_total = 0;
160 unsigned fl_lowcut = 0;
161
162 proof_post_order it(m_pr, m);
163 while (it.hasNext())
164 {
165 proof* cur = it.next();
166
167 // if node is theory lemma
168 if (is_farkas_lemma(m, cur))
169 {
170 fl_total++;
171
172 // check whether farkas lemma is to be interpolated (could
173 // potentially miss farkas lemmas, which are interpolated,
174 // because we potentially don't want to use the lowest
175 // cut)
176 bool has_blue_nonred_parent = false;
177 for (unsigned i = 0; i < m.get_num_parents(cur); ++i) {
178 proof* premise = to_app(cur->get_arg(i));
179 if (!is_a_marked(premise) && is_b_marked(premise)) {
180 has_blue_nonred_parent = true;
181 break;
182 }
183 }
184
185 if (has_blue_nonred_parent && is_a_marked(cur))
186 {
187 SASSERT(is_b_marked(cur));
188 fl_lowcut++;
189 }
190 }
191 }
192
193 IF_VERBOSE(1, verbose_stream()
194 << "\n total farkas lemmas " << fl_total
195 << " farkas lemmas in lowest cut " << fl_lowcut << "\n";);
196 }
197
display_dot(std::ostream & out)198 void iuc_proof::display_dot(std::ostream& out) {
199 out << "digraph proof { \n";
200
201 std::unordered_map<unsigned, unsigned> ids;
202 unsigned last_id = 0;
203
204 proof_post_order it(m_pr, m);
205 while (it.hasNext())
206 {
207 proof* curr = it.next();
208
209 SASSERT(ids.count(curr->get_id()) == 0);
210 ids.insert(std::make_pair(curr->get_id(), last_id));
211
212 std::string color = "white";
213 if (this->is_a_marked(curr) && !this->is_b_marked(curr))
214 color = "red";
215 else if (!this->is_a_marked(curr) && this->is_b_marked(curr))
216 color = "blue";
217 else if (this->is_a_marked(curr) && this->is_b_marked(curr) )
218 color = "purple";
219
220 // compute node label
221 std::ostringstream label_ostream;
222 label_ostream << mk_epp(m.get_fact(curr), m) << "\n";
223 std::string label = escape_dot(label_ostream.str());
224
225 // compute edge-label
226 std::string edge_label = "";
227 if (m.get_num_parents(curr) == 0) {
228 switch (curr->get_decl_kind())
229 {
230 case PR_ASSERTED:
231 edge_label = "asserted:";
232 break;
233 case PR_HYPOTHESIS:
234 edge_label = "hyp:";
235 color = "grey";
236 break;
237 case PR_TH_LEMMA:
238 if (is_farkas_lemma(m, curr))
239 edge_label = "th_axiom(farkas):";
240 else if (is_arith_lemma(m, curr))
241 edge_label = "th_axiom(arith):";
242 else
243 edge_label = "th_axiom:";
244 break;
245 default:
246 edge_label = "unknown axiom:";
247 }
248 }
249 else {
250 if (curr->get_decl_kind() == PR_LEMMA)
251 edge_label = "lemma:";
252 else if (curr->get_decl_kind() == PR_TH_LEMMA) {
253 if (is_farkas_lemma(m, curr))
254 edge_label = "th_lemma(farkas):";
255 else if (is_arith_lemma(m, curr))
256 edge_label = "th_lemma(arith):";
257 else
258 edge_label = "th_lemma(other):";
259 }
260 }
261
262 // generate entry for node in dot-file
263 out << "node_" << last_id << " " << "["
264 << "shape=box,style=\"filled\","
265 << "label=\"" << edge_label << " " << label << "\", "
266 << "fillcolor=\"" << color << "\"" << "]\n";
267
268 // add entry for each edge to that node
269 for (unsigned i = m.get_num_parents(curr); i > 0 ; --i)
270 {
271 proof* premise = to_app(curr->get_arg(i-1));
272 unsigned pid = ids.at(premise->get_id());
273 out << "node_" << pid << " -> " << "node_" << last_id << ";\n";
274 }
275
276 ++last_id;
277 }
278 out << "\n}" << std::endl;
279 }
280 }
281