mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge pull request #1 from wintersteiger/lackr
Minor fixes for QF_BV div0 ackermannization
This commit is contained in:
commit
0489cdc162
|
@ -35,6 +35,10 @@ public:
|
|||
expr_dependency_ref & core) {
|
||||
mc = 0;
|
||||
ast_manager& m(g->m());
|
||||
tactic_report report("ackermannize", *g);
|
||||
fail_if_unsat_core_generation("ackermannize", g);
|
||||
fail_if_proof_generation("ackermannize", g);
|
||||
|
||||
expr_ref_vector flas(m);
|
||||
const unsigned sz = g->size();
|
||||
for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
|
||||
|
@ -48,6 +52,10 @@ public:
|
|||
if (g->models_enabled()) {
|
||||
mc = mk_ackr_model_converter(m, imp->get_info());
|
||||
}
|
||||
|
||||
resg->inc_depth();
|
||||
TRACE("ackermannize", resg->display(tout););
|
||||
SASSERT(resg->is_well_sorted());
|
||||
}
|
||||
|
||||
virtual void collect_statistics(statistics & st) const {
|
||||
|
|
|
@ -285,9 +285,16 @@ struct is_non_qfbv_predicate {
|
|||
throw found();
|
||||
family_id fid = n->get_family_id();
|
||||
if (fid == m.get_basic_family_id())
|
||||
return;
|
||||
if (fid == u.get_family_id())
|
||||
return;
|
||||
return;
|
||||
if (fid == u.get_family_id()) {
|
||||
if (n->get_decl_kind() == OP_BSDIV0 ||
|
||||
n->get_decl_kind() == OP_BUDIV0 ||
|
||||
n->get_decl_kind() == OP_BSREM0 ||
|
||||
n->get_decl_kind() == OP_BUREM0 ||
|
||||
n->get_decl_kind() == OP_BSMOD0)
|
||||
throw found();
|
||||
return;
|
||||
}
|
||||
if (is_uninterp_const(n))
|
||||
return;
|
||||
throw found();
|
||||
|
@ -305,8 +312,6 @@ public:
|
|||
class is_qfbv_probe : public probe {
|
||||
public:
|
||||
virtual result operator()(goal const & g) {
|
||||
bv_rewriter rw(g.m());
|
||||
if (!rw.hi_div0()) return false;
|
||||
return !test<is_non_qfbv_predicate>(g);
|
||||
}
|
||||
};
|
||||
|
|
Loading…
Reference in a new issue