From 1244d5a22ef196ce730ebf9fd94970419cbdcb8d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 16 Dec 2014 15:28:52 +0000 Subject: [PATCH 1/3] Python API: Added BVRedAnd, BVRedOr Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index db629cd2d..713226e23 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -3813,6 +3813,18 @@ def RepeatBitVec(n, a): _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx) +def BVRedAnd(a): + """Return the reduction-and expression of `a`.""" + if __debug__: + _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") + return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx) + +def BVRedOr(a): + """Return the reduction-and expression of `a`.""" + if __debug__: + _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") + return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) + ######################################### # # Arrays From d53fdb284858f331b3d577067926a626d23e8571 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 16 Dec 2014 15:36:31 +0000 Subject: [PATCH 2/3] typo Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 713226e23..720335d41 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -3820,7 +3820,7 @@ def BVRedAnd(a): return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx) def BVRedOr(a): - """Return the reduction-and expression of `a`.""" + """Return the reduction-or expression of `a`.""" if __debug__: _z3_assert(is_bv(a), "First argument must be a Z3 Bitvector expression") return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx) From f4d256ef306dfb22aef306e73d1d7a90668aae5b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Dec 2014 11:20:34 -0800 Subject: [PATCH 3/3] fix issue 153: assert rem/mod axiom no matter what is status of second argument Signed-off-by: Nikolaj Bjorner --- README | 2 ++ src/smt/smt_context.cpp | 7 +++---- src/smt/theory_arith_core.h | 33 ++++++++++++++++----------------- 3 files changed, 21 insertions(+), 21 deletions(-) diff --git a/README b/README index 1ca0cd577..074abd2a3 100644 --- a/README +++ b/README @@ -41,3 +41,5 @@ Remark: clang does not support OpenMP yet. cd build make + +To clean Z3 you can delete the build directory and run the mk_make.py script again. \ No newline at end of file diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f3f2d4948..957d5ebe7 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3321,13 +3321,13 @@ namespace smt { CASSERT("dyn_ack", check_clauses(m_lemmas) && check_clauses(m_aux_clauses)); } - if (resource_limits_exceeded()) { - SASSERT(!inconsistent()); + if (resource_limits_exceeded() && !inconsistent()) { return l_undef; } if (m_base_lvl == m_scope_lvl && m_fparams.m_simplify_clauses) simplify_clauses(); + if (!decide()) { final_check_status fcs = final_check(); @@ -3342,8 +3342,7 @@ namespace smt { } } - if (resource_limits_exceeded()) { - SASSERT(!inconsistent()); + if (resource_limits_exceeded() && !inconsistent()) { return l_undef; } } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 66d232227..a7f442e1f 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -336,8 +336,9 @@ namespace smt { theory_var theory_arith::internalize_rem(app * n) { theory_var s = mk_binary_op(n); context & ctx = get_context(); - if (!ctx.relevancy()) + if (!ctx.relevancy()) { mk_rem_axiom(n->get_arg(0), n->get_arg(1)); + } return s; } @@ -456,22 +457,20 @@ namespace smt { template void theory_arith::mk_rem_axiom(expr * dividend, expr * divisor) { - if (!m_util.is_zero(divisor)) { - // if divisor is zero, then rem is an uninterpreted function. - ast_manager & m = get_manager(); - expr * zero = m_util.mk_numeral(rational(0), true); - expr * rem = m_util.mk_rem(dividend, divisor); - expr * mod = m_util.mk_mod(dividend, divisor); - expr_ref dltz(m), eq1(m), eq2(m); - dltz = m_util.mk_lt(divisor, zero); - eq1 = m.mk_eq(rem, mod); - eq2 = m.mk_eq(rem, m_util.mk_sub(zero, mod)); - // n < 0 || rem(a,n) = mod(a, n) - mk_axiom(dltz, eq1); - dltz = m.mk_not(dltz); - // !n < 0 || rem(a,n) = -mod(a, n) - mk_axiom(dltz, eq2); - } + // if divisor is zero, then rem is an uninterpreted function. + ast_manager & m = get_manager(); + expr * zero = m_util.mk_numeral(rational(0), true); + expr * rem = m_util.mk_rem(dividend, divisor); + expr * mod = m_util.mk_mod(dividend, divisor); + expr_ref dltz(m), eq1(m), eq2(m); + dltz = m_util.mk_lt(divisor, zero); + eq1 = m.mk_eq(rem, mod); + eq2 = m.mk_eq(rem, m_util.mk_sub(zero, mod)); + // n < 0 || rem(a,n) = mod(a, n) + mk_axiom(dltz, eq1); + dltz = m.mk_not(dltz); + // !n < 0 || rem(a,n) = -mod(a, n) + mk_axiom(dltz, eq2); } //