mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 13:40:52 +00:00
Code Activity

Added option to extend unsat cores with literals that (potentially) provide quantifier instances.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-01-10 20:21:51 +00:00
parent ba9d36605b
commit 384468bc99
2 changed files with 160 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/params/smt_params_helper.pyg
View file

@ -17,7 +17,7 @@ def_module_params(module_name='smt',
('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'), ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'), ('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.'), ('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'), ('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'), ('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.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'), ('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.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')
)) ))

176
src/smt/smt_solver.cpp
View file

@ -22,42 +22,62 @@ Notes:
#include"smt_params.h" #include"smt_params.h"
#include"smt_params_helper.hpp" #include"smt_params_helper.hpp"
#include"mus.h" #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 { namespace smt {
class solver : public solver_na2as { class solver : public solver_na2as {
smt_params m_smt_params; smt_params m_smt_params;
params_ref m_params; params_ref m_params;
smt::kernel m_context; smt::kernel m_context;
progress_callback * m_callback; progress_callback * m_callback;
symbol m_logic; symbol m_logic;
bool m_minimizing_core; bool m_minimizing_core;
bool m_core_extend_patterns;
obj_map<expr, expr*> m_name2assertion;
public: 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), solver_na2as(m),
m_smt_params(p), m_smt_params(p),
m_params(p), m_params(p),
m_context(m, m_smt_params), m_context(m, m_smt_params),
m_minimizing_core(false) { m_minimizing_core(false),
m_core_extend_patterns(false) {
m_logic = l; m_logic = l;
if (m_logic != symbol::null) if (m_logic != symbol::null)
m_context.set_logic(m_logic); 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) { virtual solver * translate(ast_manager & m, params_ref const & p) {
solver* result = alloc(solver, m, p, m_logic); solver * result = alloc(solver, m, p, m_logic);
smt::kernel::copy(m_context, result->m_context); smt::kernel::copy(m_context, result->m_context);
ast_translation translator(get_manager(), m);
obj_map<expr, expr*>::iterator it = m_name2assertion.begin();
obj_map<expr, expr*>::iterator end = m_name2assertion.end();
for (; it != end; it++)
result->m_name2assertion.insert(translator(it->m_key),
translator(it->m_value));
return result; return result;
} }
virtual ~solver() { virtual ~solver() {
dec_ref_values(get_manager(), m_name2assertion);
} }
virtual void updt_params(params_ref const & p) { virtual void updt_params(params_ref const & p) {
m_smt_params.updt_params(p); m_smt_params.updt_params(p);
m_params.copy(p); m_params.copy(p);
m_context.updt_params(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) { virtual void collect_param_descrs(param_descrs & r) {
@ -81,6 +101,12 @@ namespace smt {
m_context.assert_expr(t); 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() { virtual void push_core() {
m_context.push(); m_context.push();
} }
@ -97,7 +123,7 @@ namespace smt {
struct scoped_minimize_core { struct scoped_minimize_core {
solver& s; solver& s;
expr_ref_vector m_assumptions; 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_minimizing_core = true;
s.m_assumptions.reset(); s.m_assumptions.reset();
} }
@ -114,17 +140,19 @@ namespace smt {
r.push_back(m_context.get_unsat_core_expr(i)); r.push_back(m_context.get_unsat_core_expr(i));
} }
if (m_minimizing_core || smt_params_helper(m_params).core_minimize() == false) { if (m_minimizing_core && smt_params_helper(m_params).core_minimize()) {
return; scoped_minimize_core scm(*this);
} mus mus(*this);
scoped_minimize_core scm(*this); mus.add_soft(r.size(), r.c_ptr());
mus mus(*this); ptr_vector<expr> r2;
mus.add_soft(r.size(), r.c_ptr()); if (l_true == mus.get_mus(r2)) {
ptr_vector<expr> r2; r.reset();
if (l_true == mus.get_mus(r2)) { r.append(r2);
r.reset(); }
r.append(r2);
} }
if (m_core_extend_patterns)
add_pattern_literals_to_core(r);
} }
virtual void get_model(model_ref & m) { virtual void get_model(model_ref & m) {
@ -149,7 +177,7 @@ namespace smt {
r.append(tmp.size(), tmp.c_ptr()); 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) { virtual void set_progress_callback(progress_callback * callback) {
m_callback = callback; m_callback = callback;
@ -165,6 +193,108 @@ namespace smt {
return m_context.get_formulas()[idx]; 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<expr> & core, vector<func_decl_set> & assrtn_fds) {
assrtn_fds.resize(m_name2assertion.size());
obj_map<expr, expr*>::iterator ait = m_name2assertion.begin();
obj_map<expr, expr*>::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<expr> & core) {
ast_manager & m = get_manager();
expr_ref_vector new_core_literals(m);
func_decl_set pattern_fds;
vector<func_decl_set> 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<expr, expr*>::iterator ait = m_name2assertion.begin();
obj_map<expr, expr*>::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());
}
}; };
}; };