From c2108f74f1e5c5ab96c6e4cc189ccbc55dca339a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Nov 2015 10:35:06 -0800 Subject: [PATCH 1/4] fix uninitialized variable Signed-off-by: Nikolaj Bjorner --- src/opt/maxsmt.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 2d3a60ea8..1bb521923 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -154,7 +154,7 @@ namespace opt { m_soft_constraints(m), m_answer(m) {} lbool maxsmt::operator()() { - lbool is_sat; + lbool is_sat = l_undef; m_msolver = 0; symbol const& maxsat_engine = m_c.maxsat_engine(); IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); From f537167080b52b9793e0f310ee824ac745688ca4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Nov 2015 18:41:16 -0800 Subject: [PATCH 2/4] Fix bug #311 Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 20 +++++++++++++++----- src/muz/pdr/pdr_context.h | 2 +- 2 files changed, 16 insertions(+), 6 deletions(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index d349da4ec..a55d0e648 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -738,6 +738,7 @@ namespace pdr { // model_node void model_node::set_closed() { + TRACE("pdr", tout << state() << "\n";); pt().close(state()); m_closed = true; } @@ -928,7 +929,7 @@ namespace pdr { model_node* p = n.parent(); while (p) { if (p->state() == n.state()) { - TRACE("pdr", tout << "repeated\n";); + TRACE("pdr", tout << n.state() << "repeated\n";); return true; } p = p->parent(); @@ -1018,6 +1019,11 @@ namespace pdr { SASSERT(n1->children().empty()); enqueue_leaf(n1); } + + if (!nodes.empty() && n.get_model_ptr() && backtrack) { + model_ref mr(n.get_model_ptr()); + nodes[0]->set_model(mr); + } if (nodes.empty()) { cache(n).remove(n.state()); } @@ -1149,17 +1155,21 @@ namespace pdr { ast_manager& m = n->pt().get_manager(); if (!n->get_model_ptr()) { if (models.find(n->state(), md)) { - TRACE("pdr", tout << mk_pp(n->state(), m) << "\n";); + TRACE("pdr", tout << n->state() << "\n";); model_ref mr(md); n->set_model(mr); datalog::rule const* rule = rules.find(n->state()); n->set_rule(rule); } else { + TRACE("pdr", tout << "no model for " << n->state() << "\n";); IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0); - verbose_stream() << mk_pp(n->state(), m) << "\n";); + verbose_stream() << n->state() << "\n";); } } + else { + TRACE("pdr", tout << n->state() << "\n";); + } todo.pop_back(); todo.append(n->children().size(), n->children().c_ptr()); } @@ -2027,11 +2037,11 @@ namespace pdr { switch (expand_state(n, cube, uses_level)) { case l_true: if (n.level() == 0) { - TRACE("pdr", tout << "reachable at level 0\n";); + TRACE("pdr", n.display(tout << "reachable at level 0\n", 0);); close_node(n); } else { - TRACE("pdr", tout << "node: " << &n << "\n";); + TRACE("pdr", n.display(tout, 0);); create_children(n); } break; diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 7cba1e0c5..35b9067b2 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -240,7 +240,7 @@ namespace pdr { void check_pre_closed(); void set_closed(); void set_open(); - void set_pre_closed() { m_closed = true; } + void set_pre_closed() { TRACE("pdr", tout << state() << "\n";); m_closed = true; } void reset() { m_children.reset(); } void set_rule(datalog::rule const* r) { m_rule = r; } From 3a3e1796e299633d6cfe79795bc132820b6f8e4d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Nov 2015 18:42:11 -0800 Subject: [PATCH 3/4] Fix bug #311. update tabs Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index a55d0e648..4cdc76ede 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -1162,14 +1162,14 @@ namespace pdr { n->set_rule(rule); } else { - TRACE("pdr", tout << "no model for " << n->state() << "\n";); + TRACE("pdr", tout << "no model for " << n->state() << "\n";); IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0); verbose_stream() << n->state() << "\n";); } } - else { - TRACE("pdr", tout << n->state() << "\n";); - } + else { + TRACE("pdr", tout << n->state() << "\n";); + } todo.pop_back(); todo.append(n->children().size(), n->children().c_ptr()); } @@ -2037,11 +2037,11 @@ namespace pdr { switch (expand_state(n, cube, uses_level)) { case l_true: if (n.level() == 0) { - TRACE("pdr", n.display(tout << "reachable at level 0\n", 0);); + TRACE("pdr", n.display(tout << "reachable at level 0\n", 0);); close_node(n); } else { - TRACE("pdr", n.display(tout, 0);); + TRACE("pdr", n.display(tout, 0);); create_children(n); } break; From b8e4871d9efa8bf966cb693a00bf1c451aca5b79 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Nov 2015 10:53:00 -0800 Subject: [PATCH 4/4] disable bottom-up coi filtering when relations contain facts. bug reported by SeanMcL Signed-off-by: Nikolaj Bjorner --- src/muz/dataflow/dataflow.h | 1 + src/muz/transforms/dl_mk_coi_filter.cpp | 3 +++ 2 files changed, 4 insertions(+) diff --git a/src/muz/dataflow/dataflow.h b/src/muz/dataflow/dataflow.h index 9e100121a..1e52c5f93 100644 --- a/src/muz/dataflow/dataflow.h +++ b/src/muz/dataflow/dataflow.h @@ -87,6 +87,7 @@ namespace datalog { for (func_decl_set::iterator I = output_preds.begin(), E = output_preds.end(); I != E; ++I) { func_decl* sym = *I; + TRACE("dl", tout << sym->get_name() << "\n";); const rule_vector& output_rules = m_rules.get_predicate_rules(sym); for (unsigned i = 0; i < output_rules.size(); ++i) { m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_down(m_context, output_rules[i]); diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index 67b88724c..c452e2611 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -41,6 +41,9 @@ namespace datalog { bool new_tail = false; bool contained = true; for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) { + if (m_context.has_facts(r->get_decl(i))) { + return 0; + } if (r->is_neg_tail(i)) { if (!engine.get_fact(r->get_decl(i)).is_reachable()) { if (!new_tail) {