mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

reuse m_bv_sym based on stack in #2842

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-01-06 16:03:45 -08:00
parent 55f59364a3
commit 2999d33ede
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/bv_decl_plugin.cpp
View file

@ -151,7 +151,7 @@ void bv_decl_plugin::mk_bv_sort(unsigned bv_size) {
else { else {
sz = sort_size(rational::power_of_two(bv_size)); sz = sort_size(rational::power_of_two(bv_size));
} }
m_bv_sorts[bv_size] = m_manager->mk_sort(symbol("bv"), sort_info(m_family_id, BV_SORT, sz, 1, &p)); m_bv_sorts[bv_size] = m_manager->mk_sort(m_bv_sym, sort_info(m_family_id, BV_SORT, sz, 1, &p));
m_manager->inc_ref(m_bv_sorts[bv_size]); m_manager->inc_ref(m_bv_sorts[bv_size]);
} }
} }
@ -163,7 +163,7 @@ inline sort * bv_decl_plugin::get_bv_sort(unsigned bv_size) {
} }
parameter p(bv_size); parameter p(bv_size);
sort_size sz(sort_size::mk_very_big()); sort_size sz(sort_size::mk_very_big());
return m_manager->mk_sort(symbol("bv"), sort_info(m_family_id, BV_SORT, sz, 1, &p)); return m_manager->mk_sort(m_bv_sym, sort_info(m_family_id, BV_SORT, sz, 1, &p));
} }
sort * bv_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { sort * bv_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
@ -853,11 +853,11 @@ bool bv_recognizers::mult_inverse(rational const & n, unsigned bv_size, rational
} }
bv_util::bv_util(ast_manager & m): bv_util::bv_util(ast_manager & m):
bv_recognizers(m.mk_family_id(symbol("bv"))), bv_recognizers(m.mk_family_id(m_plugin->m_bv_sym)),
m_manager(m) { m_manager(m) {
SASSERT(m.has_plugin(symbol("bv"))); SASSERT(m.has_plugin(m_plugin->m_bv_sym));
m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.mk_family_id("bv"))); m_plugin = static_cast<bv_decl_plugin*>(m.get_plugin(m.mk_family_id("bv")));
} }
app * bv_util::mk_numeral(rational const & val, sort* s) const { app * bv_util::mk_numeral(rational const & val, sort* s) const {
if (!is_bv_sort(s)) { if (!is_bv_sort(s)) {