From e0d8cefde44ee8181756d98f85412dfc4511c4e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 12 Jun 2019 20:15:46 -0700 Subject: [PATCH] remove cooperate Signed-off-by: Nikolaj Bjorner --- src/ackermannization/lackr.h | 2 - src/ast/expr2polynomial.cpp | 2 - src/ast/fpa/fpa2bv_rewriter.cpp | 2 - src/ast/normal_forms/nnf.cpp | 2 - .../bit_blaster/bit_blaster_rewriter.cpp | 1 - .../bit_blaster/bit_blaster_tpl_def.h | 2 - src/ast/rewriter/expr_replacer.cpp | 2 - src/ast/rewriter/th_rewriter.cpp | 2 - src/math/interval/interval_def.h | 2 - src/math/polynomial/algebraic_numbers.cpp | 2 - src/math/polynomial/polynomial.cpp | 2 - src/math/polynomial/upolynomial.cpp | 2 - src/math/realclosure/realclosure.cpp | 2 - src/math/subpaving/subpaving_t_def.h | 2 - src/math/subpaving/tactic/expr2subpaving.cpp | 2 - src/model/model_evaluator.cpp | 2 - src/muz/base/hnf.cpp | 1 - src/muz/spacer/spacer_mev_array.cpp | 1 - src/qe/qe.cpp | 2 - src/qe/qe_lite.cpp | 5 -- src/qe/qe_sat_tactic.cpp | 2 - src/qe/qe_tactic.cpp | 2 - src/sat/tactic/goal2sat.cpp | 2 - src/smt/smt_model_finder.cpp | 2 - src/smt/smt_model_finder.h | 1 - src/tactic/aig/aig.cpp | 2 - src/tactic/arith/card2bv_tactic.cpp | 1 - src/tactic/arith/degree_shift_tactic.cpp | 2 - src/tactic/arith/eq2bv_tactic.cpp | 1 - src/tactic/arith/fm_tactic.cpp | 2 - src/tactic/arith/lia2card_tactic.cpp | 1 - src/tactic/arith/pb2bv_tactic.cpp | 3 - src/tactic/bv/bv1_blaster_tactic.cpp | 2 - src/tactic/bv/bv_bound_chk_tactic.cpp | 2 - src/tactic/bv/bvarray2uf_rewriter.cpp | 1 - src/tactic/bv/elim_small_bv_tactic.cpp | 2 - src/tactic/bv/max_bv_sharing_tactic.cpp | 2 - src/tactic/core/blast_term_ite_tactic.cpp | 2 - src/tactic/core/cofactor_elim_term_ite.cpp | 2 - src/tactic/core/ctx_simplify_tactic.cpp | 2 - src/tactic/core/elim_term_ite_tactic.cpp | 2 - src/tactic/core/elim_uncnstr_tactic.cpp | 2 - src/tactic/core/occf_tactic.cpp | 2 - src/tactic/core/reduce_args_tactic.cpp | 2 - src/tactic/core/reduce_invertible_tactic.cpp | 2 - src/tactic/core/solve_eqs_tactic.cpp | 2 - src/tactic/core/tseitin_cnf_tactic.cpp | 2 - src/tactic/sls/sls_engine.cpp | 2 - src/tactic/smtlogics/qfufbv_tactic.cpp | 1 - src/util/CMakeLists.txt | 2 - src/util/cooperate.cpp | 59 ------------------- src/util/cooperate.h | 50 ---------------- 52 files changed, 204 deletions(-) delete mode 100644 src/util/cooperate.cpp delete mode 100644 src/util/cooperate.h diff --git a/src/ackermannization/lackr.h b/src/ackermannization/lackr.h index 049fb8bb3..19d4e35d8 100644 --- a/src/ackermannization/lackr.h +++ b/src/ackermannization/lackr.h @@ -20,7 +20,6 @@ #include "ackermannization/ackr_info.h" #include "ackermannization/ackr_helper.h" #include "ast/rewriter/th_rewriter.h" -#include "util/cooperate.h" #include "ast/bv_decl_plugin.h" #include "util/lbool.h" #include "model/model.h" @@ -75,7 +74,6 @@ class lackr { if (m_m.canceled()) { throw tactic_exception(TACTIC_CANCELED_MSG); } - cooperate("lackr"); } private: typedef ackr_helper::fun2terms_map fun2terms_map; diff --git a/src/ast/expr2polynomial.cpp b/src/ast/expr2polynomial.cpp index 82bace428..4831d435b 100644 --- a/src/ast/expr2polynomial.cpp +++ b/src/ast/expr2polynomial.cpp @@ -22,7 +22,6 @@ Notes: #include "ast/arith_decl_plugin.h" #include "ast/ast_smt2_pp.h" #include "util/z3_exception.h" -#include "util/cooperate.h" #include "util/common_msgs.h" struct expr2polynomial::imp { @@ -96,7 +95,6 @@ struct expr2polynomial::imp { void checkpoint() { if (m_cancel) throw default_exception(Z3_CANCELED_MSG); - cooperate("expr2polynomial"); } void throw_not_polynomial() { diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 7195f7179..b9a8a346c 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -20,7 +20,6 @@ Notes: #include "ast/rewriter/rewriter_def.h" #include "ast/fpa/fpa2bv_rewriter.h" -#include "util/cooperate.h" #include "ast/fpa/fpa2bv_rewriter_params.hpp" @@ -50,7 +49,6 @@ void fpa2bv_rewriter_cfg::updt_params(params_ref const & p) { } bool fpa2bv_rewriter_cfg::max_steps_exceeded(unsigned num_steps) const { - cooperate("fpa2bv"); return num_steps > m_max_steps; } diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 26ffc1709..d8db6df81 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -19,7 +19,6 @@ Notes: --*/ #include "util/warning.h" -#include "util/cooperate.h" #include "ast/normal_forms/nnf.h" #include "ast/normal_forms/nnf_params.hpp" #include "ast/used_vars.h" @@ -380,7 +379,6 @@ struct nnf::imp { void checkpoint() { - cooperate("nnf"); if (memory::get_allocation_size() > m_max_memory) throw nnf_exception(Z3_MAX_MEMORY_MSG); if (m.canceled()) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index fe750acdd..d1dd3bc9b 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -142,7 +142,6 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg { bool rewrite_patterns() const { return true; } bool max_steps_exceeded(unsigned num_steps) const { - cooperate("bit blaster"); if (memory::get_allocation_size() > m_max_memory) throw rewriter_exception(Z3_MAX_MEMORY_MSG); return num_steps > m_max_steps; diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index a3bb3b6e1..11be2f72e 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -19,7 +19,6 @@ Revision History: #include "ast/rewriter/bit_blaster/bit_blaster_tpl.h" #include "util/rational.h" #include "ast/ast_pp.h" -#include "util/cooperate.h" #include "util/common_msgs.h" #include "ast/rewriter/rewriter_types.h" @@ -30,7 +29,6 @@ void bit_blaster_tpl::checkpoint() { throw rewriter_exception(Z3_MAX_MEMORY_MSG); if (m().canceled()) throw rewriter_exception(m().limit().get_cancel_msg()); - cooperate("bit-blaster"); } /** diff --git a/src/ast/rewriter/expr_replacer.cpp b/src/ast/rewriter/expr_replacer.cpp index c9bf834fd..d26a10b19 100644 --- a/src/ast/rewriter/expr_replacer.cpp +++ b/src/ast/rewriter/expr_replacer.cpp @@ -19,7 +19,6 @@ Notes: #include "ast/rewriter/expr_replacer.h" #include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/th_rewriter.h" -#include "util/cooperate.h" void expr_replacer::operator()(expr * t, expr_ref & result, proof_ref & result_pr) { expr_dependency_ref result_dep(m()); @@ -74,7 +73,6 @@ struct default_expr_replacer_cfg : public default_rewriter_cfg { } bool max_steps_exceeded(unsigned num_steps) const { - cooperate("simplifier"); return false; } }; diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 3f1f168dd..0e73a3623 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -16,7 +16,6 @@ Author: Notes: --*/ -#include "util/cooperate.h" #include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/rewriter_params.hpp" #include "ast/rewriter/bool_rewriter.h" @@ -108,7 +107,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg { bool cache_all_results() const { return m_cache_all; } bool max_steps_exceeded(unsigned num_steps) const { - cooperate("simplifier"); if (memory::get_allocation_size() > m_max_memory) throw rewriter_exception(Z3_MAX_MEMORY_MSG); return num_steps > m_max_steps; diff --git a/src/math/interval/interval_def.h b/src/math/interval/interval_def.h index a1c8df7a8..19058b231 100644 --- a/src/math/interval/interval_def.h +++ b/src/math/interval/interval_def.h @@ -23,7 +23,6 @@ Revision History: #include "util/debug.h" #include "util/trace.h" #include "util/scoped_numeral.h" -#include "util/cooperate.h" #include "util/common_msgs.h" #define DEFAULT_PI_PRECISION 2 @@ -65,7 +64,6 @@ template void interval_manager::checkpoint() { if (!m_limit.inc()) throw default_exception(Z3_CANCELED_MSG); - cooperate("interval"); } /* diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 25a1985a7..31346acd9 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -20,7 +20,6 @@ Notes: #include "math/polynomial/upolynomial.h" #include "util/mpbq.h" #include "util/basic_interval.h" -#include "util/cooperate.h" #include "math/polynomial/sexpr2upolynomial.h" #include "util/scoped_ptr_vector.h" #include "util/mpbqi.h" @@ -128,7 +127,6 @@ namespace algebraic_numbers { void checkpoint() { if (!m_limit.inc()) throw algebraic_exception(Z3_CANCELED_MSG); - cooperate("algebraic"); } void reset_statistics() { diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 8f7f08c7f..c8c204620 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -23,7 +23,6 @@ Notes: #include "util/id_gen.h" #include "util/buffer.h" #include "util/scoped_ptr_vector.h" -#include "util/cooperate.h" #include "math/polynomial/upolynomial_factorization.h" #include "math/polynomial/polynomial_primes.h" #include "util/permutation.h" @@ -2372,7 +2371,6 @@ namespace polynomial { if (!m_limit.inc()) { throw polynomial_exception(Z3_CANCELED_MSG); } - cooperate("polynomial"); } mpzzp_manager & m() const { return const_cast(this)->m_manager; } diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp index 9c43d88ec..cfc8339d7 100644 --- a/src/math/polynomial/upolynomial.cpp +++ b/src/math/polynomial/upolynomial.cpp @@ -25,7 +25,6 @@ Notes: #include "math/polynomial/upolynomial_factorization.h" #include "math/polynomial/polynomial_primes.h" #include "util/buffer.h" -#include "util/cooperate.h" #include "util/common_msgs.h" namespace upolynomial { @@ -157,7 +156,6 @@ namespace upolynomial { void core_manager::checkpoint() { if (!m_limit.inc()) throw upolynomial_exception(Z3_CANCELED_MSG); - cooperate("upolynomial"); } // Eliminate leading zeros from buffer. diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 3e05be734..c43fca4d4 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -28,7 +28,6 @@ Notes: #include "util/obj_ref.h" #include "util/ref_vector.h" #include "util/ref_buffer.h" -#include "util/cooperate.h" #include "util/common_msgs.h" #ifndef REALCLOSURE_INI_BUFFER_SIZE @@ -550,7 +549,6 @@ namespace realclosure { void checkpoint() { if (!m_limit.inc()) throw exception(Z3_CANCELED_MSG); - cooperate("rcf"); } value * one() const { diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h index b13f41c54..f72eacdb7 100644 --- a/src/math/subpaving/subpaving_t_def.h +++ b/src/math/subpaving/subpaving_t_def.h @@ -19,7 +19,6 @@ Revision History: #include "math/subpaving/subpaving_t.h" #include "math/interval/interval_def.h" #include "util/buffer.h" -#include "util/cooperate.h" #include "util/z3_exception.h" #include "util/common_msgs.h" @@ -463,7 +462,6 @@ void context_t::checkpoint() { throw default_exception(Z3_CANCELED_MSG); if (memory::get_allocation_size() > m_max_memory) throw default_exception(Z3_MAX_MEMORY_MSG); - cooperate("subpaving"); } template diff --git a/src/math/subpaving/tactic/expr2subpaving.cpp b/src/math/subpaving/tactic/expr2subpaving.cpp index 1eb4ad108..b5e27abea 100644 --- a/src/math/subpaving/tactic/expr2subpaving.cpp +++ b/src/math/subpaving/tactic/expr2subpaving.cpp @@ -21,7 +21,6 @@ Notes: #include "ast/expr2var.h" #include "util/ref_util.h" #include "util/z3_exception.h" -#include "util/cooperate.h" #include "ast/arith_decl_plugin.h" #include "util/scoped_numeral_buffer.h" #include "util/common_msgs.h" @@ -96,7 +95,6 @@ struct expr2subpaving::imp { void checkpoint() { if (m().canceled()) throw default_exception(Z3_CANCELED_MSG); - cooperate("expr2subpaving"); } subpaving::var mk_var_for(expr * t) { diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 1bd274316..ca670cc04 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -16,7 +16,6 @@ Author: Revision History: --*/ -#include "util/cooperate.h" #include "model/model.h" #include "model/model_evaluator_params.hpp" #include "model/model_evaluator.h" @@ -342,7 +341,6 @@ struct evaluator_cfg : public default_rewriter_cfg { bool max_steps_exceeded(unsigned num_steps) const { - cooperate("model evaluator"); if (memory::get_allocation_size() > m_max_memory) throw rewriter_exception(Z3_MAX_MEMORY_MSG); return num_steps > m_max_steps; diff --git a/src/muz/base/hnf.cpp b/src/muz/base/hnf.cpp index 1e6196950..d2ba9b999 100644 --- a/src/muz/base/hnf.cpp +++ b/src/muz/base/hnf.cpp @@ -50,7 +50,6 @@ Notes: #include "ast/rewriter/var_subst.h" #include "ast/normal_forms/name_exprs.h" #include "ast/act_cache.h" -#include "util/cooperate.h" #include "ast/ast_pp.h" #include "ast/rewriter/quant_hoist.h" #include "ast/ast_util.h" diff --git a/src/muz/spacer/spacer_mev_array.cpp b/src/muz/spacer/spacer_mev_array.cpp index 7a4bc321b..fe7b54101 100644 --- a/src/muz/spacer/spacer_mev_array.cpp +++ b/src/muz/spacer/spacer_mev_array.cpp @@ -25,7 +25,6 @@ Revision History: #include"ast/rewriter/datatype_rewriter.h" #include"ast/rewriter/array_rewriter.h" #include"ast/rewriter/rewriter_def.h" -#include"util/cooperate.h" #include"ast/ast_pp.h" #include"model/func_interp.h" diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 1b6639e8b..77d2fe248 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -41,7 +41,6 @@ Revision History: #include "model/model_evaluator.h" #include "ast/has_free_vars.h" #include "ast/rewriter/rewriter_def.h" -#include "util/cooperate.h" #include "tactic/tactical.h" #include "model/model_v2_pp.h" #include "util/obj_hashtable.h" @@ -2048,7 +2047,6 @@ namespace qe { void checkpoint() { if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); - cooperate("qe"); } diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 15f1f6176..7f2ac4b19 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -32,7 +32,6 @@ Revision History: #include "ast/rewriter/th_rewriter.h" #include "ast/for_each_expr.h" #include "ast/rewriter/expr_safe_replace.h" -#include "util/cooperate.h" #include "ast/datatype_decl_plugin.h" #include "qe/qe_vartest.h" @@ -687,7 +686,6 @@ namespace eq { } void checkpoint() { - cooperate("der"); if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); } @@ -878,7 +876,6 @@ namespace ar { } void checkpoint() { - cooperate("der"); if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); } @@ -2154,7 +2151,6 @@ namespace fm { } void checkpoint() { - cooperate("fm"); if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); } @@ -2428,7 +2424,6 @@ class qe_lite_tactic : public tactic { void checkpoint() { if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); - cooperate("qe-lite"); } void debug_diff(expr* a, expr* b) { diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp index 5fbe10d35..d9858b3c1 100644 --- a/src/qe/qe_sat_tactic.cpp +++ b/src/qe/qe_sat_tactic.cpp @@ -25,7 +25,6 @@ Revision History: #include "ast/ast_pp.h" #include "smt/smt_kernel.h" #include "qe/qe.h" -#include "util/cooperate.h" #include "model/model_v2_pp.h" #include "ast/rewriter/expr_replacer.h" #include "ast/rewriter/th_rewriter.h" @@ -657,7 +656,6 @@ namespace qe { if (m.canceled()) { throw tactic_exception(m.limit().get_cancel_msg()); } - cooperate("qe-sat"); } void check_success(bool ok) { diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp index a4e04485b..db0543d4f 100644 --- a/src/qe/qe_tactic.cpp +++ b/src/qe/qe_tactic.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include "tactic/tactical.h" -#include "util/cooperate.h" #include "qe/qe.h" class qe_tactic : public tactic { @@ -46,7 +45,6 @@ class qe_tactic : public tactic { void checkpoint() { if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); - cooperate("qe"); } void operator()(goal_ref const & g, diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index b329cb06e..76578ebf5 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -27,7 +27,6 @@ Notes: --*/ #include "util/ref_util.h" -#include "util/cooperate.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_pp.h" #include "ast/pb_decl_plugin.h" @@ -749,7 +748,6 @@ struct goal2sat::imp { } while (!m_frame_stack.empty()) { loop: - cooperate("goal2sat"); if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); if (memory::get_allocation_size() > m_max_memory) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 814538a88..77d9a30f4 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -16,7 +16,6 @@ Author: Revision History: --*/ -#include "util/cooperate.h" #include "util/backtrackable_set.h" #include "ast/ast_util.h" #include "ast/macros/macro_util.h" @@ -3179,7 +3178,6 @@ namespace smt { } void model_finder::checkpoint(char const* msg) { - cooperate(msg); if (m_context && m_context->get_cancel_flag()) throw tactic_exception(m_context->get_manager().limit().get_cancel_msg()); } diff --git a/src/smt/smt_model_finder.h b/src/smt/smt_model_finder.h index 842a18db8..122d578fe 100644 --- a/src/smt/smt_model_finder.h +++ b/src/smt/smt_model_finder.h @@ -49,7 +49,6 @@ Revision History: #include "ast/ast.h" #include "ast/func_decl_dependencies.h" #include "smt/proto_model/proto_model.h" -#include "util/cooperate.h" #include "tactic/tactic_exception.h" namespace smt { diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index faedf0e0c..cd0be62b5 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -19,7 +19,6 @@ Notes: #include "tactic/aig/aig.h" #include "tactic/goal.h" #include "ast/ast_smt2_pp.h" -#include "util/cooperate.h" #define USE_TWO_LEVEL_RULES #define FIRST_NODE_ID (UINT_MAX/2) @@ -129,7 +128,6 @@ struct aig_manager::imp { throw aig_exception(TACTIC_MAX_MEMORY_MSG); if (m().canceled()) throw aig_exception(m().limit().get_cancel_msg()); - cooperate("aig"); } void dec_ref_core(aig_lit const & r) { dec_ref_core(r.ptr()); } diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 65b8d8bf3..f68a6e082 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -17,7 +17,6 @@ Notes: --*/ #include "tactic/tactical.h" -#include "util/cooperate.h" #include "ast/ast_smt2_pp.h" #include "tactic/arith/card2bv_tactic.h" #include "ast/rewriter/pb2bv_rewriter.h" diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index b713c3055..403f0a317 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -21,7 +21,6 @@ Revision History: --*/ #include "tactic/tactical.h" #include "tactic/generic_model_converter.h" -#include "util/cooperate.h" #include "ast/arith_decl_plugin.h" #include "tactic/core/simplify_tactic.h" #include "ast/ast_smt2_pp.h" @@ -100,7 +99,6 @@ class degree_shift_tactic : public tactic { void checkpoint() { if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); - cooperate("degree_shift"); } void visit(expr * t, expr_fast_mark1 & visited) { diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index 616ba69c9..f44029d70 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -18,7 +18,6 @@ Notes: --*/ #include "tactic/tactical.h" -#include "util/cooperate.h" #include "tactic/arith/bound_manager.h" #include "ast/ast_pp.h" #include "ast/arith_decl_plugin.h" diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index bd99e4303..22b73874f 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -25,7 +25,6 @@ Revision History: #include "tactic/tactical.h" #include "ast/arith_decl_plugin.h" #include "ast/for_each_expr.h" -#include "util/cooperate.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_pp.h" #include "util/id_gen.h" @@ -1543,7 +1542,6 @@ class fm_tactic : public tactic { } void checkpoint() { - cooperate("fm"); if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); if (memory::get_allocation_size() > m_max_memory) diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index c2c90284c..8567ca13b 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -16,7 +16,6 @@ Author: Notes: --*/ -#include "util/cooperate.h" #include "ast/ast_pp.h" #include "ast/pb_decl_plugin.h" #include "ast/arith_decl_plugin.h" diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 7a64c9f16..b1cb74f65 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -17,7 +17,6 @@ Notes: --*/ #include "tactic/tactical.h" -#include "util/cooperate.h" #include "tactic/arith/bound_manager.h" #include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/rewriter_def.h" @@ -182,7 +181,6 @@ private: }; void checkpoint() { - cooperate("pb2bv"); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); } @@ -209,7 +207,6 @@ private: } bool max_steps_exceeded(unsigned num_steps) const { - cooperate("pb2bv"); if (memory::get_allocation_size() > owner.m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); return false; diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index bf9ca4101..e67b5f9b8 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -27,7 +27,6 @@ Notes: #include "ast/bv_decl_plugin.h" #include "ast/rewriter/rewriter_def.h" #include "ast/for_each_expr.h" -#include "util/cooperate.h" #include "ast/rewriter/bv_rewriter.h" class bv1_blaster_tactic : public tactic { @@ -73,7 +72,6 @@ class bv1_blaster_tactic : public tactic { bool rewrite_patterns() const { UNREACHABLE(); return false; } bool max_steps_exceeded(unsigned num_steps) const { - cooperate("bv1 blaster"); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); return num_steps > m_max_steps; diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index cf35afef4..f71fcd5e4 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -21,7 +21,6 @@ #include "ast/rewriter/bv_bounds.h" #include "ast/rewriter/rewriter_params.hpp" #include "ast/rewriter/bool_rewriter.h" -#include "util/cooperate.h" struct bv_bound_chk_stats { unsigned m_unsats; @@ -80,7 +79,6 @@ struct bv_bound_chk_rewriter_cfg : public default_rewriter_cfg { } bool max_steps_exceeded(unsigned long long num_steps) const { - cooperate("bv-bound-chk"); if (num_steps > m_max_steps) return true; if (memory::get_allocation_size() > m_max_memory) diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp index 97947c03a..a628b601c 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.cpp +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -18,7 +18,6 @@ Notes: --*/ -#include "util/cooperate.h" #include "ast/bv_decl_plugin.h" #include "ast/array_decl_plugin.h" #include "util/params.h" diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index 256586896..47e4e9d3e 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -19,7 +19,6 @@ Revision History: #include "tactic/tactical.h" #include "ast/rewriter/rewriter_def.h" #include "tactic/generic_model_converter.h" -#include "util/cooperate.h" #include "ast/bv_decl_plugin.h" #include "ast/used_vars.h" #include "ast/well_sorted.h" @@ -56,7 +55,6 @@ class elim_small_bv_tactic : public tactic { } bool max_steps_exceeded(unsigned long long num_steps) const { - cooperate("elim-small-bv"); if (num_steps > m_max_steps) return true; if (memory::get_allocation_size() > m_max_memory) diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index 98936ccad..71edd0a61 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -24,7 +24,6 @@ Revision History: #include "ast/rewriter/rewriter_def.h" #include "util/obj_pair_hashtable.h" #include "ast/ast_lt.h" -#include "util/cooperate.h" class max_bv_sharing_tactic : public tactic { @@ -61,7 +60,6 @@ class max_bv_sharing_tactic : public tactic { } bool max_steps_exceeded(unsigned num_steps) const { - cooperate("max bv sharing"); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); return num_steps > m_max_steps; diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index 259b479c5..05924e32e 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -16,7 +16,6 @@ Author: Notes: --*/ -#include "util/cooperate.h" #include "ast/normal_forms/defined_names.h" #include "ast/rewriter/rewriter_def.h" #include "ast/scoped_proof.h" @@ -60,7 +59,6 @@ class blast_term_ite_tactic : public tactic { bool max_steps_exceeded(unsigned num_steps) const { - cooperate("blast term ite"); // if (memory::get_allocation_size() > m_max_memory) // throw tactic_exception(TACTIC_MAX_MEMORY_MSG); return num_steps >= m_max_steps; diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index 6afcdee41..3a4f3ce0c 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -19,7 +19,6 @@ Revision History: #include "tactic/core/cofactor_elim_term_ite.h" #include "ast/rewriter/mk_simplified_app.h" #include "ast/rewriter/rewriter_def.h" -#include "util/cooperate.h" #include "ast/for_each_expr.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_ll_pp.h" @@ -32,7 +31,6 @@ struct cofactor_elim_term_ite::imp { bool m_cofactor_equalities; void checkpoint() { - cooperate("cofactor ite"); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); if (m.canceled()) diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index b143bf933..4336ee1ac 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -18,7 +18,6 @@ Notes: --*/ #include "tactic/core/ctx_simplify_tactic.h" #include "ast/rewriter/mk_simplified_app.h" -#include "util/cooperate.h" #include "ast/ast_ll_pp.h" #include "ast/ast_pp.h" @@ -202,7 +201,6 @@ struct ctx_simplify_tactic::imp { } void checkpoint() { - cooperate("ctx_simplify_tactic"); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); if (m.canceled()) diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index 0bb59afcf..a317b2ce0 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -21,7 +21,6 @@ Notes: #include "ast/normal_forms/defined_names.h" #include "ast/rewriter/rewriter_def.h" #include "tactic/generic_model_converter.h" -#include "util/cooperate.h" class elim_term_ite_tactic : public tactic { @@ -35,7 +34,6 @@ class elim_term_ite_tactic : public tactic { unsigned m_num_fresh; bool max_steps_exceeded(unsigned num_steps) const { - cooperate("elim term ite"); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); return false; diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 5b77fb9a2..bca13366f 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -24,7 +24,6 @@ Notes: #include "ast/array_decl_plugin.h" #include "ast/datatype_decl_plugin.h" #include "tactic/core/collect_occs.h" -#include "util/cooperate.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_ll_pp.h" @@ -67,7 +66,6 @@ class elim_uncnstr_tactic : public tactic { ast_manager & m() const { return m_a_util.get_manager(); } bool max_steps_exceeded(unsigned num_steps) const { - cooperate("elim-uncnstr-vars"); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); return num_steps > m_max_steps; diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp index 9bd6300ba..de8cb9375 100644 --- a/src/tactic/core/occf_tactic.cpp +++ b/src/tactic/core/occf_tactic.cpp @@ -24,7 +24,6 @@ Revision History: #include "tactic/tactical.h" #include "tactic/core/occf_tactic.h" #include "tactic/generic_model_converter.h" -#include "util/cooperate.h" class occf_tactic : public tactic { struct imp { @@ -38,7 +37,6 @@ class occf_tactic : public tactic { void checkpoint() { if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); - cooperate("occf"); } bool is_literal(expr * t) const { diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 24898320d..6f55ca2f7 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -17,7 +17,6 @@ Notes: --*/ #include "tactic/tactical.h" -#include "util/cooperate.h" #include "ast/ast_smt2_pp.h" #include "ast/has_free_vars.h" #include "util/map.h" @@ -115,7 +114,6 @@ struct reduce_args_tactic::imp { void checkpoint() { if (m_manager.canceled()) throw tactic_exception(m_manager.limit().get_cancel_msg()); - cooperate("reduce-args"); } struct find_non_candidates_proc { diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index 3420a3f99..d7c79e454 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -20,7 +20,6 @@ Notes: --*/ -#include "util/cooperate.h" #include "ast/bv_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "ast/ast_pp.h" @@ -97,7 +96,6 @@ private: void checkpoint() { if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); - cooperate("reduce-invertible"); } expr_mark m_inverted; diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 1ab4c823b..bb600cb70 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include "ast/rewriter/expr_replacer.h" -#include "util/cooperate.h" #include "ast/occurs.h" #include "ast/ast_util.h" #include "ast/ast_pp.h" @@ -87,7 +86,6 @@ class solve_eqs_tactic : public tactic { void checkpoint() { if (m().canceled()) throw tactic_exception(m().limit().get_cancel_msg()); - cooperate("solve-eqs"); } // Check if the number of occurrences of t is below the specified threshold :solve-eqs-max-occs diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index 929168ed0..e8e996396 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -54,7 +54,6 @@ Notes: #include "tactic/generic_model_converter.h" #include "ast/rewriter/bool_rewriter.h" #include "tactic/core/simplify_tactic.h" -#include "util/cooperate.h" static void swap_if_gt(expr * & n1, expr * & n2) { if (n1->get_id() > n2->get_id()) @@ -785,7 +784,6 @@ class tseitin_cnf_tactic : public tactic { void checkpoint() { - cooperate("tseitin cnf"); if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); if (memory::get_allocation_size() > m_max_memory) diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index f55aa41aa..bf3cede69 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -24,7 +24,6 @@ Notes: #include "ast/rewriter/var_subst.h" #include "model/model_pp.h" #include "tactic/tactic.h" -#include "util/cooperate.h" #include "util/luby.h" #include "tactic/sls/sls_params.hpp" @@ -96,7 +95,6 @@ void sls_engine::collect_statistics(statistics& st) const { void sls_engine::checkpoint() { if (m_manager.canceled()) throw tactic_exception(m_manager.limit().get_cancel_msg()); - cooperate("sls"); } bool sls_engine::full_eval(model & mdl) { diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 8dd77cba2..9cf565c09 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -30,7 +30,6 @@ Notes: #include "tactic/smtlogics/qfufbv_tactic_params.hpp" /////////////// #include "model/model_smt2_pp.h" -#include "util/cooperate.h" #include "ackermannization/lackr.h" #include "ackermannization/ackermannization_params.hpp" #include "tactic/smtlogics/qfufbv_ackr_model_converter.h" diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 5346b9770..13bc4715c 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -16,7 +16,6 @@ z3_add_component(util bit_vector.cpp cmd_context_types.cpp common_msgs.cpp - cooperate.cpp debug.cpp env_params.cpp fixed_bit_vector.cpp @@ -63,7 +62,6 @@ z3_add_component(util EXTRA_REGISTER_MODULE_HEADERS env_params.h MEMORY_INIT_FINALIZER_HEADERS - cooperate.h debug.h gparams.h prime_generator.h diff --git a/src/util/cooperate.cpp b/src/util/cooperate.cpp deleted file mode 100644 index 4a11cdb02..000000000 --- a/src/util/cooperate.cpp +++ /dev/null @@ -1,59 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - cooperate.cpp - -Abstract: - - Cooperation support - -Author: - - Leonardo (leonardo) 2011-05-17 - -Notes: - ---*/ - -#ifndef SINGLE_THREAD - -#include "util/cooperate.h" -#include "util/trace.h" -#include "util/debug.h" -#include -#include -#include - -static std::mutex* s_mux = nullptr; - -void initialize_cooperate() { - s_mux = new std::mutex(); -} -void finalize_cooperate() { - delete s_mux; -} - -static std::atomic owner_thread; - -bool cooperation_ctx::g_cooperate = false; - -void cooperation_ctx::checkpoint(char const * task) { - SASSERT(cooperation_ctx::enabled()); - - std::thread::id tid = std::this_thread::get_id(); - if (owner_thread == tid) { - owner_thread = std::thread::id(); - s_mux->unlock(); - } - - // this critical section is used to force the owner thread to give a chance to - // another thread to get the lock - std::this_thread::yield(); - s_mux->lock(); - TRACE("cooperate_detail", tout << task << ", tid: " << tid << "\n";); - owner_thread = tid; -} - -#endif diff --git a/src/util/cooperate.h b/src/util/cooperate.h deleted file mode 100644 index a8cb7e8e8..000000000 --- a/src/util/cooperate.h +++ /dev/null @@ -1,50 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - cooperate.h - -Abstract: - - Cooperation support - -Author: - - Leonardo (leonardo) 2011-05-17 - -Notes: - ---*/ -#pragma once - -#ifndef SINGLE_THREAD - -class cooperation_ctx { - static bool g_cooperate; -public: - static bool enabled() { return g_cooperate; } - static void checkpoint(char const * task); -}; - -inline void cooperate(char const * task) { - if (cooperation_ctx::enabled()) cooperation_ctx::checkpoint(task); -} - -void initialize_cooperate(); -void finalize_cooperate(); - -#else -inline void cooperate(char const *) {} -inline void initialize_cooperate() {} -inline void finalize_cooperate() {} - -#endif - - -/* - ADD_INITIALIZER('initialize_cooperate();') - ADD_FINALIZER('finalize_cooperate();') -*/ - -