mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

fix in emonomials

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-30 12:50:11 -07:00
parent 25edc98f36
commit b32f2703d4
4 changed files with 0 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_context_pp.cpp
View file

@ -493,7 +493,6 @@ namespace smt {
TRACE("lemma", tout << strm.str() << "\n";); TRACE("lemma", tout << strm.str() << "\n";);
display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic); display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
out.close(); out.close();
if (m_lemma_id==6998) exit(0);
return m_lemma_id; return m_lemma_id;
} }

4
src/util/lp/emonomials.cpp
View file

@ -150,7 +150,6 @@ monomial const* emonomials::find_canonical(svector<lpvar> const& vars) const {
void emonomials::remove_cg(lpvar v) { void emonomials::remove_cg(lpvar v) {
cell* c = m_use_lists[v].m_head; cell* c = m_use_lists[v].m_head;
CTRACE("nla_solver", v == 14, tout << c << "\n";);
if (c == nullptr) { if (c == nullptr) {
return; return;
} }
@ -160,7 +159,6 @@ void emonomials::remove_cg(lpvar v) {
unsigned idx = c->m_index; unsigned idx = c->m_index;
c = c->m_next; c = c->m_next;
monomial & m = m_monomials[idx]; monomial & m = m_monomials[idx];
CTRACE("nla_solver", v == 14, tout << m << "\n";);
if (!is_visited(m)) { if (!is_visited(m)) {
set_visited(m); set_visited(m);
remove_cg(idx, m); remove_cg(idx, m);
@ -201,7 +199,6 @@ void emonomials::remove_cg(unsigned idx, monomial& m) {
*/ */
void emonomials::insert_cg(lpvar v) { void emonomials::insert_cg(lpvar v) {
cell* c = m_use_lists[v].m_head; cell* c = m_use_lists[v].m_head;
CTRACE("nla_solver", v == 14, tout << c << "\n";);
if (c == nullptr) { if (c == nullptr) {
return; return;
@ -213,7 +210,6 @@ void emonomials::insert_cg(lpvar v) {
unsigned idx = c->m_index; unsigned idx = c->m_index;
c = c->m_next; c = c->m_next;
monomial & m = m_monomials[idx]; monomial & m = m_monomials[idx];
CTRACE("nla_solver", v == 14, tout << m << "\n";);
if (!is_visited(m)) { if (!is_visited(m)) {
set_visited(m); set_visited(m);
insert_cg(idx, m); insert_cg(idx, m);

2
src/util/lp/nla_core.cpp
View file

@ -112,9 +112,7 @@ void core::push() {
void core::pop(unsigned n) { void core::pop(unsigned n) {
TRACE("nla_solver", tout << "n = " << n << "\n";); TRACE("nla_solver", tout << "n = " << n << "\n";);
TRACE("nla_solver", tout << "before pop mons = " << pp_emons(*this, m_emons) << "\n";);
m_emons.pop(n); m_emons.pop(n);
TRACE("nla_solver", tout << "after pop mons = " << pp_emons(*this, m_emons) << "\n";);
} }
rational core::product_value(const unsigned_vector & m) const { rational core::product_value(const unsigned_vector & m) const {

2
src/util/lp/var_eqs.cpp
View file

@ -120,8 +120,6 @@ void var_eqs::explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) cons
} }
void var_eqs::explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) const { void var_eqs::explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) const {
static int ddd=0;
TRACE("nla_solver", tout << ++ddd << "\n";);
SASSERT(find(v1) == find(v2)); SASSERT(find(v1) == find(v2));
if (v1 == v2) { if (v1 == v2) {
return; return;