From 514c3d7a3b9ad3c6d4451770cc0cb709317c2199 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 10 Feb 2020 11:08:35 -0800 Subject: [PATCH] move the content of nla_params.pyg to smt_params_helper.pyg Signed-off-by: Lev Nachmanson --- src/math/lp/CMakeLists.txt | 1 - src/math/lp/nla_params.pyg | 22 -------------------- src/smt/params/smt_params_helper.pyg | 22 ++++++++++++++++---- src/smt/theory_lra.cpp | 31 ++++++++++++++-------------- 4 files changed, 33 insertions(+), 43 deletions(-) delete mode 100644 src/math/lp/nla_params.pyg diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index 7edfe69ca..39cb39985 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -53,7 +53,6 @@ z3_add_component(lp nlsat PYG_FILES lp_params.pyg - nla_params.pyg ) include_directories(${src_SOURCE_DIR}) diff --git a/src/math/lp/nla_params.pyg b/src/math/lp/nla_params.pyg deleted file mode 100644 index 024dc146b..000000000 --- a/src/math/lp/nla_params.pyg +++ /dev/null @@ -1,22 +0,0 @@ -def_module_params('nla', - export=True, - description='Parameters for non-linear arithmetic solving', - params=( - ('order', BOOL, True, 'run order lemmas'), - ('tangents', BOOL, True, 'run tangent lemmas'), - ('horner', BOOL, True, 'run horner\'s heuristic'), - ('horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), - ('horner_frequency', UINT, 4, 'horner\'s call frequency'), - ('horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'), - ('grobner', BOOL, True, 'run grobner\'s basis heuristic'), - ('grobner_eqs_growth', UINT, 10, 'grobner\'s number of equalities growth '), - ('grobner_expr_size_growth', UINT, 2, 'grobner\'s maximum expr size growth'), - ('grobner_expr_degree_growth', UINT, 2, 'grobner\'s maximum expr degree growth'), - ('grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'), - ('grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), - ('gr_q', UINT, 10, 'grobner\'s quota'), - ('grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only') - )) - - - diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index cc9b44321..0f9df8680 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -41,10 +41,24 @@ def_module_params(module_name='smt', ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), - ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'), - ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false'), - ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'), - ('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic'), + ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), + ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=2'), + ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2'), + ('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'), + ('arith.nl.order', BOOL, True, 'run order lemmas'), + ('arith.nl.tangents', BOOL, True, 'run tangent lemmas'), + ('arith.nl.horner', BOOL, True, 'run horner\'s heuristic'), + ('arith.nl.horner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), + ('arith.nl.horner_frequency', UINT, 4, 'horner\'s call frequency'), + ('arith.nl.horner_row_length_limit', UINT, 10, 'row is disregarded by the heuristic if its length is longer than the value'), + ('arith.nl.grobner', BOOL, True, 'run grobner\'s basis heuristic'), + ('arith.nl.grobner_eqs_growth', UINT, 10, 'grobner\'s number of equalities growth '), + ('arith.nl.grobner_expr_size_growth', UINT, 2, 'grobner\'s maximum expr size growth'), + ('arith.nl.grobner_expr_degree_growth', UINT, 2, 'grobner\'s maximum expr degree growth'), + ('arith.nl.grobner_max_simplified', UINT, 10000, 'grobner\'s maximum number of simplifications'), + ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), + ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), + ('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), ('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 245111818..7957435ed 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -456,23 +456,22 @@ class theory_lra::imp { (void)_s; m_nla->push(); } - nla_params nla(ctx().get_params()); - m_nla->get_core()->m_nla_settings.run_order() = nla.order(); - m_nla->get_core()->m_nla_settings.run_tangents() = nla.tangents(); - m_nla->get_core()->m_nla_settings.run_horner() = nla.horner(); - m_nla->get_core()->m_nla_settings.horner_subs_fixed() = nla.horner_subs_fixed(); - - m_nla->get_core()->m_nla_settings.horner_frequency() = nla.horner_frequency(); - m_nla->get_core()->m_nla_settings.horner_row_length_limit() = nla.horner_row_length_limit(); - m_nla->get_core()->m_nla_settings.run_grobner() = nla.grobner(); - m_nla->get_core()->m_nla_settings.grobner_subs_fixed() = nla.grobner_subs_fixed(); - m_nla->get_core()->m_nla_settings.grobner_eqs_growth() = nla.grobner_eqs_growth(); - m_nla->get_core()->m_nla_settings.grobner_expr_size_growth() = nla.grobner_expr_size_growth(); - m_nla->get_core()->m_nla_settings.grobner_expr_degree_growth() = nla.grobner_expr_degree_growth(); - m_nla->get_core()->m_nla_settings.grobner_max_simplified() = nla.grobner_max_simplified(); - m_nla->get_core()->m_nla_settings.grobner_number_of_conflicts_to_report() = nla.grobner_cnfl_to_report(); - m_nla->get_core()->m_grobner_quota = nla.gr_q(); + smt_params_helper prms(ctx().get_params()); + m_nla->get_core()->m_nla_settings.run_order() = prms.arith_nl_order(); + m_nla->get_core()->m_nla_settings.run_tangents() = prms.arith_nl_tangents(); + m_nla->get_core()->m_nla_settings.run_horner() = prms.arith_nl_horner(); + m_nla->get_core()->m_nla_settings.horner_subs_fixed() = prms.arith_nl_horner_subs_fixed(); + m_nla->get_core()->m_nla_settings.horner_frequency() = prms.arith_nl_horner_frequency(); + m_nla->get_core()->m_nla_settings.horner_row_length_limit() = prms.arith_nl_horner_row_length_limit(); + m_nla->get_core()->m_nla_settings.run_grobner() = prms.arith_nl_grobner(); + m_nla->get_core()->m_nla_settings.grobner_subs_fixed() = prms.arith_nl_grobner_subs_fixed(); + m_nla->get_core()->m_nla_settings.grobner_eqs_growth() = prms.arith_nl_grobner_eqs_growth(); + m_nla->get_core()->m_nla_settings.grobner_expr_size_growth() = prms.arith_nl_grobner_expr_size_growth(); + m_nla->get_core()->m_nla_settings.grobner_expr_degree_growth() = prms.arith_nl_grobner_expr_degree_growth(); + m_nla->get_core()->m_nla_settings.grobner_max_simplified() = prms.arith_nl_grobner_max_simplified(); + m_nla->get_core()->m_nla_settings.grobner_number_of_conflicts_to_report() = prms.arith_nl_grobner_cnfl_to_report(); + m_nla->get_core()->m_grobner_quota = prms.arith_nl_gr_q(); } }