From 34272152bb11c2bdffe6e4d76bbfcf0985499161 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 2 Apr 2022 17:52:54 -0700
Subject: [PATCH] add stubs to control memory usage

---
 src/tactic/arith/bv2real_rewriter.cpp | 12 ++++++++----
 src/tactic/arith/bv2real_rewriter.h   |  3 +++
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/tactic/arith/bv2real_rewriter.cpp b/src/tactic/arith/bv2real_rewriter.cpp
index d7bca705e07..03acc8161a0 100644
--- a/src/tactic/arith/bv2real_rewriter.cpp
+++ b/src/tactic/arith/bv2real_rewriter.cpp
@@ -17,6 +17,7 @@ Module Name:
 
 --*/
 #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
diff --git a/src/tactic/arith/bv2real_rewriter.h b/src/tactic/arith/bv2real_rewriter.h
index 7b3915105f6..4c3c63c2ada 100644
--- a/src/tactic/arith/bv2real_rewriter.h
+++ b/src/tactic/arith/bv2real_rewriter.h
@@ -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 @@ class bv2real_util {
 
     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()); }