From 82fd2a062dc3859c44ee005d421eed0dc2fb3369 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 15 May 2020 12:16:40 -0700 Subject: [PATCH] make calling nra from nla optional Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 4 +--- src/math/lp/nla_settings.h | 7 ++++++- src/smt/params/smt_params_helper.pyg | 1 + src/smt/theory_lra.cpp | 1 + 4 files changed, 9 insertions(+), 4 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 94371039b..0a3da1a64 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1474,10 +1474,8 @@ lbool core::check(vector& l_vec) { m_tangents.tangent_lemma(); } -#if 0 - if (false && l_vec.empty() && !done()) + if (l_vec.empty() && !done() && m_nla_settings.run_nra()) ret = m_nra.check(); -#endif if (ret == l_undef && !l_vec.empty() && m_reslim.inc()) ret = l_false; diff --git a/src/math/lp/nla_settings.h b/src/math/lp/nla_settings.h index 4ba271afb..e51dc19e0 100644 --- a/src/math/lp/nla_settings.h +++ b/src/math/lp/nla_settings.h @@ -28,6 +28,7 @@ class nla_settings { unsigned m_grobner_max_simplified; unsigned m_grobner_number_of_conflicts_to_report; unsigned m_grobner_quota; + bool m_run_nra; public: nla_settings() : m_run_order(true), m_run_tangents(true), @@ -38,7 +39,8 @@ public: m_run_grobner(true), m_grobner_row_length_limit(50), m_grobner_subs_fixed(false), - m_grobner_quota(0) + m_grobner_quota(0), + m_run_nra(false) {} unsigned grobner_eqs_growth() const { return m_grobner_eqs_growth;} unsigned& grobner_eqs_growth() { return m_grobner_eqs_growth;} @@ -61,6 +63,9 @@ public: bool run_grobner() const { return m_run_grobner; } bool& run_grobner() { return m_run_grobner; } + bool run_nra() const { return m_run_nra; } + bool& run_nra() { return m_run_nra; } + unsigned grobner_row_length_limit() const { return m_grobner_row_length_limit; } unsigned& grobner_row_length_limit() { return m_grobner_row_length_limit; } unsigned grobner_subs_fixed() const { return m_grobner_subs_fixed; } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 5c1ac5d9d..9359ceed3 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -44,6 +44,7 @@ def_module_params(module_name='smt', ('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, 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.nra', BOOL, False, 'call nra_solver when incremental lianirization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'), ('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'), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0d7623615..bbb16723b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -407,6 +407,7 @@ class theory_lra::imp { m_nla->settings().horner_frequency() = prms.arith_nl_horner_frequency(); m_nla->settings().horner_row_length_limit() = prms.arith_nl_horner_row_length_limit(); m_nla->settings().run_grobner() = prms.arith_nl_grobner(); + m_nla->settings().run_nra() = prms.arith_nl_nra(); m_nla->settings().grobner_subs_fixed() = prms.arith_nl_grobner_subs_fixed(); m_nla->settings().grobner_eqs_growth() = prms.arith_nl_grobner_eqs_growth(); m_nla->settings().grobner_expr_size_growth() = prms.arith_nl_grobner_expr_size_growth();