mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

add stubs to control memory usage

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-02 17:52:54 -07:00
parent 4b495e4b96
commit 34272152bb
2 changed files with 11 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/tactic/arith/bv2real_rewriter.cpp
View file

@ -17,6 +17,7 @@ Notes:
--*/
#include "tactic/arith/bv2real_rewriter.h"
#include "tactic/tactic_exception.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/ast_pp.h"
#include "ast/for_each_expr.h"
@ -40,6 +41,7 @@ bv2real_util::bv2real_util(ast_manager& m, rational const& default_root, rationa
m_pos_le = m.mk_fresh_func_decl("<=","",2,domain,m.mk_bool_sort());
m_decls.push_back(m_pos_lt);
m_decls.push_back(m_pos_le);
m_max_memory = std::max((1ull << 31ull), 3*memory::get_allocation_size());
}
bool bv2real_util::is_bv2real(func_decl* f) const {
@ -178,12 +180,10 @@ void bv2real_util::align_divisors(expr_ref& s1, expr_ref& s2, expr_ref& t1, expr
expr* bv2real_util::mk_bv_mul(expr* s, expr* t) {
SASSERT(m_bv.is_bv(s));
SASSERT(m_bv.is_bv(t));
if (is_zero(s)) {
if (is_zero(s))
return s;
}
if (is_zero(t)) {
if (is_zero(t))
return t;
}
expr_ref s1(s, m()), t1(t, m());
align_sizes(s1, t1);
unsigned n = m_bv.get_bv_size(t1);
@ -343,6 +343,10 @@ bool bv2real_util::mk_is_divisible_by(expr_ref& s, rational const& _overflow) {
}
bool bv2real_util::memory_exceeded() const {
return m_max_memory <= memory::get_allocation_size();
}
// ---------------------------------------------------------------------
// bv2real_rewriter

3
src/tactic/arith/bv2real_rewriter.h
View file

@ -65,6 +65,7 @@ class bv2real_util {
rational m_default_divisor;
rational m_max_divisor;
unsigned m_max_num_bits;
uint64_t m_max_memory;
class contains_bv2real_proc;
@ -81,6 +82,8 @@ public:
bool contains_bv2real(expr* e) const;
bool memory_exceeded() const;
bool mk_bv2real(expr* s, expr* t, rational& d, rational& r, expr_ref& result);
expr* mk_bv2real_c(expr* s, expr* t, rational const& d, rational const& r);
expr* mk_bv2real(expr* n, expr* m) { return mk_bv2real_c(n, m, default_divisor(), default_root()); }