mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

add catch for cancellation intermixed with return value l_true. To address regressions in QF_LIA tests

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-09-29 16:50:59 -07:00
parent 77c423b9aa
commit 5d71190468
6 changed files with 97 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/smt/smt_context.cpp
View file

@ -2956,9 +2956,13 @@ namespace smt {
/**
\brief Execute some finalization code after performing the search.
*/
void context::check_finalize(lbool r) {
lbool context::check_finalize(lbool r) {
TRACE("after_search", display(tout << "result: " << r << "\n"););
display_profile(verbose_stream());
if (r == l_true && get_cancel_flag()) {
r = l_undef;
}
return r;
}
/**
@ -2990,7 +2994,7 @@ namespace smt {
r = search();
}
}
check_finalize(r);
r = check_finalize(r);
return r;
}
@ -3081,7 +3085,7 @@ namespace smt {
}
}
}
check_finalize(r);
r = check_finalize(r);
return r;
}
@ -3191,6 +3195,7 @@ namespace smt {
if (status != l_false) {
// build candidate model before returning
mk_proto_model(status);
// status = l_undef;
}
break;
}
@ -3312,7 +3317,7 @@ namespace smt {
if (resource_limits_exceeded())
return l_undef;
if (!m_manager.limit().inc())
if (get_cancel_flag())
return l_undef;
if (m_num_conflicts_since_restart > m_restart_threshold && m_scope_lvl - m_base_lvl > 2) {
@ -3340,7 +3345,7 @@ namespace smt {
return l_undef;
}
if (!m_manager.limit().inc())
if (get_cancel_flag())
return l_undef;
if (m_base_lvl == m_scope_lvl && m_fparams.m_simplify_clauses)

2
src/smt/smt_context.h
View file

@ -1315,7 +1315,7 @@ namespace smt {
bool already_internalized_theory_core(theory * th, expr_ref_vector const & s) const;
#endif
bool check_preamble(bool reset_cancel);
void check_finalize(lbool r);
lbool check_finalize(lbool r);
// -----------------------------------
//

90
src/tactic/smtlogics/qflia_tactic.cpp
View file

@ -66,7 +66,7 @@ static tactic * mk_no_cut_smt_tactic(unsigned rs) {
params_ref solver_p;
solver_p.set_uint("arith.branch_cut_ratio", 10000000);
solver_p.set_uint("random_seed", rs);
return using_params(mk_smt_tactic_using(false), solver_p);
return annotate_tactic("no-cut-smt-tactic", using_params(mk_smt_tactic_using(false), solver_p));
}
// Create SMT solver that does not use cuts
@ -75,7 +75,7 @@ static tactic * mk_no_cut_no_relevancy_smt_tactic(unsigned rs) {
solver_p.set_uint("arith.branch_cut_ratio", 10000000);
solver_p.set_uint("random_seed", rs);
solver_p.set_uint("relevancy", 0);
return using_params(mk_smt_tactic_using(false), solver_p);
return annotate_tactic("no-cut-relevancy-tactic", using_params(mk_smt_tactic_using(false), solver_p));
}
static tactic * mk_bv2sat_tactic(ast_manager & m) {
@ -106,16 +106,18 @@ static tactic * mk_pb_tactic(ast_manager & m) {
params_ref bv2sat_p;
bv2sat_p.set_bool("ite_extra", true);
return and_then(fail_if_not(mk_is_pb_probe()),
fail_if(mk_produce_proofs_probe()),
fail_if(mk_produce_unsat_cores_probe()),
or_else(and_then(fail_if(mk_ge(mk_num_exprs_probe(), mk_const_probe(SMALL_SIZE))),
fail_if_not(mk_is_ilp_probe()),
// try_for(mk_mip_tactic(m), 8000),
mk_fail_if_undecided_tactic()),
and_then(using_params(mk_pb2bv_tactic(m), pb2bv_p),
fail_if_not(mk_is_qfbv_probe()),
using_params(mk_bv2sat_tactic(m), bv2sat_p))));
return annotate_tactic(
"pb-tactic",
and_then(fail_if_not(mk_is_pb_probe()),
fail_if(mk_produce_proofs_probe()),
fail_if(mk_produce_unsat_cores_probe()),
or_else(and_then(fail_if(mk_ge(mk_num_exprs_probe(), mk_const_probe(SMALL_SIZE))),
fail_if_not(mk_is_ilp_probe()),
// try_for(mk_mip_tactic(m), 8000),
mk_fail_if_undecided_tactic()),
and_then(using_params(mk_pb2bv_tactic(m), pb2bv_p),
fail_if_not(mk_is_qfbv_probe()),
using_params(mk_bv2sat_tactic(m), bv2sat_p)))));
}
@ -126,15 +128,17 @@ static tactic * mk_lia2sat_tactic(ast_manager & m) {
params_ref bv2sat_p;
bv2sat_p.set_bool("ite_extra", true);
return and_then(fail_if(mk_is_unbounded_probe()),
fail_if(mk_produce_proofs_probe()),
fail_if(mk_produce_unsat_cores_probe()),
mk_propagate_ineqs_tactic(m),
mk_normalize_bounds_tactic(m),
mk_lia2pb_tactic(m),
using_params(mk_pb2bv_tactic(m), pb2bv_p),
fail_if_not(mk_is_qfbv_probe()),
using_params(mk_bv2sat_tactic(m), bv2sat_p));
return annotate_tactic(
"lia2sat-tactic",
and_then(fail_if(mk_is_unbounded_probe()),
fail_if(mk_produce_proofs_probe()),
fail_if(mk_produce_unsat_cores_probe()),
mk_propagate_ineqs_tactic(m),
mk_normalize_bounds_tactic(m),
mk_lia2pb_tactic(m),
using_params(mk_pb2bv_tactic(m), pb2bv_p),
fail_if_not(mk_is_qfbv_probe()),
using_params(mk_bv2sat_tactic(m), bv2sat_p)));
}
// Try to find a model for an unbounded ILP problem.
@ -147,29 +151,33 @@ static tactic * mk_ilp_model_finder_tactic(ast_manager & m) {
add_bounds_p2.set_rat("add_bound_lower", rational(-32));
add_bounds_p2.set_rat("add_bound_upper", rational(31));
return and_then(fail_if_not(mk_and(mk_is_ilp_probe(), mk_is_unbounded_probe())),
fail_if(mk_produce_proofs_probe()),
fail_if(mk_produce_unsat_cores_probe()),
mk_propagate_ineqs_tactic(m),
or_else(// try_for(mk_mip_tactic(m), 5000),
try_for(mk_no_cut_smt_tactic(100), 2000),
and_then(using_params(mk_add_bounds_tactic(m), add_bounds_p1),
try_for(mk_lia2sat_tactic(m), 5000)),
try_for(mk_no_cut_smt_tactic(200), 5000),
and_then(using_params(mk_add_bounds_tactic(m), add_bounds_p2),
try_for(mk_lia2sat_tactic(m), 10000))
// , mk_mip_tactic(m)
),
mk_fail_if_undecided_tactic());
return annotate_tactic(
"ilp-model-finder-tactic",
and_then(fail_if_not(mk_and(mk_is_ilp_probe(), mk_is_unbounded_probe())),
fail_if(mk_produce_proofs_probe()),
fail_if(mk_produce_unsat_cores_probe()),
mk_propagate_ineqs_tactic(m),
or_else(// try_for(mk_mip_tactic(m), 5000),
try_for(mk_no_cut_smt_tactic(100), 2000),
and_then(using_params(mk_add_bounds_tactic(m), add_bounds_p1),
try_for(mk_lia2sat_tactic(m), 5000)),
try_for(mk_no_cut_smt_tactic(200), 5000),
and_then(using_params(mk_add_bounds_tactic(m), add_bounds_p2),
try_for(mk_lia2sat_tactic(m), 10000))
// , mk_mip_tactic(m)
),
mk_fail_if_undecided_tactic()));
}
static tactic * mk_bounded_tactic(ast_manager & m) {
return and_then(fail_if(mk_is_unbounded_probe()),
or_else(try_for(mk_no_cut_smt_tactic(100), 5000),
try_for(mk_no_cut_no_relevancy_smt_tactic(200), 5000),
try_for(mk_no_cut_smt_tactic(300), 15000)
),
mk_fail_if_undecided_tactic());
return annotate_tactic(
"bounded-tactic",
and_then(fail_if(mk_is_unbounded_probe()),
or_else(try_for(mk_no_cut_smt_tactic(100), 5000),
try_for(mk_no_cut_no_relevancy_smt_tactic(200), 5000),
try_for(mk_no_cut_smt_tactic(300), 15000)
),
mk_fail_if_undecided_tactic()));
}
tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {

2
src/tactic/tactic.cpp
View file

@ -120,7 +120,7 @@ class report_verbose_tactic : public skip_tactic {
unsigned m_lvl;
public:
report_verbose_tactic(char const * msg, unsigned lvl) : m_msg(msg), m_lvl(lvl) {}
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,

35
src/tactic/tactical.cpp
View file

@ -1259,6 +1259,41 @@ tactic * using_params(tactic * t, params_ref const & p) {
return alloc(using_params_tactical, t, p);
}
class annotate_tactical : public unary_tactical {
std::string m_name;
struct scope {
std::string m_name;
scope(std::string const& name) : m_name(name) {
IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(" << m_name << " start)\n";);
}
~scope() {
IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(" << m_name << " done)\n";);
}
};
public:
annotate_tactical(char const* name, tactic* t):
unary_tactical(t), m_name(name) {}
virtual void operator()(goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
scope _scope(m_name);
m_t->operator()(in, result, mc, pc, core);
}
virtual tactic * translate(ast_manager & m) {
tactic * new_t = m_t->translate(m);
return alloc(annotate_tactical, m_name.c_str(), new_t);
}
};
tactic * annotate_tactic(char const* name, tactic * t) {
return alloc(annotate_tactical, name, t);
}
class cond_tactical : public binary_tactical {
probe * m_p;
public:

1
src/tactic/tactical.h
View file

@ -63,6 +63,7 @@ tactic * par_and_then(tactic * t1, tactic * t2);
tactic * try_for(tactic * t, unsigned msecs);
tactic * clean(tactic * t);
tactic * using_params(tactic * t, params_ref const & p);
tactic * annotate_tactic(char const* name, tactic * t);
// Create a tactic that fails if the result returned by probe p is true.
tactic * fail_if(probe * p);