From 795e0c641a6a44362b47707c5885f921a07265e1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Nov 2017 14:44:59 -0800 Subject: [PATCH] add method to create bit-vectors directly from an array of Booleans Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 2 +- src/api/api_numeral.cpp | 14 ++++++++++++++ src/api/c++/z3++.h | 6 ++++++ src/api/dotnet/Context.cs | 14 ++++++++++++++ src/api/z3_api.h | 8 ++++++++ src/ast/ast.cpp | 14 +------------- src/ast/rewriter/poly_rewriter_def.h | 2 +- 7 files changed, 45 insertions(+), 15 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 2828a63f8..2096e00ba 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -957,7 +957,7 @@ def def_API(name, result, params): log_c.write(" }\n") log_c.write(" Au(a%s);\n" % sz) exe_c.write("in.get_uint_array(%s)" % i) - elif ty == INT: + elif ty == INT or ty == BOOL: log_c.write("U(a%s[i]);" % i) log_c.write(" }\n") log_c.write(" Au(a%s);\n" % sz) diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 95bc0bef9..effa5f411 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -387,4 +387,18 @@ extern "C" { Z3_CATCH_RETURN(Z3_FALSE); } + Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const* bits) { + Z3_TRY; + LOG_Z3_mk_bv_numeral(c, sz, bits); + RESET_ERROR_CODE(); + rational r(0), two(2), one(1); + for (unsigned i = 0; i < sz; ++i) { + r *= two; + if (bits[i]) r += one; + } + ast * a = mk_c(c)->mk_numeral_core(r, mk_c(c)->bvutil().mk_sort(sz)); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(0); + } + }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 23a7bd22e..df385db78 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -301,6 +301,7 @@ namespace z3 { expr bv_val(__int64 n, unsigned sz); expr bv_val(__uint64 n, unsigned sz); expr bv_val(char const * n, unsigned sz); + expr bv_val(unsigned n, bool const* bits); expr string_val(char const* s); expr string_val(std::string const& s); @@ -2455,6 +2456,11 @@ namespace z3 { inline expr context::bv_val(__int64 n, unsigned sz) { Z3_ast r = Z3_mk_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); } inline expr context::bv_val(__uint64 n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); } inline expr context::bv_val(char const * n, unsigned sz) { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); } + inline expr context::bv_val(unsigned n, bool const* bits) { + array _bits(n); + for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0; + Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r); + } inline expr context::string_val(char const* s) { Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); } inline expr context::string_val(std::string const& s) { Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 27711be81..914cee615 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3127,6 +3127,20 @@ namespace Microsoft.Z3 return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); } + + /// + /// Create a bit-vector numeral. + /// + /// An array of bits representing the bit-vector. Least signficant bit is at position 0. + public BitVecNum MkBV(bool[] bits) + { + Contract.Ensures(Contract.Result() != null); + int[] _bits = new int[bits.Length]; + for (int i = 0; i < bits.Length; ++i) _bits[i] = bits[i] ? 1 : 0; + return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits)); + } + + #endregion #endregion // Numerals diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9f155b45e..cf1c8fca7 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3248,6 +3248,14 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, __uint64 v, Z3_sort ty); + /** + \brief create a bit-vector numeral from a vector of Booleans. + + \sa Z3_mk_numeral + def_API('Z3_mk_bv_numeral', AST, (_in(CONTEXT), _in(UINT), _in_array(1, BOOL))) + */ + Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, Z3_bool const* bits); + /*@}*/ /** @name Sequences and regular expressions */ diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 98c1bdfed..d0921c8de 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -26,6 +26,7 @@ Revision History: #include "util/string_buffer.h" #include "ast/ast_util.h" #include "ast/ast_smt2_pp.h" +#include "ast/bv_decl_plugin.h" // ----------------------------------- // @@ -1684,22 +1685,9 @@ ast * ast_manager::register_node_core(ast * n) { CASSERT("nondet_bug", contains || slow_not_contains(n)); #endif -#if 0 - static unsigned counter = 0; - counter++; - if (counter % 100000 == 0) - verbose_stream() << "[ast-table] counter: " << counter << " collisions: " << m_ast_table.collisions() << " capacity: " << m_ast_table.capacity() << " size: " << m_ast_table.size() << "\n"; -#endif - ast * r = m_ast_table.insert_if_not_there(n); SASSERT(r->m_hash == h); if (r != n) { -#if 0 - static unsigned reused = 0; - reused++; - if (reused % 100000 == 0) - verbose_stream() << "[ast-table] reused: " << reused << "\n"; -#endif SASSERT(contains); SASSERT(m_ast_table.contains(n)); if (is_func_decl(r) && to_func_decl(r)->get_range() != to_func_decl(n)->get_range()) { diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index 3bb963a7f..71a9079a0 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -687,7 +687,7 @@ br_status poly_rewriter::mk_sub(unsigned num_args, expr * const * args, } set_curr_sort(m().get_sort(args[0])); expr_ref minus_one(mk_numeral(numeral(-1)), m()); - ptr_buffer new_args; + expr_ref_buffer new_args(m()); new_args.push_back(args[0]); for (unsigned i = 1; i < num_args; i++) { if (is_zero(args[i])) continue;