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

change model evaluator to respect resource limits (#5184)

Browse source
This commit is contained in:
Nuno Lopes 2021-04-14 19:48:39 +01:00 • committed by GitHub
parent 7f8e2a9f75
commit 21e59f7c6e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/model/model_evaluator.cpp
View file

@ -616,7 +616,6 @@ struct model_evaluator::imp : public rewriter_tpl<mev::evaluator_cfg> {
false, // no proofs for evaluator false, // no proofs for evaluator
m_cfg), m_cfg),
m_cfg(md.get_manager(), md, p) { m_cfg(md.get_manager(), md, p) {
set_cancel_check(false);
} }
void expand_stores(expr_ref &val) {m_cfg.expand_stores(val);} void expand_stores(expr_ref &val) {m_cfg.expand_stores(val);}
void reset() { void reset() {

8
src/smt/smt_model_checker.cpp
View file

@ -162,13 +162,13 @@ namespace smt {
The variables are replaced by skolem constants. These constants are stored in sks. The variables are replaced by skolem constants. These constants are stored in sks.
*/ */
void model_checker::assert_neg_q_m(quantifier * q, expr_ref_vector & sks) { bool model_checker::assert_neg_q_m(quantifier * q, expr_ref_vector & sks) {
expr_ref tmp(m); expr_ref tmp(m);
TRACE("model_checker", tout << "curr_model:\n"; model_pp(tout, *m_curr_model);); TRACE("model_checker", tout << "curr_model:\n"; model_pp(tout, *m_curr_model););
if (!m_curr_model->eval(q->get_expr(), tmp, true)) { if (!m_curr_model->eval(q->get_expr(), tmp, true)) {
return; return false;
} }
TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";); TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);
ptr_buffer<expr> subst_args; ptr_buffer<expr> subst_args;
@ -191,6 +191,7 @@ namespace smt {
r = m.mk_not(sk_body); r = m.mk_not(sk_body);
TRACE("model_checker", tout << "mk_neg_q_m:\n" << mk_ismt2_pp(r, m) << "\n";); TRACE("model_checker", tout << "mk_neg_q_m:\n" << mk_ismt2_pp(r, m) << "\n";);
m_aux_context->assert_expr(r); m_aux_context->assert_expr(r);
return true;
} }
bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) { bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) {
@ -333,7 +334,8 @@ namespace smt {
TRACE("model_checker", tout << "model checking:\n" << expr_ref(flat_q->get_expr(), m) << "\n";); TRACE("model_checker", tout << "model checking:\n" << expr_ref(flat_q->get_expr(), m) << "\n";);
expr_ref_vector sks(m); expr_ref_vector sks(m);
assert_neg_q_m(flat_q, sks); if (!assert_neg_q_m(flat_q, sks))
return false;
TRACE("model_checker", tout << "skolems:\n" << sks << "\n";); TRACE("model_checker", tout << "skolems:\n" << sks << "\n";);
flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true); flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true);

2
src/smt/smt_model_checker.h
View file

@ -62,7 +62,7 @@ namespace smt {
expr * get_type_compatible_term(expr * val); expr * get_type_compatible_term(expr * val);
expr_ref replace_value_from_ctx(expr * e); expr_ref replace_value_from_ctx(expr * e);
void restrict_to_universe(expr * sk, obj_hashtable<expr> const & universe); void restrict_to_universe(expr * sk, obj_hashtable<expr> const & universe);
void assert_neg_q_m(quantifier * q, expr_ref_vector & sks); bool assert_neg_q_m(quantifier * q, expr_ref_vector & sks);
bool add_blocking_clause(model * cex, expr_ref_vector & sks); bool add_blocking_clause(model * cex, expr_ref_vector & sks);
bool check(quantifier * q); bool check(quantifier * q);
void check_quantifiers(bool& found_relevant, unsigned& num_failures); void check_quantifiers(bool& found_relevant, unsigned& num_failures);