From c8f09fa955ce4f6bb259eea03697db8944c9cd2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 16 Nov 2015 22:59:07 -0800 Subject: [PATCH] fix for unsound results reported in #313 Signed-off-by: Nikolaj Bjorner --- src/ast/ast_util.cpp | 9 ++++++ src/ast/ast_util.h | 7 +++++ src/muz/pdr/pdr_context.cpp | 61 +++++++++++++++++++++++-------------- src/muz/pdr/pdr_context.h | 1 - 4 files changed, 54 insertions(+), 24 deletions(-) diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index 94e7b642c..eba4d526b 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -166,6 +166,11 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args) { return m.mk_and(num_args, args); } +app* mk_and(ast_manager & m, unsigned num_args, app * const * args) { + return to_app(mk_and(m, num_args, (expr* const*) args)); +} + + expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) { if (num_args == 0) return m.mk_false(); @@ -175,6 +180,10 @@ expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) { return m.mk_or(num_args, args); } +app* mk_or(ast_manager & m, unsigned num_args, app * const * args) { + return to_app(mk_or(m, num_args, (expr* const*) args)); +} + expr * mk_not(ast_manager & m, expr * arg) { expr * atom; if (m.is_not(arg, atom)) diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h index 87a3a90d9..311001a19 100644 --- a/src/ast/ast_util.h +++ b/src/ast/ast_util.h @@ -107,6 +107,9 @@ expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx); Return true if num_args == 0 */ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args); +app * mk_and(ast_manager & m, unsigned num_args, app * const * args); +inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); } +inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); } /** Return (or args[0] ... args[num_args-1]) if num_args >= 2 @@ -114,6 +117,10 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args); Return false if num_args == 0 */ expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args); +app * mk_or(ast_manager & m, unsigned num_args, app * const * args); +inline app_ref mk_or(app_ref_vector const& args) { return app_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); } +inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); } + /** Return a if arg = (not a) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 4cdc76ede..5140c9eff 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -50,6 +50,7 @@ Notes: #include "blast_term_ite_tactic.h" #include "model_implicant.h" #include "expr_safe_replace.h" +#include "ast_util.h" namespace pdr { @@ -448,6 +449,7 @@ namespace pdr { else if (is_sat == l_false) { uses_level = m_solver.assumes_level(); } + m_solver.set_model(0); return is_sat; } @@ -481,6 +483,7 @@ namespace pdr { prop_solver::scoped_level _sl(m_solver, level); m_solver.set_core(&core); m_solver.set_subset_based_core(true); + m_solver.set_model(0); lbool res = m_solver.check_assumptions_and_formula(lits, fml); if (res == l_false) { lits.reset(); @@ -775,6 +778,13 @@ namespace pdr { } // only initial states are not set by the PDR search. SASSERT(m_model.get()); + if (!m_model.get()) { + std::stringstream msg; + msg << "no model for node " << state(); + IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); + throw default_exception(msg.str()); + } + datalog::rule const& rl1 = pt().find_rule(*m_model); if (is_ini(rl1)) { set_rule(&rl1); @@ -793,15 +803,23 @@ namespace pdr { } } SASSERT(!tags.empty()); - ini_tags = m.mk_or(tags.size(), tags.c_ptr()); + ini_tags = ::mk_or(tags); ini_state = m.mk_and(ini_tags, pt().initial_state(), state()); model_ref mdl; pt().get_solver().set_model(&mdl); - TRACE("pdr", tout << mk_pp(ini_state, m) << "\n";); - VERIFY(l_true == pt().get_solver().check_conjunction_as_assumptions(ini_state)); + TRACE("pdr", tout << ini_state << "\n";); + if (l_true != pt().get_solver().check_conjunction_as_assumptions(ini_state)) { + std::stringstream msg; + msg << "Unsatisfiable initial state: " << ini_state << "\n"; + display(msg, 2); + IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); + throw default_exception(msg.str()); + } + SASSERT(mdl.get()); datalog::rule const& rl2 = pt().find_rule(*mdl); SASSERT(is_ini(rl2)); set_rule(&rl2); + pt().get_solver().set_model(0); return const_cast(m_rule); } @@ -830,7 +848,7 @@ namespace pdr { } r0 = get_rule(); app_ref_vector& inst = pt().get_inst(r0); - TRACE("pdr", tout << mk_pp(state(), m) << " instance: " << inst.size() << "\n";); + TRACE("pdr", tout << state() << " instance: " << inst.size() << "\n";); for (unsigned i = 0; i < inst.size(); ++i) { expr* v; if (model.find(inst[i].get(), v)) { @@ -852,7 +870,7 @@ namespace pdr { for (unsigned i = 0; i < indent; ++i) out << " "; out << m_level << " " << m_pt.head()->get_name() << " " << (m_closed?"closed":"open") << "\n"; for (unsigned i = 0; i < indent; ++i) out << " "; - out << " " << mk_pp(m_state, m_state.get_manager(), indent) << "\n"; + out << " " << mk_pp(m_state, m_state.get_manager(), indent) << " " << m_state->get_id() << "\n"; for (unsigned i = 0; i < children().size(); ++i) { children()[i]->display(out, indent + 1); } @@ -925,17 +943,6 @@ namespace pdr { } } - bool model_search::is_repeated(model_node& n) const { - model_node* p = n.parent(); - while (p) { - if (p->state() == n.state()) { - TRACE("pdr", tout << n.state() << "repeated\n";); - return true; - } - p = p->parent(); - } - return false; - } void model_search::add_leaf(model_node& n) { SASSERT(n.children().empty()); @@ -1012,11 +1019,11 @@ namespace pdr { nodes.erase(&n); bool is_goal = n.is_goal(); remove_goal(n); - if (!nodes.empty() && is_goal && backtrack) { + // TBD: siblings would also fail if n is not a goal. + if (!nodes.empty() && backtrack && nodes[0]->children().empty() && nodes[0]->is_closed()) { 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()); + n1->set_open(); enqueue_leaf(n1); } @@ -1702,7 +1709,15 @@ namespace pdr { void context::validate_search() { expr_ref tr = m_search.get_trace(*this); - // TBD: tr << "\n"; + smt::kernel solver(m, get_fparams()); + solver.assert_expr(tr); + lbool res = solver.check(); + if (res != l_true) { + std::stringstream msg; + msg << "rule validation failed when checking: " << tr; + IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); + throw default_exception(msg.str()); + } } void context::validate_model() { @@ -1938,11 +1953,11 @@ namespace pdr { proof_ref proof(m); SASSERT(m_last_result == l_true); proof = m_search.get_proof_trace(*this); - TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";); + TRACE("pdr", tout << "PDR trace: " << proof << "\n";); apply(m, m_pc.get(), proof); - TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";); + TRACE("pdr", tout << "PDR trace: " << proof << "\n";); // proof_utils::push_instantiations_up(proof); - // TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";); + // TRACE("pdr", tout << "PDR up: " << proof << "\n";); return proof; } diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h index 35b9067b2..ad4b44d90 100644 --- a/src/muz/pdr/pdr_context.h +++ b/src/muz/pdr/pdr_context.h @@ -268,7 +268,6 @@ namespace pdr { 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: