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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-04 07:26:50 +07:00
parent c744b19bce
commit b86432e2a3
1 changed files with 10 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/qe/nlqsat.cpp
View file

@ -517,18 +517,15 @@ namespace qe {
Ackermanize division Ackermanize division
For each p/q: For each p/q:
p = 0 & q = 0 => div = delta0 q != 0 => div_pq*q = p
p != 0 & q = 0 => div = p*delta1
q != 0 => div*q = p For each p/q, p'/q'
p = p', q = q' => div_pq = div_pq'
delta0 stands for 0/0
delta1 stands for 1/0
assumption: p * 1/0 = p/0 for p != 0,
so 2/0 != a * 1/0 & a = 2 is unsat by fiat.
*/ */
void purify(expr_ref& fml, div_rewriter_star& rw, expr_ref_vector& paxioms) { void ackermanize_div(expr_ref& fml) {
is_pure_proc is_pure(*this); is_pure_proc is_pure(*this);
{ {
expr_fast_mark1 visited; expr_fast_mark1 visited;
quick_for_each_expr(is_pure, visited, fml); quick_for_each_expr(is_pure, visited, fml);
@ -536,11 +533,13 @@ namespace qe {
if (is_pure.has_divs()) { if (is_pure.has_divs()) {
arith_util arith(m); arith_util arith(m);
proof_ref pr(m); proof_ref pr(m);
expr_ref_vector paxioms(m);
div_rewriter_star rw(*this);
rw(fml, fml, pr); rw(fml, fml, pr);
paxioms.push_back(fml);
vector<div> const& divs = rw.divs(); vector<div> const& divs = rw.divs();
for (unsigned i = 0; i < divs.size(); ++i) { for (unsigned i = 0; i < divs.size(); ++i) {
expr_ref den_is0(m.mk_eq(divs[i].den, arith.mk_real(0)), m); expr_ref den_is0(m.mk_eq(divs[i].den, arith.mk_real(0)), m);
expr_ref num_is0(m.mk_eq(divs[i].num, arith.mk_real(0)), m);
paxioms.push_back(m.mk_or(den_is0, m.mk_eq(divs[i].num, arith.mk_mul(divs[i].den, divs[i].name)))); paxioms.push_back(m.mk_or(den_is0, 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) {
paxioms.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)),
@ -548,21 +547,10 @@ namespace qe {
m.mk_eq(divs[i].name, divs[j].name))); m.mk_eq(divs[i].name, divs[j].name)));
} }
} }
fml = mk_and(paxioms);
} }
} }
void ackermanize_div(expr_ref& fml) {
app_ref_vector pvars(m);
expr_ref_vector paxioms(m);
div_rewriter_star rw(*this);
purify(fml, rw, paxioms);
if (!paxioms.empty()) {
fml = m.mk_and(fml, mk_and(paxioms));
TRACE("qe", tout << fml << "\n";);
}
}
void reset() override { void reset() override {
//m_solver.reset(); //m_solver.reset();
m_asms.reset(); m_asms.reset();