mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #6582

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-02-13 13:20:55 -08:00
parent 2b77012993
commit 3dc91de531
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1745,6 +1745,13 @@ bool core::influences_nl_var(lpvar j) const {
return false; return false;
} }
void core::set_use_nra_model(bool m) {
if (m != m_use_nra_model) {
trail().push(value_trail(m_use_nra_model));
m_use_nra_model = m;
}
}
void core::collect_statistics(::statistics & st) { void core::collect_statistics(::statistics & st) {
st.update("arith-nla-explanations", m_stats.m_nla_explanations); st.update("arith-nla-explanations", m_stats.m_nla_explanations);
st.update("arith-nla-lemmas", m_stats.m_nla_lemmas); st.update("arith-nla-lemmas", m_stats.m_nla_lemmas);

2
src/math/lp/nla_core.h
View file

@ -418,7 +418,7 @@ public:
bool var_is_big(lpvar) const; bool var_is_big(lpvar) const;
bool has_real(const factorization&) const; bool has_real(const factorization&) const;
bool has_real(const monic& m) const; bool has_real(const monic& m) const;
void set_use_nra_model(bool m) { m_use_nra_model = m; } void set_use_nra_model(bool m);
bool use_nra_model() const { return m_use_nra_model; } bool use_nra_model() const { return m_use_nra_model; }
void collect_statistics(::statistics&); void collect_statistics(::statistics&);
private: private: