From ece2e53c98c9434bbfd6a892db0b537f49e26443 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 5 Jun 2018 12:00:13 -0700 Subject: [PATCH] Ported model_search and model_node from pdr into spacer --- src/muz/spacer/CMakeLists.txt | 1 + src/muz/spacer/spacer_pdr.cpp | 221 ++++++++++++++++++++++++++++++++++ src/muz/spacer/spacer_pdr.h | 107 ++++++++++++++++ 3 files changed, 329 insertions(+) create mode 100644 src/muz/spacer/spacer_pdr.cpp create mode 100644 src/muz/spacer/spacer_pdr.h diff --git a/src/muz/spacer/CMakeLists.txt b/src/muz/spacer/CMakeLists.txt index 162216055..8e41d5ae7 100644 --- a/src/muz/spacer/CMakeLists.txt +++ b/src/muz/spacer/CMakeLists.txt @@ -26,6 +26,7 @@ z3_add_component(spacer spacer_json.cpp spacer_iuc_proof.cpp spacer_mbc.cpp + spacer_pdr.cpp COMPONENT_DEPENDENCIES arith_tactics core_tactics diff --git a/src/muz/spacer/spacer_pdr.cpp b/src/muz/spacer/spacer_pdr.cpp new file mode 100644 index 000000000..ce3f53963 --- /dev/null +++ b/src/muz/spacer/spacer_pdr.cpp @@ -0,0 +1,221 @@ +/**++ +Copyright (c) 2018 Arie Gurfinkel + +Module Name: + + spacer_pdr.h + +Abstract: + + SPACER gPDR strategy implementation + +Author: + + Arie Gurfinkel + + Based on muz/pdr + +Notes: + +--*/ +#include "muz/spacer/spacer_pdr.h" + +namespace spacer { +model_node::model_node(model_node* parent, pob_ref &pob): + m_pob(pob), m_parent(parent), m_next(nullptr), m_prev(nullptr), + m_orig_level(m_pob->level()), m_depth(0), + m_closed(false) { + SASSERT(m_pob); + if (m_parent) m_parent->add_child(*this); +} + +void model_node::add_child(model_node &kid) { + m_children.push_back(this); + SASSERT(level() == kid.level() + 1); + SASSERT(level() > 0); + kid.m_depth = m_depth + 1; + if (is_closed()) set_open(); +} + +unsigned model_node::index_in_parent() const { + if (!m_parent) return 0; + for (unsigned i = 0, sz = m_parent->children().size(); i < sz; ++i) { + if (this == m_parent->children().get(i)) return i; + } + UNREACHABLE(); + return 0; +} + +void model_node::check_pre_closed() { + for (auto *kid : m_children) {if (kid->is_open()) return;} + + set_pre_closed(); + model_node* p = m_parent; + while (p && p->is_1closed()) { + p->set_pre_closed(); + p = p->parent(); + } +} +void model_node::set_open() { + SASSERT(m_closed); + m_closed = false; + model_node* p = parent(); + while (p && p->is_closed()) { + p->m_closed = false; + p = p->parent(); + } +} + +void model_node::detach(model_node*& qhead) { + if (!in_queue()) return; + SASSERT(children().empty()); + if (this == m_next) { + SASSERT(m_prev == this); + SASSERT(this == qhead); + qhead = nullptr; + } + else { + m_next->m_prev = m_prev; + m_prev->m_next = m_next; + if (this == qhead) qhead = m_next; + } + + // detach + m_prev = nullptr; + m_next = nullptr; +} + + +// insert node n after this in the queue +// requires: this is in a queue or this == n +void model_node::insert_after(model_node* n) { + SASSERT(!in_queue()); + if (this == n) { + m_next = n; + m_prev = n; + } + else { + n->m_next = m_next; + m_next->m_prev = n; + m_next = n; + n->m_prev = this; + } +} + +void model_search::reset() { + m_cache.reset(); + if (m_root) { + erase_children(*m_root, false); + remove_node(*m_root, false); + dealloc(m_root); + m_root = nullptr; + } +} + +model_node* model_search::pop_front() { + if (!m_qhead) return nullptr; + model_node *res = m_qhead; + res->detach(m_qhead); + return res; +} + +void model_search::add_leaf(model_node& n) { + SASSERT(n.children().empty()); + model_nodes ns; + model_nodes& nodes = cache(n).insert_if_not_there2(n.post(), ns)->get_data().m_value; + if (nodes.contains(&n)) return; + + nodes.push_back(&n); + if (nodes.size() == 1) { + SASSERT(n.is_open()); + enqueue_leaf(n); + } + else n.set_pre_closed(); +} + +void model_search::enqueue_leaf(model_node& n) { + SASSERT(n.is_open()); + // queue is empty, initialize it with n + if (!m_qhead) { + m_qhead = &n; + m_qhead->insert_after(m_qhead); + } + // insert n after m_qhead + else if (m_bfs) { + m_qhead->insert_after(&n); + } + // insert n after m_qhead()->next() + else { + m_qhead->next()->insert_after(&n); + } +} + + + +void model_search::set_root(model_node* root) { + reset(); + m_root = root; + SASSERT(m_root); + SASSERT(m_root->children().empty()); + SASSERT(cache(*root).empty()); + // XXX Don't get why 1 is legal here + cache(*root).insert(root->post(), 1); + enqueue_leaf(*root); +} + +void model_search::backtrack_level(bool uses_level, model_node& n) { + SASSERT(m_root); + if (uses_level) {NOT_IMPLEMENTED_YET();} + if (uses_level && m_root->level() > n.level()) { + n.increase_level(); + enqueue_leaf(n); + } + else { + model_node* p = n.parent(); + if (p) { + erase_children(*p, true); + enqueue_leaf(*p); + } + } +} + +obj_map >& model_search::cache(model_node const& n) { + unsigned l = n.orig_level(); + if (l >= m_cache.size()) m_cache.resize(l + 1); + return m_cache[l]; +} + +void model_search::erase_children(model_node& n, bool backtrack) { + ptr_vector todo, nodes; + todo.append(n.children()); + // detach n from queue + n.detach(m_qhead); + n.reset(); + while (!todo.empty()) { + model_node* m = todo.back(); + todo.pop_back(); + nodes.push_back(m); + todo.append(m->children()); + remove_node(*m, backtrack); + } + std::for_each(nodes.begin(), nodes.end(), delete_proc()); +} + +// removes node from the search tree and from the cache +void model_search::remove_node(model_node& n, bool backtrack) { + model_nodes& nodes = cache(n).find(n.post()); + nodes.erase(&n); + n.detach(m_qhead); + // TBD: siblings would also fail if n is not a goal. + if (!nodes.empty() && backtrack && + nodes[0]->children().empty() && nodes[0]->is_closed()) { + model_node* n1 = nodes[0]; + n1->set_open(); + enqueue_leaf(*n1); + } + + if (nodes.empty()) cache(n).remove(n.post()); +} + + +} diff --git a/src/muz/spacer/spacer_pdr.h b/src/muz/spacer/spacer_pdr.h new file mode 100644 index 000000000..dd62230bd --- /dev/null +++ b/src/muz/spacer/spacer_pdr.h @@ -0,0 +1,107 @@ +/**++ +Copyright (c) 2018 Arie Gurfinkel + +Module Name: + + spacer_pdr.h + +Abstract: + + SPACER gPDR strategy implementation + +Author: + + Arie Gurfinkel + + Based on muz/pdr + +Notes: + +--*/ +#ifndef _SPACER_PDR_H_ +#define _SPACER_PDR_H_ + +#include "muz/spacer/spacer_context.h" + +namespace spacer { +// structure for counter-example search. +class model_node { + pob_ref m_pob; // proof obligation + model_node* m_parent; // parent in the search tree + ptr_vector m_children; // children in the search tree + model_node* m_next; // next element of an in-place circular queue + model_node* m_prev; // prev element of an in-place circular queue + unsigned m_orig_level; // level at which this search node was created + unsigned m_depth; // + bool m_closed; // whether the pob is derivable +public: + model_node(model_node* parent, pob_ref &pob); + void add_child(model_node &kid); + + expr *post() const {return m_pob->post();} + unsigned level() const { return m_pob->level(); } + unsigned orig_level() const { return m_orig_level; } + unsigned depth() const { return m_depth; } + void increase_level() { m_pob->inc_level(); } + const pob_ref &pob() const { return m_pob; } + ptr_vector const& children() { return m_children; } + pred_transformer& pt() const { return m_pob->pt(); } + model_node* parent() const { return m_parent; } + // order in children of the parent + unsigned index_in_parent() const; + + bool is_closed() const { return m_closed; } + bool is_open() const { return !is_closed(); } + + // closed or has children and they are all closed + bool is_1closed() { + if (is_closed()) return true; + if (m_children.empty()) return false; + for (auto kid : m_children) {if (kid->is_open()) return false;} + return true; + } + + void check_pre_closed(); + void set_pre_closed() {m_closed = true;} + + void set_closed() {m_closed = true;} + void set_open(); + void reset() {m_children.reset();} + + /// queue + + // remove this node from the given queue + void detach(model_node*& qhead); + void insert_after(model_node* n); + model_node* next() const {return m_next;} + bool in_queue() {return m_next && m_prev;} +}; + +class model_search { + typedef ptr_vector model_nodes; + bool m_bfs; + model_node* m_root; + model_node* m_qhead; + vector > m_cache; + obj_map& cache(model_node const& n); + void erase_children(model_node& n, bool backtrack); + void remove_node(model_node& n, bool backtrack); + void add_leaf(model_node* n); // add leaf to priority queue. + +public: + model_search(bool bfs): m_bfs(bfs), m_root(nullptr), m_qhead(nullptr) {} + ~model_search() {reset();} + + void set_root(model_node* n); + + void reset(); + model_node* pop_front(); + void add_leaf(model_node& n); // add fresh node. + model_node& get_root() const { return *m_root; } + void backtrack_level(bool uses_level, model_node& n); + void remove_goal(model_node& n); + + void enqueue_leaf(model_node &n); +}; +} +#endif