mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

update Ackerman reduction for division to make Andre and Nathan happy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-10 23:43:21 +02:00
parent 082936bca6
commit 7b47b0380e
2 changed files with 35 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/seq_rewriter.cpp
View file

@ -656,8 +656,8 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
unsigned sz = as.size(); unsigned sz = as.size();
expr* b0 = bs[0].get(); expr* b0 = bs[0].get();
expr* bL = bs[bs.size()-1].get(); expr* bL = bs[bs.size()-1].get();
for (; offs < as.size() && m().are_distinct(b0, as[offs].get()); ++offs) {}; for (; offs < as.size() && m_util.str.is_unit(b0) && m_util.str.is_unit(as[offs].get()) && m().are_distinct(b0, as[offs].get()); ++offs) {};
for (; sz > offs && m().are_distinct(bL, as[sz-1].get()); --sz) {} for (; sz > offs && m_util.str.is_unit(bL) && m_util.str.is_unit(as[sz-1].get()) && m().are_distinct(bL, as[sz-1].get()); --sz) {}
if (offs == sz) { if (offs == sz) {
result = m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b))); result = m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b)));
return BR_REWRITE2; return BR_REWRITE2;

47
src/qe/nlqsat.cpp
View file

@ -429,8 +429,9 @@ namespace qe {
} }
struct div { struct div {
expr_ref num, den, name; expr_ref num, den;
div(ast_manager& m, expr* n, expr* d, expr* nm): app_ref name;
div(ast_manager& m, expr* n, expr* d, app* nm):
num(n, m), den(d, m), name(nm, m) {} num(n, m), den(d, m), name(nm, m) {}
}; };
@ -442,9 +443,9 @@ namespace qe {
div_rewriter_cfg(nlqsat& s): m(s.m), a(s.m) {} div_rewriter_cfg(nlqsat& s): m(s.m), a(s.m) {}
~div_rewriter_cfg() {} ~div_rewriter_cfg() {}
br_status reduce_app(func_decl* f, unsigned sz, expr* const* args, expr_ref& result, proof_ref& pr) { br_status reduce_app(func_decl* f, unsigned sz, expr* const* args, expr_ref& result, proof_ref& pr) {
if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && !a.is_numeral(args[1]) && is_ground(args[0]) && is_ground(args[1])) { if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && !a.is_numeral(args[1])) {
result = m.mk_fresh_const("div", a.mk_real()); result = m.mk_fresh_const("div", a.mk_real());
m_divs.push_back(div(m, args[0], args[1], result)); m_divs.push_back(div(m, args[0], args[1], to_app(result)));
return BR_DONE; return BR_DONE;
} }
return BR_FAILED; return BR_FAILED;
@ -496,7 +497,7 @@ namespace qe {
if (a.is_power(n, n1, n2) && a.is_numeral(n2, r) && r.is_unsigned()) { if (a.is_power(n, n1, n2) && a.is_numeral(n2, r) && r.is_unsigned()) {
return; return;
} }
if (a.is_div(n, n1, n2) && is_ground(n1) && is_ground(n2) && s.m_mode == qsat_t) { if (a.is_div(n, n1, n2) && s.m_mode == qsat_t) {
m_has_divs = true; m_has_divs = true;
return; return;
} }
@ -508,7 +509,7 @@ namespace qe {
bool has_divs() const { return m_has_divs; } bool has_divs() const { return m_has_divs; }
}; };
void purify(expr_ref& fml) { void purify(expr_ref& fml, app_ref_vector& pvars, expr_ref_vector& paxioms) {
is_pure_proc is_pure(*this); is_pure_proc is_pure(*this);
{ {
expr_fast_mark1 visited; expr_fast_mark1 visited;
@ -520,19 +521,34 @@ namespace qe {
proof_ref pr(m); proof_ref pr(m);
rw(fml, fml, pr); rw(fml, fml, pr);
vector<div> const& divs = rw.divs(); vector<div> const& divs = rw.divs();
expr_ref_vector axioms(m);
for (unsigned i = 0; i < divs.size(); ++i) { for (unsigned i = 0; i < divs.size(); ++i) {
axioms.push_back( pvars.push_back(divs[i].name);
paxioms.push_back(
m.mk_or(m.mk_eq(divs[i].den, arith.mk_numeral(rational(0), false)), m.mk_or(m.mk_eq(divs[i].den, arith.mk_numeral(rational(0), false)),
m.mk_eq(divs[i].num, arith.mk_mul(divs[i].den, divs[i].name)))); m.mk_eq(divs[i].num, arith.mk_mul(divs[i].den, divs[i].name))));
for (unsigned j = i + 1; j < divs.size(); ++j) { for (unsigned j = i + 1; j < divs.size(); ++j) {
axioms.push_back(m.mk_or(m.mk_not(m.mk_eq(divs[i].den, divs[j].den)), paxioms.push_back(m.mk_or(m.mk_not(m.mk_eq(divs[i].den, divs[j].den)),
m.mk_not(m.mk_eq(divs[i].num, divs[j].num)), m.mk_not(m.mk_eq(divs[i].num, divs[j].num)),
m.mk_eq(divs[i].name, divs[j].name))); m.mk_eq(divs[i].name, divs[j].name)));
} }
} }
axioms.push_back(fml); }
fml = mk_and(axioms); }
void ackermanize_div(bool is_forall, vector<app_ref_vector>& qvars, expr_ref& fml) {
app_ref_vector pvars(m);
expr_ref_vector paxioms(m);
purify(fml, pvars, paxioms);
if (pvars.empty()) {
return;
}
expr_ref ante = mk_and(paxioms);
qvars[qvars.size()-2].append(pvars);
if (!is_forall) {
fml = m.mk_implies(ante, fml);
}
else {
fml = m.mk_and(fml, ante);
} }
} }
@ -602,7 +618,6 @@ namespace qe {
app_ref_vector vars(m); app_ref_vector vars(m);
bool is_forall = false; bool is_forall = false;
pred_abs abs(m); pred_abs abs(m);
purify(fml);
abs.get_free_vars(fml, vars); abs.get_free_vars(fml, vars);
insert_set(m_free_vars, vars); insert_set(m_free_vars, vars);
qvars.push_back(vars); qvars.push_back(vars);
@ -624,8 +639,12 @@ namespace qe {
} }
while (!vars.empty()); while (!vars.empty());
SASSERT(qvars.back().empty()); SASSERT(qvars.back().empty());
ackermanize_div(is_forall, qvars, fml);
init_expr2var(qvars); init_expr2var(qvars);
goal2nlsat g2s; goal2nlsat g2s;
expr_ref is_true(m), fml1(m), fml2(m); expr_ref is_true(m), fml1(m), fml2(m);