1 /**++
2 Copyright (c) 2018 Arie Gurfinkel
3
4 Module Name:
5
6 spacer_pdr.h
7
8 Abstract:
9
10 SPACER gPDR strategy implementation
11
12 Author:
13
14 Arie Gurfinkel
15
16 Based on muz/pdr
17
18 Notes:
19
20 --*/
21 #include "muz/spacer/spacer_pdr.h"
22 #include "muz/base/dl_context.h"
23 #include "muz/spacer/spacer_mbc.h"
24
25 namespace spacer {
model_node(model_node * parent,class pob * pob)26 model_node::model_node(model_node* parent, class pob *pob):
27 m_pob(pob), m_parent(parent), m_next(nullptr), m_prev(nullptr),
28 m_orig_level(m_pob->level()), m_depth(0),
29 m_closed(false) {
30 SASSERT(m_pob);
31 if (m_parent) m_parent->add_child(this);
32 }
33
add_child(model_node * kid)34 void model_node::add_child(model_node* kid) {
35 m_children.push_back(kid);
36 SASSERT(level() == kid->level() + 1);
37 SASSERT(level() > 0);
38 kid->m_depth = m_depth + 1;
39 if (is_closed()) set_open();
40 }
41
index_in_parent() const42 unsigned model_node::index_in_parent() const {
43 if (!m_parent) return 0;
44 for (unsigned i = 0, sz = m_parent->children().size(); i < sz; ++i) {
45 if (this == m_parent->children().get(i)) return i;
46 }
47 UNREACHABLE();
48 return 0;
49 }
50
check_pre_closed()51 void model_node::check_pre_closed() {
52 for (auto *kid : m_children) {if (kid->is_open()) return;}
53
54 set_pre_closed();
55 model_node* p = m_parent;
56 while (p && p->is_1closed()) {
57 p->set_pre_closed();
58 p = p->parent();
59 }
60 }
set_open()61 void model_node::set_open() {
62 SASSERT(m_closed);
63 m_closed = false;
64 model_node* p = parent();
65 while (p && p->is_closed()) {
66 p->m_closed = false;
67 p = p->parent();
68 }
69 }
70
detach(model_node * & qhead)71 void model_node::detach(model_node*& qhead) {
72 SASSERT(in_queue());
73 SASSERT(children().empty());
74 if (this == m_next) {
75 SASSERT(m_prev == this);
76 SASSERT(this == qhead);
77 qhead = nullptr;
78 }
79 else {
80 m_next->m_prev = m_prev;
81 m_prev->m_next = m_next;
82 if (this == qhead) qhead = m_next;
83 }
84
85 // detach
86 m_prev = nullptr;
87 m_next = nullptr;
88 }
89
90
91 // insert node n after this in the queue
92 // requires: this is in a queue or this == n
insert_after(model_node * n)93 void model_node::insert_after(model_node* n) {
94 SASSERT(this == n || in_queue());
95 SASSERT(n);
96 SASSERT(!n->in_queue());
97 if (this == n) {
98 m_next = n;
99 m_prev = n;
100 }
101 else {
102 n->m_next = m_next;
103 m_next->m_prev = n;
104 m_next = n;
105 n->m_prev = this;
106 }
107 }
108
reset()109 void model_search::reset() {
110 if (m_root) {
111 erase_children(*m_root, false);
112 remove_node(m_root, false);
113 dealloc(m_root);
114 m_root = nullptr;
115 }
116 m_cache.reset();
117 }
118
pop_front()119 model_node* model_search::pop_front() {
120 model_node *res = m_qhead;
121 if (res) {
122 res->detach(m_qhead);
123 }
124 return res;
125 }
126
add_leaf(model_node * _n)127 void model_search::add_leaf(model_node* _n) {
128 model_node& n = *_n;
129 SASSERT(n.children().empty());
130 model_nodes ns;
131 model_nodes& nodes = cache(n).insert_if_not_there(n.post(), ns);
132 if (nodes.contains(&n)) return;
133
134 nodes.push_back(_n);
135 if (nodes.size() == 1) {
136 SASSERT(n.is_open());
137 enqueue_leaf(n);
138 }
139 else {
140 n.set_pre_closed();
141 }
142 }
143
enqueue_leaf(model_node & n)144 void model_search::enqueue_leaf(model_node& n) {
145 SASSERT(n.is_open());
146 SASSERT(!n.in_queue());
147 // queue is empty, initialize it with n
148 if (!m_qhead) {
149 m_qhead = &n;
150 m_qhead->insert_after(m_qhead);
151 }
152 // insert n after m_qhead
153 else if (m_bfs) {
154 m_qhead->insert_after(&n);
155 }
156 // insert n after m_qhead()->next()
157 else {
158 m_qhead->next()->insert_after(&n);
159 }
160 }
161
162
163
set_root(model_node * root)164 void model_search::set_root(model_node* root) {
165 reset();
166 m_root = root;
167 SASSERT(m_root);
168 SASSERT(m_root->children().empty());
169 add_leaf(root);
170 }
171
backtrack_level(bool uses_level,model_node & n)172 void model_search::backtrack_level(bool uses_level, model_node& n) {
173 SASSERT(m_root);
174 if (uses_level) {NOT_IMPLEMENTED_YET();}
175 if (uses_level && m_root->level() > n.level()) {
176 n.increase_level();
177 enqueue_leaf(n);
178 }
179 else {
180 model_node* p = n.parent();
181 if (p) {
182 erase_children(*p, true);
183 enqueue_leaf(*p);
184 }
185 }
186 }
187
cache(model_node const & n)188 obj_map<expr, ptr_vector<model_node> >& model_search::cache(model_node const& n) {
189 unsigned l = n.orig_level();
190 if (l >= m_cache.size()) m_cache.resize(l + 1);
191 return m_cache[l];
192 }
193
erase_children(model_node & n,bool backtrack)194 void model_search::erase_children(model_node& n, bool backtrack) {
195 ptr_vector<model_node> todo, nodes;
196 todo.append(n.children());
197 // detach n from queue
198 if (n.in_queue()) n.detach(m_qhead);
199 n.reset_children();
200 while (!todo.empty()) {
201 model_node* m = todo.back();
202 todo.pop_back();
203 nodes.push_back(m);
204 todo.append(m->children());
205 remove_node(m, backtrack);
206 }
207 std::for_each(nodes.begin(), nodes.end(), delete_proc<model_node>());
208 }
209
210 // removes node from the search tree and from the cache
remove_node(model_node * _n,bool backtrack)211 void model_search::remove_node(model_node* _n, bool backtrack) {
212 model_node& n = *_n;
213 model_nodes& nodes = cache(n).find(n.post());
214 nodes.erase(_n);
215 if (n.in_queue()) n.detach(m_qhead);
216 // TBD: siblings would also fail if n is not a goal.
217 if (!nodes.empty() && backtrack &&
218 nodes[0]->children().empty() && nodes[0]->is_closed()) {
219 model_node* n1 = nodes[0];
220 n1->set_open();
221 enqueue_leaf(*n1);
222 }
223
224 if (nodes.empty()) cache(n).remove(n.post());
225 }
226
227
gpdr_solve_core()228 lbool context::gpdr_solve_core() {
229 scoped_watch _w_(m_solve_watch);
230 //if there is no query predicate, abort
231 if (!m_rels.find(m_query_pred, m_query)) { return l_false; }
232
233 model_search ms(m_pdr_bfs);
234 unsigned lvl = 0;
235 unsigned max_level = m_max_level;
236 for (lvl = 0; lvl < max_level; ++lvl) {
237 checkpoint();
238 IF_VERBOSE(1,verbose_stream() << "GPDR Entering level "<< lvl << "\n";);
239 STRACE("spacer_progress", tout << "\n* LEVEL " << lvl << "\n";);
240 m_expanded_lvl = infty_level();
241 m_stats.m_max_query_lvl = lvl;
242 if (gpdr_check_reachability(lvl, ms)) {return l_true;}
243 if (lvl > 0) {
244 if (propagate(m_expanded_lvl, lvl, UINT_MAX)) {return l_false;}
245 }
246 }
247
248 // communicate failure to datalog::context
249 if (m_context) {
250 m_context->set_status(datalog::BOUNDED);
251 }
252 return l_undef;
253 }
254
gpdr_check_reachability(unsigned lvl,model_search & ms)255 bool context::gpdr_check_reachability(unsigned lvl, model_search &ms) {
256 pob_ref root_pob = m_query->mk_pob(nullptr, lvl, 0, m.mk_true());
257 model_node *root_node = alloc(model_node, nullptr, root_pob.get());
258
259 ms.set_root(root_node);
260 pob_ref_buffer new_pobs;
261
262 while (model_node *node = ms.pop_front()) {
263 IF_VERBOSE(2, verbose_stream() << "Expand node: "
264 << node->level() << "\n";);
265 new_pobs.reset();
266 checkpoint();
267 pred_transformer &pt = node->pt();
268
269 // check reachable cache
270 if (pt.is_must_reachable(node->pob()->post(), nullptr)) {
271 TRACE("spacer",
272 tout << "must-reachable: " << pt.head()->get_name() << " level: "
273 << node->level() << " depth: " << node->depth () << "\n";
274 tout << mk_pp(node->pob()->post(), m) << "\n";);
275
276 node->set_closed();
277 if (node == root_node) return true;
278 continue;
279 }
280
281 switch (expand_pob(*node->pob(), new_pobs)){
282 case l_true:
283 node->set_closed();
284 if (node == root_node) return true;
285 break;
286 case l_false:
287 ms.backtrack_level(false, *node);
288 if (node == root_node) return false;
289 break;
290 case l_undef:
291 SASSERT(!new_pobs.empty());
292 for (auto pob : new_pobs) {
293 TRACE("spacer_pdr",
294 tout << "looking at pob at level " << pob->level() << " "
295 << mk_pp(pob->post(), m) << "\n";);
296 if (pob != node->pob())
297 ms.add_leaf(alloc(model_node, node, pob));
298 }
299 node->check_pre_closed();
300 break;
301 }
302 }
303
304 return root_node->is_closed();
305 }
306
gpdr_create_split_children(pob & n,const datalog::rule & r,expr * trans,model & mdl,pob_ref_buffer & out)307 bool context::gpdr_create_split_children(pob &n, const datalog::rule &r,
308 expr *trans,
309 model &mdl,
310 pob_ref_buffer &out) {
311 pred_transformer &pt = n.pt();
312 ptr_vector<func_decl> preds;
313 pt.find_predecessors(r, preds);
314 SASSERT(preds.size() > 1);
315
316 ptr_vector<pred_transformer> ppts;
317 for (auto *p : preds) ppts.push_back(&get_pred_transformer(p));
318
319 mbc::partition_map pmap;
320 for (unsigned i = 0, sz = preds.size(); i < sz; ++i) {
321 func_decl *p = preds.get(i);
322 pred_transformer &ppt = *ppts.get(i);
323 for (unsigned j = 0, jsz = p->get_arity(); j < jsz; ++j) {
324 pmap.insert(m_pm.o2o(ppt.sig(j), 0, i), i);
325 }
326 }
327
328
329 spacer::mbc _mbc(m);
330 expr_ref_vector lits(m);
331 flatten_and(trans, lits);
332 vector<expr_ref_vector> res(preds.size(), expr_ref_vector(m));
333 _mbc(pmap, lits, mdl, res);
334
335 // pick an order to process children
336 unsigned_vector kid_order;
337 kid_order.resize(preds.size(), 0);
338 for (unsigned i = 0, sz = preds.size(); i < sz; ++i) kid_order[i] = i;
339 if (m_children_order == CO_REV_RULE) {
340 kid_order.reverse();
341 }
342 else if (m_children_order == CO_RANDOM) {
343 shuffle(kid_order.size(), kid_order.data(), m_random);
344 }
345
346
347 for (unsigned i = 0, sz = res.size(); i < sz; ++i) {
348 unsigned j = kid_order[i];
349 expr_ref post(m);
350 pred_transformer &ppt = *ppts.get(j);
351 post = mk_and(res.get(j));
352 m_pm.formula_o2n(post.get(), post, j, true);
353 pob * k = ppt.mk_pob(&n, prev_level(n.level()), n.depth(), post);
354 out.push_back(k);
355 IF_VERBOSE (1, verbose_stream()
356 << "\n\tcreate_child: " << k->pt().head()->get_name()
357 << " (" << k->level() << ", " << k->depth() << ") "
358 << (k->use_farkas_generalizer() ? "FAR " : "SUB ")
359 << k->post()->get_id();
360 verbose_stream().flush(););
361 TRACE ("spacer",
362 tout << "create-pob: " << k->pt().head()->get_name()
363 << " level: " << k->level()
364 << " depth: " << k->depth ()
365 << " fvsz: " << k->get_free_vars_size() << "\n"
366 << mk_pp(k->post(), m) << "\n";);
367
368
369 }
370
371 return true;
372 }
373
374
375 } // spacer
376