mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 12:11:23 +00:00
Code Activity

add some nla statistics generate not more than one pl lemma an a rm monomial

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-07 15:35:04 -07:00
parent 4ba3ccfc99
commit a323eaf1c8
2 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_lra.cpp
View file

@ -116,6 +116,8 @@ struct stats {
unsigned m_bound_propagations2; unsigned m_bound_propagations2;
unsigned m_assert_diseq; unsigned m_assert_diseq;
unsigned m_gomory_cuts; unsigned m_gomory_cuts;
unsigned m_nla_explanations;
unsigned m_nla_lemmas;
stats() { reset(); } stats() { reset(); }
void reset() { void reset() {
memset(this, 0, sizeof(*this)); memset(this, 0, sizeof(*this));
@ -2146,9 +2148,11 @@ public:
lbool check_aftermath_nla(lbool r, const vector<nla::lemma>& lv) { lbool check_aftermath_nla(lbool r, const vector<nla::lemma>& lv) {
switch (r) { switch (r) {
case l_false: { case l_false: {
m_stats.m_nla_lemmas += lv.size();
for(const nla::lemma & l : lv) { for(const nla::lemma & l : lv) {
m_lemma = l; //todo avoit the copy m_lemma = l; //todo avoid the copy
m_explanation = l.expl(); m_explanation = l.expl();
m_stats.m_nla_explanations += l.expl().size();
false_case_of_check_nla(); false_case_of_check_nla();
} }
break; break;
@ -3761,7 +3765,8 @@ public:
st.update("arith-patches", lp().settings().st().m_patches); st.update("arith-patches", lp().settings().st().m_patches);
st.update("arith-patches-success", lp().settings().st().m_patches_success); st.update("arith-patches-success", lp().settings().st().m_patches_success);
st.update("arith-hnf-calls", lp().settings().st().m_hnf_cutter_calls); st.update("arith-hnf-calls", lp().settings().st().m_hnf_cutter_calls);
st.update("arith-hnf-cuts", lp().settings().st().m_hnf_cuts); st.update("nla-explanations", m_stats.m_nla_explanations);
st.update("nla-lemmas", m_stats.m_nla_lemmas);
} }
}; };

1
src/util/lp/nla_solver.cpp
View file

@ -1698,6 +1698,7 @@ struct solver::imp {
for (factor f : factorization) { for (factor f : factorization) {
if (abs(vvr(f)) > rmv) { if (abs(vvr(f)) > rmv) {
generate_pl(rm, factorization, factor_index); generate_pl(rm, factorization, factor_index);
return;
} }
factor_index++; factor_index++;
} }