From 5d711904687af9264a951e5a25157e914e76581d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Sep 2015 16:50:59 -0700 Subject: [PATCH] add catch for cancellation intermixed with return value l_true. To address regressions in QF_LIA tests Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 15 +++-- src/smt/smt_context.h | 2 +- src/tactic/smtlogics/qflia_tactic.cpp | 90 +++++++++++++++------------ src/tactic/tactic.cpp | 2 +- src/tactic/tactical.cpp | 35 +++++++++++ src/tactic/tactical.h | 1 + 6 files changed, 97 insertions(+), 48 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index e19ee34dd..43757b432 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index fc7f076f1..605d23876 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -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); // ----------------------------------- // diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index 00f6480d8..fd10d8ecb 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -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) { diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 5025b4449..0cfc9e3b2 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -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, diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 149cbc272..9786ccc8d 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -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: diff --git a/src/tactic/tactical.h b/src/tactic/tactical.h index 5022ac4a7..9aac3d42d 100644 --- a/src/tactic/tactical.h +++ b/src/tactic/tactical.h @@ -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);