From 5f90e72d856674730522dfcfc3a7ad0da5b3187a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Nov 2019 19:18:54 -0800 Subject: [PATCH] ensure generation is increased #2667 Signed-off-by: Nikolaj Bjorner --- src/smt/cost_evaluator.cpp | 17 ++-- src/smt/cost_evaluator.h | 2 +- src/smt/qi_queue.cpp | 12 +-- src/tactic/fd_solver/smtfd_solver.cpp | 107 +++++++++----------------- 4 files changed, 52 insertions(+), 86 deletions(-) diff --git a/src/smt/cost_evaluator.cpp b/src/smt/cost_evaluator.cpp index 0719d0961..51c025e66 100644 --- a/src/smt/cost_evaluator.cpp +++ b/src/smt/cost_evaluator.cpp @@ -20,30 +20,27 @@ Revision History: #include "util/warning.h" cost_evaluator::cost_evaluator(ast_manager & m): - m_manager(m), + m(m), m_util(m) { } float cost_evaluator::eval(expr * f) const { #define E(IDX) eval(to_app(f)->get_arg(IDX)) if (is_app(f)) { - unsigned num_args; family_id fid = to_app(f)->get_family_id(); - if (fid == m_manager.get_basic_family_id()) { + if (fid == m.get_basic_family_id()) { switch (to_app(f)->get_decl_kind()) { case OP_TRUE: return 1.0f; case OP_FALSE: return 0.0f; case OP_NOT: return E(0) == 0.0f ? 1.0f : 0.0f; - case OP_AND: - num_args = to_app(f)->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - if (E(i) == 0.0f) + case OP_AND: + for (expr* arg : *to_app(f)) + if (eval(arg) == 0.0f) return 0.0f; return 1.0f; case OP_OR: - num_args = to_app(f)->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - if (E(i) != 0.0f) + for (expr* arg : *to_app(f)) + if (eval(arg) != 0.0f) return 1.0f; return 0.0f; case OP_ITE: return E(0) != 0.0f ? E(1) : E(2); diff --git a/src/smt/cost_evaluator.h b/src/smt/cost_evaluator.h index 73b307fbe..18ca3f8a6 100644 --- a/src/smt/cost_evaluator.h +++ b/src/smt/cost_evaluator.h @@ -23,7 +23,7 @@ Revision History: #include "ast/arith_decl_plugin.h" class cost_evaluator { - ast_manager & m_manager; + ast_manager & m; arith_util m_util; unsigned m_num_args; float const * m_args; diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index aa656ee71..47ef73792 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -16,13 +16,13 @@ Author: Revision History: --*/ -#include "smt/smt_context.h" -#include "smt/qi_queue.h" #include "util/warning.h" +#include "util/stats.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "ast/rewriter/var_subst.h" -#include "util/stats.h" +#include "smt/smt_context.h" +#include "smt/qi_queue.h" namespace smt { @@ -130,7 +130,7 @@ namespace smt { // max_top_generation and min_top_generation are not available for computing inc_gen set_values(q, nullptr, generation, 0, 0, cost); float r = m_evaluator(m_new_gen_function, m_vals.size(), m_vals.c_ptr()); - return static_cast(r); + return std::max(generation + 1, static_cast(r)); } void qi_queue::insert(fingerprint * f, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) { @@ -140,7 +140,7 @@ namespace smt { tout << "new instance of " << q->get_qid() << ", weight " << q->get_weight() << ", generation: " << generation << ", scope_level: " << m_context.get_scope_level() << ", cost: " << cost << "\n"; for (unsigned i = 0; i < f->get_num_args(); i++) { - tout << "#" << f->get_arg(i)->get_owner_id() << " "; + tout << "#" << f->get_arg(i)->get_owner_id() << " d:" << f->get_arg(i)->get_owner()->get_depth() << " "; } tout << "\n";); TRACE("new_entries_bug", tout << "[qi:insert]\n";); @@ -201,7 +201,7 @@ namespace smt { ent.m_instantiated = true; - TRACE("qi_queue_profile", tout << q->get_qid() << ", gen: " << generation << " " << *f;); + TRACE("qi_queue_profile", tout << q->get_qid() << ", gen: " << generation << " " << *f << " cost: " << ent.m_cost << "\n";); if (m_checker.is_sat(q->get_expr(), num_bindings, bindings)) { TRACE("checker", tout << "instance already satisfied\n";); diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index 55cca5787..90fcc14cf 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -780,9 +780,27 @@ namespace smtfd { {} void check_term(expr* t, unsigned round) override { + sort* s = m.get_sort(t); if (round == 0 && is_uf(t)) { TRACE("smtfd_verbose", tout << "check-term: " << mk_bounded_pp(t, m, 2) << "\n";); - enforce_congruence(to_app(t)->get_decl(), to_app(t), m.get_sort(t)); + enforce_congruence(to_app(t)->get_decl(), to_app(t), s); + } + else if (round == 1 && sort_covered(s) && m.is_value(t)) { + expr_ref v = eval_abs(t); + val2elem_t& v2e = get_table(s); + expr* e; + if (v2e.find(v, e)) { + if (e != t) { + m_context.add(m.mk_not(m.mk_eq(e, t)), __FUNCTION__); + } + } + else { + m_pinned.push_back(v); + v2e.insert(v, t); + } + } + if (m.is_value(t)) { + // std::cout << mk_bounded_pp(t, m, 2) << " " << eval_abs(t) << " " << mk_pp(s, m) << "\n"; } } @@ -797,7 +815,7 @@ namespace smtfd { } } check_term(t, 0); - return is_uf(t) || is_uninterp_const(t); + return is_uf(t) || is_uninterp_const(t) || sort_covered(s); } bool sort_covered(sort* s) override { @@ -1352,7 +1370,10 @@ namespace smtfd { if (!m_model->eval_expr(q->get_expr(), tmp, true)) { return l_undef; } - if (m.is_true(tmp)) { + if (is_forall(q) && m.is_true(tmp)) { + return l_false; + } + if (is_exists(q) && m.is_false(tmp)) { return l_false; } TRACE("smtfd", @@ -1664,27 +1685,31 @@ namespace smtfd { m_context.reset(m_model); expr_ref_vector terms(core); terms.append(m_axioms); - TRACE("smtfd", tout << "axioms: " << m_axioms << "\n";); for (expr* t : subterms(core)) { if (is_forall(t) || is_exists(t)) { has_q = true; } } for (expr* t : subterms(terms)) { - if (!m_context.term_covered(t) || !m_context.sort_covered(m.get_sort(t))) { + if (!is_forall(t) && !is_exists(t) && (!m_context.term_covered(t) || !m_context.sort_covered(m.get_sort(t)))) { is_decided = l_false; } } m_context.populate_model(m_model, terms); TRACE("smtfd", - for (expr* a : subterms(terms)) { - expr_ref val0 = (*m_model)(a); - expr_ref val1 = (*m_model)(abs(a)); - if (val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) { - tout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n"; - } - }); - TRACE("smtfd", tout << "has quantifier: " << has_q << "\n" << core << "\n";); + tout << "axioms: " << m_axioms << "\n"; + for (expr* a : subterms(terms)) { + expr_ref val0 = (*m_model)(a); + expr_ref val1 = (*m_model)(abs(a)); + if (val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) { + tout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n"; + } + if (!is_forall(a) && !is_exists(a) && (!m_context.term_covered(a) || !m_context.sort_covered(m.get_sort(a)))) { + tout << "not covered: " << mk_pp(a, m) << " " << mk_pp(m.get_sort(a), m) << " "; + tout << m_context.term_covered(a) << " " << m_context.sort_covered(m.get_sort(a)) << "\n"; + } + } + tout << "has quantifier: " << has_q << "\n" << core << "\n";); if (!has_q) { return is_decided; } @@ -1850,59 +1875,6 @@ namespace smtfd { TRACE("smtfd", tout << "block:\n" << mk_bounded_pp(fml, m, 3) << "\n" << mk_bounded_pp(abs(fml), m, 3) << "\n";); assert_fd(fml); } -#if 0 - lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override { - init(); - flush_assertions(); - lbool r; - expr_ref_vector core(m); - while (true) { - IF_VERBOSE(1, verbose_stream() << "(smtfd-check-sat :rounds " << m_stats.m_num_rounds << " lemmas: " << m_stats.m_num_lemmas << " :qi " << m_stats.m_num_mbqi << ")\n"); - m_stats.m_num_rounds++; - checkpoint(); - - // phase 1: check sat of abs - r = check_abs(num_assumptions, assumptions); - if (r != l_true) { - return r; - } - - // phase 2: find prime implicate over FD (abstraction) - r = get_prime_implicate(num_assumptions, assumptions, core); - if (r != l_false) { - return r; - } - - // phase 3: prime implicate over SMT - r = check_smt(core); - if (r == l_true) { - return r; - } - - // phase 4: add theory lemmas - if (r == l_false) { - block_core(core); - } - if (add_theory_axioms(core)) { - continue; - } - if (r != l_undef) { - continue; - } - switch (is_decided_sat(core)) { - case l_true: - return l_true; - case l_undef: - break; - case l_false: - // m_max_conflicts = UINT_MAX; - break; - } - } - return l_undef; - } - -#else lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override { init(); @@ -2008,9 +1980,6 @@ namespace smtfd { return r; } -#endif - - void updt_params(params_ref const & p) override { ::solver::updt_params(p); if (m_fd_sat_solver) {