mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity

disable nex grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-31 14:32:49 -08:00
parent f4165fe5cf
commit 2334ed5b66
4 changed files with 8 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/math/lp/nla_core.cpp
View file

@ -1288,25 +1288,9 @@ lbool core::inner_check(bool constraint_derived) {
if (need_to_call_algebraic_methods())
if (!m_horner.horner_lemmas()) {
clear_and_resize_active_var_set();
find_nl_cluster();
switch(m_nla_settings.run_grobner()) {
case nla_settings::NEX_AND_BDD_GROBNER:
init_nex_grobner(m_nex_grobner.get_nex_creator());
m_nex_grobner.grobner_lemmas();
if (m_nla_settings.run_grobner()) {
find_nl_cluster();
run_pdd_grobner();
break;
case nla_settings::NEX_GROBNER:
init_nex_grobner(m_nex_grobner.get_nex_creator());
m_nex_grobner.grobner_lemmas();
break;
case nla_settings::PDD_GROBNER:
run_pdd_grobner();
break;
case nla_settings::NO_GROBNER:
break;
default:
UNREACHABLE();
break;
}
}
if (done()) {