From 9b3e242990aa47a72713800bdaea5ea9459d5644 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 28 Sep 2015 13:37:59 -0700
Subject: [PATCH] adding rlimit resource limit facility to provide platform and
architecture independent method for canceling activities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/api_context.h | 1 +
src/api/api_datalog.cpp | 2 +
src/api/api_solver.cpp | 3 ++
src/ast/ast.h | 4 ++
src/ast/rewriter/rewriter_def.h | 2 +
src/cmd_context/cmd_context.cpp | 4 ++
src/cmd_context/context_params.cpp | 7 ++++
src/cmd_context/context_params.h | 1 +
src/cmd_context/tactic_cmds.cpp | 1 +
src/muz/base/dl_context.cpp | 1 +
src/opt/opt_context.cpp | 1 +
src/sat/sat_bceq.cpp | 2 +-
src/sat/sat_solver.cpp | 3 +-
src/sat/sat_solver.h | 6 ++-
src/sat/sat_solver/inc_sat_solver.cpp | 2 +-
src/sat/tactic/sat_tactic.cpp | 2 +-
src/shell/dimacs_frontend.cpp | 6 ++-
src/smt/params/smt_params.cpp | 1 +
src/smt/params/smt_params.h | 2 +
src/smt/params/smt_params_helper.pyg | 1 +
src/smt/smt_context.cpp | 17 ++++++---
src/smt/smt_context.h | 2 +-
src/util/rlimit.cpp | 55 +++++++++++++++++++++++++++
src/util/rlimit.h | 47 +++++++++++++++++++++++
src/util/statistics.cpp | 4 ++
src/util/statistics.h | 2 +
26 files changed, 165 insertions(+), 14 deletions(-)
create mode 100644 src/util/rlimit.cpp
create mode 100644 src/util/rlimit.h
diff --git a/src/api/api_context.h b/src/api/api_context.h
index 882974005..3d5f0c2bf 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -117,6 +117,7 @@ namespace api {
bool produce_unsat_cores() const { return m_params.m_unsat_core; }
bool use_auto_config() const { return m_params.m_auto_config; }
unsigned get_timeout() const { return m_params.m_timeout; }
+ unsigned get_rlimit() const { return m_params.m_rlimit; }
arith_util & autil() { return m_arith_util; }
bv_util & bvutil() { return m_bv_util; }
datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index 9ed82191b..c3fdeb94b 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -287,9 +287,11 @@ extern "C" {
lbool r = l_undef;
cancel_eh<api::fixedpoint_context> eh(*to_fixedpoint_ref(d));
unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
+ unsigned rlimit = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_timer timer(timeout, &eh);
+ scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
r = to_fixedpoint_ref(d)->ctx().query(to_expr(q));
}
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 50b0c6e22..4daf3956f 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -254,6 +254,7 @@ extern "C" {
}
expr * const * _assumptions = to_exprs(assumptions);
unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
+ unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false);
cancel_eh<solver> eh(*to_solver_ref(s));
api::context::set_interruptable si(*(mk_c(c)), eh);
@@ -261,6 +262,7 @@ extern "C" {
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_timer timer(timeout, &eh);
+ scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
result = to_solver_ref(s)->check_sat(num_assumptions, _assumptions);
}
@@ -356,6 +358,7 @@ extern "C" {
Z3_stats_ref * st = alloc(Z3_stats_ref);
to_solver_ref(s)->collect_statistics(st->m_stats);
get_memory_statistics(st->m_stats);
+ get_rlimit_statistics(mk_c(c)->m().limit(), st->m_stats);
mk_c(c)->save_object(st);
Z3_stats r = of_stats(st);
RETURN_Z3(r);
diff --git a/src/ast/ast.h b/src/ast/ast.h
index c1ee603c7..deddd3cad 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -44,6 +44,7 @@ Revision History:
#include"chashtable.h"
#include"z3_exception.h"
#include"dependency.h"
+#include"rlimit.h"
#define RECYCLE_FREE_AST_INDICES
@@ -1424,6 +1425,7 @@ public:
void show_id_gen();
protected:
+ reslimit m_limit;
small_object_allocator m_alloc;
family_manager m_family_manager;
expr_array_manager m_expr_array_manager;
@@ -1519,6 +1521,8 @@ public:
fid == m_user_sort_family_id;
}
+ reslimit& limit() { return m_limit; }
+
void register_plugin(symbol const & s, decl_plugin * plugin);
void register_plugin(family_id id, decl_plugin * plugin);
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index be3bfbd0a..505197f33 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -578,6 +578,8 @@ void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr)
while (!frame_stack().empty()) {
if (m_cancel)
throw rewriter_exception(Z3_CANCELED_MSG);
+ if (!m().limit().inc())
+ throw rewriter_exception(Z3_CANCELED_MSG);
SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
frame & fr = frame_stack().back();
expr * t = fr.m_curr;
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 8fda13289..8648775ee 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1390,6 +1390,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
TRACE("before_check_sat", dump_assertions(tout););
init_manager();
unsigned timeout = m_params.m_timeout;
+ unsigned rlimit = m_params.m_rlimit;
scoped_watch sw(*this);
lbool r;
@@ -1399,6 +1400,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
cancel_eh<opt_wrapper> eh(*get_opt());
scoped_ctrl_c ctrlc(eh);
scoped_timer timer(timeout, &eh);
+ scoped_rlimit _rlimit(m().limit(), rlimit);
ptr_vector<expr> cnstr(m_assertions);
cnstr.append(num_assumptions, assumptions);
get_opt()->set_hard_constraints(cnstr);
@@ -1436,6 +1438,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
cancel_eh<solver> eh(*m_solver);
scoped_ctrl_c ctrlc(eh);
scoped_timer timer(timeout, &eh);
+ scoped_rlimit _rlimit(m().limit(), rlimit);
try {
r = m_solver->check_sat(num_assumptions, assumptions);
}
@@ -1646,6 +1649,7 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) {
st.update("total time", total_time);
st.update("time", get_seconds());
get_memory_statistics(st);
+ get_rlimit_statistics(m().limit(), st);
if (m_check_sat_result) {
m_check_sat_result->collect_statistics(st);
}
diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp
index 5a9b1a4f3..add1b5b3d 100644
--- a/src/cmd_context/context_params.cpp
+++ b/src/cmd_context/context_params.cpp
@@ -35,6 +35,7 @@ context_params::context_params() {
m_smtlib2_compliant = false;
m_well_sorted_check = false;
m_timeout = UINT_MAX;
+ m_rlimit = UINT_MAX;
updt_params();
}
@@ -65,6 +66,10 @@ void context_params::set(char const * param, char const * value) {
long val = strtol(value, 0, 10);
m_timeout = static_cast<unsigned>(val);
}
+ if (p == "rlimit") {
+ long val = strtol(value, 0, 10);
+ m_rlimit = static_cast<unsigned>(val);
+ }
else if (p == "type_check" || p == "well_sorted_check") {
set_bool(m_well_sorted_check, param, value);
}
@@ -115,6 +120,7 @@ void context_params::updt_params() {
void context_params::updt_params(params_ref const & p) {
m_timeout = p.get_uint("timeout", m_timeout);
+ m_rlimit = p.get_uint("rlimit", m_rlimit);
m_well_sorted_check = p.get_bool("type_check", p.get_bool("well_sorted_check", m_well_sorted_check));
m_auto_config = p.get_bool("auto_config", m_auto_config);
m_proof = p.get_bool("proof", m_proof);
@@ -130,6 +136,7 @@ void context_params::updt_params(params_ref const & p) {
void context_params::collect_param_descrs(param_descrs & d) {
d.insert("timeout", CPK_UINT, "default timeout (in milliseconds) used for solvers", "4294967295");
+ d.insert("rlimit", CPK_UINT, "default resource limit used for solvers", "4294967295");
d.insert("well_sorted_check", CPK_BOOL, "type checker", "false");
d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h
index bdd77fb1c..2c75b5743 100644
--- a/src/cmd_context/context_params.h
+++ b/src/cmd_context/context_params.h
@@ -40,6 +40,7 @@ public:
bool m_unsat_core;
bool m_smtlib2_compliant; // it must be here because it enable/disable the use of coercions in the ast_manager.
unsigned m_timeout;
+ unsigned m_rlimit;
context_params();
void set(char const * param, char const * value);
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index 9d4c18262..ab2ad3922 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -158,6 +158,7 @@ public:
void display_statistics(cmd_context & ctx, tactic * t) {
statistics stats;
get_memory_statistics(stats);
+ get_rlimit_statistics(ctx.m().limit(), stats);
stats.update("time", ctx.get_seconds());
t->collect_statistics(stats);
stats.display_smt2(ctx.regular_stream());
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 60de96e1d..c2db15e3a 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -948,6 +948,7 @@ namespace datalog {
m_engine->collect_statistics(st);
}
get_memory_statistics(st);
+ get_rlimit_statistics(m.limit(), st);
}
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 0264ea70f..dda38e566 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1258,6 +1258,7 @@ namespace opt {
it->m_value->collect_statistics(stats);
}
get_memory_statistics(stats);
+ get_rlimit_statistics(m.limit(), stats);
}
void context::collect_param_descrs(param_descrs & r) {
diff --git a/src/sat/sat_bceq.cpp b/src/sat/sat_bceq.cpp
index 179749dac..a194cdfd8 100644
--- a/src/sat/sat_bceq.cpp
+++ b/src/sat/sat_bceq.cpp
@@ -497,7 +497,7 @@ namespace sat {
flet<unsigned> _bound_maxc(m_solver.m_config.m_max_conflicts, 1500);
use_list ul;
- solver s(m_solver.m_params, 0);
+ solver s(m_solver.m_params, m_solver.rlimit(), 0);
s.m_config.m_bcd = false;
s.m_config.m_minimize_core = false;
s.m_config.m_optimize_model = false;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 0ecda2808..008ba8a18 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -31,8 +31,9 @@ Revision History:
namespace sat {
- solver::solver(params_ref const & p, extension * ext):
+ solver::solver(params_ref const & p, reslimit& l, extension * ext):
m_cancel(false),
+ m_rlimit(l),
m_config(p),
m_ext(ext),
m_cleaner(*this),
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 97a27502d..23033d940 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -38,6 +38,7 @@ Revision History:
#include"statistics.h"
#include"stopwatch.h"
#include"trace.h"
+#include"rlimit.h"
namespace sat {
@@ -71,6 +72,7 @@ namespace sat {
struct abort_solver {};
protected:
volatile bool m_cancel;
+ reslimit& m_rlimit;
config m_config;
stats m_stats;
extension * m_ext;
@@ -145,7 +147,7 @@ namespace sat {
friend class bceq;
friend struct mk_stat;
public:
- solver(params_ref const & p, extension * ext);
+ solver(params_ref const & p, reslimit& l, extension * ext);
~solver();
// -----------------------
@@ -238,6 +240,7 @@ namespace sat {
clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
void checkpoint() {
if (m_cancel) throw solver_exception(Z3_CANCELED_MSG);
+ if (!m_rlimit.inc()) { m_cancel = true; throw solver_exception(Z3_CANCELED_MSG); }
++m_num_checkpoints;
if (m_num_checkpoints < 10) return;
m_num_checkpoints = 0;
@@ -415,6 +418,7 @@ namespace sat {
void user_push();
void user_pop(unsigned num_scopes);
void pop_to_base_level();
+ reslimit& rlimit() { return m_rlimit; }
// -----------------------
//
// Simplification
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index a64be2075..fd1f4cfd0 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -63,7 +63,7 @@ class inc_sat_solver : public solver {
typedef obj_map<expr, sat::literal> dep2asm_t;
public:
inc_sat_solver(ast_manager& m, params_ref const& p):
- m(m), m_solver(p,0),
+ m(m), m_solver(p, m.limit(), 0),
m_params(p), m_optimize_model(false),
m_fmls(m),
m_asmsf(m),
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index e4d5e6df5..f04100ca2 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -34,7 +34,7 @@ class sat_tactic : public tactic {
imp(ast_manager & _m, params_ref const & p):
m(_m),
- m_solver(p, 0),
+ m_solver(p, m.limit(), 0),
m_params(p) {
SASSERT(!m.proofs_enabled());
}
diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp
index abaa2eace..54e78ac8f 100644
--- a/src/shell/dimacs_frontend.cpp
+++ b/src/shell/dimacs_frontend.cpp
@@ -20,6 +20,7 @@ Revision History:
#include<time.h>
#include<signal.h>
#include"timeout.h"
+#include"rlimit.h"
#include"dimacs.h"
#include"sat_solver.h"
#include"gparams.h"
@@ -132,7 +133,8 @@ unsigned read_dimacs(char const * file_name) {
signal(SIGINT, on_ctrl_c);
params_ref p = gparams::get_module("sat");
p.set_bool("produce_models", true);
- sat::solver solver(p, 0);
+ reslimit limit;
+ sat::solver solver(p, limit, 0);
g_solver = &solver;
if (file_name) {
@@ -150,7 +152,7 @@ unsigned read_dimacs(char const * file_name) {
lbool r;
vector<sat::literal_vector> tracking_clauses;
- sat::solver solver2(p, 0);
+ sat::solver solver2(p, limit, 0);
if (p.get_bool("dimacs.core", false)) {
g_solver = &solver2;
sat::literal_vector assumptions;
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
index 2ef9a0d54..c31b2fb6d 100644
--- a/src/smt/params/smt_params.cpp
+++ b/src/smt/params/smt_params.cpp
@@ -35,6 +35,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_delay_units_threshold = p.delay_units_threshold();
m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
m_timeout = p.timeout();
+ m_rlimit = p.rlimit();
m_max_conflicts = p.max_conflicts();
m_core_validate = p.core_validate();
model_params mp(_p);
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index e67591d0e..2c1ac13c5 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -206,6 +206,7 @@ struct smt_params : public preprocessor_params,
bool m_user_theory_preprocess_axioms;
bool m_user_theory_persist_axioms;
unsigned m_timeout;
+ unsigned m_rlimit;
bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
bool m_dump_goal_as_smt;
@@ -275,6 +276,7 @@ struct smt_params : public preprocessor_params,
m_user_theory_preprocess_axioms(false),
m_user_theory_persist_axioms(false),
m_timeout(0),
+ m_rlimit(0),
m_at_labels_cex(false),
m_check_at_labels(false),
m_dump_goal_as_smt(false),
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index fa73f9725..e84f3654c 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -16,6 +16,7 @@ def_module_params(module_name='smt',
('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
('timeout', UINT, 0, 'timeout (0 means no timeout)'),
+ ('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index b0abc0de0..e19ee34dd 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -199,7 +199,7 @@ namespace smt {
bool context::bcp() {
SASSERT(!inconsistent());
while (m_qhead < m_assigned_literals.size()) {
- if (m_cancel_flag) {
+ if (get_cancel_flag()) {
return true;
}
literal l = m_assigned_literals[m_qhead];
@@ -1616,7 +1616,7 @@ namespace smt {
unsigned qhead = m_qhead;
if (!bcp())
return false;
- if (m_cancel_flag)
+ if (get_cancel_flag())
return true;
SASSERT(!inconsistent());
propagate_relevancy(qhead);
@@ -2773,7 +2773,7 @@ namespace smt {
}
void context::assert_expr_core(expr * e, proof * pr) {
- if (m_cancel_flag) return;
+ if (get_cancel_flag()) return;
SASSERT(is_well_sorted(m_manager, e));
TRACE("begin_assert_expr", tout << mk_pp(e, m_manager) << "\n";);
TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m_manager) << "\n";);
@@ -2803,7 +2803,7 @@ namespace smt {
}
void context::internalize_assertions() {
- if (m_cancel_flag) return;
+ if (get_cancel_flag()) return;
TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
reduce_assertions();
@@ -3311,6 +3311,9 @@ namespace smt {
if (!inconsistent()) {
if (resource_limits_exceeded())
return l_undef;
+
+ if (!m_manager.limit().inc())
+ return l_undef;
if (m_num_conflicts_since_restart > m_restart_threshold && m_scope_lvl - m_base_lvl > 2) {
TRACE("search_bug", tout << "bounded-search return undef, inconsistent: " << inconsistent() << "\n";);
@@ -3337,9 +3340,11 @@ namespace smt {
return l_undef;
}
+ if (!m_manager.limit().inc())
+ return l_undef;
+
if (m_base_lvl == m_scope_lvl && m_fparams.m_simplify_clauses)
simplify_clauses();
-
if (!decide()) {
final_check_status fcs = final_check();
@@ -3381,7 +3386,7 @@ namespace smt {
}
}
- if (m_cancel_flag) {
+ if (get_cancel_flag()) {
m_last_search_failure = CANCELED;
return true;
}
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 231b73fe3..fc7f076f1 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -235,7 +235,7 @@ namespace smt {
virtual void set_cancel_flag(bool f = true);
- bool get_cancel_flag() { return m_cancel_flag; }
+ bool get_cancel_flag() { return m_cancel_flag || !m_manager.limit().inc(); }
region & get_region() {
return m_region;
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
new file mode 100644
index 000000000..338bd5582
--- /dev/null
+++ b/src/util/rlimit.cpp
@@ -0,0 +1,55 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+ rlimit.cpp
+
+Abstract:
+
+ Resource limit container.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2015-09-28
+
+Revision History:
+
+--*/
+#include "rlimit.h"
+
+reslimit::reslimit():
+ m_count(0),
+ m_limit(UINT_MAX) {
+}
+
+unsigned reslimit::count() const {
+ return m_count;
+}
+
+bool reslimit::inc() {
+ ++m_count;
+ return m_count <= m_limit;
+}
+
+bool reslimit::inc(unsigned offset) {
+ m_count += offset;
+ return m_count <= m_limit;
+}
+
+void reslimit::push(unsigned delta_limit) {
+ unsigned new_limit = UINT_MAX;
+ if (delta_limit > 0 && delta_limit + m_count > m_count) {
+ new_limit = delta_limit + m_count;
+ }
+ m_limits.push_back(m_limit);
+ m_limit = std::min(new_limit, m_limit);
+}
+
+void reslimit::pop() {
+ if (m_count > m_limit) {
+ m_count = m_limit;
+ }
+ m_limit = m_limits.back();
+ m_limits.pop_back();
+}
diff --git a/src/util/rlimit.h b/src/util/rlimit.h
new file mode 100644
index 000000000..36912de40
--- /dev/null
+++ b/src/util/rlimit.h
@@ -0,0 +1,47 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+ rlimit.h
+
+Abstract:
+
+ Resource limit container.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2015-09-28
+
+Revision History:
+
+--*/
+#ifndef RLIMIT_H_
+#define RLIMIT_H_
+
+#include "vector.h"
+
+class reslimit {
+ unsigned m_count;
+ unsigned m_limit;
+ unsigned_vector m_limits;
+public:
+ reslimit();
+ bool inc();
+ bool inc(unsigned offset);
+ void push(unsigned delta_limit);
+ void pop();
+ unsigned count() const;
+};
+
+class scoped_rlimit {
+ reslimit& m_limit;
+public:
+ scoped_rlimit(reslimit& r, unsigned l): m_limit(r) {
+ r.push(l);
+ }
+ ~scoped_rlimit() { m_limit.pop(); }
+
+};
+
+#endif
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index 6e50fd4a8..e1a0928fe 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -236,3 +236,7 @@ void get_memory_statistics(statistics& st) {
st.update("memory", static_cast<double>(mem)/100.0);
st.update("num allocs", static_cast<double>(memory::get_allocation_count()));
}
+
+void get_rlimit_statistics(reslimit& l, statistics& st) {
+ st.update("rlimit-count", l.count());
+}
diff --git a/src/util/statistics.h b/src/util/statistics.h
index 258ffbe29..041c2cf99 100644
--- a/src/util/statistics.h
+++ b/src/util/statistics.h
@@ -21,6 +21,7 @@ Notes:
#include<iostream>
#include"vector.h"
+#include"rlimit.h"
class statistics {
typedef std::pair<char const *, unsigned> key_val_pair;
@@ -43,5 +44,6 @@ public:
};
void get_memory_statistics(statistics& st);
+void get_rlimit_statistics(reslimit& l, statistics& st);
#endif