From c3099a57190a0735e0ecef2f9ab2d587a9e74e66 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Dec 2019 11:13:00 -0800 Subject: [PATCH] call algebraic routines only basing on the frequency Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.h | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index cfa643bb9..9ef0d88db 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -148,10 +148,9 @@ public: // returns true if the combination of the Horner's schema and Grobner Basis should be called bool need_to_call_algebraic_methods() const { return - lp_settings().stats().m_nla_calls < 20 || lp_settings().stats().m_nla_calls % m_nla_settings.horner_frequency() == 0; - } - + } + lbool incremental_linearization(bool); svector sorted_rvars(const factor& f) const;