diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 739af8bfe..178b2117f 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -1,4 +1,4 @@ -def_module_params(module_name='smt', +def_module_params(module_name='smt', class_name='smt_params_helper', description='smt solver based on lazy smt', export=True, @@ -17,7 +17,7 @@ def_module_params(module_name='smt', ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'), ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), - ('rlimit', UINT, 0, 'resource limit (0 means no limit)'), + ('rlimit', UINT, 0, 'resource limit (0 means no limit)'), ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'), ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'), ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'), @@ -62,5 +62,6 @@ def_module_params(module_name='smt', ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'), ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'), - ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context') + ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'), + ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances') )) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 2ea4fea20..703e4489e 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -22,42 +22,62 @@ Notes: #include"smt_params.h" #include"smt_params_helper.hpp" #include"mus.h" - +#include"for_each_expr.h" +#include"ast_smt2_pp.h" +#include"func_decl_dependencies.h" +#include"dec_ref_util.h" namespace smt { class solver : public solver_na2as { - smt_params m_smt_params; - params_ref m_params; - smt::kernel m_context; - progress_callback * m_callback; - symbol m_logic; - bool m_minimizing_core; + smt_params m_smt_params; + params_ref m_params; + smt::kernel m_context; + progress_callback * m_callback; + symbol m_logic; + bool m_minimizing_core; + bool m_core_extend_patterns; + obj_map m_name2assertion; + public: - solver(ast_manager & m, params_ref const & p, symbol const & l): + solver(ast_manager & m, params_ref const & p, symbol const & l) : solver_na2as(m), m_smt_params(p), m_params(p), m_context(m, m_smt_params), - m_minimizing_core(false) { + m_minimizing_core(false), + m_core_extend_patterns(false) { m_logic = l; if (m_logic != symbol::null) m_context.set_logic(m_logic); + smt_params_helper smth(p); + m_core_extend_patterns = smth.core_extend_patterns(); } - virtual solver* translate(ast_manager& m, params_ref const& p) { - solver* result = alloc(solver, m, p, m_logic); + virtual solver * translate(ast_manager & m, params_ref const & p) { + solver * result = alloc(solver, m, p, m_logic); smt::kernel::copy(m_context, result->m_context); + + ast_translation translator(get_manager(), m); + obj_map::iterator it = m_name2assertion.begin(); + obj_map::iterator end = m_name2assertion.end(); + for (; it != end; it++) + result->m_name2assertion.insert(translator(it->m_key), + translator(it->m_value)); + return result; } - + virtual ~solver() { + dec_ref_values(get_manager(), m_name2assertion); } virtual void updt_params(params_ref const & p) { m_smt_params.updt_params(p); m_params.copy(p); m_context.updt_params(p); + smt_params_helper smth(p); + m_core_extend_patterns = smth.core_extend_patterns(); } virtual void collect_param_descrs(param_descrs & r) { @@ -81,6 +101,12 @@ namespace smt { m_context.assert_expr(t); } + virtual void assert_expr(expr * t, expr * a) { + solver_na2as::assert_expr(t, a); + get_manager().inc_ref(t); + m_name2assertion.insert(a, t); + } + virtual void push_core() { m_context.push(); } @@ -97,7 +123,7 @@ namespace smt { struct scoped_minimize_core { solver& s; expr_ref_vector m_assumptions; - scoped_minimize_core(solver& s): s(s), m_assumptions(s.m_assumptions) { + scoped_minimize_core(solver& s) : s(s), m_assumptions(s.m_assumptions) { s.m_minimizing_core = true; s.m_assumptions.reset(); } @@ -114,17 +140,19 @@ namespace smt { r.push_back(m_context.get_unsat_core_expr(i)); } - if (m_minimizing_core || smt_params_helper(m_params).core_minimize() == false) { - return; - } - scoped_minimize_core scm(*this); - mus mus(*this); - mus.add_soft(r.size(), r.c_ptr()); - ptr_vector r2; - if (l_true == mus.get_mus(r2)) { - r.reset(); - r.append(r2); + if (m_minimizing_core && smt_params_helper(m_params).core_minimize()) { + scoped_minimize_core scm(*this); + mus mus(*this); + mus.add_soft(r.size(), r.c_ptr()); + ptr_vector r2; + if (l_true == mus.get_mus(r2)) { + r.reset(); + r.append(r2); + } } + + if (m_core_extend_patterns) + add_pattern_literals_to_core(r); } virtual void get_model(model_ref & m) { @@ -149,7 +177,7 @@ namespace smt { r.append(tmp.size(), tmp.c_ptr()); } - virtual ast_manager& get_manager() const { return m_context.m(); } + virtual ast_manager & get_manager() const { return m_context.m(); } virtual void set_progress_callback(progress_callback * callback) { m_callback = callback; @@ -159,12 +187,114 @@ namespace smt { virtual unsigned get_num_assertions() const { return m_context.size(); } - + virtual expr * get_assertion(unsigned idx) const { SASSERT(idx < get_num_assertions()); return m_context.get_formulas()[idx]; - } + } + struct collect_fds_proc { + ast_manager & m; + func_decl_set & m_fds; + collect_fds_proc(ast_manager & m, func_decl_set & fds) : + m(m), m_fds(fds) { + } + void operator()(var * n) {} + void operator()(app * n) { + func_decl * fd = n->get_decl(); + if (fd->get_family_id() == null_family_id) + m_fds.insert_if_not_there(fd); + } + void operator()(quantifier * n) {} + }; + + struct collect_pattern_fds_proc { + ast_manager & m; + expr_fast_mark1 m_visited; + func_decl_set & m_fds; + collect_pattern_fds_proc(ast_manager & m, func_decl_set & fds) : + m(m), m_fds(fds) { + m_visited.reset(); + } + void operator()(var * n) {} + void operator()(app * n) {} + void operator()(quantifier * n) { + collect_fds_proc p(m, m_fds); + + unsigned sz = n->get_num_patterns(); + for (unsigned i = 0; i < sz; i++) + quick_for_each_expr(p, m_visited, n->get_pattern(i)); + + sz = n->get_num_no_patterns(); + for (unsigned i = 0; i < sz; i++) + quick_for_each_expr(p, m_visited, n->get_no_pattern(i)); + } + }; + + void collect_pattern_func_decls(expr_ref & e, func_decl_set & fds) { + collect_pattern_fds_proc p(get_manager(), fds); + expr_mark visited; + for_each_expr(p, visited, e); + } + + void compute_assrtn_fds(ptr_vector & core, vector & assrtn_fds) { + assrtn_fds.resize(m_name2assertion.size()); + obj_map::iterator ait = m_name2assertion.begin(); + obj_map::iterator aend = m_name2assertion.end(); + for (unsigned i = 0; ait != aend; ait++, i++) { + if (core.contains(ait->m_key)) + continue; + collect_fds_proc p(m, assrtn_fds[i]); + expr_fast_mark1 visited; + quick_for_each_expr(p, visited, ait->m_value); + } + } + + bool fds_intersect(func_decl_set & pattern_fds, func_decl_set & assrtn_fds) { + func_decl_set::iterator it = pattern_fds.begin(); + func_decl_set::iterator end = pattern_fds.end(); + for (; it != end; it++) { + func_decl * fd = *it; + if (assrtn_fds.contains(fd)) + return true; + } + return false; + } + + void add_pattern_literals_to_core(ptr_vector & core) { + ast_manager & m = get_manager(); + expr_ref_vector new_core_literals(m); + + func_decl_set pattern_fds; + vector assrtn_fds; + + do { + new_core_literals.reset(); + + unsigned sz = core.size(); + for (unsigned i = 0; i < sz; i++) { + expr_ref name(core[i], m); + expr_ref assrtn(m_name2assertion.find(name), m); + collect_pattern_func_decls(assrtn, pattern_fds); + } + + if (!pattern_fds.empty()) { + if (assrtn_fds.empty()) + compute_assrtn_fds(core, assrtn_fds); + + obj_map::iterator ait = m_name2assertion.begin(); + obj_map::iterator aend = m_name2assertion.end(); + for (unsigned i = 0; ait != aend; ait++, i++) { + if (!core.contains(ait->m_key) && + fds_intersect(pattern_fds, assrtn_fds[i])) + new_core_literals.push_back(ait->m_key); + } + } + + core.append(new_core_literals.size(), new_core_literals.c_ptr()); + } + while (!new_core_literals.empty()); + } }; };