From 9978cba5a8beab2d5e3ee4e24f4fd5357e1e58d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Apr 2015 16:27:15 -0700 Subject: [PATCH] Codeplex issue 191: inconsistent results from PDR engine. The report exposed bugs in the implementation of the priority queue leaving unexplored leaves durin search. The priority queue has now been revised to address the exposed bugs Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 242 ++++++++++++++++++++++++++++-------- src/muz/pdr/pdr_context.h | 48 ++++--- src/test/main.cpp | 1 + src/test/pdr.cpp | 116 +++++++++++++++++ 4 files changed, 339 insertions(+), 68 deletions(-) create mode 100644 src/test/pdr.cpp diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 177b87820..3b7d5c056 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -622,14 +622,14 @@ namespace pdr { m_rule2transition.insert(&rule, fml.get()); rules.push_back(&rule); } - m_rule2inst.insert(&rule,&var_reprs); + m_rule2inst.insert(&rule, &var_reprs); m_rule2vars.insert(&rule, aux_vars); TRACE("pdr", tout << rule.get_decl()->get_name() << "\n"; for (unsigned i = 0; i < var_reprs.size(); ++i) { tout << mk_pp(var_reprs[i].get(), m) << " "; } - tout << "\n";); + if (!var_reprs.empty()) tout << "\n";); } bool pred_transformer::check_filled(app_ref_vector const& v) const { @@ -742,9 +742,26 @@ namespace pdr { m_closed = true; } - void model_node::reopen() { + 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::check_pre_closed() { + for (unsigned i = 0; i < children().size(); ++i) { + if (children()[i]->is_open()) return; + } + set_pre_closed(); + model_node* p = parent(); + while (p && p->is_1closed()) { + p->set_pre_closed(); + p = p->parent(); + } } static bool is_ini(datalog::rule const& r) { @@ -852,22 +869,66 @@ namespace pdr { } + void model_node::dequeue(model_node*& root) { + TRACE("pdr", tout << this << " " << state() << "\n";); + if (!m_next && !m_prev) return; + SASSERT(m_next); + SASSERT(m_prev); + SASSERT(children().empty()); + if (this == m_next) { + SASSERT(root == this); + root = 0; + } + else { + m_next->m_prev = m_prev; + m_prev->m_next = m_next; + if (this == root) { + root = m_next; + } + } + TRACE("pdr", tout << "new root: " << root << "\n";); + m_prev = 0; + m_next = 0; + } + + + void model_node::enqueue(model_node* n) { + TRACE("pdr", tout << n << " " << n->state() << "\n";); + SASSERT(!n->m_next); + SASSERT(!n->m_prev); + 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; + } + } // ---------------- // model_search + /** + \brief Dequeue the next goal. + */ model_node* model_search::next() { - if (m_leaves.empty()) { + if (!m_goal) { return 0; } - model_node* result = m_leaves.back(); - m_leaves.pop_back(); - return result; + else { + model_node* result = m_goal; + result->dequeue(m_goal); + return result; + } } bool model_search::is_repeated(model_node& n) const { model_node* p = n.parent(); while (p) { if (p->state() == n.state()) { + TRACE("pdr", tout << "repeated\n";); return true; } p = p->parent(); @@ -876,10 +937,15 @@ namespace pdr { } 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.state(), ns)->get_data().m_value; + if (nodes.contains(&n)) { + return; + } nodes.push_back(&n); - if (nodes.size() == 1 || is_repeated(n)) { + TRACE("pdr_verbose", tout << "add: " << n.level() << ": " << &n << " " << n.state() << "\n";); + if (nodes.size() == 1) { set_leaf(n); } else { @@ -890,15 +956,21 @@ namespace pdr { void model_search::set_leaf(model_node& n) { erase_children(n, true); SASSERT(n.is_open()); - enqueue_leaf(n); + enqueue_leaf(&n); } - void model_search::enqueue_leaf(model_node& n) { - if (m_bfs) { - m_leaves.push_front(&n); + void model_search::enqueue_leaf(model_node* n) { + TRACE("pdr_verbose", tout << n << " " << n->state() << " goal: " << m_goal << "\n";); + SASSERT(n->is_open()); + if (!m_goal) { + m_goal = n; + m_goal->enqueue(n); + } + else if (m_bfs) { + m_goal->enqueue(n); } else { - m_leaves.push_back(&n); + m_goal->next()->enqueue(n); } } @@ -921,56 +993,132 @@ namespace pdr { void model_search::erase_children(model_node& n, bool backtrack) { ptr_vector todo, nodes; todo.append(n.children()); - erase_leaf(n); + remove_goal(n); n.reset(); while (!todo.empty()) { model_node* m = todo.back(); todo.pop_back(); nodes.push_back(m); todo.append(m->children()); - erase_leaf(*m); remove_node(*m, backtrack); } std::for_each(nodes.begin(), nodes.end(), delete_proc()); } void model_search::remove_node(model_node& n, bool backtrack) { + TRACE("pdr_verbose", tout << "remove: " << n.level() << ": " << &n << " " << n.state() << "\n";); model_nodes& nodes = cache(n).find(n.state()); nodes.erase(&n); - if (nodes.size() > 0 && n.is_open() && backtrack) { - for (unsigned i = 0; i < nodes.size(); ++i) { - nodes[i]->reopen(); - } + bool is_goal = n.is_goal(); + remove_goal(n); + if (!nodes.empty() && is_goal && backtrack) { + TRACE("pdr_verbose", for (unsigned i = 0; i < nodes.size(); ++i) n.display(tout << &n << "\n", 2);); + model_node* n1 = nodes[0]; + n1->set_open(); + SASSERT(n1->children().empty()); + enqueue_leaf(n1); } if (nodes.empty()) { cache(n).remove(n.state()); } } - void model_search::erase_leaf(model_node& n) { - if (n.children().empty() && n.is_open()) { - std::deque::iterator - it = m_leaves.begin(), - end = m_leaves.end(); - for (; it != end; ++it) { - if (*it == &n) { - m_leaves.erase(it); - break; + void model_search::remove_goal(model_node& n) { + n.dequeue(m_goal); + } + + void model_search::well_formed() { + // each open leaf is in the set of m_goal. + ptr_vector nodes; + nodes.push_back(&get_root()); + for (unsigned i = 0; i < nodes.size(); ++i) { + model_node* n = nodes[i]; + if (!n->children().empty()) { + nodes.append(n->children()); + } + else if (n->is_open() && !n->is_goal() && n->parent()) { + TRACE("pdr", n->display(tout << "node " << n << " not found among leaves\n", 0); display(tout);); + UNREACHABLE(); + return; + } + } + if (m_goal) { + model_node* n = m_goal; + do { + if (!n->is_open() || !n->children().empty()) { + TRACE("pdr", n->display(tout << "invalid leaf\n", 0); + display(tout);); + UNREACHABLE(); + return; + } + n = n->next(); + } + while (m_goal != n); + } + + // each state appears in at most one goal per level. + bool found = true; + for (unsigned l = 0; m_goal && found; ++l) { + found = false; + obj_hashtable open_states; + model_node* n = m_goal; + do { + if (n->level() == l) { + found = true; + if (n->is_open()) { + if (open_states.contains(n->state())) { + TRACE("pdr", n->display(tout << "repeated leaf\n", 0); display(tout);); + UNREACHABLE(); + } + open_states.insert(n->state()); + } + } + n = n->next(); + } + while (m_goal != n); + } + // a node is open if and only if it contains an + // open child which is a goal. + for (unsigned i = 0; i < nodes.size(); ++i) { + model_node* n = nodes[i]; + if (!n->children().empty() && n->parent()) { + found = false; + for (unsigned j = 0; !found && j < n->children().size(); ++j) { + found = n->children()[j]->is_open(); + } + if (n->is_open() != found) { + TRACE("pdr", n->display(tout << "node in inconsistent state\n", 0); display(tout);); + UNREACHABLE(); } } } } + unsigned model_search::num_goals() const { + model_node* n = m_goal; + unsigned num = 0; + if (n) { + do { + ++num; + n = n->next(); + } + while (n != m_goal); + } + return num; + } + std::ostream& model_search::display(std::ostream& out) const { if (m_root) { m_root->display(out, 0); } - out << "goals\n"; - std::deque::const_iterator - it = m_leaves.begin(), - end = m_leaves.end(); - for (; it != end; ++it) { - (*it)->display(out, 1); + out << "goals " << num_goals() << "\n"; + model_node* n = m_goal; + if (n) { + do { + n->display(out, 1); + n = n->next(); + } + while (n != m_goal); } return out; } @@ -1253,8 +1401,8 @@ namespace pdr { remove_node(*m_root, false); dealloc(m_root); m_root = 0; - m_cache.reset(); } + m_cache.reset(); } void model_search::backtrack_level(bool uses_level, model_node& n) { @@ -1262,7 +1410,7 @@ namespace pdr { if (uses_level && m_root->level() > n.level()) { IF_VERBOSE(2, verbose_stream() << "Increase level " << n.level() << "\n";); n.increase_level(); - enqueue_leaf(n); + enqueue_leaf(&n); } else { model_node* p = n.parent(); @@ -1270,15 +1418,16 @@ namespace pdr { set_leaf(*p); } } + DEBUG_CODE(well_formed();); } // ---------------- // context context::context( - smt_params& fparams, - fixedpoint_params const& params, - ast_manager& m + smt_params& fparams, + fixedpoint_params const& params, + ast_manager& m ) : m_fparams(fparams), m_params(params), @@ -1862,17 +2011,6 @@ namespace pdr { } } - void context::check_pre_closed(model_node& n) { - for (unsigned i = 0; i < n.children().size(); ++i) { - if (!n.children()[i]->is_closed()) return; - } - n.set_pre_closed(); - model_node* p = n.parent(); - while (p && p->is_1closed()) { - p->set_pre_closed(); - p = p->parent(); - } - } void context::expand_node(model_node& n) { SASSERT(n.is_open()); @@ -2143,10 +2281,10 @@ namespace pdr { model_node* child = alloc(model_node, &n, n_cube, pt, n.level()-1); ++m_stats.m_num_nodes; m_search.add_leaf(*child); - IF_VERBOSE(3, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";); + IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(n_cube, m) << " " << (child->is_closed()?"closed":"open") << "\n";); m_stats.m_max_depth = std::max(m_stats.m_max_depth, child->depth()); } - check_pre_closed(n); + n.check_pre_closed(); TRACE("pdr", m_search.display(tout);); } diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 44fba03d8..070a80ca4 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -186,6 +186,8 @@ namespace pdr { // structure for counter-example search. class model_node { model_node* m_parent; + model_node* m_next; + model_node* m_prev; pred_transformer& m_pt; expr_ref m_state; model_ref m_model; @@ -197,13 +199,17 @@ namespace pdr { datalog::rule const* m_rule; public: model_node(model_node* parent, expr_ref& state, pred_transformer& pt, unsigned level): - m_parent(parent), m_pt(pt), m_state(state), m_model(0), - m_level(level), m_orig_level(level), m_depth(0), m_closed(false), m_rule(0) { - if (m_parent) { - m_parent->m_children.push_back(this); - SASSERT(m_parent->m_level == level+1); - SASSERT(m_parent->m_level > 0); - m_depth = m_parent->m_depth+1; + m_parent(parent), m_next(0), m_prev(0), m_pt(pt), m_state(state), m_model(0), + m_level(level), m_orig_level(level), m_depth(0), m_closed(false), m_rule(0) { + model_node* p = m_parent; + if (p) { + p->m_children.push_back(this); + SASSERT(p->m_level == level+1); + SASSERT(p->m_level > 0); + m_depth = p->m_depth+1; + if (p && p->is_closed()) { + p->set_open(); + } } } void set_model(model_ref& m) { m_model = m; } @@ -211,7 +217,7 @@ namespace pdr { unsigned orig_level() const { return m_orig_level; } unsigned depth() const { return m_depth; } void increase_level() { ++m_level; } - expr* state() const { return m_state; } + expr_ref const& state() const { return m_state; } ptr_vector const& children() { return m_children; } pred_transformer& pt() const { return m_pt; } model_node* parent() const { return m_parent; } @@ -231,8 +237,9 @@ namespace pdr { return true; } + void check_pre_closed(); void set_closed(); - void reopen(); + void set_open(); void set_pre_closed() { m_closed = true; } void reset() { m_children.reset(); } @@ -242,36 +249,45 @@ namespace pdr { void mk_instantiate(datalog::rule_ref& r0, datalog::rule_ref& r1, expr_ref_vector& binding); std::ostream& display(std::ostream& out, unsigned indent); + + void dequeue(model_node*& root); + void enqueue(model_node* n); + model_node* next() const { return m_next; } + bool is_goal() const { return 0 != next(); } }; class model_search { typedef ptr_vector model_nodes; bool m_bfs; model_node* m_root; - std::deque m_leaves; + model_node* m_goal; vector > m_cache; obj_map& cache(model_node const& n); void erase_children(model_node& n, bool backtrack); - void erase_leaf(model_node& n); void remove_node(model_node& n, bool backtrack); - void enqueue_leaf(model_node& n); // add leaf to priority queue. + void enqueue_leaf(model_node* n); // add leaf to priority queue. void update_models(); + void set_leaf(model_node& n); // Set node as leaf, remove children. + bool is_repeated(model_node& n) const; + unsigned num_goals() const; + public: - model_search(bool bfs): m_bfs(bfs), m_root(0) {} + model_search(bool bfs): m_bfs(bfs), m_root(0), m_goal(0) {} ~model_search(); void reset(); model_node* next(); - bool is_repeated(model_node& n) const; void add_leaf(model_node& n); // add fresh node. - void set_leaf(model_node& n); // Set node as leaf, remove children. - + void set_root(model_node* n); model_node& get_root() const { return *m_root; } std::ostream& display(std::ostream& out) const; expr_ref get_trace(context const& ctx); proof_ref get_proof_trace(context const& ctx); void backtrack_level(bool uses_level, model_node& n); + void remove_goal(model_node& n); + + void well_formed(); }; struct model_exception { }; diff --git a/src/test/main.cpp b/src/test/main.cpp index d5608a7d4..7b01e35c1 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -224,6 +224,7 @@ int main(int argc, char ** argv) { TST(theory_pb); TST(simplex); TST(sat_user_scope); + TST(pdr); //TST_ARGV(hs); } diff --git a/src/test/pdr.cpp b/src/test/pdr.cpp new file mode 100644 index 000000000..82448e6f5 --- /dev/null +++ b/src/test/pdr.cpp @@ -0,0 +1,116 @@ +#include "pdr_context.h" +#include "reg_decl_plugins.h" + + +using namespace pdr; + +static expr_ref mk_state(expr_ref_vector const& states, random_gen& rand) { + expr_ref result(states.get_manager()); + result = states[rand(states.size())]; + return result; +} + + +struct test_model_search { + struct init_test { + init_test(func_decl_ref& fn) { + ast_manager& m = fn.get_manager(); + reg_decl_plugins(m); + fn = m.mk_const_decl(symbol("f"), m.mk_bool_sort()); + } + }; + + ast_manager m; + smt_params smt_params; + fixedpoint_params fp_params; + context ctx; + manager pm; + func_decl_ref fn; + init_test initt; + pred_transformer pt; + random_gen rand; + model_search search; + expr_ref_vector states; + + + test_model_search(): + ctx(smt_params, fp_params, m), + pm(smt_params, 10, m), + fn(m), + initt(fn), + pt(ctx, pm, fn), + rand(10), + search(true), + states(m) { + } + + void add_tree(model_node* parent, bool force_goal) { + unsigned level = parent->level(); + search.add_leaf(*parent); + if (level > 0 && (force_goal || parent->is_goal())) { + search.remove_goal(*parent); + add_tree(alloc(model_node, parent, mk_state(states, rand), pt, level-1), false); + add_tree(alloc(model_node, parent, mk_state(states, rand), pt, level-1), false); + parent->check_pre_closed(); + } + } + + bool mutate() { + model_node* leaf = search.next(); + if (!leaf) return false; + unsigned level = leaf->level(); + if (level == 0) { + if (rand(2) == 0) { + leaf->display(std::cout << "backtrack to grandparent\n", 1); + search.backtrack_level(false, *leaf->parent()); + } + else { + leaf->display(std::cout << "backtrack to parent\n", 1); + search.backtrack_level(false, *leaf); + } + } + else { + leaf->display(std::cout << "grow tree\n", 1); + add_tree(leaf, true); + } + return true; + } + + void init() { + std::cout << "pdr state-hash search tree\n"; + + expr_ref state(m); + func_decl_ref fn(m); + for (unsigned i = 0; i < 10; ++i) { + std::ostringstream strm; + strm << "s" << i; + state = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()); + fn = to_app(state)->get_decl(); + states.push_back(state); + } + state = states[0].get(); + unsigned level = 4; + for(unsigned n = 0; n < 100; ++n) { + model_node* root = alloc(model_node, 0, mk_state(states, rand), pt, level); + search.set_root(root); + add_tree(root, false); + search.display(std::cout); + + while (true) { + search.well_formed(); + if (!mutate()) break; + search.display(std::cout); + } + search.reset(); + //++level; + } + search.reset(); + } + +}; + +void tst_pdr() { + test_model_search test; + + test.init(); +}