diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c8a82a323..8441901e1 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -204,27 +204,27 @@ set(Z3_API_HEADERS ) # Create custom target to copy headers -add_custom_target(z3_headers_copy ALL - COMMENT "Copying Z3 API headers to build include directory" -) - -foreach(header_file ${Z3_API_HEADERS}) - get_filename_component(header_name "${header_file}" NAME) - set(src_file "${CMAKE_CURRENT_SOURCE_DIR}/${header_file}") - set(dst_file "${Z3_BUILD_INCLUDE_DIR}/${header_name}") - - add_custom_command( - TARGET z3_headers_copy POST_BUILD - COMMAND ${CMAKE_COMMAND} -E copy_if_different - "${src_file}" - "${dst_file}" - COMMENT "Copying ${header_name} to include directory" - VERBATIM - ) -endforeach() +#add_custom_target(z3_headers_copy ALL +# COMMENT "Copying Z3 API headers to build include directory" +#) +# +#foreach(header_file ${Z3_API_HEADERS}) +# get_filename_component(header_name "${header_file}" NAME) +# set(src_file "${CMAKE_CURRENT_SOURCE_DIR}/${header_file}") +# set(dst_file "${Z3_BUILD_INCLUDE_DIR}/${header_name}") +# +# add_custom_command( +# TARGET z3_headers_copy POST_BUILD +# COMMAND ${CMAKE_COMMAND} -E copy_if_different +# "${src_file}" +# "${dst_file}" +# COMMENT "Copying ${header_name} to include directory" +# VERBATIM +# ) +#endforeach() # Make libz3 depend on header copying -add_dependencies(libz3 z3_headers_copy) +#add_dependencies(libz3 z3_headers_copy) # Update libz3 to also expose the build include directory target_include_directories(libz3 INTERFACE diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h index df0e25303..192480226 100644 --- a/src/math/lp/cross_nested.h +++ b/src/math/lp/cross_nested.h @@ -19,6 +19,8 @@ --*/ #pragma once #include +#include "util/util.h" +#include "util/rlimit.h" #include "math/lp/nex.h" #include "math/lp/nex_creator.h" @@ -26,10 +28,11 @@ namespace nla { class cross_nested { // fields + reslimit& m_limit; nex * m_e = nullptr; std::function m_call_on_result; std::function m_var_is_fixed; - std::function m_random; + random_gen m_random; bool m_done = false; ptr_vector m_b_split_vec; int m_reported = 0; @@ -45,11 +48,13 @@ public: cross_nested(std::function call_on_result, std::function var_is_fixed, - std::function random, - nex_creator& nex_cr) : + reslimit& limit, + unsigned random_seed, + nex_creator& nex_cr) : + m_limit(limit), m_call_on_result(call_on_result), m_var_is_fixed(var_is_fixed), - m_random(random), + m_random(random_seed), m_done(false), m_reported(0), m_mk_scalar([this]{return m_nex_creator.mk_scalar(rational(1));}), @@ -58,6 +63,7 @@ public: void run(nex *e) { + TRACE(nla_cn, tout << *e << "\n";); SASSERT(m_nex_creator.is_simplified(*e)); m_e = e; @@ -279,6 +285,8 @@ public: TRACE(nla_cn, tout << "m_e=" << *m_e << "\nc=" << **c << "\nj = " << nex_creator::ch(j) << "\nfront="; print_front(front, tout) << "\n";); if (!split_with_var(*c, j, front)) return; + if (!m_limit.inc()) + return; TRACE(nla_cn, tout << "after split c=" << **c << "\nfront="; print_front(front, tout) << "\n";); if (front.empty()) { #ifdef Z3DEBUG diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 2afad8980..89c528a9d 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -90,7 +90,9 @@ bool horner::lemmas_on_row(const T& row) { cross_nested cn( [this, dep](const nex* n) { return c().m_intervals.check_nex(n, dep); }, [this](unsigned j) { return c().var_is_fixed(j); }, - [this]() { return c().random(); }, m_nex_creator); + c().reslim(), + c().random(), + m_nex_creator); bool ret = lemmas_on_expr(cn, to_sum(e)); c().m_intervals.get_dep_intervals().reset(); // clean the memory allocated by the interval bound dependencies return ret; diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index a89707e45..42d6d8ef6 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -43,4 +43,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums(); m_dio_calls_period = lp_p.dio_calls_period(); m_dio_run_gcd = lp_p.dio_run_gcd(); + m_max_conflicts = p.max_conflicts(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 13288a214..d86b7d70e 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -103,6 +103,7 @@ struct statistics { unsigned m_make_feasible = 0; unsigned m_total_iterations = 0; unsigned m_iters_with_no_cost_growing = 0; + unsigned m_num_factorizations = 0; unsigned m_num_of_implied_bounds = 0; unsigned m_need_to_solve_inf = 0; unsigned m_max_cols = 0; @@ -136,47 +137,45 @@ struct statistics { unsigned m_bounds_tightening_conflicts = 0; unsigned m_bounds_tightenings = 0; unsigned m_nla_throttled_lemmas = 0; - unsigned m_nla_bounds_lemmas = 0; - unsigned m_nla_bounds_propagations = 0; + ::statistics m_st = {}; void reset() { *this = statistics{}; } void collect_statistics(::statistics& st) const { - st.update("arith-lp-make-feasible", m_make_feasible); - st.update("arith-lp-max-columns", m_max_cols); - st.update("arith-lp-max-rows", m_max_rows); - st.update("arith-lp-offset-eqs", m_offset_eqs); - st.update("arith-lp-fixed-eqs", m_fixed_eqs); - st.update("arith-lia-patches", m_patches); - st.update("arith-lia-patches-success", m_patches_success); - st.update("arith-lia-gcd-calls", m_gcd_calls); - st.update("arith-lia-gcd-conflict", m_gcd_conflicts); - st.update("arith-lia-cube-calls", m_cube_calls); - st.update("arith-lia-cube-success", m_cube_success); - st.update("arith-lia-hermite-calls", m_hnf_cutter_calls); - st.update("arith-lia-hermite-cuts", m_hnf_cuts); - st.update("arith-lia-gomory-cuts", m_gomory_cuts); - st.update("arith-lia-diophantine-calls", m_dio_calls); - st.update("arith-lia-diophantine-tighten-conflicts", m_dio_tighten_conflicts); - st.update("arith-lia-diophantine-rewrite-conflicts", m_dio_rewrite_conflicts); - st.update("arith-lia-bounds-tightening-conflicts", m_bounds_tightening_conflicts); - st.update("arith-lia-bounds-tightenings", m_bounds_tightenings); - st.update("arith-nla-horner-calls", m_horner_calls); - st.update("arith-nla-horner-conflicts", m_horner_conflicts); - st.update("arith-nla-horner-cross-nested-forms", m_cross_nested_forms); - st.update("arith-nla-grobner-calls", m_grobner_calls); - st.update("arith-nla-grobner-conflicts", m_grobner_conflicts); + st.update("arith-factorizations", m_num_factorizations); + st.update("arith-make-feasible", m_make_feasible); + st.update("arith-max-columns", m_max_cols); + st.update("arith-max-rows", m_max_rows); + st.update("arith-gcd-calls", m_gcd_calls); + st.update("arith-gcd-conflict", m_gcd_conflicts); + st.update("arith-cube-calls", m_cube_calls); + st.update("arith-cube-success", m_cube_success); + st.update("arith-patches", m_patches); + st.update("arith-patches-success", m_patches_success); + st.update("arith-hnf-calls", m_hnf_cutter_calls); + st.update("arith-hnf-cuts", m_hnf_cuts); + st.update("arith-gomory-cuts", m_gomory_cuts); + st.update("arith-horner-calls", m_horner_calls); + st.update("arith-horner-conflicts", m_horner_conflicts); + st.update("arith-horner-cross-nested-forms", m_cross_nested_forms); + st.update("arith-grobner-calls", m_grobner_calls); + st.update("arith-grobner-conflicts", m_grobner_conflicts); + st.update("arith-offset-eqs", m_offset_eqs); + st.update("arith-fixed-eqs", m_fixed_eqs); st.update("arith-nla-add-bounds", m_nla_add_bounds); st.update("arith-nla-propagate-bounds", m_nla_propagate_bounds); st.update("arith-nla-propagate-eq", m_nla_propagate_eq); st.update("arith-nla-lemmas", m_nla_lemmas); - st.update("arith-nla-nra-calls", m_nra_calls); - st.update("arith-nla-bounds-improvements", m_nla_bounds_improvements); + st.update("arith-nra-calls", m_nra_calls); + st.update("arith-bounds-improvements", m_nla_bounds_improvements); + st.update("arith-dio-calls", m_dio_calls); + st.update("arith-dio-tighten-conflicts", m_dio_tighten_conflicts); + st.update("arith-dio-rewrite-conflicts", m_dio_rewrite_conflicts); + st.update("arith-bounds-tightening-conflicts", m_bounds_tightening_conflicts); + st.update("arith-bounds-tightenings", m_bounds_tightenings); st.update("arith-nla-throttled-lemmas", m_nla_throttled_lemmas); - st.update("arith-nla-bounds-lemmas", m_nla_bounds_lemmas); - st.update("artih-nla-bounds-propagations", m_nla_bounds_propagations); st.copy(m_st); } }; @@ -223,11 +222,13 @@ public: unsigned percent_of_entering_to_check = 5; // we try to find a profitable column in a percentage of the columns bool use_scaling = true; unsigned max_number_of_iterations_with_no_improvements = 2000000; - double time_limit; // the maximum time limit of the total run time in seconds + double time_limit; // the maximum time limit of the total run time in seconds // end of dual section bool m_bound_propagation = true; bool presolve_with_double_solver_for_lar = true; simplex_strategy_enum m_simplex_strategy; + + unsigned m_max_conflicts = 0; int report_frequency = 1000; bool print_statistics = false; diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 3d947dbe8..66505c698 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -378,7 +378,6 @@ namespace nla { bool monomial_bounds::add_lemma() { if (c().lra.get_status() != lp::lp_status::INFEASIBLE) return false; - c().lp_settings().stats().m_nla_bounds_lemmas++; lp::explanation exp; c().lra.get_infeasibility_explanation(exp); lemma_builder lemma(c(), "propagate fixed - infeasible lra"); @@ -423,7 +422,6 @@ namespace nla { TRACE(nla_solver, tout << "propagate fixed " << m << " = 0, fixed_to_zero = " << fixed_to_zero << "\n";); c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, rational(0), dep); - c().lp_settings().stats().m_nla_bounds_propagations++; // propagate fixed equality auto exp = get_explanation(dep); c().add_fixed_equality(m.var(), rational(0), exp); @@ -433,7 +431,7 @@ namespace nla { auto* dep = explain_fixed(m, k); TRACE(nla_solver, tout << "propagate fixed " << m << " = " << k << "\n";); c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep); - c().lp_settings().stats().m_nla_bounds_propagations++; + // propagate fixed equality auto exp = get_explanation(dep); c().add_fixed_equality(m.var(), k, exp); @@ -450,7 +448,6 @@ namespace nla { if (k == 1) { lp::explanation exp = get_explanation(dep); - c().lp_settings().stats().m_nla_bounds_propagations++; c().add_equality(m.var(), w, exp); } } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 235274931..4253f55f1 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -39,7 +39,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : m_grobner(this), m_emons(m_evars), m_use_nra_model(false), - m_nra(s, m_nra_lim, *this), + m_nra(s, m_nra_lim, *this, p), m_throttle(lra.trail(), lra.settings().stats()) { m_nlsat_delay_bound = lp_settings().nlsat_delay(); @@ -1366,6 +1366,9 @@ lbool core::check() { if (no_effect() && params().arith_nl_nra()) { scoped_limits sl(m_reslim); sl.push_child(&m_nra_lim); + params_ref p; + p.set_uint("max_conflicts", lp_settings().m_max_conflicts); + m_nra.updt_params(p); ret = m_nra.check(); lp_settings().stats().m_nra_calls++; } @@ -1400,7 +1403,7 @@ lbool core::bounded_nlsat() { scoped_rlimit sr(m_nra_lim, 100000); ret = m_nra.check(); } - p.set_uint("max_conflicts", UINT_MAX); + p.set_uint("max_conflicts", lp_settings().m_max_conflicts); m_nra.updt_params(p); lp_settings().stats().m_nra_calls++; if (ret == l_undef)