mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

adding rlimit resource limit facility to provide platform and architecture independent method for canceling activities

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-09-28 13:37:59 -07:00
parent ad16cc0ce2
commit 9b3e242990
26 changed files with 165 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/api/api_context.h
View file

@ -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; }

2
src/api/api_datalog.cpp
View file

@ -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));
}

3
src/api/api_solver.cpp
View file

@ -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);

4
src/ast/ast.h
View file

@ -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);

2
src/ast/rewriter/rewriter_def.h
View file

@ -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;

4
src/cmd_context/cmd_context.cpp
View file

@ -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);
}

7
src/cmd_context/context_params.cpp
View file

@ -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");

1
src/cmd_context/context_params.h
View file

@ -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);

1
src/cmd_context/tactic_cmds.cpp
View file

@ -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());

1
src/muz/base/dl_context.cpp
View file

@ -948,6 +948,7 @@ namespace datalog {
m_engine->collect_statistics(st);
}
get_memory_statistics(st);
get_rlimit_statistics(m.limit(), st);
}

1
src/opt/opt_context.cpp
View file

@ -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) {

2
src/sat/sat_bceq.cpp
View file

@ -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;

3
src/sat/sat_solver.cpp
View file

@ -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),

6
src/sat/sat_solver.h
View file

@ -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

2
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -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),

2
src/sat/tactic/sat_tactic.cpp
View file

@ -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());
}

6
src/shell/dimacs_frontend.cpp
View file

@ -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;

1
src/smt/params/smt_params.cpp
View file

@ -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);

2
src/smt/params/smt_params.h
View file

@ -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),

1
src/smt/params/smt_params_helper.pyg
View file

@ -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'),

17
src/smt/smt_context.cpp
View file

@ -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;
}

2
src/smt/smt_context.h
View file

@ -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;

55
src/util/rlimit.cpp Normal file
View file

@ -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();
}

47
src/util/rlimit.h Normal file
View file

@ -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

4
src/util/statistics.cpp
View file

@ -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());
}

2
src/util/statistics.h
View file

@ -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