mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-06-29 08:52:44 -07:00
commit 7e29cc0b12
8 changed files with 110 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz/base/fp_params.pyg
View file

@ -150,6 +150,8 @@ def_module_params('fp',
('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'),
('spacer.q3', BOOL, True, 'Allow quantified lemmas in frames'),
('spacer.q3.instantiate', BOOL, True, 'Instantiate quantified lemmas'),
('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'),
('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'),
('spacer.iuc', UINT, 1,
'0 = use old implementation of unsat-core-generation, ' +
'1 = use new implementation of IUC generation, ' +
@ -164,8 +166,6 @@ def_module_params('fp',
('spacer.iuc.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging)'),
('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes (debugging)'),
('spacer.simplify_pob', BOOL, False, 'simplify pobs by removing redundant constraints'),
('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'),
('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'),
('spacer.p3.share_lemmas', BOOL, False, 'Share frame lemmas'),
('spacer.p3.share_invariants', BOOL, False, "Share invariants lemmas"),
('spacer.min_level', UINT, 0, 'Minimal level to explore'),

17
src/muz/spacer/spacer_context.cpp
View file

@ -126,7 +126,15 @@ void pob::get_skolems(app_ref_vector &v) {
}
}
std::ostream &pob::display(std::ostream &out, bool full) const {
out << pt().head()->get_name ()
<< " level: " << level()
<< " depth: " << depth()
<< " post_id: " << post()->get_id()
<< (is_in_queue() ? " in_queue" : "");
if (full) out << "\n" << m_post;
return out;
}
// ----------------
// pob_queue
@ -538,7 +546,8 @@ void lemma::mk_expr_core() {
SASSERT(!m_cube.empty());
m_body = ::mk_and(m_cube);
// normalize works better with a cube
normalize(m_body, m_body);
normalize(m_body, m_body, false /* no simplify bounds */, false /* term_graph */);
m_body = ::push_not(m_body);
if (!m_zks.empty() && has_zk_const(m_body)) {
@ -2173,9 +2182,7 @@ pob* pred_transformer::pob_manager::mk_pob(pob *parent,
p.set_post(post, b);
if (m_pobs.contains(p.post())) {
auto &buf = m_pobs[p.post()];
for (unsigned i = 0, sz = buf.size(); i < sz; ++i) {
pob *f = buf.get(i);
for (auto *f : m_pobs[p.post()]) {
if (f->parent() == parent && !f->is_in_queue()) {
f->inherit(p);
return f;

4
src/muz/spacer/spacer_context.h
View file

@ -693,6 +693,7 @@ public:
if (m_ref_count == 0) {dealloc(this);}
}
std::ostream &display(std::ostream &out, bool full = false) const;
class on_expand_event
{
pob &m_p;
@ -702,6 +703,9 @@ public:
};
};
inline std::ostream &operator<<(std::ostream &out, pob const &p) {
return p.display(out);
}
struct pob_lt_proc : public std::binary_function<const pob*, const pob*, bool> {
bool operator() (const pob *pn1, const pob *pn2) const;

3
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -56,6 +56,7 @@ prop_solver::prop_solver(ast_manager &m,
m_use_push_bg(p.spacer_keep_proxy())
{
m_random.set_seed(p.spacer_random_seed());
m_solvers[0] = solver0;
m_solvers[1] = solver1;
@ -363,6 +364,8 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
hard.append(_hard.size(), _hard.c_ptr());
flatten_and(hard);
shuffle(hard.size(), hard.c_ptr(), m_random);
m_ctx = m_contexts [solver_id == 0 ? 0 : 0 /* 1 */].get();
// can be disabled if use_push_bg == true

2
src/muz/spacer/spacer_prop_solver.h
View file

@ -61,6 +61,8 @@ private:
bool m_use_push_bg;
unsigned m_current_level; // set when m_in_level
random_gen m_random;
void assert_level_atoms(unsigned level);
void ensure_level(unsigned lvl);

94
src/muz/spacer/spacer_quant_generalizer.cpp
View file

@ -80,6 +80,51 @@ struct index_lt_proc : public std::binary_function<app*, app *, bool> {
}
};
struct has_nlira_functor {
struct found{};
ast_manager &m;
arith_util u;
has_nlira_functor(ast_manager &_m) : m(_m), u(m) {}
void operator()(var *) {}
void operator()(quantifier *) {}
void operator()(app *n) {
family_id fid = n->get_family_id();
if (fid != u.get_family_id()) return;
switch(n->get_decl_kind()) {
case OP_MUL:
if (n->get_num_args() != 2)
throw found();
if (!u.is_numeral(n->get_arg(0)) && !u.is_numeral(n->get_arg(1)))
throw found();
return;
case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
if (!u.is_numeral(n->get_arg(1)))
throw found();
return;
default:
return;
}
return;
}
};
bool has_nlira(expr_ref_vector &v) {
has_nlira_functor fn(v.m());
expr_fast_mark1 visited;
try {
for (expr *e : v)
quick_for_each_expr(fn, visited, e);
}
catch (has_nlira_functor::found e) {
return true;
}
return false;
}
}
namespace spacer {
@ -191,9 +236,15 @@ expr* times_minus_one(expr *e, arith_util &arith) {
Find sub-expression of the form (select A (+ sk!0 t)) and replaces
(+ sk!0 t) --> sk!0 and sk!0 --> (+ sk!0 (* (- 1) t))
Current implementation is an ugly hack for one special case
rewrites bind to (+ bsk!0 t) where bsk!0 is the original binding for sk!0
Current implementation is an ugly hack for one special
case. Should be rewritten based on an equality solver from qe
*/
void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector const &zks, expr_ref &bind) {
void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube,
app_ref_vector const &zks,
expr_ref &bind) {
if (zks.size() != 1) return;
arith_util arith(m);
@ -219,8 +270,8 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector
kids_bind.push_back(bind);
}
else {
kids.push_back (times_minus_one(arg, arith));
kids_bind.push_back (times_minus_one(arg, arith));
kids.push_back(times_minus_one(arg, arith));
kids_bind.push_back(arg);
}
}
if (!found) continue;
@ -228,7 +279,8 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector
rep = arith.mk_add(kids.size(), kids.c_ptr());
bind = arith.mk_add(kids_bind.size(), kids_bind.c_ptr());
TRACE("spacer_qgen",
tout << "replace " << mk_pp(idx, m) << " with " << mk_pp(rep, m) << "\n";);
tout << "replace " << mk_pp(idx, m) << " with " << mk_pp(rep, m) << "\n"
<< "bind is: " << bind << "\n";);
break;
}
}
@ -454,9 +506,15 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
mk_abs_cube(lemma, term, var, gnd_cube, abs_cube, lb, ub, stride);
if (abs_cube.empty()) {return false;}
if (has_nlira(abs_cube)) {
TRACE("spacer_qgen",
tout << "non-linear expression: " << abs_cube << "\n";);
return false;
}
TRACE("spacer_qgen",
tout << "abs_cube is: " << mk_and(abs_cube) << "\n";
tout << "term: " << mk_pp(term, m) << "\n";
tout << "lb = ";
if (lb) tout << mk_pp(lb, m); else tout << "none";
tout << "\n";
@ -473,7 +531,7 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
lb = abs_cube.back();
}
if (!ub) {
abs_cube.push_back (m_arith.mk_lt(var, term));
abs_cube.push_back (m_arith.mk_le(var, term));
ub = abs_cube.back();
}
@ -489,10 +547,10 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
TRACE("spacer_qgen",
tout << "mod=" << mod << " init=" << init << " stride=" << stride << "\n";
tout.flush(););
abs_cube.push_back(m.mk_eq(
m_arith.mk_mod(var, m_arith.mk_numeral(rational(stride), true)),
m_arith.mk_numeral(rational(mod), true)));
}
abs_cube.push_back
(m.mk_eq(m_arith.mk_mod(var,
m_arith.mk_numeral(rational(stride), true)),
m_arith.mk_numeral(rational(mod), true)));}
// skolemize
expr_ref gnd(m);
@ -512,21 +570,21 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
<< "New CUBE is: " << gnd_cube << "\n";);
SASSERT(zks.size() >= static_cast<unsigned>(m_offset));
// lift quantified variables to top of select
// lift quantified variables to top of select
expr_ref ext_bind(m);
ext_bind = term;
cleanup(gnd_cube, zks, ext_bind);
// XXX better do that check before changing bind in cleanup()
// XXX Or not because substitution might introduce _n variable into bind
// XXX better do that check before changing bind in cleanup()
// XXX Or not because substitution might introduce _n variable into bind
if (m_ctx.get_manager().is_n_formula(ext_bind)) {
// XXX this creates an instance, but not necessarily the needed one
// XXX this creates an instance, but not necessarily the needed one
// XXX This is sound because any instance of
// XXX universal quantifier is sound
// XXX This is sound because any instance of
// XXX universal quantifier is sound
// XXX needs better long term solution. leave
// comment here for the future
// XXX needs better long term solution. leave
// comment here for the future
m_ctx.get_manager().formula_n2o(ext_bind, ext_bind, 0);
}

5
src/muz/spacer/spacer_util.cpp
View file

@ -666,9 +666,6 @@ namespace {
flatten_and(out, v);
if (v.size() > 1) {
// sort arguments of the top-level and
std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc());
if (use_simplify_bounds) {
// remove redundant inequalities
simplify_bounds(v);
@ -680,6 +677,8 @@ namespace {
v.reset();
egraph.to_lits(v);
}
// sort arguments of the top-level and
std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc());
TRACE("spacer_normalize",
tout << "Normalized:\n"

16
src/smt/mam.cpp
View file

@ -2000,7 +2000,8 @@ namespace smt {
if (t->filter_candidates()) {
for (enode* app : t->get_candidates()) {
if (!app->is_marked() && app->is_cgr()) {
execute_core(t, app);
if (m_context.resource_limits_exceeded() || !execute_core(t, app))
return;
app->set_mark();
}
}
@ -2014,14 +2015,15 @@ namespace smt {
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
if (app->is_cgr()) {
TRACE("trigger_bug", tout << "is_cgr\n";);
execute_core(t, app);
if (m_context.resource_limits_exceeded() || !execute_core(t, app))
return;
}
}
}
}
// init(t) must be invoked before execute_core
void execute_core(code_tree * t, enode * n);
bool execute_core(code_tree * t, enode * n);
// Return the min, max generation of the enodes in m_pattern_instances.
@ -2250,7 +2252,7 @@ namespace smt {
display_instr_input_reg(out, m_pc);
}
void interpreter::execute_core(code_tree * t, enode * n) {
bool interpreter::execute_core(code_tree * t, enode * n) {
TRACE("trigger_bug", tout << "interpreter::execute_core\n"; t->display(tout); tout << "\nenode\n" << mk_ismt2_pp(n->get_owner(), m_ast_manager) << "\n";);
unsigned since_last_check = 0;
@ -2494,7 +2496,7 @@ namespace smt {
#define ON_MATCH(NUM) \
m_max_generation = std::max(m_max_generation, get_max_generation(NUM, m_bindings.begin())); \
if (m_context.get_cancel_flag()) { \
return; \
return false; \
} \
m_mam.on_match(static_cast<const yield *>(m_pc)->m_qa, \
static_cast<const yield *>(m_pc)->m_pat, \
@ -2647,7 +2649,7 @@ namespace smt {
#ifdef _PROFILE_MAM
t->get_watch().stop();
#endif
return; // no more alternatives
return true; // no more alternatives
}
backtrack_point & bp = m_backtrack_stack[m_top - 1];
m_max_generation = bp.m_old_max_generation;
@ -2675,7 +2677,7 @@ namespace smt {
#ifdef _PROFILE_MAM
t->get_watch().stop();
#endif
return;
return false;
}
}