mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

refactor: remove t_str_refcount_hack traces

Browse source
This commit is contained in:
Murphy Berzish 2017-02-23 15:01:55 -05:00
parent cff7c450c3
commit 5107e5cafc
3 changed files with 0 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/ast.cpp
View file

@ -1829,7 +1829,6 @@ void ast_manager::delete_node(ast * n) {
TRACE("ast", tout << "Deleting object " << n->m_id << " " << n << "\n";); TRACE("ast", tout << "Deleting object " << n->m_id << " " << n << "\n";);
CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";); CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";);
TRACE("mk_var_bug", tout << "del_ast: " << n->m_id << "\n";); TRACE("mk_var_bug", tout << "del_ast: " << n->m_id << "\n";);
TRACE("t_str_refcount_hack", tout << "delete ast " << n->m_id << std::endl;);
TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";); TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";);
SASSERT(m_ast_table.contains(n)); SASSERT(m_ast_table.contains(n));

8
src/smt/smt_context.cpp
View file

@ -2403,9 +2403,6 @@ namespace smt {
*/ */
unsigned context::pop_scope_core(unsigned num_scopes) { unsigned context::pop_scope_core(unsigned num_scopes) {
TRACE("t_str_refcount_hack", tout << "begin pop_scope_core in smt_context" << std::endl;);
if (m_manager.has_trace_stream()) if (m_manager.has_trace_stream())
m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n"; m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
@ -2453,9 +2450,7 @@ namespace smt {
ptr_vector<theory>::iterator it = m_theory_set.begin(); ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end(); ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) { for (; it != end; ++it) {
TRACE("t_str_refcount_hack", tout << "begin theory pop_scope_eh" << std::endl;);
(*it)->pop_scope_eh(num_scopes); (*it)->pop_scope_eh(num_scopes);
TRACE("t_str_refcount_hack", tout << "end theory pop_scope_eh" << std::endl;);
} }
del_justifications(m_justifications, s.m_justifications_lim); del_justifications(m_justifications, s.m_justifications_lim);
@ -2482,9 +2477,6 @@ namespace smt {
reassert_units(units_to_reassert_lim); reassert_units(units_to_reassert_lim);
TRACE("pop_scope_detail", tout << "end of pop_scope: \n"; display(tout);); TRACE("pop_scope_detail", tout << "end of pop_scope: \n"; display(tout););
CASSERT("context", check_invariant()); CASSERT("context", check_invariant());
TRACE("t_str_refcount_hack", tout << "end pop_scope_core in smt_context" << std::endl;);
return num_bool_vars; return num_bool_vars;
} }

15
src/smt/theory_str.cpp
View file

@ -1793,7 +1793,6 @@ void theory_str::reset_eh() {
* Then add an assertion: (y2 == (Concat ce m2)) AND ("str3" == (Concat abc x2)) -> (y2 != "str3") * Then add an assertion: (y2 == (Concat ce m2)) AND ("str3" == (Concat abc x2)) -> (y2 != "str3")
*/ */
bool theory_str::new_eq_check(expr * lhs, expr * rhs) { bool theory_str::new_eq_check(expr * lhs, expr * rhs) {
TRACE("t_str_refcount_hack", tout << "begin new_eq_check in theory_str" << std::endl;);
context & ctx = get_context(); context & ctx = get_context();
ast_manager & m = get_manager(); ast_manager & m = get_manager();
@ -1819,7 +1818,6 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) {
expr_ref to_assert(m.mk_not(ctx.mk_eq_atom(eqc_nn1, eqc_nn2)), m); expr_ref to_assert(m.mk_not(ctx.mk_eq_atom(eqc_nn1, eqc_nn2)), m);
assert_axiom(to_assert); assert_axiom(to_assert);
// this shouldn't use the integer theory at all, so we don't allow the option of quick-return // this shouldn't use the integer theory at all, so we don't allow the option of quick-return
TRACE("t_str_refcount_hack", tout << "end new_eq_check in theory_str" << std::endl;);
return false; return false;
} }
if (!check_length_consistency(eqc_nn1, eqc_nn2)) { if (!check_length_consistency(eqc_nn1, eqc_nn2)) {
@ -1827,7 +1825,6 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) {
if (opt_NoQuickReturn_IntegerTheory){ if (opt_NoQuickReturn_IntegerTheory){
TRACE("t_str_detail", tout << "continuing in new_eq_check() due to opt_NoQuickReturn_IntegerTheory" << std::endl;); TRACE("t_str_detail", tout << "continuing in new_eq_check() due to opt_NoQuickReturn_IntegerTheory" << std::endl;);
} else { } else {
TRACE("t_str_refcount_hack", tout << "end new_eq_check in theory_str" << std::endl;);
return false; return false;
} }
} }
@ -1846,7 +1843,6 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) {
} }
// okay, all checks here passed // okay, all checks here passed
TRACE("t_str_refcount_hack", tout << "end new_eq_check in theory_str" << std::endl;);
return true; return true;
} }
@ -7276,20 +7272,11 @@ void theory_str::check_variable_scope() {
} }
void theory_str::pop_scope_eh(unsigned num_scopes) { void theory_str::pop_scope_eh(unsigned num_scopes) {
TRACE("t_str_refcount_hack", tout << "begin pop_scope_eh in theory_str" << std::endl;);
sLevel -= num_scopes; sLevel -= num_scopes;
TRACE("t_str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;); TRACE("t_str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;);
context & ctx = get_context(); context & ctx = get_context();
ast_manager & m = get_manager(); ast_manager & m = get_manager();
// {
// expr_ref_vector assignments(m);
// ctx.get_assignments(assignments);
// TRACE("t_str_refcount_hack", tout << "assignment vector about to go out of scope" << std::endl;);
// }
// TRACE("t_str_refcount_hack", tout << "assignment vector has gone out of scope" << std::endl;);
TRACE_CODE(if (is_trace_enabled("t_str_dump_assign_on_scope_change")) { dump_assignments(); }); TRACE_CODE(if (is_trace_enabled("t_str_dump_assign_on_scope_change")) { dump_assignments(); });
// list of expr* to remove from cut_var_map // list of expr* to remove from cut_var_map
@ -7337,8 +7324,6 @@ void theory_str::pop_scope_eh(unsigned num_scopes) {
theory::pop_scope_eh(num_scopes); theory::pop_scope_eh(num_scopes);
//check_variable_scope(); //check_variable_scope();
TRACE("t_str_refcount_hack", tout << "end pop_scope_eh in theory_str" << std::endl;);
} }
void theory_str::dump_assignments() { void theory_str::dump_assignments() {