From 2efcd5b78901a0635c4f0dc977a8ef06817913c0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Nov 2017 08:55:40 -0800 Subject: [PATCH 1/4] additional bit-vector operators over C++ API Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index df385db78..3d39cdb74 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -965,6 +965,13 @@ namespace z3 { friend expr operator|(expr const & a, expr const & b); friend expr operator|(expr const & a, int b); friend expr operator|(int a, expr const & b); + friend expr nand(expr const& a, expr const& b); + friend expr nor(expr const& a, expr const& b); + friend expr xnor(expr const& a, expr const& b); + + expr rotate_left(unsigned i) { Z3_ast r = Z3_mk_rotate_left(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); } + expr rotate_right(unsigned i) { Z3_ast r = Z3_mk_rotate_right(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); } + expr repeat(unsigned i) { Z3_ast r = Z3_mk_repeat(ctx(), i, *this); ctx().check_error(); return expr(ctx(), r); } friend expr operator~(expr const & a); expr extract(unsigned hi, unsigned lo) const { Z3_ast r = Z3_mk_extract(ctx(), hi, lo, *this); ctx().check_error(); return expr(ctx(), r); } @@ -1333,6 +1340,10 @@ namespace z3 { inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); } inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; } + inline expr nand(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); } + inline expr nor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); } + inline expr xnor(expr const& a, expr const& b) { check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); } + inline expr operator~(expr const & a) { Z3_ast r = Z3_mk_bvnot(a.ctx(), a); return expr(a.ctx(), r); } From a68d5131c7b91b841289f25044511f76f8232eaa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Nov 2017 09:00:14 -0800 Subject: [PATCH 2/4] add bvsmod Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 3d39cdb74..4b5e9d04e 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1418,11 +1418,18 @@ namespace z3 { inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); } /** - \brief signed reminder operator for bitvectors + \brief signed remainder operator for bitvectors */ inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); } inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); } inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); } + + /** + \brief signed modulus operator for bitvectors + */ + inline expr smod(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsmod(a.ctx(), a, b)); } + inline expr smod(expr const & a, int b) { return smod(a, a.ctx().num_val(b, a.get_sort())); } + inline expr smod(int a, expr const & b) { return smod(b.ctx().num_val(a, b.get_sort()), b); } /** \brief unsigned reminder operator for bitvectors From 62cf6aace75f9dd74d17f4fb2d0d980b447a2207 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 16 Nov 2017 10:20:21 -0800 Subject: [PATCH 3/4] avoid a warning Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 6d2cbea7d..1f1054bb6 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -1157,7 +1157,7 @@ public: bool explanation_is_correct(const vector>& explanation) const { #ifdef Z3DEBUG - lconstraint_kind kind; + lconstraint_kind kind = EQ; // initialize it just to avoid a warning SASSERT(the_relations_are_of_same_type(explanation, kind)); SASSERT(the_left_sides_sum_to_zero(explanation)); mpq rs = sum_of_right_sides_of_explanation(explanation); From f5ff9fae3477850d849d217193857f37c2ee5e0d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 17 Nov 2017 21:15:30 +0000 Subject: [PATCH 4/4] Fixed bug check in bv2fpa converter. Fixes #1291. --- src/ast/fpa/bv2fpa_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 2f5a7c3c1..d87929864 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -297,7 +297,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * // The BV model may have multiple equivalent entries using different // representations of NaN. We can only keep one and we check that // the results for all those entries are the same. - if (ft_fres != fe->get_result()) + if (m_fpa_util.is_float(rng) && ft_fres != fe->get_result()) throw default_exception("BUG: UF function entries disagree with each other"); } }