use param_ref in nla_solver (#6862)

* use param_ref in nla_solver

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* add parameters

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

* add parameters

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

* replace nla_setting by command line parameters

* delete nla_setting.h

---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/lp/horner.cpp

@@ -40,7 +40,7 @@ bool horner::row_has_monomial_to_refine(const T& row) const {
 template <typename T>
 bool horner::row_is_interesting(const T& row) const {
     TRACE("nla_solver_details", c().print_row(row, tout););
-    if (row.size() > c().m_nla_settings.horner_row_length_limit) {
+    if (row.size() > c().params().arith_nl_horner_row_length_limit()) {
         TRACE("nla_solver_details", tout << "disregard\n";);
         return false;
     }
@@ -98,7 +98,7 @@ bool horner::lemmas_on_row(const T& row) {
 }
 
 bool horner::horner_lemmas() {
-    if (!c().m_nla_settings.run_horner) {
+    if (!c().params().arith_nl_horner()) {
         TRACE("nla_solver", tout << "not generating horner lemmas\n";);
         return false;
     }

src/math/lp/nla_common.cpp

@@ -71,11 +71,11 @@ void common::add_deps_of_fixed(lpvar j, u_dependency*& dep) {
 // creates a nex expression for the coeff and var, 
 nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, u_dependency*& dep) {
     SASSERT(!coeff.is_zero());
-    if (c().m_nla_settings.horner_subs_fixed == 1 && c().var_is_fixed(j)) {
+    if (c().params().arith_nl_horner_subs_fixed() == 1 && c().var_is_fixed(j)) {
         add_deps_of_fixed(j, dep);
         return cn.mk_scalar(coeff * c().m_lar_solver.column_lower_bound(j).x);
     }
-    if (c().m_nla_settings.horner_subs_fixed == 2 && c().var_is_fixed_to_zero(j)) {
+    if (c().params().arith_nl_horner_subs_fixed() == 2 && c().var_is_fixed_to_zero(j)) {
         add_deps_of_fixed(j, dep);
         return cn.mk_scalar(rational(0));
     }
@@ -89,10 +89,10 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, u_depende
     mf *= coeff;
     u_dependency * initial_dep = dep;
     for (lpvar k : m.vars()) {
-        if (c().m_nla_settings.horner_subs_fixed == 1 && c().var_is_fixed(k)) {
+        if (c().params().arith_nl_horner_subs_fixed() == 1 && c().var_is_fixed(k)) {
             add_deps_of_fixed(k, dep);
             mf *= c().m_lar_solver.column_lower_bound(k).x;
-        } else if (c().m_nla_settings.horner_subs_fixed == 2 &&
+        } else if (c().params().arith_nl_horner_subs_fixed() == 2 &&
                    c().var_is_fixed_to_zero(k)) {
             dep = initial_dep;
             add_deps_of_fixed(k, dep);

src/math/lp/nla_core.cpp

@@ -21,10 +21,11 @@ namespace nla {
 
 typedef lp::lar_term term;
 
-core::core(lp::lar_solver& s, reslimit & lim) :
+core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
     m_evars(),
     m_lar_solver(s),
     m_reslim(lim),
+    m_params(p),
     m_tangents(this),
     m_basics(this),
     m_order(this),
@@ -1428,7 +1429,7 @@ void core::patch_monomials_on_to_refine() {
 void core::patch_monomials() {
     m_cautious_patching = true;
     patch_monomials_on_to_refine();
-    if (m_to_refine.size() == 0 || !m_nla_settings.expensive_patching) {
+    if (m_to_refine.size() == 0 || !params().arith_nl_expensive_patching()) {
         return;
     }
     NOT_IMPLEMENTED_YET();
@@ -1566,11 +1567,11 @@ lbool core::check(vector<lemma>& l_vec) {
         check_weighted(3, checks);
 
         unsigned num_calls = lp_settings().stats().m_nla_calls;
-        if (!conflict_found() && m_nla_settings.run_nra && num_calls % 50 == 0 && num_calls > 500) 
+        if (!conflict_found() && params().arith_nl_nra() && num_calls % 50 == 0 && num_calls > 500) 
             ret = bounded_nlsat();
     }
 
-    if (l_vec.empty() && !done() && m_nla_settings.run_nra && ret == l_undef) {
+    if (l_vec.empty() && !done() && params().arith_nl_nra() && ret == l_undef) {
         ret = m_nra.check();
         m_stats.m_nra_calls++;
     }
@@ -1590,7 +1591,7 @@ lbool core::check(vector<lemma>& l_vec) {
 }
 
 bool core::should_run_bounded_nlsat() {
-    if (!m_nla_settings.run_nra)
+    if (!params().arith_nl_nra())
         return false;
     if (m_nlsat_delay > m_nlsat_fails)
         ++m_nlsat_fails;

src/math/lp/nla_core.h

@@ -22,12 +22,12 @@
 #include "math/lp/nla_powers.h"
 #include "math/lp/nla_divisions.h"
 #include "math/lp/emonics.h"
-#include "math/lp/nla_settings.h"
 #include "math/lp/nex.h"
 #include "math/lp/horner.h"
 #include "math/lp/monomial_bounds.h"
 #include "math/lp/nla_intervals.h"
 #include "nlsat/nlsat_solver.h"
+#include "smt/params/smt_params_helper.hpp"
 
 namespace nra {
     class solver;
@@ -54,7 +54,6 @@ class core {
     friend struct tangents;
     friend class monotone;
     friend class powers;
-    friend struct nla_settings;
     friend class intervals;
     friend class horner;
     friend class solver;
@@ -82,6 +81,7 @@ class core {
 
     lp::lar_solver&          m_lar_solver;
     reslimit&                m_reslim;
+    smt_params_helper        m_params;
     std::function<bool(lpvar)> m_relevant;
     vector<lemma> *          m_lemma_vec;
     indexed_uint_set                m_to_refine;
@@ -93,8 +93,7 @@ class core {
     divisions                m_divisions;
     intervals                m_intervals; 
     monomial_bounds          m_monomial_bounds;
-    nla_settings             m_nla_settings;        
-
+    
     horner                   m_horner;
     grobner                  m_grobner;
     emonics                  m_emons;
@@ -113,7 +112,7 @@ class core {
 
 public:    
     // constructor
-    core(lp::lar_solver& s, reslimit&);
+    core(lp::lar_solver& s, params_ref const& p, reslimit&);
 
     void insert_to_refine(lpvar j);
     void erase_from_to_refine(lpvar j);
@@ -165,13 +164,15 @@ public:
     
     lpvar var(const factor& f) const { return f.var(); }
 
+    smt_params_helper const & params() const { return m_params; }
+
     // returns true if the combination of the Horner's schema and Grobner Basis should be called
     bool need_run_horner() const { 
-        return m_nla_settings.run_horner && lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency == 0; 
+        return params().arith_nl_horner() && lp_settings().stats().m_nla_calls % params().arith_nl_horner_frequency() == 0; 
     }
 
     bool need_run_grobner() const { 
-        return m_nla_settings.run_grobner && lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency == 0; 
+        return params().arith_nl_grobner() && lp_settings().stats().m_nla_calls % params().arith_nl_grobner_frequency() == 0; 
     }
 
     void set_active_vars_weights(nex_creator&);

src/math/lp/nla_grobner.cpp

@@ -24,8 +24,8 @@ namespace nla {
         common(c),
         m_pdd_manager(m_core.m_lar_solver.number_of_vars()),
         m_solver(m_core.m_reslim, m_pdd_manager),
-        m_lar_solver(m_core.m_lar_solver)
-
+        m_lar_solver(m_core.m_lar_solver),
+        m_quota(m_core.params().arith_nl_gr_q())
     {}
 
     lp::lp_settings& grobner::lp_settings() {
@@ -33,8 +33,10 @@ namespace nla {
     }
 
     void grobner::operator()() {
-        unsigned& quota = c().m_nla_settings.grobner_quota;
-        if (quota == 1)
+        if (m_quota == 0)
+            m_quota = c().params().arith_nl_gr_q();                    
+
+        if (m_quota == 1)
             return;
 
         lp_settings().stats().m_grobner_calls++;
@@ -59,12 +61,14 @@ namespace nla {
             
         }
 
-        if (quota > 1)
-            quota--;
+        if (m_quota > 0)
+           --m_quota;
 
-        IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << quota << "\n");
+        IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
         IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
 
+
+
 #if 0
         // diagnostics: did we miss something
         vector<dd::pdd> eqs;
@@ -239,11 +243,11 @@ namespace nla {
    
         struct dd::solver::config cfg;
         cfg.m_max_steps = m_solver.equations().size();
-        cfg.m_max_simplified = c().m_nla_settings.grobner_max_simplified;
-        cfg.m_eqs_growth = c().m_nla_settings.grobner_eqs_growth;
-        cfg.m_expr_size_growth = c().m_nla_settings.grobner_expr_size_growth;
-        cfg.m_expr_degree_growth = c().m_nla_settings.grobner_expr_degree_growth;
-        cfg.m_number_of_conflicts_to_report = c().m_nla_settings.grobner_number_of_conflicts_to_report;
+        cfg.m_max_simplified = c().params().arith_nl_grobner_max_simplified();
+        cfg.m_eqs_growth = c().params().arith_nl_grobner_eqs_growth();
+        cfg.m_expr_size_growth = c().params().arith_nl_grobner_expr_size_growth();
+        cfg.m_expr_degree_growth = c().params().arith_nl_grobner_expr_degree_growth();
+        cfg.m_number_of_conflicts_to_report = c().params().arith_nl_grobner_cnfl_to_report();
         m_solver.set(cfg);
         m_solver.adjust_cfg();
         m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
@@ -348,9 +352,9 @@ namespace nla {
             unsigned k = m_lar_solver.get_base_column_in_row(row);
             if (m_lar_solver.column_is_free(k) && k != j)
                 continue;
-            CTRACE("grobner", matrix.m_rows[row].size() > c().m_nla_settings.grobner_row_length_limit,
+            CTRACE("grobner", matrix.m_rows[row].size() > c().params().arith_nl_grobner_row_length_limit(),
                    tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";); 
-            if (matrix.m_rows[row].size() > c().m_nla_settings.grobner_row_length_limit)
+            if (matrix.m_rows[row].size() > c().params().arith_nl_horner_row_length_limit())
                 continue;
             for (auto& rc : matrix.m_rows[row]) 
                 add_var_and_its_factors_to_q_and_collect_new_rows(rc.var(), q);
@@ -373,12 +377,12 @@ namespace nla {
         while (!vars.empty()) {
             j = vars.back();
             vars.pop_back();
-            if (c().m_nla_settings.grobner_subs_fixed > 0 && c().var_is_fixed_to_zero(j)) {
+            if (c().params().arith_nl_grobner_subs_fixed() > 0 && c().var_is_fixed_to_zero(j)) {
                 r = m_pdd_manager.mk_val(val_of_fixed_var_with_deps(j, zero_dep));
                 dep = zero_dep;
                 return r;
             }
-            if (c().m_nla_settings.grobner_subs_fixed == 1 && c().var_is_fixed(j))
+            if (c().params().arith_nl_grobner_subs_fixed() == 1 && c().var_is_fixed(j))
                 r *= val_of_fixed_var_with_deps(j, dep);
             else if (!c().is_monic_var(j))
                 r *= m_pdd_manager.mk_var(j);

src/math/lp/nla_grobner.h

@@ -22,7 +22,8 @@ namespace nla {
         dd::pdd_manager          m_pdd_manager;
         dd::solver               m_solver;
         lp::lar_solver&          m_lar_solver;
-        indexed_uint_set                m_rows;
+        indexed_uint_set         m_rows;
+        unsigned                 m_quota = 0;
 
         lp::lp_settings& lp_settings();
 

src/math/lp/nla_order_lemmas.cpp

@@ -19,7 +19,7 @@ typedef lp::lar_term term;
 // a > b && c > 0 => ac > bc
 void order::order_lemma() {
     TRACE("nla_solver", );
-    if (!c().m_nla_settings.run_order) {
+    if (!c().params().arith_nl_order()) {
         TRACE("nla_solver", tout << "not generating order lemmas\n";);
         return;
     }

src/math/lp/nla_settings.h

@@ -1,46 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Author:
-
-    Lev Nachmanson (levnach)
-
---*/
-
-#pragma once
-namespace nla {
-    struct nla_settings {
-        bool     run_order     = true;
-        bool     run_tangents  = true;
-        
-        // horner fields
-        bool     run_horner              = true;
-        unsigned horner_frequency        = 4;
-        unsigned horner_row_length_limit = 10;
-        unsigned horner_subs_fixed       = 2;
-
-        
-        // grobner fields
-        bool     run_grobner                = true;
-        unsigned grobner_row_length_limit   = 50;
-        unsigned grobner_subs_fixed         = 1;
-        unsigned grobner_eqs_growth         = 10;
-        unsigned grobner_tree_size_growth   = 2;
-        unsigned grobner_expr_size_growth   = 2;
-        unsigned grobner_expr_degree_growth = 2;
-        unsigned grobner_max_simplified     = 10000;
-        unsigned grobner_number_of_conflicts_to_report = 1;
-        unsigned grobner_quota      = 0;
-        unsigned grobner_frequency  = 4;
-
-
-        // nra fields
-        bool     run_nra = false;
-    
-        // expensive patching
-        bool     expensive_patching = false;
-
-        nla_settings() {}
-
-    };
-}

src/math/lp/nla_solver.cpp

@@ -16,9 +16,6 @@
 #include "math/polynomial/algebraic_numbers.h"
 
 namespace nla {
-
-    nla_settings& solver::settings() { return m_core->m_nla_settings; }
-
     void solver::add_monic(lpvar v, unsigned sz, lpvar const* vs) {
         m_core->add_monic(v, sz, vs);
     }
@@ -57,8 +54,8 @@ namespace nla {
         m_core->pop(n);
     }
     
-    solver::solver(lp::lar_solver& s, reslimit& limit): 
-        m_core(alloc(core, s, limit)) {
+    solver::solver(lp::lar_solver& s, params_ref const& p, reslimit& limit): 
+        m_core(alloc(core, s, p, limit)) {
     }
     
     bool solver::influences_nl_var(lpvar j) const {    

src/math/lp/nla_solver.h

@@ -13,7 +13,6 @@ Author:
 #include "util/params.h"
 #include "math/lp/lar_solver.h"
 #include "math/lp/monic.h"
-#include "math/lp/nla_settings.h"
 #include "math/lp/nla_core.h"
 namespace nra {
     class solver;
@@ -25,7 +24,7 @@ namespace nla {
         core* m_core;
     public:
 
-        solver(lp::lar_solver& s, reslimit& limit);
+        solver(lp::lar_solver& s, params_ref const& p, reslimit& limit);
         ~solver();
 
         void add_monic(lpvar v, unsigned sz, lpvar const* vs);
@@ -34,7 +33,6 @@ namespace nla {
         void add_bounded_division(lpvar q, lpvar x, lpvar y);
         void check_bounded_divisions(vector<lemma>&);
         void set_relevant(std::function<bool(lpvar)>& is_relevant);
-        nla_settings& settings();
         void push();
         void pop(unsigned scopes);
         bool need_check();

src/math/lp/nla_tangent_lemmas.cpp

@@ -186,7 +186,7 @@ tangents::tangents(core * c) : common(c) {}
 void tangents::tangent_lemma() {
     factorization bf(nullptr);
     const monic* m = nullptr;
-    if (c().m_nla_settings.run_tangents && c().find_bfc_to_refine(m, bf)) {
+    if (c().params().arith_nl_tangents() && c().find_bfc_to_refine(m, bf)) {
         lpvar j = m->var();
         tangent_imp tangent(point(val(bf[0]), val(bf[1])), c().val(j), *m, bf, *this);
         tangent();