mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
improvements to arithmetic preprocessing simplificaiton and axiom generation for #1683
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
86c39c971d
commit
8a29c2803c
|
@ -800,52 +800,105 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
|
|||
result = m_util.mk_numeral(div(v1, v2), is_int);
|
||||
return BR_DONE;
|
||||
}
|
||||
expr_ref quot(m());
|
||||
if (divides(arg1, arg2, quot)) {
|
||||
result = m_util.mk_mul(quot, m_util.mk_idiv(arg1, arg1));
|
||||
return BR_REWRITE2;
|
||||
if (m_util.is_numeral(arg2, v2, is_int) && v2.is_one()) {
|
||||
result = arg1;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) {
|
||||
return BR_FAILED;
|
||||
}
|
||||
if (arg1 == arg2) {
|
||||
expr_ref zero(m_util.mk_int(0), m());
|
||||
result = m().mk_ite(m().mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1));
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
if (divides(arg1, arg2, result)) {
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
bool arith_rewriter::divides(expr* d, expr* n, expr_ref& quot) {
|
||||
if (d == n) {
|
||||
quot = m_util.mk_numeral(rational(1), m_util.is_int(d));
|
||||
|
||||
//
|
||||
// implement div ab ac = floor( ab / ac) = floor (b / c) = div b c
|
||||
//
|
||||
bool arith_rewriter::divides(expr* num, expr* den, expr_ref& result) {
|
||||
expr_fast_mark1 mark;
|
||||
rational num_r(1), den_r(1);
|
||||
expr* num_e = nullptr, *den_e = nullptr;
|
||||
ptr_buffer<expr> args1, args2;
|
||||
flat_mul(num, args1);
|
||||
flat_mul(den, args2);
|
||||
for (expr * arg : args1) {
|
||||
mark.mark(arg);
|
||||
if (m_util.is_numeral(arg, num_r)) num_e = arg;
|
||||
}
|
||||
for (expr* arg : args2) {
|
||||
if (mark.is_marked(arg)) {
|
||||
result = remove_divisor(arg, num, den);
|
||||
return true;
|
||||
}
|
||||
if (m_util.is_numeral(arg, den_r)) den_e = arg;
|
||||
}
|
||||
rational g = gcd(num_r, den_r);
|
||||
if (!g.is_one()) {
|
||||
SASSERT(g.is_pos());
|
||||
// replace num_e, den_e by their gcd reduction.
|
||||
for (unsigned i = 0; i < args1.size(); ++i) {
|
||||
if (args1[i] == num_e) {
|
||||
args1[i] = m_util.mk_numeral(num_r / g, true);
|
||||
break;
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < args2.size(); ++i) {
|
||||
if (args2[i] == den_e) {
|
||||
args2[i] = m_util.mk_numeral(den_r / g, true);
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
num = m_util.mk_mul(args1.size(), args1.c_ptr());
|
||||
den = m_util.mk_mul(args2.size(), args2.c_ptr());
|
||||
result = m_util.mk_idiv(num, den);
|
||||
return true;
|
||||
}
|
||||
if (m_util.is_mul(n)) {
|
||||
expr_ref_vector muls(m());
|
||||
muls.push_back(n);
|
||||
expr* n1, *n2;
|
||||
rational r1, r2;
|
||||
for (unsigned i = 0; i < muls.size(); ++i) {
|
||||
if (m_util.is_mul(muls[i].get(), n1, n2)) {
|
||||
muls[i] = n1;
|
||||
muls.push_back(n2);
|
||||
--i;
|
||||
}
|
||||
}
|
||||
if (m_util.is_numeral(d, r1) && !r1.is_zero()) {
|
||||
for (unsigned i = 0; i < muls.size(); ++i) {
|
||||
if (m_util.is_numeral(muls[i].get(), r2) && (r2 / r1).is_int()) {
|
||||
muls[i] = m_util.mk_numeral(r2 / r1, m_util.is_int(d));
|
||||
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < muls.size(); ++i) {
|
||||
if (d == muls[i].get()) {
|
||||
muls[i] = muls.back();
|
||||
muls.pop_back();
|
||||
quot = m_util.mk_mul(muls.size(), muls.c_ptr());
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) {
|
||||
ptr_buffer<expr> args1, args2;
|
||||
flat_mul(num, args1);
|
||||
flat_mul(den, args2);
|
||||
remove_divisor(arg, args1);
|
||||
remove_divisor(arg, args2);
|
||||
expr_ref zero(m_util.mk_int(0), m());
|
||||
num = args1.empty() ? m_util.mk_int(1) : m_util.mk_mul(args1.size(), args1.c_ptr());
|
||||
den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.c_ptr());
|
||||
return expr_ref(m().mk_ite(m().mk_eq(zero, arg), m_util.mk_idiv(zero, zero), m_util.mk_idiv(num, den)), m());
|
||||
}
|
||||
|
||||
void arith_rewriter::flat_mul(expr* e, ptr_buffer<expr>& args) {
|
||||
args.push_back(e);
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
e = args[i];
|
||||
if (m_util.is_mul(e)) {
|
||||
args.append(to_app(e)->get_num_args(), to_app(e)->get_args());
|
||||
args[i] = args.back();
|
||||
args.shrink(args.size()-1);
|
||||
--i;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void arith_rewriter::remove_divisor(expr* d, ptr_buffer<expr>& args) {
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
if (args[i] == d) {
|
||||
args[i] = args.back();
|
||||
args.shrink(args.size()-1);
|
||||
return;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
||||
br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {
|
||||
|
|
|
@ -95,7 +95,10 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
|
|||
expr_ref neg_monomial(expr * e) const;
|
||||
expr * mk_sin_value(rational const & k);
|
||||
app * mk_sqrt(rational const & k);
|
||||
bool divides(expr* d, expr* n, expr_ref& quot);
|
||||
bool divides(expr* d, expr* n, expr_ref& result);
|
||||
expr_ref remove_divisor(expr* arg, expr* num, expr* den);
|
||||
void flat_mul(expr* e, ptr_buffer<expr>& args);
|
||||
void remove_divisor(expr* d, ptr_buffer<expr>& args);
|
||||
|
||||
public:
|
||||
arith_rewriter(ast_manager & m, params_ref const & p = params_ref()):
|
||||
|
|
|
@ -865,9 +865,7 @@ namespace smt {
|
|||
That is, during execution time, the variables will be already bound
|
||||
*/
|
||||
bool all_args_are_bound_vars(app * n) {
|
||||
unsigned num_args = n->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
expr * arg = n->get_arg(i);
|
||||
for (expr* arg : *n) {
|
||||
if (!is_var(arg))
|
||||
return false;
|
||||
if (m_vars[to_var(arg)->get_idx()] == -1)
|
||||
|
@ -884,9 +882,7 @@ namespace smt {
|
|||
if (n->is_ground()) {
|
||||
return;
|
||||
}
|
||||
unsigned num_args = n->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
expr * arg = n->get_arg(i);
|
||||
for (expr* arg : *n) {
|
||||
if (is_var(arg)) {
|
||||
sz++;
|
||||
unsigned var_id = to_var(arg)->get_idx();
|
||||
|
@ -928,10 +924,7 @@ namespace smt {
|
|||
unsigned first_app_sz;
|
||||
unsigned first_app_num_unbound_vars;
|
||||
// generate first the non-BIND operations
|
||||
unsigned_vector::iterator it = m_todo.begin();
|
||||
unsigned_vector::iterator end = m_todo.end();
|
||||
for (; it != end; ++it) {
|
||||
unsigned reg = *it;
|
||||
for (unsigned reg : m_todo) {
|
||||
expr * p = m_registers[reg];
|
||||
SASSERT(!is_quantifier(p));
|
||||
if (is_var(p)) {
|
||||
|
@ -1249,10 +1242,7 @@ namespace smt {
|
|||
SASSERT(head->m_next == 0);
|
||||
m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin())));
|
||||
|
||||
ptr_vector<instruction>::iterator it = m_seq.begin();
|
||||
ptr_vector<instruction>::iterator end = m_seq.end();
|
||||
for (; it != end; ++it) {
|
||||
instruction * curr = *it;
|
||||
for (instruction * curr : m_seq) {
|
||||
head->m_next = curr;
|
||||
head = curr;
|
||||
}
|
||||
|
@ -1495,10 +1485,8 @@ namespace smt {
|
|||
}
|
||||
if (num_instr > SIMPLE_SEQ_THRESHOLD || (curr != nullptr && curr->m_opcode == CHOOSE))
|
||||
simple = false;
|
||||
unsigned_vector::iterator it = m_to_reset.begin();
|
||||
unsigned_vector::iterator end = m_to_reset.end();
|
||||
for (; it != end; ++it)
|
||||
m_registers[*it] = 0;
|
||||
for (unsigned reg : m_to_reset)
|
||||
m_registers[reg] = 0;
|
||||
return weight;
|
||||
}
|
||||
|
||||
|
@ -1716,11 +1704,9 @@ namespace smt {
|
|||
m_num_choices++;
|
||||
// set: head -> c1 -> c2 -> c3 -> new_child_head1
|
||||
curr = head;
|
||||
ptr_vector<instruction>::iterator it1 = m_compatible.begin();
|
||||
ptr_vector<instruction>::iterator end1 = m_compatible.end();
|
||||
for (; it1 != end1; ++it1) {
|
||||
set_next(curr, *it1);
|
||||
curr = *it1;
|
||||
for (instruction* instr : m_compatible) {
|
||||
set_next(curr, instr);
|
||||
curr = instr;
|
||||
}
|
||||
set_next(curr, new_child_head1);
|
||||
// set: new_child_head1:CHOOSE(new_child_head2) -> i1 -> i2 -> first_child_head
|
||||
|
|
|
@ -508,13 +508,14 @@ namespace smt {
|
|||
mk_axiom(eqz, lower, !is_numeral);
|
||||
mk_axiom(eqz, upper, !is_numeral);
|
||||
rational k;
|
||||
context& ctx = get_context();
|
||||
(void)ctx;
|
||||
if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&
|
||||
k.is_pos() && k < rational(8)) {
|
||||
rational j(0);
|
||||
#if 1
|
||||
literal_buffer lits;
|
||||
expr_ref mod_j(m);
|
||||
context& ctx = get_context();
|
||||
while(j < k) {
|
||||
mod_j = m.mk_eq(mod, m_util.mk_numeral(j, true));
|
||||
ctx.internalize(mod_j, false);
|
||||
|
@ -542,6 +543,31 @@ namespace smt {
|
|||
}
|
||||
#endif
|
||||
}
|
||||
if (!m_util.is_numeral(divisor)) {
|
||||
//
|
||||
// forall x . (or (= y 0) (= (div (* x y) y) x))
|
||||
// forall x . (=> (= y 0) (= (div (* x y) y) (div 0 0)))
|
||||
//
|
||||
sort* intS = m_util.mk_int();
|
||||
var_ref v(m.mk_var(0, intS), m);
|
||||
app_ref mul(m_util.mk_mul(divisor, v), m);
|
||||
app_ref div(m_util.mk_idiv(mul, divisor), m);
|
||||
expr_ref divp1(m.mk_pattern(div), m);
|
||||
app_ref mul2(m_util.mk_mul(v, divisor), m);
|
||||
app_ref div2(m_util.mk_idiv(mul2, divisor), m);
|
||||
expr_ref divp2(m.mk_pattern(div2), m);
|
||||
expr_ref fml1(m.mk_or(m.mk_not(eqz), m.mk_eq(div, m_util.mk_idiv(zero, zero))), m);
|
||||
expr_ref fml2(m.mk_or(eqz, m.mk_eq(div, v)), m);
|
||||
symbol name("?x");
|
||||
expr* pats[2] = { divp1, divp2 };
|
||||
expr_ref fml(m);
|
||||
fml = m.mk_forall(1, &intS, &name, fml1, 0, symbol::null, symbol::null, 2, pats, 0, nullptr);
|
||||
proof_ref pr(m.mk_asserted(fml), m);
|
||||
ctx.internalize_assertion(fml, pr, 0);
|
||||
fml = m.mk_forall(1, &intS, &name, fml2, 0, symbol::null, symbol::null, 2, pats, 0, nullptr);
|
||||
pr = m.mk_asserted(fml);
|
||||
ctx.internalize_assertion(fml, pr, 0);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue