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

add useful div lemma for case #2079

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-10 17:20:01 -08:00
parent 6e60926cc3
commit 434eb25004
2 changed files with 14 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/smt/theory_arith_core.h
View file

@ -482,12 +482,12 @@ namespace smt {
template<typename Ext> template<typename Ext>
void theory_arith<Ext>::mk_idiv_mod_axioms(expr * dividend, expr * divisor) { void theory_arith<Ext>::mk_idiv_mod_axioms(expr * dividend, expr * divisor) {
th_rewriter & s = get_context().get_rewriter();
if (!m_util.is_zero(divisor)) { if (!m_util.is_zero(divisor)) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
// if divisor is zero, then idiv and mod are uninterpreted functions. // if divisor is zero, then idiv and mod are uninterpreted functions.
expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m); expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m);
expr_ref eqz(m), eq(m), lower(m), upper(m); expr_ref eqz(m), eq(m), lower(m), upper(m);
th_rewriter & s = get_context().get_rewriter();
div = m_util.mk_idiv(dividend, divisor); div = m_util.mk_idiv(dividend, divisor);
mod = m_util.mk_mod(dividend, divisor); mod = m_util.mk_mod(dividend, divisor);
zero = m_util.mk_int(0); zero = m_util.mk_int(0);
@ -508,6 +508,17 @@ namespace smt {
mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor)); mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
rational k; rational k;
context& ctx = get_context(); context& ctx = get_context();
if (!m_util.is_numeral(divisor)) {
// (=> (> y 0) (<= (* y (div x y)) x))
// (=> (< y 0) ???)
expr_ref div_ge(m), div_non_pos(m);
div_ge = m_util.mk_ge(m_util.mk_sub(dividend, m_util.mk_mul(divisor, div)), zero);
s(div_ge);
div_non_pos = m_util.mk_le(divisor, zero);
mk_axiom(div_non_pos, div_ge, false);
}
(void)ctx; (void)ctx;
if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) && if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&
k.is_pos() && k < rational(8)) { k.is_pos() && k < rational(8)) {
@ -542,6 +553,7 @@ namespace smt {
} }
#endif #endif
} }
#if 0 #if 0
// e-matching is too restrictive for multiplication. // e-matching is too restrictive for multiplication.
// also suffers from use-after free so formulas have to be pinned in solver. // also suffers from use-after free so formulas have to be pinned in solver.

2
src/smt/theory_seq.cpp
View file

@ -251,7 +251,7 @@ void theory_seq::init(context* ctx) {
m_arith_value.init(ctx); m_arith_value.init(ctx);
} }
#define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(10, verbose_stream() << s << "\n"); } #define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(11, verbose_stream() << s << "\n"); }
final_check_status theory_seq::final_check_eh() { final_check_status theory_seq::final_check_eh() {