port improvements from ilana branch to master regarding nla

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/CMakeLists.txt

@@ -204,27 +204,27 @@ set(Z3_API_HEADERS
 )
 
 # Create custom target to copy headers
-add_custom_target(z3_headers_copy ALL
+#add_custom_target(z3_headers_copy ALL
-  COMMENT "Copying Z3 API headers to build include directory"
+#  COMMENT "Copying Z3 API headers to build include directory"
-)
+#)
-
+#
-foreach(header_file ${Z3_API_HEADERS})
+#foreach(header_file ${Z3_API_HEADERS})
-  get_filename_component(header_name "${header_file}" NAME)
+#  get_filename_component(header_name "${header_file}" NAME)
-  set(src_file "${CMAKE_CURRENT_SOURCE_DIR}/${header_file}")
+#  set(src_file "${CMAKE_CURRENT_SOURCE_DIR}/${header_file}")
-  set(dst_file "${Z3_BUILD_INCLUDE_DIR}/${header_name}")
+#  set(dst_file "${Z3_BUILD_INCLUDE_DIR}/${header_name}")
-
+#
-  add_custom_command(
+#  add_custom_command(
-    TARGET z3_headers_copy POST_BUILD
+#    TARGET z3_headers_copy POST_BUILD
-    COMMAND ${CMAKE_COMMAND} -E copy_if_different
+#    COMMAND ${CMAKE_COMMAND} -E copy_if_different
-            "${src_file}"
+#            "${src_file}"
-            "${dst_file}"
+#            "${dst_file}"
-    COMMENT "Copying ${header_name} to include directory"
+#    COMMENT "Copying ${header_name} to include directory"
-    VERBATIM
+#    VERBATIM
-  )
+#  )
-endforeach()
+#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

src/math/lp/cross_nested.h

@@ -19,6 +19,8 @@
   --*/
 #pragma once
 #include <functional>
+#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<bool (const nex*)>                  m_call_on_result;
     std::function<bool (unsigned)>                    m_var_is_fixed;
-    std::function<unsigned ()>                        m_random;    
+    random_gen                                        m_random;
     bool                                              m_done = false;
     ptr_vector<nex>                                   m_b_split_vec;
     int                                               m_reported = 0;
@@ -45,11 +48,13 @@ public:
     
     cross_nested(std::function<bool (const nex*)> call_on_result,
                  std::function<bool (unsigned)> var_is_fixed,
-                 std::function<unsigned ()> random,
+                 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

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;

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();
 }

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-factorizations", m_num_factorizations);
-        st.update("arith-lp-max-columns", m_max_cols);
+        st.update("arith-make-feasible", m_make_feasible);
-        st.update("arith-lp-max-rows", m_max_rows);
+        st.update("arith-max-columns", m_max_cols);
-        st.update("arith-lp-offset-eqs", m_offset_eqs);
+        st.update("arith-max-rows", m_max_rows);
-        st.update("arith-lp-fixed-eqs", m_fixed_eqs);
+        st.update("arith-gcd-calls", m_gcd_calls);
-        st.update("arith-lia-patches", m_patches);
+        st.update("arith-gcd-conflict", m_gcd_conflicts);
-        st.update("arith-lia-patches-success", m_patches_success);
+        st.update("arith-cube-calls", m_cube_calls);
-        st.update("arith-lia-gcd-calls", m_gcd_calls);
+        st.update("arith-cube-success", m_cube_success);
-        st.update("arith-lia-gcd-conflict", m_gcd_conflicts);
+        st.update("arith-patches", m_patches);
-        st.update("arith-lia-cube-calls", m_cube_calls);
+        st.update("arith-patches-success", m_patches_success);
-        st.update("arith-lia-cube-success", m_cube_success);
+        st.update("arith-hnf-calls", m_hnf_cutter_calls);
-        st.update("arith-lia-hermite-calls", m_hnf_cutter_calls);
+        st.update("arith-hnf-cuts", m_hnf_cuts);
-        st.update("arith-lia-hermite-cuts", m_hnf_cuts);
+        st.update("arith-gomory-cuts", m_gomory_cuts);
-        st.update("arith-lia-gomory-cuts", m_gomory_cuts);
+        st.update("arith-horner-calls", m_horner_calls);
-        st.update("arith-lia-diophantine-calls", m_dio_calls);
+        st.update("arith-horner-conflicts", m_horner_conflicts);
-        st.update("arith-lia-diophantine-tighten-conflicts", m_dio_tighten_conflicts);
+        st.update("arith-horner-cross-nested-forms", m_cross_nested_forms);
-        st.update("arith-lia-diophantine-rewrite-conflicts", m_dio_rewrite_conflicts);
+        st.update("arith-grobner-calls", m_grobner_calls);
-        st.update("arith-lia-bounds-tightening-conflicts", m_bounds_tightening_conflicts);
+        st.update("arith-grobner-conflicts", m_grobner_conflicts);
-        st.update("arith-lia-bounds-tightenings", m_bounds_tightenings);
+        st.update("arith-offset-eqs", m_offset_eqs);
-        st.update("arith-nla-horner-calls", m_horner_calls);
+        st.update("arith-fixed-eqs", m_fixed_eqs);
-        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-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-nra-calls", m_nra_calls);   
-        st.update("arith-nla-bounds-improvements", m_nla_bounds_improvements);
+        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,12 +222,14 @@ 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;
     unsigned         column_norms_update_frequency = 12000;

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);
         }
     }

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)