From cd838e5cf4f96d1d288287e8468e87d581c4d3ae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 13 Aug 2015 14:29:48 +0200 Subject: [PATCH] fix bug reported in issue #193: MBQI needs to avoid instantiating data-types that contain model values in nested positions Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bceq.cpp | 45 +++++++++++++++------------ src/sat/sat_bceq.h | 2 ++ src/sat/sat_solver/inc_sat_solver.cpp | 2 ++ src/smt/smt_model_checker.cpp | 26 +++++++++++++++- src/smt/smt_model_checker.h | 7 +++++ src/smt/smt_model_finder.cpp | 45 +++++++++++++++++++++------ src/smt/theory_opt.cpp | 13 ++------ 7 files changed, 100 insertions(+), 40 deletions(-) diff --git a/src/sat/sat_bceq.cpp b/src/sat/sat_bceq.cpp index e3613515f..48145010f 100644 --- a/src/sat/sat_bceq.cpp +++ b/src/sat/sat_bceq.cpp @@ -45,6 +45,7 @@ namespace sat { m_R.reset(); m_L_blits.reset(); m_R_blits.reset(); + m_bce_use_list.finalize(); clause * const* it = m_solver.begin_clauses(); clause * const* end = m_solver.end_clauses(); for (; it != end; ++it) { @@ -140,7 +141,6 @@ namespace sat { for (unsigned i = 0; i < m_L.size(); ++i) { ul.insert(*m_L[i]); } -#define MOVE_R_TO_L \ // cheap pass: add clauses from R in order // such that they are blocked with respect to @@ -161,6 +161,10 @@ namespace sat { } // expensive pass: add clauses from R as long // as BCE produces the empty set of clauses. + m_bce_use_list.init(m_solver.num_vars()); + for (unsigned i = 0; i < m_L.size(); ++i) { + m_bce_use_list.insert(*m_L[i]); + } for (unsigned i = 0; i < m_R.size(); ++i) { if (bce(*m_R[i])) { m_R[i] = m_R.back(); @@ -173,29 +177,29 @@ namespace sat { m_use_list = save; } - bool bceq::bce(clause& cls) { + bool bceq::bce(clause& cls0) { + IF_VERBOSE(1, verbose_stream() << "bce " << m_L.size() << " " << m_R.size() << " " << cls0 << "\n";); svector live_clauses; - use_list ul; - m_use_list = &ul; - ul.init(m_solver.num_vars()); - for (unsigned i = 0; i < m_L.size(); ++i) { - ul.insert(*m_L[i]); - } - ul.insert(cls); + m_use_list = &m_bce_use_list; + m_bce_use_list.insert(cls0); svector clauses(m_L), new_clauses; literal_vector blits(m_L_blits), new_blits; - clauses.push_back(&cls); + clauses.push_back(&cls0); blits.push_back(null_literal); bool removed = false; m_removed.reset(); do { removed = false; for (unsigned i = 0; i < clauses.size(); ++i) { - clause& cls = *clauses[i]; - literal lit = find_blocked(cls); - if (lit != null_literal) { - m_removed.setx(cls.id(), true, false); - new_clauses.push_back(&cls); + clause& cls1 = *clauses[i]; + literal lit = find_blocked(cls1); + if (lit == null_literal) { + m_bce_use_list.erase(cls1); + } + else { + IF_VERBOSE(2, verbose_stream() << "; remove " << cls1 << "\n";); + m_removed.setx(cls1.id(), true, false); + new_clauses.push_back(&cls1); new_blits.push_back(lit); removed = true; clauses[i] = clauses.back(); @@ -215,7 +219,7 @@ namespace sat { m_L.append(new_clauses); m_L_blits.append(new_blits); } - if (!clauses.empty()) std::cout << "Number left after BCE: " << clauses.size() << "\n"; + IF_VERBOSE(1, if (!clauses.empty()) verbose_stream() << "; clauses left after BCE: " << clauses.size() << "\n";); return clauses.empty(); } @@ -442,9 +446,10 @@ namespace sat { roots[l2.var()] = l1; vars.push_back(l2.var()); elim_eqs elim(m_solver); - for (unsigned i = 0; i < vars.size(); ++i) { - std::cout << "var: " << vars[i] << " root: " << roots[vars[i]] << "\n"; - } + IF_VERBOSE(1, + for (unsigned i = 0; i < vars.size(); ++i) { + verbose_stream() << "var: " << vars[i] << " root: " << roots[vars[i]] << "\n"; + }); elim(roots, vars); } @@ -473,7 +478,7 @@ namespace sat { init(); pure_decompose(); post_decompose(); - std::cout << "Decomposed set " << m_L.size() << " rest: " << m_R.size() << "\n"; + IF_VERBOSE(1, verbose_stream() << "Decomposed set " << m_L.size() << " rest: " << m_R.size() << "\n";); TRACE("sat", tout << "Decomposed set " << m_L.size() << "\n"; diff --git a/src/sat/sat_bceq.h b/src/sat/sat_bceq.h index 4718b6ef1..cd18ee456 100644 --- a/src/sat/sat_bceq.h +++ b/src/sat/sat_bceq.h @@ -21,6 +21,7 @@ Revision History: #include"sat_types.h" #include "union_find.h" +#include "sat_simplifier.h" namespace sat { @@ -33,6 +34,7 @@ namespace sat { typedef svector bin_clauses; solver & m_solver; use_list* m_use_list; + use_list m_bce_use_list; solver* m_s; random_gen m_rand; svector m_clauses; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 99dd24dc7..742a02d3c 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -100,6 +100,7 @@ public: virtual void set_progress_callback(progress_callback * callback) {} virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) { + m_solver.pop_to_base_level(); dep2asm_t dep2asm; m_model = 0; @@ -112,6 +113,7 @@ public: r = initialize_soft_constraints(); if (r != l_true) return r; + m_solver.display_dimacs(std::cout); r = m_solver.check(m_asms.size(), m_asms.c_ptr()); switch (r) { case l_true: diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 066185aa3..59b54a319 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -171,7 +171,7 @@ namespace smt { sk_value = sk_term; } } - if (m_manager.is_model_value(sk_value)) + if (contains_model_value(sk_value)) return false; bindings.set(num_decls - i - 1, sk_value); } @@ -190,6 +190,30 @@ namespace smt { return true; } + void model_checker::operator()(expr *n) { + if (m_manager.is_model_value(n)) { + throw is_model_value(); + } + } + + bool model_checker::contains_model_value(expr* n) { + if (m_manager.is_model_value(n)) { + return true; + } + if (is_app(n) && to_app(n)->get_num_args() == 0) { + return false; + } + m_visited.reset(); + try { + for_each_expr(*this, m_visited, n); + } + catch (is_model_value) { + return true; + } + return false; + } + + bool model_checker::add_blocking_clause(model * cex, expr_ref_vector & sks) { SASSERT(cex != 0); unsigned num_sks = sks.size(); diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h index 93488ff65..f7fcd8198 100644 --- a/src/smt/smt_model_checker.h +++ b/src/smt/smt_model_checker.h @@ -80,6 +80,10 @@ namespace smt { quantifier * get_flat_quantifier(quantifier * q); + struct is_model_value {}; + expr_mark m_visited; + bool contains_model_value(expr* e); + public: model_checker(ast_manager & m, qi_params const & p, model_finder & mf); ~model_checker(); @@ -95,6 +99,9 @@ namespace smt { void reset(); void set_cancel(bool f) { m_cancel = f; } + + void operator()(expr* e); + }; }; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index fea9f9bce..8494bf336 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -83,6 +83,7 @@ namespace smt { ast_manager & m_manager; obj_map m_elems; // and the associated generation obj_map m_inv; + expr_mark m_visited; public: instantiation_set(ast_manager & m):m_manager(m) {} @@ -98,11 +99,11 @@ namespace smt { obj_map const & get_elems() const { return m_elems; } void insert(expr * n, unsigned generation) { - if (m_elems.contains(n)) + if (m_elems.contains(n) || contains_model_value(n)) return; + TRACE("model_finder", tout << mk_pp(n, m_manager) << "\n";); m_manager.inc_ref(n); m_elems.insert(n, generation); - CTRACE("model_finder", m_manager.is_model_value(n), tout << mk_pp(n, m_manager) << "\n";); SASSERT(!m_manager.is_model_value(n)); } @@ -145,9 +146,10 @@ namespace smt { obj_map::iterator end = m_elems.end(); for (; it != end; ++it) { expr * t = (*it).m_key; - SASSERT(!m_manager.is_model_value(t)); + SASSERT(!contains_model_value(t)); unsigned gen = (*it).m_value; expr * t_val = ev.eval(t, true); + TRACE("model_finder", tout << mk_pp(t, m_manager) << "\n";); expr * old_t = 0; if (m_inv.find(t_val, old_t)) { @@ -167,6 +169,30 @@ namespace smt { obj_map const & get_inv_map() const { return m_inv; } + + struct is_model_value {}; + void operator()(expr *n) { + if (m_manager.is_model_value(n)) { + throw is_model_value(); + } + } + + bool contains_model_value(expr* n) { + if (m_manager.is_model_value(n)) { + return true; + } + if (is_app(n) && to_app(n)->get_num_args() == 0) { + return false; + } + m_visited.reset(); + try { + for_each_expr(*this, m_visited, n); + } + catch (is_model_value) { + return true; + } + return false; + } }; /** @@ -286,7 +312,7 @@ namespace smt { return get_root()->m_signed_proj; } - void mk_instatiation_set(ast_manager & m) { + void mk_instantiation_set(ast_manager & m) { SASSERT(is_root()); m_set = alloc(instantiation_set, m); } @@ -527,13 +553,13 @@ namespace smt { return 0; } - void mk_instatiation_sets() { + void mk_instantiation_sets() { ptr_vector::const_iterator it = m_nodes.begin(); ptr_vector::const_iterator end = m_nodes.end(); for (; it != end; ++it) { node * curr = *it; if (curr->is_root()) { - curr->mk_instatiation_set(m_manager); + curr->mk_instantiation_set(m_manager); } } } @@ -695,6 +721,7 @@ namespace smt { return 0; m_model->register_decl(k_decl, r); SASSERT(m_model->get_const_interp(k_decl) == r); + TRACE("model_finder", tout << mk_pp(r, m_manager) << "\n";); return r; } @@ -1204,7 +1231,7 @@ namespace smt { // a necessary instantiation. enode * e_arg = n->get_arg(m_arg_i); expr * arg = e_arg->get_owner(); - A_f_i->insert(arg, e_arg->get_generation()); + A_f_i->insert(arg, e_arg->get_generation()); } } } @@ -1225,7 +1252,7 @@ namespace smt { if (ctx->is_relevant(n)) { enode * e_arg = n->get_arg(m_arg_i); expr * arg = e_arg->get_owner(); - s->insert(arg, e_arg->get_generation()); + s->insert(arg, e_arg->get_generation()); } } } @@ -3378,7 +3405,7 @@ namespace smt { quantifier_info * qi = get_quantifier_info(q); qi->process_auf(*(m_auf_solver.get()), m_context); } - m_auf_solver->mk_instatiation_sets(); + m_auf_solver->mk_instantiation_sets(); it = qs.begin(); for (; it != end; ++it) { quantifier * q = *it; diff --git a/src/smt/theory_opt.cpp b/src/smt/theory_opt.cpp index 279863885..9e6fa452c 100644 --- a/src/smt/theory_opt.cpp +++ b/src/smt/theory_opt.cpp @@ -68,17 +68,10 @@ namespace smt { bool theory_opt::is_numeral(arith_util& a, expr* term) { - while (true) { - if (a.is_uminus(term) || a.is_to_real(term) || a.is_to_int(term)) { - term = to_app(term)->get_arg(0); - } - else if (a.is_numeral(term)) { - return true; - } - else { - return false; - } + while (a.is_uminus(term) || a.is_to_real(term) || a.is_to_int(term)) { + term = to_app(term)->get_arg(0); } + return a.is_numeral(term); } };