From 8ce93b4ee528776bba150a7fa88d10bce790b777 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 24 Apr 2017 15:39:25 -0400 Subject: [PATCH] unify tracing in theory_str to 'str' tag --- src/smt/theory_str.cpp | 832 ++++++++++++++++++++--------------------- 1 file changed, 416 insertions(+), 416 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index bddd0b78e..01123a22c 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -174,7 +174,7 @@ void theory_str::assert_axiom(expr * e) { } if (get_manager().is_true(e)) return; - TRACE("t_str_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;); + TRACE("str", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;); context & ctx = get_context(); if (!ctx.b_internalized(e)) { ctx.internalize(e, false); @@ -186,7 +186,7 @@ void theory_str::assert_axiom(expr * e) { // crash/error avoidance: add all axioms to the trail m_trail.push_back(e); - //TRACE("t_str_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;); + //TRACE("str", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;); } expr * theory_str::rewrite_implication(expr * premise, expr * conclusion) { @@ -196,7 +196,7 @@ expr * theory_str::rewrite_implication(expr * premise, expr * conclusion) { void theory_str::assert_implication(expr * premise, expr * conclusion) { ast_manager & m = get_manager(); - TRACE("t_str_detail", tout << "asserting implication " << mk_ismt2_pp(premise, m) << " -> " << mk_ismt2_pp(conclusion, m) << std::endl;); + TRACE("str", tout << "asserting implication " << mk_ismt2_pp(premise, m) << " -> " << mk_ismt2_pp(conclusion, m) << std::endl;); expr_ref axiom(m.mk_or(m.mk_not(premise), conclusion), m); assert_axiom(axiom); } @@ -210,7 +210,7 @@ bool theory_str::internalize_term(app * term) { ast_manager & m = get_manager(); SASSERT(term->get_family_id() == get_family_id()); - TRACE("t_str_detail", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << std::endl;); + TRACE("str", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << std::endl;); // emulation of user_smt_theory::internalize_term() @@ -234,14 +234,14 @@ bool theory_str::internalize_term(app * term) { for (unsigned i = 0; i < num_args; ++i) { enode * arg = e->get_arg(i); theory_var v_arg = mk_var(arg); - TRACE("t_str_detail", tout << "arg has theory var #" << v_arg << std::endl;); + TRACE("str", tout << "arg has theory var #" << v_arg << std::endl;); } theory_var v = mk_var(e); - TRACE("t_str_detail", tout << "term has theory var #" << v << std::endl;); + TRACE("str", tout << "term has theory var #" << v << std::endl;); if (opt_EagerStringConstantLengthAssertions && u.str.is_string(term)) { - TRACE("t_str", tout << "eagerly asserting length of string term " << mk_pp(term, m) << std::endl;); + TRACE("str", tout << "eagerly asserting length of string term " << mk_pp(term, m) << std::endl;); m_basicstr_axiom_todo.insert(e); } return true; @@ -260,23 +260,23 @@ enode* theory_str::ensure_enode(expr* e) { void theory_str::refresh_theory_var(expr * e) { enode * en = ensure_enode(e); theory_var v = mk_var(en); - TRACE("t_str_detail", tout << "refresh " << mk_pp(e, get_manager()) << ": v#" << v << std::endl;); + TRACE("str", tout << "refresh " << mk_pp(e, get_manager()) << ": v#" << v << std::endl;); m_basicstr_axiom_todo.push_back(en); } theory_var theory_str::mk_var(enode* n) { - TRACE("t_str_detail", tout << "mk_var for " << mk_pp(n->get_owner(), get_manager()) << std::endl;); + TRACE("str", tout << "mk_var for " << mk_pp(n->get_owner(), get_manager()) << std::endl;); ast_manager & m = get_manager(); if (!(m.get_sort(n->get_owner()) == u.str.mk_string_sort())) { return null_theory_var; } if (is_attached_to_var(n)) { - TRACE("t_str_detail", tout << "already attached to theory var" << std::endl;); + TRACE("str", tout << "already attached to theory var" << std::endl;); return n->get_th_var(get_id()); } else { theory_var v = theory::mk_var(n); m_find.mk_var(); - TRACE("t_str_detail", tout << "new theory var v#" << v << std::endl;); + TRACE("str", tout << "new theory var v#" << v << std::endl;); get_context().attach_th_var(n, this, v); get_context().mark_as_relevant(n); return v; @@ -320,14 +320,14 @@ void theory_str::add_cut_info_one_node(expr * baseNode, int slevel, expr * node) varInfo->vars[node] = 1; cut_var_map.insert(baseNode, std::stack()); cut_var_map[baseNode].push(varInfo); - TRACE("t_str_cut_var_map", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;); + TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;); } else { if (cut_var_map[baseNode].empty()) { T_cut * varInfo = alloc(T_cut); varInfo->level = slevel; varInfo->vars[node] = 1; cut_var_map[baseNode].push(varInfo); - TRACE("t_str_cut_var_map", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;); + TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;); } else { if (cut_var_map[baseNode].top()->level < slevel) { T_cut * varInfo = alloc(T_cut); @@ -335,10 +335,10 @@ void theory_str::add_cut_info_one_node(expr * baseNode, int slevel, expr * node) cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars); varInfo->vars[node] = 1; cut_var_map[baseNode].push(varInfo); - TRACE("t_str_cut_var_map", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;); + TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;); } else if (cut_var_map[baseNode].top()->level == slevel) { cut_var_map[baseNode].top()->vars[node] = 1; - TRACE("t_str_cut_var_map", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;); + TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;); } else { get_manager().raise_exception("entered illegal state during add_cut_info_one_node()"); } @@ -364,7 +364,7 @@ void theory_str::add_cut_info_merge(expr * destNode, int slevel, expr * srcNode) cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars); cut_var_map.insert(destNode, std::stack()); cut_var_map[destNode].push(varInfo); - TRACE("t_str_cut_var_map", tout << "merge var info for destNode=" << mk_pp(destNode, get_manager()) << ", srcNode=" << mk_pp(srcNode, get_manager()) << " [" << slevel << "]" << std::endl;); + TRACE("str", tout << "merge var info for destNode=" << mk_pp(destNode, get_manager()) << ", srcNode=" << mk_pp(srcNode, get_manager()) << " [" << slevel << "]" << std::endl;); } else { if (cut_var_map[destNode].empty() || cut_var_map[destNode].top()->level < slevel) { T_cut * varInfo = alloc(T_cut); @@ -372,10 +372,10 @@ void theory_str::add_cut_info_merge(expr * destNode, int slevel, expr * srcNode) cut_vars_map_copy(varInfo->vars, cut_var_map[destNode].top()->vars); cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars); cut_var_map[destNode].push(varInfo); - TRACE("t_str_cut_var_map", tout << "merge var info for destNode=" << mk_pp(destNode, get_manager()) << ", srcNode=" << mk_pp(srcNode, get_manager()) << " [" << slevel << "]" << std::endl;); + TRACE("str", tout << "merge var info for destNode=" << mk_pp(destNode, get_manager()) << ", srcNode=" << mk_pp(srcNode, get_manager()) << " [" << slevel << "]" << std::endl;); } else if (cut_var_map[destNode].top()->level == slevel) { cut_vars_map_copy(cut_var_map[destNode].top()->vars, cut_var_map[srcNode].top()->vars); - TRACE("t_str_cut_var_map", tout << "merge var info for destNode=" << mk_pp(destNode, get_manager()) << ", srcNode=" << mk_pp(srcNode, get_manager()) << " [" << slevel << "]" << std::endl;); + TRACE("str", tout << "merge var info for destNode=" << mk_pp(destNode, get_manager()) << ", srcNode=" << mk_pp(srcNode, get_manager()) << " [" << slevel << "]" << std::endl;); } else { get_manager().raise_exception("illegal state in add_cut_info_merge(): inconsistent slevels"); } @@ -446,7 +446,7 @@ app * theory_str::mk_int_var(std::string name) { context & ctx = get_context(); ast_manager & m = get_manager(); - TRACE("t_str_detail", tout << "creating integer variable " << name << " at scope level " << sLevel << std::endl;); + TRACE("str", tout << "creating integer variable " << name << " at scope level " << sLevel << std::endl;); sort * int_sort = m.mk_sort(m_autil.get_family_id(), INT_SORT); app * a = m.mk_fresh_const(name.c_str(), int_sort); @@ -481,12 +481,12 @@ app * theory_str::mk_str_var(std::string name) { context & ctx = get_context(); ast_manager & m = get_manager(); - TRACE("t_str_detail", tout << "creating string variable " << name << " at scope level " << sLevel << std::endl;); + TRACE("str", tout << "creating string variable " << name << " at scope level " << sLevel << std::endl;); sort * string_sort = u.str.mk_string_sort(); app * a = m.mk_fresh_const(name.c_str(), string_sort); - TRACE("t_str_detail", tout << "a->get_family_id() = " << a->get_family_id() << std::endl + TRACE("str", tout << "a->get_family_id() = " << a->get_family_id() << std::endl << "this->get_family_id() = " << this->get_family_id() << std::endl;); // I have a hunch that this may not get internalized for free... @@ -496,7 +496,7 @@ app * theory_str::mk_str_var(std::string name) { // this might help?? mk_var(ctx.get_enode(a)); m_basicstr_axiom_todo.push_back(ctx.get_enode(a)); - TRACE("t_str_axiom_bug", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;); + TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;); m_trail.push_back(a); variable_set.insert(a); @@ -518,7 +518,7 @@ app * theory_str::mk_regex_rep_var() { SASSERT(ctx.e_internalized(a)); mk_var(ctx.get_enode(a)); m_basicstr_axiom_todo.push_back(ctx.get_enode(a)); - TRACE("t_str_axiom_bug", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;); + TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;); m_trail.push_back(a); variable_set.insert(a); @@ -560,7 +560,7 @@ app * theory_str::mk_nonempty_str_var() { tmpStringVarCount++; std::string name = "$$_str" + ss.str(); - TRACE("t_str_detail", tout << "creating nonempty string variable " << name << " at scope level " << sLevel << std::endl;); + TRACE("str", tout << "creating nonempty string variable " << name << " at scope level " << sLevel << std::endl;); sort * string_sort = u.str.mk_string_sort(); app * a = m.mk_fresh_const(name.c_str(), string_sort); @@ -784,12 +784,12 @@ bool theory_str::can_propagate() { void theory_str::propagate() { context & ctx = get_context(); while (can_propagate()) { - TRACE("t_str_detail", tout << "propagating..." << std::endl;); + TRACE("str", tout << "propagating..." << std::endl;); for (unsigned i = 0; i < m_basicstr_axiom_todo.size(); ++i) { instantiate_basic_string_axioms(m_basicstr_axiom_todo[i]); } m_basicstr_axiom_todo.reset(); - TRACE("t_str_axiom_bug", tout << "reset m_basicstr_axiom_todo" << std::endl;); + TRACE("str", tout << "reset m_basicstr_axiom_todo" << std::endl;); for (unsigned i = 0; i < m_str_eq_todo.size(); ++i) { std::pair pair = m_str_eq_todo[i]; @@ -840,7 +840,7 @@ void theory_str::propagate() { } else if (u.str.is_in_re(a)) { instantiate_axiom_RegexIn(e); } else { - TRACE("t_str", tout << "BUG: unhandled library-aware term " << mk_pp(e->get_owner(), get_manager()) << std::endl;); + TRACE("str", tout << "BUG: unhandled library-aware term " << mk_pp(e->get_owner(), get_manager()) << std::endl;); NOT_IMPLEMENTED_YET(); } } @@ -868,7 +868,7 @@ void theory_str::try_eval_concat(enode * cat) { context & ctx = get_context(); ast_manager & m = get_manager(); - TRACE("t_str_detail", tout << "attempting to flatten " << mk_pp(a_cat, m) << std::endl;); + TRACE("str", tout << "attempting to flatten " << mk_pp(a_cat, m) << std::endl;); std::stack worklist; zstring flattenedString(""); @@ -894,13 +894,13 @@ void theory_str::try_eval_concat(enode * cat) { worklist.push(arg1); worklist.push(arg0); } else { - TRACE("t_str_detail", tout << "non-constant term in concat -- giving up." << std::endl;); + TRACE("str", tout << "non-constant term in concat -- giving up." << std::endl;); constOK = false; break; } } if (constOK) { - TRACE("t_str_detail", tout << "flattened to \"" << flattenedString.encode().c_str() << "\"" << std::endl;); + TRACE("str", tout << "flattened to \"" << flattenedString.encode().c_str() << "\"" << std::endl;); expr_ref constStr(mk_string(flattenedString), m); expr_ref axiom(ctx.mk_eq_atom(a_cat, constStr), m); assert_axiom(axiom); @@ -917,7 +917,7 @@ void theory_str::instantiate_concat_axiom(enode * cat) { ast_manager & m = get_manager(); - TRACE("t_str_detail", tout << "instantiating concat axiom for " << mk_ismt2_pp(a_cat, m) << std::endl;); + TRACE("str", tout << "instantiating concat axiom for " << mk_ismt2_pp(a_cat, m) << std::endl;); // build LHS expr_ref len_xy(m); @@ -960,11 +960,11 @@ void theory_str::instantiate_basic_string_axioms(enode * str) { context & ctx = get_context(); ast_manager & m = get_manager(); - TRACE("t_str_axiom_bug", tout << "set up basic string axioms on " << mk_pp(str->get_owner(), m) << std::endl;); + TRACE("str", tout << "set up basic string axioms on " << mk_pp(str->get_owner(), m) << std::endl;); // TESTING: attempt to avoid a crash here when a variable goes out of scope if (str->get_iscope_lvl() > ctx.get_scope_level()) { - TRACE("t_str_detail", tout << "WARNING: skipping axiom setup on out-of-scope string term" << std::endl;); + TRACE("str", tout << "WARNING: skipping axiom setup on out-of-scope string term" << std::endl;); return; } @@ -977,7 +977,7 @@ void theory_str::instantiate_basic_string_axioms(enode * str) { zstring strconst; u.str.is_string(str->get_owner(), strconst); - TRACE("t_str_detail", tout << "instantiating constant string axioms for \"" << strconst.encode().c_str() << "\"" << std::endl;); + TRACE("str", tout << "instantiating constant string axioms for \"" << strconst.encode().c_str() << "\"" << std::endl;); unsigned int l = strconst.length(); expr_ref len(m_autil.mk_numeral(rational(l), true), m); @@ -998,7 +998,7 @@ void theory_str::instantiate_basic_string_axioms(enode * str) { // build LHS >= RHS and assert app * lhs_ge_rhs = m_autil.mk_ge(len_str, zero); SASSERT(lhs_ge_rhs); - TRACE("t_str_detail", tout << "string axiom 1: " << mk_ismt2_pp(lhs_ge_rhs, m) << std::endl;); + TRACE("str", tout << "string axiom 1: " << mk_ismt2_pp(lhs_ge_rhs, m) << std::endl;); assert_axiom(lhs_ge_rhs); } @@ -1022,7 +1022,7 @@ void theory_str::instantiate_basic_string_axioms(enode * str) { rhs = ctx.mk_eq_atom(a_str, empty_str); SASSERT(rhs); // build LHS <=> RHS and assert - TRACE("t_str_detail", tout << "string axiom 2: " << mk_ismt2_pp(lhs, m) << " <=> " << mk_ismt2_pp(rhs, m) << std::endl;); + TRACE("str", tout << "string axiom 2: " << mk_ismt2_pp(lhs, m) << " <=> " << mk_ismt2_pp(rhs, m) << std::endl;); literal l(mk_eq(lhs, rhs, true)); ctx.mark_as_relevant(l); ctx.mk_th_axiom(get_id(), 1, &l); @@ -1052,7 +1052,7 @@ void theory_str::instantiate_str_eq_length_axiom(enode * lhs, enode * rhs) { SASSERT(len_rhs); expr_ref conclusion(ctx.mk_eq_atom(len_lhs, len_rhs), m); - TRACE("t_str_detail", tout << "string-eq length-eq axiom: " + TRACE("str", tout << "string-eq length-eq axiom: " << mk_ismt2_pp(premise, m) << " -> " << mk_ismt2_pp(conclusion, m) << std::endl;); assert_implication(premise, conclusion); } @@ -1063,12 +1063,12 @@ void theory_str::instantiate_axiom_CharAt(enode * e) { app * expr = e->get_owner(); if (axiomatized_terms.contains(expr)) { - TRACE("t_str_detail", tout << "already set up CharAt axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "already set up CharAt axiom for " << mk_pp(expr, m) << std::endl;); return; } axiomatized_terms.insert(expr); - TRACE("t_str_detail", tout << "instantiate CharAt axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "instantiate CharAt axiom for " << mk_pp(expr, m) << std::endl;); expr_ref ts0(mk_str_var("ts0"), m); expr_ref ts1(mk_str_var("ts1"), m); @@ -1106,12 +1106,12 @@ void theory_str::instantiate_axiom_prefixof(enode * e) { app * expr = e->get_owner(); if (axiomatized_terms.contains(expr)) { - TRACE("t_str_detail", tout << "already set up prefixof axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "already set up prefixof axiom for " << mk_pp(expr, m) << std::endl;); return; } axiomatized_terms.insert(expr); - TRACE("t_str_detail", tout << "instantiate prefixof axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "instantiate prefixof axiom for " << mk_pp(expr, m) << std::endl;); expr_ref ts0(mk_str_var("ts0"), m); expr_ref ts1(mk_str_var("ts1"), m); @@ -1143,12 +1143,12 @@ void theory_str::instantiate_axiom_suffixof(enode * e) { app * expr = e->get_owner(); if (axiomatized_terms.contains(expr)) { - TRACE("t_str_detail", tout << "already set up suffixof axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "already set up suffixof axiom for " << mk_pp(expr, m) << std::endl;); return; } axiomatized_terms.insert(expr); - TRACE("t_str_detail", tout << "instantiate suffixof axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "instantiate suffixof axiom for " << mk_pp(expr, m) << std::endl;); expr_ref ts0(mk_str_var("ts0"), m); expr_ref ts1(mk_str_var("ts1"), m); @@ -1180,7 +1180,7 @@ void theory_str::instantiate_axiom_Contains(enode * e) { app * ex = e->get_owner(); if (axiomatized_terms.contains(ex)) { - TRACE("t_str_detail", tout << "already set up Contains axiom for " << mk_pp(ex, m) << std::endl;); + TRACE("str", tout << "already set up Contains axiom for " << mk_pp(ex, m) << std::endl;); return; } axiomatized_terms.insert(ex); @@ -1189,7 +1189,7 @@ void theory_str::instantiate_axiom_Contains(enode * e) { // at minimum it should fix z3str/concat-006.smt2 zstring haystackStr, needleStr; if (u.str.is_string(ex->get_arg(0), haystackStr) && u.str.is_string(ex->get_arg(1), needleStr)) { - TRACE("t_str_detail", tout << "eval constant Contains term " << mk_pp(ex, m) << std::endl;); + TRACE("str", tout << "eval constant Contains term " << mk_pp(ex, m) << std::endl;); if (haystackStr.contains(needleStr)) { assert_axiom(ex); } else { @@ -1208,7 +1208,7 @@ void theory_str::instantiate_axiom_Contains(enode * e) { contain_pair_idx_map[substr].insert(key); } - TRACE("t_str_detail", tout << "instantiate Contains axiom for " << mk_pp(ex, m) << std::endl;); + TRACE("str", tout << "instantiate Contains axiom for " << mk_pp(ex, m) << std::endl;); expr_ref ts0(mk_str_var("ts0"), m); expr_ref ts1(mk_str_var("ts1"), m); @@ -1224,12 +1224,12 @@ void theory_str::instantiate_axiom_Indexof(enode * e) { app * expr = e->get_owner(); if (axiomatized_terms.contains(expr)) { - TRACE("t_str_detail", tout << "already set up Indexof axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "already set up Indexof axiom for " << mk_pp(expr, m) << std::endl;); return; } axiomatized_terms.insert(expr); - TRACE("t_str_detail", tout << "instantiate Indexof axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "instantiate Indexof axiom for " << mk_pp(expr, m) << std::endl;); expr_ref x1(mk_str_var("x1"), m); expr_ref x2(mk_str_var("x2"), m); @@ -1280,12 +1280,12 @@ void theory_str::instantiate_axiom_Indexof2(enode * e) { app * expr = e->get_owner(); if (axiomatized_terms.contains(expr)) { - TRACE("t_str_detail", tout << "already set up Indexof2 axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "already set up Indexof2 axiom for " << mk_pp(expr, m) << std::endl;); return; } axiomatized_terms.insert(expr); - TRACE("t_str_detail", tout << "instantiate Indexof2 axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "instantiate Indexof2 axiom for " << mk_pp(expr, m) << std::endl;); // ------------------------------------------------------------------------------- // if (arg[2] >= length(arg[0])) // ite2 @@ -1348,12 +1348,12 @@ void theory_str::instantiate_axiom_LastIndexof(enode * e) { app * expr = e->get_owner(); if (axiomatized_terms.contains(expr)) { - TRACE("t_str_detail", tout << "already set up LastIndexof axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "already set up LastIndexof axiom for " << mk_pp(expr, m) << std::endl;); return; } axiomatized_terms.insert(expr); - TRACE("t_str_detail", tout << "instantiate LastIndexof axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "instantiate LastIndexof axiom for " << mk_pp(expr, m) << std::endl;); expr_ref x1(mk_str_var("x1"), m); expr_ref x2(mk_str_var("x2"), m); @@ -1417,12 +1417,12 @@ void theory_str::instantiate_axiom_Substr(enode * e) { app * expr = e->get_owner(); if (axiomatized_terms.contains(expr)) { - TRACE("t_str_detail", tout << "already set up Substr axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "already set up Substr axiom for " << mk_pp(expr, m) << std::endl;); return; } axiomatized_terms.insert(expr); - TRACE("t_str_detail", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;); expr_ref substrBase(expr->get_arg(0), m); expr_ref substrPos(expr->get_arg(1), m); @@ -1510,12 +1510,12 @@ void theory_str::instantiate_axiom_Replace(enode * e) { app * expr = e->get_owner(); if (axiomatized_terms.contains(expr)) { - TRACE("t_str_detail", tout << "already set up Replace axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "already set up Replace axiom for " << mk_pp(expr, m) << std::endl;); return; } axiomatized_terms.insert(expr); - TRACE("t_str_detail", tout << "instantiate Replace axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "instantiate Replace axiom for " << mk_pp(expr, m) << std::endl;); expr_ref x1(mk_str_var("x1"), m); expr_ref x2(mk_str_var("x2"), m); @@ -1560,12 +1560,12 @@ void theory_str::instantiate_axiom_str_to_int(enode * e) { app * ex = e->get_owner(); if (axiomatized_terms.contains(ex)) { - TRACE("t_str_detail", tout << "already set up str.to-int axiom for " << mk_pp(ex, m) << std::endl;); + TRACE("str", tout << "already set up str.to-int axiom for " << mk_pp(ex, m) << std::endl;); return; } axiomatized_terms.insert(ex); - TRACE("t_str_detail", tout << "instantiate str.to-int axiom for " << mk_pp(ex, m) << std::endl;); + TRACE("str", tout << "instantiate str.to-int axiom for " << mk_pp(ex, m) << std::endl;); // let expr = (str.to-int S) // axiom 1: expr >= -1 @@ -1607,12 +1607,12 @@ void theory_str::instantiate_axiom_int_to_str(enode * e) { app * ex = e->get_owner(); if (axiomatized_terms.contains(ex)) { - TRACE("t_str_detail", tout << "already set up str.from-int axiom for " << mk_pp(ex, m) << std::endl;); + TRACE("str", tout << "already set up str.from-int axiom for " << mk_pp(ex, m) << std::endl;); return; } axiomatized_terms.insert(ex); - TRACE("t_str_detail", tout << "instantiate str.from-int axiom for " << mk_pp(ex, m) << std::endl;); + TRACE("str", tout << "instantiate str.from-int axiom for " << mk_pp(ex, m) << std::endl;); // axiom 1: N < 0 <==> (str.from-int N) = "" expr * N = ex->get_arg(0); @@ -1674,7 +1674,7 @@ zstring theory_str::get_std_regex_str(expr * regex) { zstring reg1Str = get_std_regex_str(reg1Ast); return zstring("(") + reg1Str + zstring(")*"); } else { - TRACE("t_str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;); + TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;); UNREACHABLE(); return zstring(""); } } @@ -1685,12 +1685,12 @@ void theory_str::instantiate_axiom_RegexIn(enode * e) { app * ex = e->get_owner(); if (axiomatized_terms.contains(ex)) { - TRACE("t_str_detail", tout << "already set up RegexIn axiom for " << mk_pp(ex, m) << std::endl;); + TRACE("str", tout << "already set up RegexIn axiom for " << mk_pp(ex, m) << std::endl;); return; } axiomatized_terms.insert(ex); - TRACE("t_str_detail", tout << "instantiate RegexIn axiom for " << mk_pp(ex, m) << std::endl;); + TRACE("str", tout << "instantiate RegexIn axiom for " << mk_pp(ex, m) << std::endl;); { zstring regexStr = get_std_regex_str(ex->get_arg(1)); @@ -1710,7 +1710,7 @@ void theory_str::instantiate_axiom_RegexIn(enode * e) { expr_ref finalAxiom(m.mk_iff(ex, rhs), m); SASSERT(finalAxiom); assert_axiom(finalAxiom); - TRACE("t_str", tout << "set up Str2Reg: (RegexIn " << mk_pp(str, m) << " " << mk_pp(regex, m) << ")" << std::endl;); + TRACE("str", tout << "set up Str2Reg: (RegexIn " << mk_pp(str, m) << " " << mk_pp(regex, m) << ")" << std::endl;); } else if (u.re.is_concat(regex)) { expr_ref var1(mk_regex_rep_var(), m); expr_ref var2(mk_regex_rep_var(), m); @@ -1753,7 +1753,7 @@ void theory_str::instantiate_axiom_RegexIn(enode * e) { SASSERT(finalAxiom); assert_axiom(finalAxiom); } else { - TRACE("t_str_detail", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;); + TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;); NOT_IMPLEMENTED_YET(); } } @@ -1762,11 +1762,11 @@ void theory_str::attach_new_th_var(enode * n) { context & ctx = get_context(); theory_var v = mk_var(n); ctx.attach_th_var(n, this, v); - TRACE("t_str_detail", tout << "new theory var: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " := v#" << v << std::endl;); + TRACE("str", tout << "new theory var: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " := v#" << v << std::endl;); } void theory_str::reset_eh() { - TRACE("t_str", tout << "resetting" << std::endl;); + TRACE("str", tout << "resetting" << std::endl;); m_trail_stack.reset(); m_basicstr_axiom_todo.reset(); @@ -1804,19 +1804,19 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) { do { expr * eqc_nn2 = rhs; do { - TRACE("t_str_detail", tout << "checking whether " << mk_pp(eqc_nn1, m) << " and " << mk_pp(eqc_nn2, m) << " can be equal" << std::endl;); + TRACE("str", tout << "checking whether " << mk_pp(eqc_nn1, m) << " and " << mk_pp(eqc_nn2, m) << " can be equal" << std::endl;); // inconsistency check: value if (!can_two_nodes_eq(eqc_nn1, eqc_nn2)) { - TRACE("t_str", tout << "inconsistency detected: " << mk_pp(eqc_nn1, m) << " cannot be equal to " << mk_pp(eqc_nn2, m) << std::endl;); + TRACE("str", tout << "inconsistency detected: " << mk_pp(eqc_nn1, m) << " cannot be equal to " << mk_pp(eqc_nn2, m) << std::endl;); expr_ref to_assert(m.mk_not(ctx.mk_eq_atom(eqc_nn1, eqc_nn2)), m); assert_axiom(to_assert); // this shouldn't use the integer theory at all, so we don't allow the option of quick-return return false; } if (!check_length_consistency(eqc_nn1, eqc_nn2)) { - TRACE("t_str", tout << "inconsistency detected: " << mk_pp(eqc_nn1, m) << " and " << mk_pp(eqc_nn2, m) << " have inconsistent lengths" << std::endl;); + TRACE("str", tout << "inconsistency detected: " << mk_pp(eqc_nn1, m) << " and " << mk_pp(eqc_nn2, m) << " have inconsistent lengths" << std::endl;); if (opt_NoQuickReturn_IntegerTheory){ - TRACE("t_str_detail", tout << "continuing in new_eq_check() due to opt_NoQuickReturn_IntegerTheory" << std::endl;); + TRACE("str", tout << "continuing in new_eq_check() due to opt_NoQuickReturn_IntegerTheory" << std::endl;); } else { return false; } @@ -1831,7 +1831,7 @@ bool theory_str::new_eq_check(expr * lhs, expr * rhs) { } if (!regex_in_bool_map.empty()) { - TRACE("t_str", tout << "checking regex consistency" << std::endl;); + TRACE("str", tout << "checking regex consistency" << std::endl;); check_regex_in(lhs, rhs); } @@ -1963,7 +1963,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { ast_manager & m = get_manager(); context & ctx = get_context(); - TRACE("t_str", tout << "simplifying parents of " << mk_ismt2_pp(nn, m) + TRACE("str", tout << "simplifying parents of " << mk_ismt2_pp(nn, m) << " with respect to " << mk_ismt2_pp(eq_str, m) << std::endl;); ctx.internalize(nn, false); @@ -1973,7 +1973,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { expr * n_eqNode = nn; do { enode * n_eq_enode = ctx.get_enode(n_eqNode); - TRACE("t_str_detail", tout << "considering all parents of " << mk_ismt2_pp(n_eqNode, m) << std::endl + TRACE("str", tout << "considering all parents of " << mk_ismt2_pp(n_eqNode, m) << std::endl << "associated n_eq_enode has " << n_eq_enode->get_num_parents() << " parents" << std::endl;); // the goal of this next bit is to avoid dereferencing a bogus e_parent in the following loop. @@ -1990,7 +1990,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { SASSERT(e_parent != NULL); app * a_parent = e_parent->get_owner(); - TRACE("t_str_detail", tout << "considering parent " << mk_ismt2_pp(a_parent, m) << std::endl;); + TRACE("str", tout << "considering parent " << mk_ismt2_pp(a_parent, m) << std::endl;); if (u.str.is_concat(a_parent)) { expr * arg0 = a_parent->get_arg(0); @@ -2004,7 +2004,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { bool arg0Len_exists = get_len_value(eq_str, arg0Len); bool arg1Len_exists = get_len_value(arg1, arg1Len); - TRACE("t_str_detail", + TRACE("str", tout << "simplify_parent #1:" << std::endl << "* parent = " << mk_ismt2_pp(a_parent, m) << std::endl << "* |parent| = " << rational_to_string_if_exists(parentLen, parentLen_exists) << std::endl @@ -2013,7 +2013,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { ); if (parentLen_exists && !arg1Len_exists) { - TRACE("t_str_detail", tout << "make up len for arg1" << std::endl;); + TRACE("str", tout << "make up len for arg1" << std::endl;); expr_ref implyL11(m.mk_and(ctx.mk_eq_atom(mk_strlen(a_parent), mk_int(parentLen)), ctx.mk_eq_atom(mk_strlen(arg0), mk_int(arg0Len))), m); rational makeUpLenArg1 = parentLen - arg0Len; @@ -2075,7 +2075,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { bool arg0Len_exists = get_len_value(arg0, arg0Len); bool arg1Len_exists = get_len_value(eq_str, arg1Len); - TRACE("t_str_detail", + TRACE("str", tout << "simplify_parent #2:" << std::endl << "* parent = " << mk_ismt2_pp(a_parent, m) << std::endl << "* |parent| = " << rational_to_string_if_exists(parentLen, parentLen_exists) << std::endl @@ -2083,7 +2083,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { << "* |arg1| = " << rational_to_string_if_exists(arg1Len, arg1Len_exists) << std::endl; ); if (parentLen_exists && !arg0Len_exists) { - TRACE("t_str_detail", tout << "make up len for arg0" << std::endl;); + TRACE("str", tout << "make up len for arg0" << std::endl;); expr_ref implyL11(m.mk_and(ctx.mk_eq_atom(mk_strlen(a_parent), mk_int(parentLen)), ctx.mk_eq_atom(mk_strlen(arg1), mk_int(arg1Len))), m); rational makeUpLenArg0 = parentLen - arg1Len; @@ -2144,7 +2144,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { // Case (2-1) begin: (Concat n_eqNode (Concat str var)) if (arg0 == n_eqNode && u.str.is_concat(to_app(arg1))) { app * a_arg1 = to_app(arg1); - TRACE("t_str_detail", tout << "simplify_parent #3" << std::endl;); + TRACE("str", tout << "simplify_parent #3" << std::endl;); expr * r_concat_arg0 = a_arg1->get_arg(0); if (u.str.is_string(r_concat_arg0)) { expr * combined_str = eval_concat(eq_str, r_concat_arg0); @@ -2168,7 +2168,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { // Case (2-2) begin: (Concat (Concat var str) n_eqNode) if (u.str.is_concat(to_app(arg0)) && arg1 == n_eqNode) { app * a_arg0 = to_app(arg0); - TRACE("t_str_detail", tout << "simplify_parent #4" << std::endl;); + TRACE("str", tout << "simplify_parent #4" << std::endl;); expr * l_concat_arg1 = a_arg0->get_arg(1); if (u.str.is_string(l_concat_arg1)) { expr * combined_str = eval_concat(l_concat_arg1, eq_str); @@ -2199,7 +2199,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { expr * concat_parent_arg0 = concat_parent->get_arg(0); expr * concat_parent_arg1 = concat_parent->get_arg(1); if (concat_parent_arg0 == a_parent && u.str.is_string(concat_parent_arg1)) { - TRACE("t_str_detail", tout << "simplify_parent #5" << std::endl;); + TRACE("str", tout << "simplify_parent #5" << std::endl;); expr * combinedStr = eval_concat(eq_str, concat_parent_arg1); SASSERT(combinedStr); expr_ref implyL(m); @@ -2225,7 +2225,7 @@ void theory_str::simplify_parent(expr * nn, expr * eq_str) { expr * concat_parent_arg0 = concat_parent->get_arg(0); expr * concat_parent_arg1 = concat_parent->get_arg(1); if (concat_parent_arg1 == a_parent && u.str.is_string(concat_parent_arg0)) { - TRACE("t_str_detail", tout << "simplify_parent #6" << std::endl;); + TRACE("str", tout << "simplify_parent #6" << std::endl;); expr * combinedStr = eval_concat(concat_parent_arg0, eq_str); SASSERT(combinedStr); expr_ref implyL(m); @@ -2275,10 +2275,10 @@ expr * theory_str::simplify_concat(expr * node) { expr * vArg = get_eqc_value(argVec[i], vArgHasEqcValue); resultAst = mk_concat(resultAst, vArg); } - TRACE("t_str_detail", tout << mk_ismt2_pp(node, m) << " is simplified to " << mk_ismt2_pp(resultAst, m) << std::endl;); + TRACE("str", tout << mk_ismt2_pp(node, m) << " is simplified to " << mk_ismt2_pp(resultAst, m) << std::endl;); if (in_same_eqc(node, resultAst)) { - TRACE("t_str_detail", tout << "SKIP: both concats are already in the same equivalence class" << std::endl;); + TRACE("str", tout << "SKIP: both concats are already in the same equivalence class" << std::endl;); } else { expr_ref_vector items(m); int pos = 0; @@ -2327,7 +2327,7 @@ bool theory_str::infer_len_concat(expr * n, rational & nLen) { expr_ref axl(m.mk_and(l_items.size(), l_items.c_ptr()), m); rational nnLen = arg0_len + arg1_len; expr_ref axr(ctx.mk_eq_atom(mk_strlen(n), mk_int(nnLen)), m); - TRACE("t_str_detail", tout << "inferred (Length " << mk_pp(n, m) << ") = " << nnLen << std::endl;); + TRACE("str", tout << "inferred (Length " << mk_pp(n, m) << ") = " << nnLen << std::endl;); assert_implication(axl, axr); nLen = nnLen; return true; @@ -2507,10 +2507,10 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { bool a2_arg0_len_exists = get_len_value(a2_arg0, a2_arg0_len); bool a2_arg1_len_exists = get_len_value(a2_arg1, a2_arg1_len); - TRACE("t_str", tout << "nn1 = " << mk_ismt2_pp(nn1, m) << std::endl + TRACE("str", tout << "nn1 = " << mk_ismt2_pp(nn1, m) << std::endl << "nn2 = " << mk_ismt2_pp(nn2, m) << std::endl;); - TRACE("t_str_detail", tout + TRACE("str", tout << "len(" << mk_pp(a1_arg0, m) << ") = " << (a1_arg0_len_exists ? a1_arg0_len.to_string() : "?") << std::endl << "len(" << mk_pp(a1_arg1, m) << ") = " << (a1_arg1_len_exists ? a1_arg1_len.to_string() : "?") << std::endl << "len(" << mk_pp(a2_arg0, m) << ") = " << (a2_arg0_len_exists ? a2_arg0_len.to_string() : "?") << std::endl @@ -2527,7 +2527,7 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { expr_ref conclusion(m.mk_and(eq1, eq2), m); assert_implication(premise, conclusion); } - TRACE("t_str_detail", tout << "SKIP: a1_arg0 == a2_arg0" << std::endl;); + TRACE("str", tout << "SKIP: a1_arg0 == a2_arg0" << std::endl;); return; } @@ -2539,7 +2539,7 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { expr_ref conclusion(m.mk_and(eq1, eq2), m); assert_implication(premise, conclusion); } - TRACE("t_str_detail", tout << "SKIP: a1_arg1 == a2_arg1" << std::endl;); + TRACE("str", tout << "SKIP: a1_arg1 == a2_arg1" << std::endl;); return; } @@ -2547,10 +2547,10 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { if (in_same_eqc(a1_arg0, a2_arg0)) { if (in_same_eqc(a1_arg1, a2_arg1)) { - TRACE("t_str_detail", tout << "SKIP: a1_arg0 =~ a2_arg0 and a1_arg1 =~ a2_arg1" << std::endl;); + TRACE("str", tout << "SKIP: a1_arg0 =~ a2_arg0 and a1_arg1 =~ a2_arg1" << std::endl;); return; } else { - TRACE("t_str_detail", tout << "quick path 1-1: a1_arg0 =~ a2_arg0" << std::endl;); + TRACE("str", tout << "quick path 1-1: a1_arg0 =~ a2_arg0" << std::endl;); expr_ref premise(m.mk_and(ctx.mk_eq_atom(nn1, nn2), ctx.mk_eq_atom(a1_arg0, a2_arg0)), m); expr_ref conclusion(m.mk_and(ctx.mk_eq_atom(a1_arg1, a2_arg1), ctx.mk_eq_atom(mk_strlen(a1_arg1), mk_strlen(a2_arg1))), m); assert_implication(premise, conclusion); @@ -2558,7 +2558,7 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { } } else { if (in_same_eqc(a1_arg1, a2_arg1)) { - TRACE("t_str_detail", tout << "quick path 1-2: a1_arg1 =~ a2_arg1" << std::endl;); + TRACE("str", tout << "quick path 1-2: a1_arg1 =~ a2_arg1" << std::endl;); expr_ref premise(m.mk_and(ctx.mk_eq_atom(nn1, nn2), ctx.mk_eq_atom(a1_arg1, a2_arg1)), m); expr_ref conclusion(m.mk_and(ctx.mk_eq_atom(a1_arg0, a2_arg0), ctx.mk_eq_atom(mk_strlen(a1_arg0), mk_strlen(a2_arg0))), m); assert_implication(premise, conclusion); @@ -2569,7 +2569,7 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { // quick path 2-1 if (a1_arg0_len_exists && a2_arg0_len_exists && a1_arg0_len == a2_arg0_len) { if (!in_same_eqc(a1_arg0, a2_arg0)) { - TRACE("t_str_detail", tout << "quick path 2-1: len(nn1.arg0) == len(nn2.arg0)" << std::endl;); + TRACE("str", tout << "quick path 2-1: len(nn1.arg0) == len(nn2.arg0)" << std::endl;); expr_ref ax_l1(ctx.mk_eq_atom(nn1, nn2), m); expr_ref ax_l2(ctx.mk_eq_atom(mk_strlen(a1_arg0), mk_strlen(a2_arg0)), m); expr_ref ax_r1(ctx.mk_eq_atom(a1_arg0, a2_arg0), m); @@ -2581,7 +2581,7 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { assert_implication(premise, conclusion); if (opt_NoQuickReturn_IntegerTheory) { - TRACE("t_str_detail", tout << "bypassing quick return from the end of this case" << std::endl;); + TRACE("str", tout << "bypassing quick return from the end of this case" << std::endl;); } else { return; } @@ -2590,7 +2590,7 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { if (a1_arg1_len_exists && a2_arg1_len_exists && a1_arg1_len == a2_arg1_len) { if (!in_same_eqc(a1_arg1, a2_arg1)) { - TRACE("t_str_detail", tout << "quick path 2-2: len(nn1.arg1) == len(nn2.arg1)" << std::endl;); + TRACE("str", tout << "quick path 2-2: len(nn1.arg1) == len(nn2.arg1)" << std::endl;); expr_ref ax_l1(ctx.mk_eq_atom(nn1, nn2), m); expr_ref ax_l2(ctx.mk_eq_atom(mk_strlen(a1_arg1), mk_strlen(a2_arg1)), m); expr_ref ax_r1(ctx.mk_eq_atom(a1_arg0, a2_arg0), m); @@ -2601,7 +2601,7 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { assert_implication(premise, conclusion); if (opt_NoQuickReturn_IntegerTheory) { - TRACE("t_str_detail", tout << "bypassing quick return from the end of this case" << std::endl;); + TRACE("str", tout << "bypassing quick return from the end of this case" << std::endl;); } else { return; } @@ -2613,17 +2613,17 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { app * a_new_nn1 = to_app(new_nn1); app * a_new_nn2 = to_app(new_nn2); - TRACE("t_str_detail", tout << "new_nn1 = " << mk_ismt2_pp(new_nn1, m) << std::endl + TRACE("str", tout << "new_nn1 = " << mk_ismt2_pp(new_nn1, m) << std::endl << "new_nn2 = " << mk_ismt2_pp(new_nn2, m) << std::endl;); if (new_nn1 == new_nn2) { - TRACE("t_str_detail", tout << "equal concats, return" << std::endl;); + TRACE("str", tout << "equal concats, return" << std::endl;); return; } if (!can_two_nodes_eq(new_nn1, new_nn2)) { expr_ref detected(m.mk_not(ctx.mk_eq_atom(new_nn1, new_nn2)), m); - TRACE("t_str_detail", tout << "inconsistency detected: " << mk_ismt2_pp(detected, m) << std::endl;); + TRACE("str", tout << "inconsistency detected: " << mk_ismt2_pp(detected, m) << std::endl;); assert_axiom(detected); return; } @@ -2633,13 +2633,13 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { bool n1IsConcat = u.str.is_concat(a_new_nn1); bool n2IsConcat = u.str.is_concat(a_new_nn2); if (!n1IsConcat && n2IsConcat) { - TRACE("t_str_detail", tout << "nn1_new is not a concat" << std::endl;); + TRACE("str", tout << "nn1_new is not a concat" << std::endl;); if (u.str.is_string(a_new_nn1)) { simplify_parent(new_nn2, new_nn1); } return; } else if (n1IsConcat && !n2IsConcat) { - TRACE("t_str_detail", tout << "nn2_new is not a concat" << std::endl;); + TRACE("str", tout << "nn2_new is not a concat" << std::endl;); if (u.str.is_string(a_new_nn2)) { simplify_parent(new_nn1, new_nn2); } @@ -2647,7 +2647,7 @@ void theory_str::simplify_concat_equality(expr * nn1, expr * nn2) { } else if (!n1IsConcat && !n2IsConcat) { // normally this should never happen, because group_terms_by_eqc() should have pre-simplified // as much as possible. however, we make a defensive check here just in case - TRACE("t_str_detail", tout << "WARNING: nn1_new and nn2_new both simplify to non-concat terms" << std::endl;); + TRACE("str", tout << "WARNING: nn1_new and nn2_new both simplify to non-concat terms" << std::endl;); return; } @@ -2750,7 +2750,7 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { expr * v2_arg0 = a_new_nn2->get_arg(0); expr * v2_arg1 = a_new_nn2->get_arg(1); - TRACE("t_str_detail", tout << "checking whether " << mk_pp(new_nn1, m) << " and " << mk_pp(new_nn1, m) << " might overlap." << std::endl;); + TRACE("str", tout << "checking whether " << mk_pp(new_nn1, m) << " and " << mk_pp(new_nn1, m) << " might overlap." << std::endl;); check_and_init_cut_var(v1_arg0); check_and_init_cut_var(v1_arg1); @@ -2761,17 +2761,17 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { // case 1: concat(x, y) = concat(m, n) //************************************************************* if (is_concat_eq_type1(new_nn1, new_nn2)) { - TRACE("t_str_detail", tout << "Type 1 check." << std::endl;); + TRACE("str", tout << "Type 1 check." << std::endl;); expr * x = to_app(new_nn1)->get_arg(0); expr * y = to_app(new_nn1)->get_arg(1); expr * m = to_app(new_nn2)->get_arg(0); expr * n = to_app(new_nn2)->get_arg(1); if (has_self_cut(m, y)) { - TRACE("t_str_detail", tout << "Possible overlap found" << std::endl; print_cut_var(m, tout); print_cut_var(y, tout);); + TRACE("str", tout << "Possible overlap found" << std::endl; print_cut_var(m, tout); print_cut_var(y, tout);); return true; } else if (has_self_cut(x, n)) { - TRACE("t_str_detail", tout << "Possible overlap found" << std::endl; print_cut_var(x, tout); print_cut_var(n, tout);); + TRACE("str", tout << "Possible overlap found" << std::endl; print_cut_var(x, tout); print_cut_var(n, tout);); return true; } else { return false; @@ -2799,7 +2799,7 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { } if (has_self_cut(m, y)) { - TRACE("t_str_detail", tout << "Possible overlap found" << std::endl; print_cut_var(m, tout); print_cut_var(y, tout);); + TRACE("str", tout << "Possible overlap found" << std::endl; print_cut_var(m, tout); print_cut_var(y, tout);); return true; } else { return false; @@ -2826,7 +2826,7 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { x = v1_arg0; } if (has_self_cut(x, n)) { - TRACE("t_str_detail", tout << "Possible overlap found" << std::endl; print_cut_var(x, tout); print_cut_var(n, tout);); + TRACE("str", tout << "Possible overlap found" << std::endl; print_cut_var(x, tout); print_cut_var(n, tout);); return true; } else { return false; @@ -2868,14 +2868,14 @@ bool theory_str::will_result_in_overlap(expr * lhs, expr * rhs) { m = v1_arg0; } if (has_self_cut(m, y)) { - TRACE("t_str_detail", tout << "Possible overlap found" << std::endl; print_cut_var(m, tout); print_cut_var(y, tout);); + TRACE("str", tout << "Possible overlap found" << std::endl; print_cut_var(m, tout); print_cut_var(y, tout);); return true; } else { return false; } } - TRACE("t_str_detail", tout << "warning: unrecognized concat case" << std::endl;); + TRACE("str", tout << "warning: unrecognized concat case" << std::endl;); return false; } @@ -2902,17 +2902,17 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { bool overlapAssumptionUsed = false; - TRACE("t_str_detail", tout << "process_concat_eq TYPE 1" << std::endl + TRACE("str", tout << "process_concat_eq TYPE 1" << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; ); if (!u.str.is_concat(to_app(concatAst1))) { - TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;); + TRACE("str", tout << "concatAst1 is not a concat function" << std::endl;); return; } if (!u.str.is_concat(to_app(concatAst2))) { - TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;); + TRACE("str", tout << "concatAst2 is not a concat function" << std::endl;); return; } expr * x = to_app(concatAst1)->get_arg(0); @@ -2928,7 +2928,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { int splitType = -1; if (x_len_exists && m_len_exists) { - TRACE("t_str_int", tout << "length values found: x/m" << std::endl;); + TRACE("str", tout << "length values found: x/m" << std::endl;); if (x_len < m_len) { splitType = 0; } else if (x_len == m_len) { @@ -2939,7 +2939,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { } if (splitType == -1 && y_len_exists && n_len_exists) { - TRACE("t_str_int", tout << "length values found: y/n" << std::endl;); + TRACE("str", tout << "length values found: y/n" << std::endl;); if (y_len > n_len) { splitType = 0; } else if (y_len == n_len) { @@ -2949,7 +2949,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { } } - TRACE("t_str_detail", tout + TRACE("str", tout << "len(x) = " << (x_len_exists ? x_len.to_string() : "?") << std::endl << "len(y) = " << (y_len_exists ? y_len.to_string() : "?") << std::endl << "len(m) = " << (m_len_exists ? m_len.to_string() : "?") << std::endl @@ -2996,7 +2996,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { } } - TRACE("t_str_detail", tout << "entry 1 " << (entry1InScope ? "in scope" : "not in scope") << std::endl + TRACE("str", tout << "entry 1 " << (entry1InScope ? "in scope" : "not in scope") << std::endl << "entry 2 " << (entry2InScope ? "in scope" : "not in scope") << std::endl;); if (!entry1InScope && !entry2InScope) { @@ -3076,8 +3076,8 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { assert_implication(ax_l, tester); add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); } else { - TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); - TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); + TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); if (!overlapAssumptionUsed) { overlapAssumptionUsed = true; @@ -3139,8 +3139,8 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { assert_implication(ax_l, tester); add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); } else { - TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); - TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); + TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); if (!overlapAssumptionUsed) { overlapAssumptionUsed = true; @@ -3195,8 +3195,8 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { arrangement_disjunction.push_back(tester); add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); } else { - TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); - TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); + TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); if (!overlapAssumptionUsed) { overlapAssumptionUsed = true; @@ -3244,8 +3244,8 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { arrangement_disjunction.push_back(tester); add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); } else { - TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); - TRACE("t_str_detail", {print_cut_var(x, tout); print_cut_var(n, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); + TRACE("str", {print_cut_var(x, tout); print_cut_var(n, tout);}); if (!overlapAssumptionUsed) { overlapAssumptionUsed = true; @@ -3282,7 +3282,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { // assert mutual exclusion between each branch of the arrangement generate_mutual_exclusion(arrangement_disjunction); } else { - TRACE("t_str", tout << "STOP: no split option found for two EQ concats." << std::endl;); + TRACE("str", tout << "STOP: no split option found for two EQ concats." << std::endl;); } } // (splitType == -1) } @@ -3313,17 +3313,17 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { bool overlapAssumptionUsed = false; - TRACE("t_str_detail", tout << "process_concat_eq TYPE 2" << std::endl + TRACE("str", tout << "process_concat_eq TYPE 2" << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; ); if (!u.str.is_concat(to_app(concatAst1))) { - TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;); + TRACE("str", tout << "concatAst1 is not a concat function" << std::endl;); return; } if (!u.str.is_concat(to_app(concatAst2))) { - TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;); + TRACE("str", tout << "concatAst2 is not a concat function" << std::endl;); return; } @@ -3400,7 +3400,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { } } - TRACE("t_str_detail", tout << "entry 1 " << (entry1InScope ? "in scope" : "not in scope") << std::endl + TRACE("str", tout << "entry 1 " << (entry1InScope ? "in scope" : "not in scope") << std::endl << "entry 2 " << (entry2InScope ? "in scope" : "not in scope") << std::endl;); @@ -3439,7 +3439,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { splitType = 2; } - TRACE("t_str_detail", tout << "Split type " << splitType << std::endl;); + TRACE("str", tout << "Split type " << splitType << std::endl;); // Provide fewer split options when length information is available. @@ -3491,8 +3491,8 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { assert_implication(ax_l, tester); add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); } else { - TRACE("t_str", tout << "AVOID LOOP: SKIP" << std::endl;); - TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIP" << std::endl;); + TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); if (!overlapAssumptionUsed) { overlapAssumptionUsed = true; @@ -3526,7 +3526,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { l_items.push_back(ctx.mk_eq_atom(mk_strlen(y), mk_int(y_len))); lenDelta = str_len - y_len; } - TRACE("t_str", + TRACE("str", tout << "xLen? " << (x_len_exists ? "yes" : "no") << std::endl << "mLen? " << (m_len_exists ? "yes" : "no") << std::endl @@ -3562,7 +3562,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { } } else { // negate! It's impossible to split str with these lengths - TRACE("t_str", tout << "CONFLICT: Impossible to split str with these lengths." << std::endl;); + TRACE("str", tout << "CONFLICT: Impossible to split str with these lengths." << std::endl;); expr_ref ax_l(mk_and(l_items), mgr); assert_axiom(mgr.mk_not(ax_l)); } @@ -3597,8 +3597,8 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { arrangement_disjunction.push_back(tester); add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); } else { - TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); - TRACE("t_str_detail", {print_cut_var(m, tout); print_cut_var(y, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); + TRACE("str", {print_cut_var(m, tout); print_cut_var(y, tout);}); if (!overlapAssumptionUsed) { overlapAssumptionUsed = true; @@ -3645,7 +3645,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { } generate_mutual_exclusion(arrangement_disjunction); } else { - TRACE("t_str", tout << "STOP: Should not split two EQ concats." << std::endl;); + TRACE("str", tout << "STOP: Should not split two EQ concats." << std::endl;); } } // (splitType == -1) } @@ -3676,17 +3676,17 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { bool overlapAssumptionUsed = false; - TRACE("t_str_detail", tout << "process_concat_eq TYPE 3" << std::endl + TRACE("str", tout << "process_concat_eq TYPE 3" << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; ); if (!u.str.is_concat(to_app(concatAst1))) { - TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;); + TRACE("str", tout << "concatAst1 is not a concat function" << std::endl;); return; } if (!u.str.is_concat(to_app(concatAst2))) { - TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;); + TRACE("str", tout << "concatAst2 is not a concat function" << std::endl;); return; } @@ -3756,7 +3756,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { } } - TRACE("t_str_detail", tout << "entry 1 " << (entry1InScope ? "in scope" : "not in scope") << std::endl + TRACE("str", tout << "entry 1 " << (entry1InScope ? "in scope" : "not in scope") << std::endl << "entry 2 " << (entry2InScope ? "in scope" : "not in scope") << std::endl;); @@ -3798,7 +3798,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { splitType = 2; } - TRACE("t_str_detail", tout << "Split type " << splitType << std::endl;); + TRACE("str", tout << "Split type " << splitType << std::endl;); // Provide fewer split options when length information is available. if (splitType == 0) { @@ -3836,7 +3836,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { } } else { // negate! It's impossible to split str with these lengths - TRACE("t_str", tout << "CONFLICT: Impossible to split str with these lengths." << std::endl;); + TRACE("str", tout << "CONFLICT: Impossible to split str with these lengths." << std::endl;); assert_axiom(mgr.mk_not(ax_l)); } } @@ -3899,8 +3899,8 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { assert_implication(ax_l, tester); add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); } else { - TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); - TRACE("t_str_detail", {print_cut_var(x, tout); print_cut_var(n, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIPPED" << std::endl;); + TRACE("str", {print_cut_var(x, tout); print_cut_var(n, tout);}); if (!overlapAssumptionUsed) { overlapAssumptionUsed = true; @@ -3983,8 +3983,8 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { arrangement_disjunction.push_back(tester); add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); } else { - TRACE("t_str", tout << "AVOID LOOP: SKIPPED." << std::endl;); - TRACE("t_str_detail", {print_cut_var(x, tout); print_cut_var(n, tout);}); + TRACE("str", tout << "AVOID LOOP: SKIPPED." << std::endl;); + TRACE("str", {print_cut_var(x, tout); print_cut_var(n, tout);}); if (!overlapAssumptionUsed) { overlapAssumptionUsed = true; @@ -4007,7 +4007,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { } generate_mutual_exclusion(arrangement_disjunction); } else { - TRACE("t_str", tout << "STOP: should not split two eq. concats" << std::endl;); + TRACE("str", tout << "STOP: should not split two eq. concats" << std::endl;); } } @@ -4033,17 +4033,17 @@ bool theory_str::is_concat_eq_type4(expr * concatAst1, expr * concatAst2) { void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) { ast_manager & mgr = get_manager(); context & ctx = get_context(); - TRACE("t_str_detail", tout << "process_concat_eq TYPE 4" << std::endl + TRACE("str", tout << "process_concat_eq TYPE 4" << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; ); if (!u.str.is_concat(to_app(concatAst1))) { - TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;); + TRACE("str", tout << "concatAst1 is not a concat function" << std::endl;); return; } if (!u.str.is_concat(to_app(concatAst2))) { - TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;); + TRACE("str", tout << "concatAst2 is not a concat function" << std::endl;); return; } @@ -4066,7 +4066,7 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) { int commonLen = (str1Len > str2Len) ? str2Len : str1Len; if (str1Value.extract(0, commonLen) != str2Value.extract(0, commonLen)) { - TRACE("t_str_detail", tout << "Conflict: " << mk_ismt2_pp(concatAst1, mgr) + TRACE("str", tout << "Conflict: " << mk_ismt2_pp(concatAst1, mgr) << " has no common prefix with " << mk_ismt2_pp(concatAst2, mgr) << std::endl;); expr_ref toNegate(mgr.mk_not(ctx.mk_eq_atom(concatAst1, concatAst2)), mgr); assert_axiom(toNegate); @@ -4134,17 +4134,17 @@ bool theory_str::is_concat_eq_type5(expr * concatAst1, expr * concatAst2) { void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { ast_manager & mgr = get_manager(); context & ctx = get_context(); - TRACE("t_str_detail", tout << "process_concat_eq TYPE 5" << std::endl + TRACE("str", tout << "process_concat_eq TYPE 5" << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; ); if (!u.str.is_concat(to_app(concatAst1))) { - TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;); + TRACE("str", tout << "concatAst1 is not a concat function" << std::endl;); return; } if (!u.str.is_concat(to_app(concatAst2))) { - TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;); + TRACE("str", tout << "concatAst2 is not a concat function" << std::endl;); return; } @@ -4167,7 +4167,7 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) { int cLen = (str1Len > str2Len) ? str2Len : str1Len; if (str1Value.extract(str1Len - cLen, cLen) != str2Value.extract(str2Len - cLen, cLen)) { - TRACE("t_str_detail", tout << "Conflict: " << mk_ismt2_pp(concatAst1, mgr) + TRACE("str", tout << "Conflict: " << mk_ismt2_pp(concatAst1, mgr) << " has no common suffix with " << mk_ismt2_pp(concatAst2, mgr) << std::endl;); expr_ref toNegate(mgr.mk_not(ctx.mk_eq_atom(concatAst1, concatAst2)), mgr); assert_axiom(toNegate); @@ -4235,17 +4235,17 @@ bool theory_str::is_concat_eq_type6(expr * concatAst1, expr * concatAst2) { void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { ast_manager & mgr = get_manager(); context & ctx = get_context(); - TRACE("t_str_detail", tout << "process_concat_eq TYPE 6" << std::endl + TRACE("str", tout << "process_concat_eq TYPE 6" << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl; ); if (!u.str.is_concat(to_app(concatAst1))) { - TRACE("t_str_detail", tout << "concatAst1 is not a concat function" << std::endl;); + TRACE("str", tout << "concatAst1 is not a concat function" << std::endl;); return; } if (!u.str.is_concat(to_app(concatAst2))) { - TRACE("t_str_detail", tout << "concatAst2 is not a concat function" << std::endl;); + TRACE("str", tout << "concatAst2 is not a concat function" << std::endl;); return; } @@ -4334,7 +4334,7 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { } } - TRACE("t_str_detail", tout << "entry 1 " << (entry1InScope ? "in scope" : "not in scope") << std::endl + TRACE("str", tout << "entry 1 " << (entry1InScope ? "in scope" : "not in scope") << std::endl << "entry 2 " << (entry2InScope ? "in scope" : "not in scope") << std::endl;); if (!entry1InScope && !entry2InScope) { @@ -4389,8 +4389,8 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { arrangement_disjunction.push_back(tester); add_theory_aware_branching_info(tester, m_params.m_OverlapTheoryAwarePriority, l_true); } else { - TRACE("t_str", tout << "AVOID LOOP: SKIPPED." << std::endl;); - TRACE("t_str", print_cut_var(m, tout); print_cut_var(y, tout);); + TRACE("str", tout << "AVOID LOOP: SKIPPED." << std::endl;); + TRACE("str", print_cut_var(m, tout); print_cut_var(y, tout);); // only add the overlap assumption one time if (!overlapAssumptionUsed) { @@ -4465,7 +4465,7 @@ void theory_str::process_unroll_eq_const_str(expr * unrollFunc, expr * constStr) zstring strValue; u.str.is_string(constStr, strValue); - TRACE("t_str_detail", tout << "unrollFunc: " << mk_pp(unrollFunc, m) << std::endl + TRACE("str", tout << "unrollFunc: " << mk_pp(unrollFunc, m) << std::endl << "constStr: " << mk_pp(constStr, m) << std::endl;); if (strValue == "") { @@ -4482,7 +4482,7 @@ void theory_str::process_concat_eq_unroll(expr * concat, expr * unroll) { context & ctx = get_context(); ast_manager & mgr = get_manager(); - TRACE("t_str_detail", tout << "concat = " << mk_pp(concat, mgr) << ", unroll = " << mk_pp(unroll, mgr) << std::endl;); + TRACE("str", tout << "concat = " << mk_pp(concat, mgr) << ", unroll = " << mk_pp(unroll, mgr) << std::endl;); std::pair key = std::make_pair(concat, unroll); expr_ref toAssert(mgr); @@ -4613,7 +4613,7 @@ static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) { bool theory_str::get_value(expr* e, rational& val) const { if (opt_DisableIntegerTheoryIntegration) { - TRACE("t_str_detail", tout << "WARNING: integer theory integration disabled" << std::endl;); + TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;); return false; } @@ -4623,28 +4623,28 @@ bool theory_str::get_value(expr* e, rational& val) const { if (!tha) { return false; } - TRACE("t_str_int", tout << "checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;); + TRACE("str", tout << "checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;); expr_ref _val(m); enode * en_e = ctx.get_enode(e); enode * it = en_e; do { if (m_autil.is_numeral(it->get_owner(), val) && val.is_int()) { // found an arithmetic term - TRACE("t_str_int", tout << mk_pp(it->get_owner(), m) << " is an integer ( ~= " << val << " )" + TRACE("str", tout << mk_pp(it->get_owner(), m) << " is an integer ( ~= " << val << " )" << std::endl;); return true; } else { - TRACE("t_str_int", tout << mk_pp(it->get_owner(), m) << " not a numeral" << std::endl;); + TRACE("str", tout << mk_pp(it->get_owner(), m) << " not a numeral" << std::endl;); } it = it->get_next(); } while (it != en_e); - TRACE("t_str_int", tout << "no arithmetic values found in eqc" << std::endl;); + TRACE("str", tout << "no arithmetic values found in eqc" << std::endl;); return false; } bool theory_str::lower_bound(expr* _e, rational& lo) { if (opt_DisableIntegerTheoryIntegration) { - TRACE("t_str_detail", tout << "WARNING: integer theory integration disabled" << std::endl;); + TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;); return false; } @@ -4658,7 +4658,7 @@ bool theory_str::lower_bound(expr* _e, rational& lo) { bool theory_str::upper_bound(expr* _e, rational& hi) { if (opt_DisableIntegerTheoryIntegration) { - TRACE("t_str_detail", tout << "WARNING: integer theory integration disabled" << std::endl;); + TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;); return false; } @@ -4672,7 +4672,7 @@ bool theory_str::upper_bound(expr* _e, rational& hi) { bool theory_str::get_len_value(expr* e, rational& val) { if (opt_DisableIntegerTheoryIntegration) { - TRACE("t_str_detail", tout << "WARNING: integer theory integration disabled" << std::endl;); + TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;); return false; } @@ -4681,16 +4681,16 @@ bool theory_str::get_len_value(expr* e, rational& val) { theory* th = ctx.get_theory(m_autil.get_family_id()); if (!th) { - TRACE("t_str_int", tout << "oops, can't get m_autil's theory" << std::endl;); + TRACE("str", tout << "oops, can't get m_autil's theory" << std::endl;); return false; } theory_mi_arith* tha = dynamic_cast(th); if (!tha) { - TRACE("t_str_int", tout << "oops, can't cast to theory_mi_arith" << std::endl;); + TRACE("str", tout << "oops, can't cast to theory_mi_arith" << std::endl;); return false; } - TRACE("t_str_int", tout << "checking len value of " << mk_ismt2_pp(e, m) << std::endl;); + TRACE("str", tout << "checking len value of " << mk_ismt2_pp(e, m) << std::endl;); rational val1; expr_ref len(m), len_val(m); @@ -4717,7 +4717,7 @@ bool theory_str::get_len_value(expr* e, rational& val) { len = mk_strlen(c); // debugging - TRACE("t_str_int", { + TRACE("str", { tout << mk_pp(len, m) << ":" << std::endl << (ctx.is_relevant(len.get()) ? "relevant" : "not relevant") << std::endl << (ctx.e_internalized(len) ? "internalized" : "not internalized") << std::endl @@ -4742,16 +4742,16 @@ bool theory_str::get_len_value(expr* e, rational& val) { if (ctx.e_internalized(len) && get_value(len, val1)) { val += val1; - TRACE("t_str_int", tout << "integer theory: subexpression " << mk_ismt2_pp(len, m) << " has length " << val1 << std::endl;); + TRACE("str", tout << "integer theory: subexpression " << mk_ismt2_pp(len, m) << " has length " << val1 << std::endl;); } else { - TRACE("t_str_int", tout << "integer theory: subexpression " << mk_ismt2_pp(len, m) << " has no length assignment; bailing out" << std::endl;); + TRACE("str", tout << "integer theory: subexpression " << mk_ismt2_pp(len, m) << " has no length assignment; bailing out" << std::endl;); return false; } } } - TRACE("t_str_int", tout << "length of " << mk_ismt2_pp(e, m) << " is " << val << std::endl;); + TRACE("str", tout << "length of " << mk_ismt2_pp(e, m) << " is " << val << std::endl;); return val.is_int(); } @@ -4769,11 +4769,11 @@ bool theory_str::in_same_eqc(expr * n1, expr * n2) { // that we've set this up properly for the context if (!ctx.e_internalized(n1)) { - TRACE("t_str_detail", tout << "WARNING: expression " << mk_ismt2_pp(n1, m) << " was not internalized" << std::endl;); + TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n1, m) << " was not internalized" << std::endl;); ctx.internalize(n1, false); } if (!ctx.e_internalized(n2)) { - TRACE("t_str_detail", tout << "WARNING: expression " << mk_ismt2_pp(n2, m) << " was not internalized" << std::endl;); + TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n2, m) << " was not internalized" << std::endl;); ctx.internalize(n2, false); } @@ -4824,7 +4824,7 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) { context & ctx = get_context(); ast_manager & m = get_manager(); - TRACE("t_str_detail", tout << "varNode = " << mk_pp(varNode, m) << ", constNode = " << mk_pp(constNode, m) << std::endl;); + TRACE("str", tout << "varNode = " << mk_pp(varNode, m) << ", constNode = " << mk_pp(constNode, m) << std::endl;); expr_ref_vector litems(m); @@ -4836,7 +4836,7 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) { expr * boolVar; if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) { - TRACE("t_str_detail", tout << "warning: no entry for boolVar in contain_pair_bool_map" << std::endl;); + TRACE("str", tout << "warning: no entry for boolVar in contain_pair_bool_map" << std::endl;); } // boolVar is actually a Contains term app * containsApp = to_app(boolVar); @@ -4844,13 +4844,13 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) { // we only want to inspect the Contains terms where either of strAst or substrAst // are equal to varNode. - TRACE("t_str_detail", tout << "considering Contains with strAst = " << mk_pp(strAst, m) << ", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;); + TRACE("t_str_detail", tout << "considering Contains with strAst = "str", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;); if (varNode != strAst && varNode != substrAst) { - TRACE("t_str_detail", tout << "varNode not equal to strAst or substrAst, skip" << std::endl;); + TRACE("str", tout << "varNode not equal to strAst or substrAst, skip" << std::endl;); continue; } - TRACE("t_str_detail", tout << "varNode matched one of strAst or substrAst. Continuing" << std::endl;); + TRACE("str", tout << "varNode matched one of strAst or substrAst. Continuing" << std::endl;); // varEqcNode is str if (strAst == varNode) { @@ -4873,7 +4873,7 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) { zstring subStrConst; u.str.is_string(substrValue, subStrConst); - TRACE("t_str_detail", tout << "strConst = " << strConst << ", subStrConst = " << subStrConst << "\n";); + TRACE("t_str_detail", tout << "strConst = "str", subStrConst = " << subStrConst << "\n";); if (strConst.contains(subStrConst)) { //implyR = ctx.mk_eq(ctx, boolVar, Z3_mk_true(ctx)); @@ -4914,7 +4914,7 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) { } } if (counterEgFound) { - TRACE("t_str_detail", tout << "Inconsistency found!" << std::endl;); + TRACE("str", tout << "Inconsistency found!" << std::endl;); break; } } @@ -4975,7 +4975,7 @@ void theory_str::check_contain_by_substr(expr * varNode, expr_ref_vector & willE expr * boolVar; if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) { - TRACE("t_str_detail", tout << "warning: no entry for boolVar in contain_pair_bool_map" << std::endl;); + TRACE("str", tout << "warning: no entry for boolVar in contain_pair_bool_map" << std::endl;); } // boolVar is actually a Contains term app * containsApp = to_app(boolVar); @@ -4983,19 +4983,19 @@ void theory_str::check_contain_by_substr(expr * varNode, expr_ref_vector & willE // we only want to inspect the Contains terms where either of strAst or substrAst // are equal to varNode. - TRACE("t_str_detail", tout << "considering Contains with strAst = " << mk_pp(strAst, m) << ", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;); + TRACE("t_str_detail", tout << "considering Contains with strAst = "str", substrAst = " << mk_pp(substrAst, m) << "..." << std::endl;); if (varNode != strAst && varNode != substrAst) { - TRACE("t_str_detail", tout << "varNode not equal to strAst or substrAst, skip" << std::endl;); + TRACE("str", tout << "varNode not equal to strAst or substrAst, skip" << std::endl;); continue; } - TRACE("t_str_detail", tout << "varNode matched one of strAst or substrAst. Continuing" << std::endl;); + TRACE("str", tout << "varNode matched one of strAst or substrAst. Continuing" << std::endl;); if (substrAst == varNode) { bool strAstHasVal = false; expr * strValue = get_eqc_value(strAst, strAstHasVal); if (strAstHasVal) { - TRACE("t_str_detail", tout << mk_pp(strAst, m) << " has constant eqc value " << mk_pp(strValue, m) << std::endl;); + TRACE("str", tout << mk_pp(strAst, m) << " has constant eqc value " << mk_pp(strValue, m) << std::endl;); if (strValue != strAst) { litems.push_back(ctx.mk_eq_atom(strAst, strValue)); } @@ -5014,7 +5014,7 @@ void theory_str::check_contain_by_substr(expr * varNode, expr_ref_vector & willE zstring pieceStr; u.str.is_string(*cstItor, pieceStr); if (!strConst.contains(pieceStr)) { - TRACE("t_str_detail", tout << "Inconsistency found!" << std::endl;); + TRACE("str", tout << "Inconsistency found!" << std::endl;); counterEgFound = true; if (aConcat != substrAst) { litems.push_back(ctx.mk_eq_atom(substrAst, aConcat)); @@ -5082,7 +5082,7 @@ void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) { expr * subValue1 = get_eqc_value(subAst1, subAst1HasValue); expr * subValue2 = get_eqc_value(subAst2, subAst2HasValue); - TRACE("t_str_detail", + TRACE("str", tout << "(Contains " << mk_pp(n1, m) << " " << mk_pp(subAst1, m) << ")" << std::endl; tout << "(Contains " << mk_pp(n2, m) << " " << mk_pp(subAst2, m) << ")" << std::endl; if (subAst1 != subValue1) { @@ -5182,7 +5182,7 @@ void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) { } std::pair tryKey1 = std::make_pair(eqSubVar1, eqSubVar2); if (contain_pair_bool_map.contains(tryKey1)) { - TRACE("t_str_detail", tout << "(Contains " << mk_pp(eqSubVar1, m) << " " << mk_pp(eqSubVar2, m) << ")" << std::endl;); + TRACE("str", tout << "(Contains " << mk_pp(eqSubVar1, m) << " " << mk_pp(eqSubVar2, m) << ")" << std::endl;); litems3.push_back(contain_pair_bool_map[tryKey1]); expr_ref implR(rewrite_implication(contain_pair_bool_map[key1], contain_pair_bool_map[key2]), m); assert_implication(mk_and(litems3), implR); @@ -5207,7 +5207,7 @@ void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) { } std::pair tryKey2 = std::make_pair(eqSubVar2, eqSubVar1); if (contain_pair_bool_map.contains(tryKey2)) { - TRACE("t_str_detail", tout << "(Contains " << mk_pp(eqSubVar2, m) << " " << mk_pp(eqSubVar1, m) << ")" << std::endl;); + TRACE("str", tout << "(Contains " << mk_pp(eqSubVar2, m) << " " << mk_pp(eqSubVar1, m) << ")" << std::endl;); litems4.push_back(contain_pair_bool_map[tryKey2]); expr_ref implR(rewrite_implication(contain_pair_bool_map[key2], contain_pair_bool_map[key1]), m); assert_implication(mk_and(litems4), implR); @@ -5229,7 +5229,7 @@ void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) { expr * strVal1 = get_eqc_value(str1, str1HasValue); expr * strVal2 = get_eqc_value(str2, str2HasValue); - TRACE("t_str_detail", + TRACE("str", tout << "(Contains " << mk_pp(str1, m) << " " << mk_pp(n1, m) << ")" << std::endl; tout << "(Contains " << mk_pp(str2, m) << " " << mk_pp(n2, m) << ")" << std::endl; if (str1 != strVal1) { @@ -5328,7 +5328,7 @@ void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) { } std::pair tryKey1 = std::make_pair(eqStrVar1, eqStrVar2); if (contain_pair_bool_map.contains(tryKey1)) { - TRACE("t_str_detail", tout << "(Contains " << mk_pp(eqStrVar1, m) << " " << mk_pp(eqStrVar2, m) << ")" << std::endl;); + TRACE("str", tout << "(Contains " << mk_pp(eqStrVar1, m) << " " << mk_pp(eqStrVar2, m) << ")" << std::endl;); litems3.push_back(contain_pair_bool_map[tryKey1]); // ------------ @@ -5356,7 +5356,7 @@ void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) { std::pair tryKey2 = std::make_pair(eqStrVar2, eqStrVar1); if (contain_pair_bool_map.contains(tryKey2)) { - TRACE("t_str_detail", tout << "(Contains " << mk_pp(eqStrVar2, m) << " " << mk_pp(eqStrVar1, m) << ")" << std::endl;); + TRACE("str", tout << "(Contains " << mk_pp(eqStrVar2, m) << " " << mk_pp(eqStrVar1, m) << ")" << std::endl;); litems4.push_back(contain_pair_bool_map[tryKey2]); // ------------ // key1.first = key2.first /\ containPairBoolMap[] @@ -5388,14 +5388,14 @@ void theory_str::check_contain_in_new_eq(expr * n1, expr * n2) { context & ctx = get_context(); ast_manager & m = get_manager(); - TRACE("t_str_detail", tout << "consistency check for contains wrt. " << mk_pp(n1, m) << " and " << mk_pp(n2, m) << std::endl;); + TRACE("str", tout << "consistency check for contains wrt. " << mk_pp(n1, m) << " and " << mk_pp(n2, m) << std::endl;); expr_ref_vector willEqClass(m); expr * constStrAst_1 = collect_eq_nodes(n1, willEqClass); expr * constStrAst_2 = collect_eq_nodes(n2, willEqClass); expr * constStrAst = (constStrAst_1 != NULL) ? constStrAst_1 : constStrAst_2; - TRACE("t_str_detail", tout << "eqc of n1 is {"; + TRACE("str", tout << "eqc of n1 is {"; for (expr_ref_vector::iterator it = willEqClass.begin(); it != willEqClass.end(); ++it) { expr * el = *it; tout << " " << mk_pp(el, m); @@ -5589,11 +5589,11 @@ void theory_str::get_grounded_concats(expr* node, std::map & varAl void theory_str::print_grounded_concat(expr * node, std::map, std::set > > & groundedMap) { ast_manager & m = get_manager(); - TRACE("t_str_detail", tout << mk_pp(node, m) << std::endl;); + TRACE("str", tout << mk_pp(node, m) << std::endl;); if (groundedMap.find(node) != groundedMap.end()) { std::map, std::set >::iterator itor = groundedMap[node].begin(); for (; itor != groundedMap[node].end(); ++itor) { - TRACE("t_str_detail", + TRACE("str", tout << "\t[grounded] "; std::vector::const_iterator vIt = itor->first.begin(); for (; vIt != itor->first.end(); ++vIt) { @@ -5609,7 +5609,7 @@ void theory_str::print_grounded_concat(expr * node, std::map string constant (len = " << strLen << ")" << std::endl;); + TRACE("str", tout << "inconsistent length: concat (len = " << sumLen << ") <==> string constant (len = " << strLen << ")" << std::endl;); assert_axiom(toAssert); return false; } @@ -5948,7 +5948,7 @@ bool theory_str::check_length_const_string(expr * n1, expr * constStr) { rational oLen; bool oLen_exists = get_len_value(n1, oLen); if (oLen_exists && oLen != strLen) { - TRACE("t_str_detail", tout << "inconsistent length: var (len = " << oLen << ") <==> string constant (len = " << strLen << ")" << std::endl;); + TRACE("str", tout << "inconsistent length: var (len = " << oLen << ") <==> string constant (len = " << strLen << ")" << std::endl;); expr_ref l(ctx.mk_eq_atom(n1, constStr), mgr); expr_ref r(ctx.mk_eq_atom(mk_strlen(n1), mk_strlen(constStr)), mgr); assert_implication(l, r); @@ -6027,7 +6027,7 @@ bool theory_str::check_length_concat_concat(expr * n1, expr * n2) { } if (conflict) { - TRACE("t_str_detail", tout << "inconsistent length detected in concat <==> concat" << std::endl;); + TRACE("str", tout << "inconsistent length detected in concat <==> concat" << std::endl;); expr_ref toAssert(mgr.mk_not(mk_and(items)), mgr); assert_axiom(toAssert); return false; @@ -6058,7 +6058,7 @@ bool theory_str::check_length_concat_var(expr * concat, expr * var) { } sumLen += argLen; if (sumLen > varLen) { - TRACE("t_str_detail", tout << "inconsistent length detected in concat <==> var" << std::endl;); + TRACE("str", tout << "inconsistent length detected in concat <==> var" << std::endl;); items.push_back(ctx.mk_eq_atom(mk_strlen(var), mk_int(varLen))); items.push_back(ctx.mk_eq_atom(concat, var)); expr_ref toAssert(mgr.mk_not(mk_and(items)), mgr); @@ -6080,7 +6080,7 @@ bool theory_str::check_length_var_var(expr * var1, expr * var2) { bool var2Len_exists = get_len_value(var2, var2Len); if (var1Len_exists && var2Len_exists && var1Len != var2Len) { - TRACE("t_str_detail", tout << "inconsistent length detected in var <==> var" << std::endl;); + TRACE("str", tout << "inconsistent length detected in var <==> var" << std::endl;); expr_ref_vector items(mgr); items.push_back(ctx.mk_eq_atom(mk_strlen(var1), mk_int(var1Len))); items.push_back(ctx.mk_eq_atom(mk_strlen(var2), mk_int(var2Len))); @@ -6164,7 +6164,7 @@ void nfa::convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u) { expr * arg_str = a->get_arg(0); zstring str; if (u.str.is_string(arg_str, str)) { - TRACE("t_str_rw", tout << "build NFA for '" << str << "'" << "\n";); + TRACE("str", tout << "build NFA for '" << str << "'" << "\n";); /* * For an n-character string, we make (n-1) intermediate states, @@ -6176,14 +6176,14 @@ void nfa::convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u) { for (int i = 0; i <= ((int)str.length()) - 2; ++i) { unsigned i_state = next_id(); make_transition(last, str[i], i_state); - TRACE("t_str_rw", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";); + TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";); last = i_state; } make_transition(last, str[(str.length() - 1)], end); - TRACE("t_str_rw", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); - TRACE("t_str_rw", tout << "string NFA: start = " << start << ", end = " << end << std::endl;); + TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); + TRACE("t_str_rw", tout << "str", end = " << end << std::endl;); } else { - TRACE("t_str_rw", tout << "invalid string constant in Str2Reg" << std::endl;); + TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;); m_valid = false; return; } @@ -6199,7 +6199,7 @@ void nfa::convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u) { make_epsilon_move(start, start1); make_epsilon_move(end1, start2); make_epsilon_move(end2, end); - TRACE("t_str_rw", tout << "concat NFA: start = " << start << ", end = " << end << std::endl;); + TRACE("str", tout << "concat NFA: start = " << start << ", end = " << end << std::endl;); } else if (u.re.is_union(e)) { app * a = to_app(e); expr * re1 = a->get_arg(0); @@ -6215,7 +6215,7 @@ void nfa::convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u) { make_epsilon_move(start, start2); make_epsilon_move(end1, end); make_epsilon_move(end2, end); - TRACE("t_str_rw", tout << "union NFA: start = " << start << ", end = " << end << std::endl;); + TRACE("str", tout << "union NFA: start = " << start << ", end = " << end << std::endl;); } else if (u.re.is_star(e)) { app * a = to_app(e); expr * subex = a->get_arg(0); @@ -6227,9 +6227,9 @@ void nfa::convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u) { make_epsilon_move(start, end); make_epsilon_move(end_subex, start_subex); make_epsilon_move(end_subex, end); - TRACE("t_str_rw", tout << "star NFA: start = " << start << ", end = " << end << std::endl;); + TRACE("str", tout << "star NFA: start = " << start << ", end = " << end << std::endl;); } else { - TRACE("t_str_rw", tout << "invalid regular expression" << std::endl;); + TRACE("str", tout << "invalid regular expression" << std::endl;); m_valid = false; return; } @@ -6327,17 +6327,17 @@ void theory_str::check_regex_in(expr * nn1, expr * nn2) { // TODO figure out regex NFA stuff if (regex_nfa_cache.find(regexTerm) == regex_nfa_cache.end()) { - TRACE("t_str_detail", tout << "regex_nfa_cache: cache miss" << std::endl;); + TRACE("str", tout << "regex_nfa_cache: cache miss" << std::endl;); regex_nfa_cache[regexTerm] = nfa(u, regexTerm); } else { - TRACE("t_str_detail", tout << "regex_nfa_cache: cache hit" << std::endl;); + TRACE("str", tout << "regex_nfa_cache: cache hit" << std::endl;); } nfa regexNFA = regex_nfa_cache[regexTerm]; ENSURE(regexNFA.is_valid()); bool matchRes = regexNFA.matches(constStrValue); - TRACE("t_str_detail", tout << mk_pp(*itor, m) << " in " << regStr << " : " << (matchRes ? "yes" : "no") << std::endl;); + TRACE("str", tout << mk_pp(*itor, m) << " in " << regStr << " : " << (matchRes ? "yes" : "no") << std::endl;); expr_ref implyL(ctx.mk_eq_atom(*itor, constStr), m); if (matchRes) { @@ -6362,7 +6362,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { ast_manager & m = get_manager(); context & ctx = get_context(); - TRACE("t_str_detail", tout << mk_ismt2_pp(concat, m) << " == " << mk_ismt2_pp(str, m) << std::endl;); + TRACE("str", tout << mk_ismt2_pp(concat, m) << " == " << mk_ismt2_pp(str, m) << std::endl;); zstring const_str; if (u.str.is_concat(to_app(concat)) && u.str.is_string(to_app(str), const_str)) { @@ -6372,7 +6372,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { expr * a2 = a_concat->get_arg(1); if (const_str.empty()) { - TRACE("t_str", tout << "quick path: concat == \"\"" << std::endl;); + TRACE("str", tout << "quick path: concat == \"\"" << std::endl;); // assert the following axiom: // ( (Concat a1 a2) == "" ) -> ( (a1 == "") AND (a2 == "") ) @@ -6391,7 +6391,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { expr * arg2 = get_eqc_value(a2, arg2_has_eqc_value); expr_ref newConcat(m); if (arg1 != a1 || arg2 != a2) { - TRACE("t_str", tout << "resolved concat argument(s) to eqc string constants" << std::endl;); + TRACE("str", tout << "resolved concat argument(s) to eqc string constants" << std::endl;); int iPos = 0; expr_ref_vector item1(m); if (a1 != arg1) { @@ -6419,7 +6419,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { } if (arg1_has_eqc_value && arg2_has_eqc_value) { // Case 1: Concat(const, const) == const - TRACE("t_str", tout << "Case 1: Concat(const, const) == const" << std::endl;); + TRACE("str", tout << "Case 1: Concat(const, const) == const" << std::endl;); zstring arg1_str, arg2_str; u.str.is_string(arg1, arg1_str); u.str.is_string(arg2, arg2_str); @@ -6427,7 +6427,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { zstring result_str = arg1_str + arg2_str; if (result_str != const_str) { // Inconsistency - TRACE("t_str", tout << "inconsistency detected: \"" + TRACE("str", tout << "inconsistency detected: \"" << arg1_str << "\" + \"" << arg2_str << "\" != \"" << const_str << "\"" << "\n";); expr_ref equality(ctx.mk_eq_atom(concat, str), m); @@ -6437,14 +6437,14 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { } } else if (!arg1_has_eqc_value && arg2_has_eqc_value) { // Case 2: Concat(var, const) == const - TRACE("t_str", tout << "Case 2: Concat(var, const) == const" << std::endl;); + TRACE("str", tout << "Case 2: Concat(var, const) == const" << std::endl;); zstring arg2_str; u.str.is_string(arg2, arg2_str); unsigned int resultStrLen = const_str.length(); unsigned int arg2StrLen = arg2_str.length(); if (resultStrLen < arg2StrLen) { // Inconsistency - TRACE("t_str", tout << "inconsistency detected: \"" + TRACE("str", tout << "inconsistency detected: \"" << arg2_str << "\" is longer than \"" << const_str << "\"," << " so cannot be concatenated with anything to form it" << "\n";); @@ -6458,7 +6458,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { zstring secondPart = const_str.extract(varStrLen, arg2StrLen); if (arg2_str != secondPart) { // Inconsistency - TRACE("t_str", tout << "inconsistency detected: " + TRACE("str", tout << "inconsistency detected: " << "suffix of concatenation result expected \"" << secondPart << "\", " << "actually \"" << arg2_str << "\"" << "\n";); @@ -6476,14 +6476,14 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { } } else if (arg1_has_eqc_value && !arg2_has_eqc_value) { // Case 3: Concat(const, var) == const - TRACE("t_str", tout << "Case 3: Concat(const, var) == const" << std::endl;); + TRACE("str", tout << "Case 3: Concat(const, var) == const" << std::endl;); zstring arg1_str; u.str.is_string(arg1, arg1_str); unsigned int resultStrLen = const_str.length(); unsigned int arg1StrLen = arg1_str.length(); if (resultStrLen < arg1StrLen) { // Inconsistency - TRACE("t_str", tout << "inconsistency detected: \"" + TRACE("str", tout << "inconsistency detected: \"" << arg1_str << "\" is longer than \"" << const_str << "\"," << " so cannot be concatenated with anything to form it" << "\n";); @@ -6497,7 +6497,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { zstring secondPart = const_str.extract(arg1StrLen, varStrLen); if (arg1_str != firstPart) { // Inconsistency - TRACE("t_str", tout << "inconsistency detected: " + TRACE("str", tout << "inconsistency detected: " << "prefix of concatenation result expected \"" << secondPart << "\", " << "actually \"" << arg1_str << "\"" << "\n";); @@ -6515,7 +6515,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { } } else { // Case 4: Concat(var, var) == const - TRACE("t_str", tout << "Case 4: Concat(var, var) == const" << std::endl;); + TRACE("str", tout << "Case 4: Concat(var, var) == const" << std::endl;); if (eval_concat(arg1, arg2) == NULL) { rational arg1Len, arg2Len; bool arg1Len_exists = get_len_value(arg1, arg1Len); @@ -6527,12 +6527,12 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { zstring prefixStr, suffixStr; if (arg1Len_exists) { if (arg1Len.is_neg()) { - TRACE("t_str_detail", tout << "length conflict: arg1Len = " << arg1Len << ", concatStrLen = " << concatStrLen << std::endl;); + TRACE("str", tout << "length conflict: arg1Len = " << arg1Len << ", concatStrLen = " << concatStrLen << std::endl;); expr_ref toAssert(m_autil.mk_ge(mk_strlen(arg1), mk_int(0)), m); assert_axiom(toAssert); return; } else if (arg1Len > concatStrLen) { - TRACE("t_str_detail", tout << "length conflict: arg1Len = " << arg1Len << ", concatStrLen = " << concatStrLen << std::endl;); + TRACE("str", tout << "length conflict: arg1Len = " << arg1Len << ", concatStrLen = " << concatStrLen << std::endl;); expr_ref ax_r1(m_autil.mk_le(mk_strlen(arg1), mk_int(concatStrLen)), m); assert_implication(ax_l1, ax_r1); return; @@ -6545,12 +6545,12 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { } else { // arg2's length is available if (arg2Len.is_neg()) { - TRACE("t_str_detail", tout << "length conflict: arg2Len = " << arg2Len << ", concatStrLen = " << concatStrLen << std::endl;); + TRACE("str", tout << "length conflict: arg2Len = " << arg2Len << ", concatStrLen = " << concatStrLen << std::endl;); expr_ref toAssert(m_autil.mk_ge(mk_strlen(arg2), mk_int(0)), m); assert_axiom(toAssert); return; } else if (arg2Len > concatStrLen) { - TRACE("t_str_detail", tout << "length conflict: arg2Len = " << arg2Len << ", concatStrLen = " << concatStrLen << std::endl;); + TRACE("str", tout << "length conflict: arg2Len = " << arg2Len << ", concatStrLen = " << concatStrLen << std::endl;); expr_ref ax_r1(m_autil.mk_le(mk_strlen(arg2), mk_int(concatStrLen)), m); assert_implication(ax_l1, ax_r1); return; @@ -6597,18 +6597,18 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { bool entry1InScope; if (entry1 == varForBreakConcat.end()) { - TRACE("t_str_detail", tout << "key1 no entry" << std::endl;); + TRACE("str", tout << "key1 no entry" << std::endl;); entry1InScope = false; } else { // OVERRIDE. entry1InScope = true; - TRACE("t_str_detail", tout << "key1 entry" << std::endl;); + TRACE("str", tout << "key1 entry" << std::endl;); /* if (internal_variable_set.find((entry1->second)[0]) == internal_variable_set.end()) { - TRACE("t_str_detail", tout << "key1 entry not in scope" << std::endl;); + TRACE("str", tout << "key1 entry not in scope" << std::endl;); entry1InScope = false; } else { - TRACE("t_str_detail", tout << "key1 entry in scope" << std::endl;); + TRACE("str", tout << "key1 entry in scope" << std::endl;); entry1InScope = true; } */ @@ -6616,24 +6616,24 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) { bool entry2InScope; if (entry2 == varForBreakConcat.end()) { - TRACE("t_str_detail", tout << "key2 no entry" << std::endl;); + TRACE("str", tout << "key2 no entry" << std::endl;); entry2InScope = false; } else { // OVERRIDE. entry2InScope = true; - TRACE("t_str_detail", tout << "key2 entry" << std::endl;); + TRACE("str", tout << "key2 entry" << std::endl;); /* if (internal_variable_set.find((entry2->second)[0]) == internal_variable_set.end()) { - TRACE("t_str_detail", tout << "key2 entry not in scope" << std::endl;); + TRACE("str", tout << "key2 entry not in scope" << std::endl;); entry2InScope = false; } else { - TRACE("t_str_detail", tout << "key2 entry in scope" << std::endl;); + TRACE("str", tout << "key2 entry in scope" << std::endl;); entry2InScope = true; } */ } - TRACE("t_str_detail", tout << "entry 1 " << (entry1InScope ? "in scope" : "not in scope") << std::endl + TRACE("str", tout << "entry 1 " << (entry1InScope ? "in scope" : "not in scope") << std::endl << "entry 2 " << (entry2InScope ? "in scope" : "not in scope") << std::endl;); if (!entry1InScope && !entry2InScope) { @@ -6702,14 +6702,14 @@ expr_ref theory_str::set_up_finite_model_test(expr * lhs, expr * rhs) { context & ctx = get_context(); ast_manager & m = get_manager(); - TRACE("t_str", tout << "activating finite model testing for overlapping concats " + TRACE("str", tout << "activating finite model testing for overlapping concats " << mk_pp(lhs, m) << " and " << mk_pp(rhs, m) << std::endl;); std::map concatMap; std::map unrollMap; std::map varMap; classify_ast_by_type(lhs, varMap, concatMap, unrollMap); classify_ast_by_type(rhs, varMap, concatMap, unrollMap); - TRACE("t_str_detail", tout << "found vars:"; + TRACE("str", tout << "found vars:"; for (std::map::iterator it = varMap.begin(); it != varMap.end(); ++it) { tout << " " << mk_pp(it->first, m); } @@ -6743,20 +6743,20 @@ void theory_str::finite_model_test(expr * testvar, expr * str) { zstring s; if (!u.str.is_string(str, s)) return; if (s == "yes") { - TRACE("t_str", tout << "start finite model test for " << mk_pp(testvar, m) << std::endl;); + TRACE("str", tout << "start finite model test for " << mk_pp(testvar, m) << std::endl;); ptr_vector & vars = finite_model_test_varlists[testvar]; for (ptr_vector::iterator it = vars.begin(); it != vars.end(); ++it) { expr * v = *it; bool v_has_eqc = false; get_eqc_value(v, v_has_eqc); if (v_has_eqc) { - TRACE("t_str_detail", tout << "variable " << mk_pp(v,m) << " already equivalent to a string constant" << std::endl;); + TRACE("str", tout << "variable " << mk_pp(v,m) << " already equivalent to a string constant" << std::endl;); continue; } // check for any sort of existing length tester we might interfere with if (m_params.m_UseBinarySearch) { if (binary_search_len_tester_stack.contains(v) && !binary_search_len_tester_stack[v].empty()) { - TRACE("t_str_detail", tout << "already found existing length testers for " << mk_pp(v, m) << std::endl;); + TRACE("str", tout << "already found existing length testers for " << mk_pp(v, m) << std::endl;); continue; } else { // start binary search as normal @@ -6783,19 +6783,19 @@ void theory_str::finite_model_test(expr * testvar, expr * str) { } if (map_effectively_empty) { - TRACE("t_str_detail", tout << "no existing length testers for " << mk_pp(v, m) << std::endl;); + TRACE("str", tout << "no existing length testers for " << mk_pp(v, m) << std::endl;); rational v_len; rational v_lower_bound; rational v_upper_bound; expr_ref vLengthExpr(mk_strlen(v), m); if (get_len_value(v, v_len)) { - TRACE("t_str_detail", tout << "length = " << v_len.to_string() << std::endl;); + TRACE("str", tout << "length = " << v_len.to_string() << std::endl;); v_lower_bound = v_len; v_upper_bound = v_len; } else { bool lower_bound_exists = lower_bound(vLengthExpr, v_lower_bound); bool upper_bound_exists = upper_bound(vLengthExpr, v_upper_bound); - TRACE("t_str_detail", tout << "bounds = [" << (lower_bound_exists?v_lower_bound.to_string():"?") + TRACE("str", tout << "bounds = [" << (lower_bound_exists?v_lower_bound.to_string():"?") << ".." << (upper_bound_exists?v_upper_bound.to_string():"?") << "]" << std::endl;); // make sure the bounds are non-negative @@ -6849,7 +6849,7 @@ void theory_str::finite_model_test(expr * testvar, expr * str) { expr_ref implRhs(mk_and(andList), m); assert_implication(implLhs, implRhs); } else { - TRACE("t_str_detail", tout << "already found existing length testers for " << mk_pp(v, m) << std::endl;); + TRACE("str", tout << "already found existing length testers for " << mk_pp(v, m) << std::endl;); continue; } } @@ -6862,7 +6862,7 @@ void theory_str::more_len_tests(expr * lenTester, zstring lenTesterValue) { if (lenTester_fvar_map.contains(lenTester)) { expr * fVar = lenTester_fvar_map[lenTester]; expr * toAssert = gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue); - TRACE("t_str_detail", tout << "asserting more length tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); + TRACE("str", tout << "asserting more length tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); if (toAssert != NULL) { assert_axiom(toAssert); } @@ -6875,24 +6875,24 @@ void theory_str::more_value_tests(expr * valTester, zstring valTesterValue) { expr * fVar = valueTester_fvar_map[valTester]; if (m_params.m_UseBinarySearch) { if (!binary_search_len_tester_stack.contains(fVar) || binary_search_len_tester_stack[fVar].empty()) { - TRACE("t_str_binary_search", tout << "WARNING: no active length testers for " << mk_pp(fVar, m) << std::endl;); + TRACE("str", tout << "WARNING: no active length testers for " << mk_pp(fVar, m) << std::endl;); NOT_IMPLEMENTED_YET(); } expr * effectiveLenInd = binary_search_len_tester_stack[fVar].back(); bool hasEqcValue; expr * len_indicator_value = get_eqc_value(effectiveLenInd, hasEqcValue); if (!hasEqcValue) { - TRACE("t_str_binary_search", tout << "WARNING: length tester " << mk_pp(effectiveLenInd, m) << " at top of stack for " << mk_pp(fVar, m) << " has no EQC value" << std::endl;); + TRACE("str", tout << "WARNING: length tester " << mk_pp(effectiveLenInd, m) << " at top of stack for " << mk_pp(fVar, m) << " has no EQC value" << std::endl;); } else { // safety check zstring effectiveLenIndiStr; u.str.is_string(len_indicator_value, effectiveLenIndiStr); if (effectiveLenIndiStr == "more" || effectiveLenIndiStr == "less") { - TRACE("t_str_binary_search", tout << "ERROR: illegal state -- requesting 'more value tests' but a length tester is not yet concrete!" << std::endl;); + TRACE("str", tout << "ERROR: illegal state -- requesting 'more value tests' but a length tester is not yet concrete!" << std::endl;); UNREACHABLE(); } expr * valueAssert = gen_free_var_options(fVar, effectiveLenInd, effectiveLenIndiStr, valTester, valTesterValue); - TRACE("t_str_detail", tout << "asserting more value tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); + TRACE("str", tout << "asserting more value tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); if (valueAssert != NULL) { assert_axiom(valueAssert); } @@ -6917,7 +6917,7 @@ void theory_str::more_value_tests(expr * valTester, zstring valTesterValue) { } } expr * valueAssert = gen_free_var_options(fVar, effectiveLenInd, effectiveLenIndiStr, valTester, valTesterValue); - TRACE("t_str_detail", tout << "asserting more value tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); + TRACE("str", tout << "asserting more value tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); if (valueAssert != NULL) { assert_axiom(valueAssert); } @@ -6928,13 +6928,13 @@ bool theory_str::free_var_attempt(expr * nn1, expr * nn2) { ast_manager & m = get_manager(); zstring nn2_str; if (internal_lenTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { - TRACE("t_str", tout << "acting on equivalence between length tester var " << mk_ismt2_pp(nn1, m) + TRACE("str", tout << "acting on equivalence between length tester var " << mk_ismt2_pp(nn1, m) << " and constant " << mk_ismt2_pp(nn2, m) << std::endl;); more_len_tests(nn1, nn2_str); return true; } else if (internal_valTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) { if (nn2_str == "more") { - TRACE("t_str", tout << "acting on equivalence between value var " << mk_ismt2_pp(nn1, m) + TRACE("str", tout << "acting on equivalence between value var " << mk_ismt2_pp(nn1, m) << " and constant " << mk_ismt2_pp(nn2, m) << std::endl;); more_value_tests(nn1, nn2_str); } @@ -6955,7 +6955,7 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) { sort * str_sort = u.str.mk_string_sort(); if (lhs_sort != str_sort || rhs_sort != str_sort) { - TRACE("t_str_detail", tout << "skip equality: not String sort" << std::endl;); + TRACE("str", tout << "skip equality: not String sort" << std::endl;); return; } @@ -6990,18 +6990,18 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) { expr * nn2_arg0 = to_app(rhs)->get_arg(0); expr * nn2_arg1 = to_app(rhs)->get_arg(1); if (nn1_arg0 == nn2_arg0 && in_same_eqc(nn1_arg1, nn2_arg1)) { - TRACE("t_str_detail", tout << "skip: lhs arg0 == rhs arg0" << std::endl;); + TRACE("str", tout << "skip: lhs arg0 == rhs arg0" << std::endl;); return; } if (nn1_arg1 == nn2_arg1 && in_same_eqc(nn1_arg0, nn2_arg0)) { - TRACE("t_str_detail", tout << "skip: lhs arg1 == rhs arg1" << std::endl;); + TRACE("str", tout << "skip: lhs arg1 == rhs arg1" << std::endl;); return; } } if (opt_DeferEQCConsistencyCheck) { - TRACE("t_str_detail", tout << "opt_DeferEQCConsistencyCheck is set; deferring new_eq_check call" << std::endl;); + TRACE("str", tout << "opt_DeferEQCConsistencyCheck is set; deferring new_eq_check call" << std::endl;); } else { // newEqCheck() -- check consistency wrt. existing equivalence classes if (!new_eq_check(lhs, rhs)) { @@ -7050,7 +7050,7 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) { std::set eqc_const_rhs; group_terms_by_eqc(rhs, eqc_concat_rhs, eqc_var_rhs, eqc_const_rhs); - TRACE("t_str_detail", + TRACE("str", tout << "lhs eqc:" << std::endl; tout << "Concats:" << std::endl; for (std::set::iterator it = eqc_concat_lhs.begin(); it != eqc_concat_lhs.end(); ++it) { @@ -7112,10 +7112,10 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) { for (itor2 = eqc_concat_rhs.begin(); itor2 != eqc_concat_rhs.end() && !found; ++itor2) { expr * concat_rhs = *itor2; if (will_result_in_overlap(concat_lhs, concat_rhs)) { - TRACE("t_str_detail", tout << "Concats " << mk_pp(concat_lhs, m) << " and " + TRACE("str", tout << "Concats " << mk_pp(concat_lhs, m) << " and " << mk_pp(concat_rhs, m) << " will result in overlap; skipping." << std::endl;); } else { - TRACE("t_str_detail", tout << "Concats " << mk_pp(concat_lhs, m) << " and " + TRACE("str", tout << "Concats " << mk_pp(concat_lhs, m) << " and " << mk_pp(concat_rhs, m) << " won't overlap. Simplifying here." << std::endl;); simplify_concat_equality(concat_lhs, concat_rhs); found = true; @@ -7124,7 +7124,7 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) { } } if (!found) { - TRACE("t_str_detail", tout << "All pairs of concats expected to overlap, falling back." << std::endl;); + TRACE("str", tout << "All pairs of concats expected to overlap, falling back." << std::endl;); simplify_concat_equality(*(eqc_concat_lhs.begin()), *(eqc_concat_rhs.begin())); } } else { @@ -7197,13 +7197,13 @@ void theory_str::set_up_axioms(expr * ex) { sort * int_sort = m.mk_sort(m_arith_fid, INT_SORT); if (ex_sort == str_sort) { - TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << + TRACE("str", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << ": expr is of sort String" << std::endl;); // set up basic string axioms enode * n = ctx.get_enode(ex); SASSERT(n); m_basicstr_axiom_todo.push_back(n); - TRACE("t_str_axiom_bug", tout << "add " << mk_pp(ex, m) << " to m_basicstr_axiom_todo" << std::endl;); + TRACE("str", tout << "add " << mk_pp(ex, m) << " to m_basicstr_axiom_todo" << std::endl;); if (is_app(ex)) { @@ -7225,21 +7225,21 @@ void theory_str::set_up_axioms(expr * ex) { } else if (u.str.is_at(ap) || u.str.is_extract(ap) || u.str.is_replace(ap)) { m_library_aware_axiom_todo.push_back(n); } else if (u.str.is_itos(ap)) { - TRACE("t_str_detail", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;); + TRACE("str", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;); string_int_conversion_terms.push_back(ap); m_library_aware_axiom_todo.push_back(n); } else if (ap->get_num_args() == 0 && !u.str.is_string(ap)) { // if ex is a variable, add it to our list of variables - TRACE("t_str_detail", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;); + TRACE("str", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;); variable_set.insert(ex); ctx.mark_as_relevant(ex); // this might help?? theory_var v = mk_var(n); - TRACE("t_str_detail", tout << "variable " << mk_ismt2_pp(ap, get_manager()) << " is #" << v << std::endl;); + TRACE("str", tout << "variable " << mk_ismt2_pp(ap, get_manager()) << " is #" << v << std::endl;); } } } else if (ex_sort == bool_sort) { - TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << + TRACE("str", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << ": expr is of sort Bool" << std::endl;); // set up axioms for boolean terms @@ -7255,13 +7255,13 @@ void theory_str::set_up_axioms(expr * ex) { } } } else { - TRACE("t_str_detail", tout << "WARNING: Bool term " << mk_ismt2_pp(ex, get_manager()) << " not internalized. Delaying axiom setup to prevent a crash." << std::endl;); + TRACE("str", tout << "WARNING: Bool term " << mk_ismt2_pp(ex, get_manager()) << " not internalized. Delaying axiom setup to prevent a crash." << std::endl;); ENSURE(!search_started); // infinite loop prevention m_delayed_axiom_setup_terms.push_back(ex); return; } } else if (ex_sort == int_sort) { - TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << + TRACE("str", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << ": expr is of sort Int" << std::endl;); // set up axioms for integer terms enode * n = ensure_enode(ex); @@ -7273,13 +7273,13 @@ void theory_str::set_up_axioms(expr * ex) { if (u.str.is_index(ap) /* || is_Indexof2(ap) || is_LastIndexof(ap) */) { m_library_aware_axiom_todo.push_back(n); } else if (u.str.is_stoi(ap)) { - TRACE("t_str_detail", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;); + TRACE("str", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;); string_int_conversion_terms.push_back(ap); m_library_aware_axiom_todo.push_back(n); } } } else { - TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << + TRACE("str", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << ": expr is of wrong sort, ignoring" << std::endl;); } @@ -7294,7 +7294,7 @@ void theory_str::set_up_axioms(expr * ex) { } void theory_str::add_theory_assumptions(expr_ref_vector & assumptions) { - TRACE("t_str", tout << "add overlap assumption for theory_str" << std::endl;); + TRACE("str", tout << "add overlap assumption for theory_str" << std::endl;); symbol strOverlap("!!TheoryStrOverlapAssumption!!"); seq_util m_sequtil(get_manager()); sort * s = get_manager().mk_bool_sort(); @@ -7315,7 +7315,7 @@ lbool theory_str::validate_unsat_core(expr_ref_vector & unsat_core) { e1 = get_context().get_enode(target_term); e2 = get_context().get_enode(core_term); if (e1 == e2) { - TRACE("t_str", tout << "overlap detected in unsat core, changing UNSAT to UNKNOWN" << std::endl;); + TRACE("str", tout << "overlap detected in unsat core, changing UNSAT to UNKNOWN" << std::endl;); assumptionFound = true; return l_undef; } @@ -7328,7 +7328,7 @@ void theory_str::init_search_eh() { ast_manager & m = get_manager(); context & ctx = get_context(); - TRACE("t_str_detail", + TRACE("str", tout << "dumping all asserted formulas:" << std::endl; unsigned nFormulas = ctx.get_num_asserted_formulas(); for (unsigned i = 0; i < nFormulas; ++i) { @@ -7360,7 +7360,7 @@ void theory_str::init_search_eh() { for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) { expr * ex = *i; if (m.is_eq(ex)) { - TRACE("t_str_detail", tout << "processing assignment " << mk_ismt2_pp(ex, m) << + TRACE("str", tout << "processing assignment " << mk_ismt2_pp(ex, m) << ": expr is equality" << std::endl;); app * eq = (app*)ex; SASSERT(eq->get_num_args() == 2); @@ -7372,7 +7372,7 @@ void theory_str::init_search_eh() { std::pair eq_pair(e_lhs, e_rhs); m_str_eq_todo.push_back(eq_pair); } else { - TRACE("t_str_detail", tout << "processing assignment " << mk_ismt2_pp(ex, m) + TRACE("str", tout << "processing assignment " << mk_ismt2_pp(ex, m) << ": expr ignored" << std::endl;); } } @@ -7382,13 +7382,13 @@ void theory_str::init_search_eh() { // before the first call to new_eq_eh() propagate(); - TRACE("t_str", tout << "search started" << std::endl;); + TRACE("str", tout << "search started" << std::endl;); search_started = true; } void theory_str::new_eq_eh(theory_var x, theory_var y) { - //TRACE("t_str_detail", tout << "new eq: v#" << x << " = v#" << y << std::endl;); - TRACE("t_str", tout << "new eq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " = " << + //TRACE("str", tout << "new eq: v#" << x << " = v#" << y << std::endl;); + TRACE("str", tout << "new eq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " = " << mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;); /* @@ -7403,18 +7403,18 @@ void theory_str::new_eq_eh(theory_var x, theory_var y) { } void theory_str::new_diseq_eh(theory_var x, theory_var y) { - //TRACE("t_str_detail", tout << "new diseq: v#" << x << " != v#" << y << std::endl;); - TRACE("t_str", tout << "new diseq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " != " << + //TRACE("str", tout << "new diseq: v#" << x << " != v#" << y << std::endl;); + TRACE("str", tout << "new diseq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " != " << mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;); } void theory_str::relevant_eh(app * n) { - TRACE("t_str", tout << "relevant: " << mk_ismt2_pp(n, get_manager()) << std::endl;); + TRACE("str", tout << "relevant: " << mk_ismt2_pp(n, get_manager()) << std::endl;); } void theory_str::assign_eh(bool_var v, bool is_true) { context & ctx = get_context(); - TRACE("t_str", tout << "assert: v" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << std::endl;); + TRACE("str", tout << "assert: v" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << std::endl;); } void theory_str::push_scope_eh() { @@ -7422,7 +7422,7 @@ void theory_str::push_scope_eh() { m_trail_stack.push_scope(); sLevel += 1; - TRACE("t_str", tout << "push to " << sLevel << std::endl;); + TRACE("str", tout << "push to " << sLevel << std::endl;); TRACE_CODE(if (is_trace_enabled("t_str_dump_assign_on_scope_change")) { dump_assignments(); }); } @@ -7446,7 +7446,7 @@ void theory_str::recursive_check_variable_scope(expr * ex) { // assume var if (variable_set.find(ex) == variable_set.end() && internal_variable_set.find(ex) == internal_variable_set.end()) { - TRACE("t_str_detail", tout << "WARNING: possible reference to out-of-scope variable " << mk_pp(ex, m) << std::endl;); + TRACE("str", tout << "WARNING: possible reference to out-of-scope variable " << mk_pp(ex, m) << std::endl;); } } } else { @@ -7466,7 +7466,7 @@ void theory_str::check_variable_scope() { return; } - TRACE("t_str_detail", tout << "checking scopes of variables in the current assignment" << std::endl;); + TRACE("str", tout << "checking scopes of variables in the current assignment" << std::endl;); context & ctx = get_context(); ast_manager & m = get_manager(); @@ -7481,7 +7481,7 @@ void theory_str::check_variable_scope() { void theory_str::pop_scope_eh(unsigned num_scopes) { sLevel -= num_scopes; - TRACE("t_str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;); + TRACE("str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;); context & ctx = get_context(); ast_manager & m = get_manager(); @@ -7495,7 +7495,7 @@ void theory_str::pop_scope_eh(unsigned num_scopes) { expr * e = varItor->m_key; std::stack & val = cut_var_map[varItor->m_key]; while ((val.size() > 0) && (val.top()->level != 0) && (val.top()->level >= sLevel)) { - TRACE("t_str_cut_var_map", tout << "remove cut info for " << mk_pp(e, m) << std::endl; print_cut_var(e, tout);); + TRACE("str", tout << "remove cut info for " << mk_pp(e, m) << std::endl; print_cut_var(e, tout);); T_cut * aCut = val.top(); val.pop(); // dealloc(aCut); @@ -7518,7 +7518,7 @@ void theory_str::pop_scope_eh(unsigned num_scopes) { for (ptr_vector::iterator it = m_basicstr_axiom_todo.begin(); it != m_basicstr_axiom_todo.end(); ++it) { enode * e = *it; app * a = e->get_owner(); - TRACE("t_str_axiom_bug", tout << "consider deleting " << mk_pp(a, get_manager()) + TRACE("str", tout << "consider deleting " << mk_pp(a, get_manager()) << ", enode scope level is " << e->get_iscope_lvl() << std::endl;); if (e->get_iscope_lvl() <= (unsigned)sLevel) { @@ -7559,7 +7559,7 @@ void theory_str::classify_ast_by_type(expr * node, std::map & varMap && internal_valTest_vars.find(node) == internal_valTest_vars.end() && internal_unrollTest_vars.find(node) == internal_unrollTest_vars.end()) { if (varMap[node] != 1) { - TRACE("t_str_detail", tout << "new variable: " << mk_pp(node, get_manager()) << std::endl;); + TRACE("str", tout << "new variable: " << mk_pp(node, get_manager()) << std::endl;); } varMap[node] = 1; } @@ -7622,7 +7622,7 @@ void theory_str::classify_ast_by_type_in_positive_context(std::map & // so we bypass a huge amount of work by doing the following... if (m.is_eq(argAst)) { - TRACE("t_str_detail", tout + TRACE("str", tout << "eq ast " << mk_pp(argAst, m) << " is between args of sort " << m.get_sort(to_app(argAst)->get_arg(0))->get_name() << std::endl;); @@ -7846,7 +7846,7 @@ int theory_str::ctx_dep_analysis(std::map & strVarMap, std::map::iterator it = variable_set.begin(); it != variable_set.end(); ++it) { expr* var = *it; if (internal_variable_set.find(var) == internal_variable_set.end()) { - TRACE("t_str_detail", tout << "new variable: " << mk_pp(var, m) << std::endl;); + TRACE("str", tout << "new variable: " << mk_pp(var, m) << std::endl;); strVarMap[*it] = 1; } } @@ -8030,7 +8030,7 @@ int theory_str::ctx_dep_analysis(std::map & strVarMap, std::map & strVarMap, std::map::iterator itor2 = inVarMap.begin(); itor2 != inVarMap.end(); itor2++) { expr * varInFunc = get_alias_index_ast(aliasIndexMap, itor2->first); - TRACE("t_str_detail", tout << "var in unroll = " << + TRACE("str", tout << "var in unroll = " << mk_ismt2_pp(itor2->first, m) << std::endl << "dealiased var = " << mk_ismt2_pp(varInFunc, m) << std::endl;); @@ -8255,7 +8255,7 @@ int theory_str::ctx_dep_analysis(std::map & strVarMap, std::map >::iterator itor = depMap.begin(); itor != depMap.end(); itor++) { tout << mk_pp(itor->first, m); @@ -8422,7 +8422,7 @@ bool theory_str::finalcheck_str2int(app * a) { rational Ival; bool Ival_exists = get_value(a, Ival); if (Ival_exists) { - TRACE("t_str_detail", tout << "integer theory assigns " << mk_pp(a, m) << " = " << Ival.to_string() << std::endl;); + TRACE("str", tout << "integer theory assigns " << mk_pp(a, m) << " = " << Ival.to_string() << std::endl;); // if that value is not -1, we can assert (str.to-int S) = Ival --> S = "Ival" if (!Ival.is_minus_one()) { zstring Ival_str(Ival.to_string().c_str()); @@ -8437,7 +8437,7 @@ bool theory_str::finalcheck_str2int(app * a) { } } } else { - TRACE("t_str_detail", tout << "integer theory has no assignment for " << mk_pp(a, m) << std::endl;); + TRACE("str", tout << "integer theory has no assignment for " << mk_pp(a, m) << std::endl;); NOT_IMPLEMENTED_YET(); } @@ -8457,7 +8457,7 @@ bool theory_str::finalcheck_int2str(app * a) { if (Sval_expr_exists) { zstring Sval; u.str.is_string(Sval_expr, Sval); - TRACE("t_str_detail", tout << "string theory assigns \"" << mk_pp(a, m) << " = " << Sval << "\n";); + TRACE("str", tout << "string theory assigns \"" << mk_pp(a, m) << " = " << Sval << "\n";); // empty string --> integer value < 0 if (Sval.empty()) { // ignore this. we should already assert the axiom for what happens when the string is "" @@ -8474,7 +8474,7 @@ bool theory_str::finalcheck_int2str(app * a) { convertedRepresentation = (ten * convertedRepresentation) + rational(val); } else { // not a digit, invalid - TRACE("t_str_rw", tout << "str.to-int argument contains non-digit character '" << digit << "'" << std::endl;); + TRACE("str", tout << "str.to-int argument contains non-digit character '" << digit << "'" << std::endl;); conversionOK = false; break; } @@ -8497,7 +8497,7 @@ bool theory_str::finalcheck_int2str(app * a) { } } } else { - TRACE("t_str_detail", tout << "string theory has no assignment for " << mk_pp(a, m) << std::endl;); + TRACE("str", tout << "string theory has no assignment for " << mk_pp(a, m) << std::endl;); NOT_IMPLEMENTED_YET(); } return axiomAdd; @@ -8535,7 +8535,7 @@ bool theory_str::propagate_length_within_eqc(expr * var) { ast_manager & m = get_manager(); context & ctx = get_context(); - TRACE("t_str_length", tout << "propagate_length_within_eqc: " << mk_ismt2_pp(var, m) << std::endl ;); + TRACE("str", tout << "propagate_length_within_eqc: " << mk_ismt2_pp(var, m) << std::endl ;); enode * n_eq_enode = ctx.get_enode(var); rational varLen; @@ -8565,7 +8565,7 @@ bool theory_str::propagate_length_within_eqc(expr * var) { expr_ref varLen(mk_strlen(var), m); expr_ref axr(ctx.mk_eq_atom(varLen, mk_int(varLen)), m); assert_implication(axl, axr); - TRACE("t_str_length", tout << mk_ismt2_pp(axl, m) << std::endl << " ---> " << std::endl << mk_ismt2_pp(axr, m);); + TRACE("str", tout << mk_ismt2_pp(axl, m) << std::endl << " ---> " << std::endl << mk_ismt2_pp(axr, m);); res = true; } } @@ -8598,7 +8598,7 @@ bool theory_str::propagate_length(std::set & varSet, std::set & co // the length fo concat is unresolved yet if (get_len_value(concat, lenValue)) { // but all leaf nodes have length information - TRACE("t_str_length", tout << "* length pop-up: " << mk_ismt2_pp(concat, m) << "| = " << lenValue << std::endl;); + TRACE("str", tout << "* length pop-up: " << mk_ismt2_pp(concat, m) << "| = " << lenValue << std::endl;); std::set leafNodes; get_unique_non_concat_nodes(concat, leafNodes); expr_ref_vector l_items(m); @@ -8619,7 +8619,7 @@ bool theory_str::propagate_length(std::set & varSet, std::set & co expr_ref lenValueExpr (mk_int(lenValue), m); expr_ref axr(ctx.mk_eq_atom(concatlenExpr, lenValueExpr), m); assert_implication(axl, axr); - TRACE("t_str_length", tout << mk_ismt2_pp(axl, m) << std::endl << " ---> " << std::endl << mk_ismt2_pp(axr, m)<< std::endl;); + TRACE("str", tout << mk_ismt2_pp(axl, m) << std::endl << " ---> " << std::endl << mk_ismt2_pp(axr, m)<< std::endl;); axiomAdded = true; } } @@ -8668,12 +8668,12 @@ final_check_status theory_str::final_check_eh() { finalCheckProgressIndicator = false; } - TRACE("t_str", tout << "final check" << std::endl;); + TRACE("str", tout << "final check" << std::endl;); TRACE_CODE(if (is_trace_enabled("t_str_dump_assign")) { dump_assignments(); }); check_variable_scope(); if (opt_DeferEQCConsistencyCheck) { - TRACE("t_str_detail", tout << "performing deferred EQC consistency check" << std::endl;); + TRACE("str", tout << "performing deferred EQC consistency check" << std::endl;); std::set eqc_roots; for (ptr_vector::const_iterator it = ctx.begin_enodes(); it != ctx.end_enodes(); ++it) { enode * e = *it; @@ -8687,16 +8687,16 @@ final_check_status theory_str::final_check_eh() { enode * e = *it; app * a = e->get_owner(); if (!(m.get_sort(a) == u.str.mk_string_sort())) { - TRACE("t_str_detail", tout << "EQC root " << mk_pp(a, m) << " not a string term; skipping" << std::endl;); + TRACE("str", tout << "EQC root " << mk_pp(a, m) << " not a string term; skipping" << std::endl;); } else { - TRACE("t_str_detail", tout << "EQC root " << mk_pp(a, m) << " is a string term. Checking this EQC" << std::endl;); + TRACE("str", tout << "EQC root " << mk_pp(a, m) << " is a string term. Checking this EQC" << std::endl;); // first call check_concat_len_in_eqc() on each member of the eqc enode * e_it = e; enode * e_root = e_it; do { bool status = check_concat_len_in_eqc(e_it->get_owner()); if (!status) { - TRACE("t_str_detail", tout << "concat-len check asserted an axiom on " << mk_pp(e_it->get_owner(), m) << std::endl;); + TRACE("str", tout << "concat-len check asserted an axiom on " << mk_pp(e_it->get_owner(), m) << std::endl;); found_inconsistency = true; } e_it = e_it->get_next(); @@ -8706,10 +8706,10 @@ final_check_status theory_str::final_check_eh() { enode * e1 = e; enode * e2 = e1->get_next(); if (e1 != e2) { - TRACE("t_str_detail", tout << "deferred new_eq_check() over EQC of " << mk_pp(e1->get_owner(), m) << " and " << mk_pp(e2->get_owner(), m) << std::endl;); + TRACE("str", tout << "deferred new_eq_check() over EQC of " << mk_pp(e1->get_owner(), m) << " and " << mk_pp(e2->get_owner(), m) << std::endl;); bool result = new_eq_check(e1->get_owner(), e2->get_owner()); if (!result) { - TRACE("t_str_detail", tout << "new_eq_check found inconsistencies" << std::endl;); + TRACE("str", tout << "new_eq_check found inconsistencies" << std::endl;); found_inconsistency = true; } } @@ -8717,10 +8717,10 @@ final_check_status theory_str::final_check_eh() { } if (found_inconsistency) { - TRACE("t_str", tout << "Found inconsistency in final check! Returning to search." << std::endl;); + TRACE("str", tout << "Found inconsistency in final check! Returning to search." << std::endl;); return FC_CONTINUE; } else { - TRACE("t_str", tout << "Deferred consistency check passed. Continuing in final check." << std::endl;); + TRACE("str", tout << "Deferred consistency check passed. Continuing in final check." << std::endl;); } } @@ -8753,7 +8753,7 @@ final_check_status theory_str::final_check_eh() { expr * concat_rhs_str = get_eqc_value(concat_rhs, concat_rhs_haseqc); expr * var_str = get_eqc_value(var, var_haseqc); if (concat_lhs_haseqc && concat_rhs_haseqc && !var_haseqc) { - TRACE("t_str_detail", tout << "backpropagate into " << mk_pp(var, m) << " = " << mk_pp(concat, m) << std::endl + TRACE("str", tout << "backpropagate into " << mk_pp(var, m) << " = " << mk_pp(concat, m) << std::endl << "LHS ~= " << mk_pp(concat_lhs_str, m) << " RHS ~= " << mk_pp(concat_rhs_str, m) << std::endl;); zstring lhsString, rhsString; u.str.is_string(concat_lhs_str, lhsString); @@ -8770,7 +8770,7 @@ final_check_status theory_str::final_check_eh() { } if (backpropagation_occurred) { - TRACE("t_str", tout << "Resuming search due to axioms added by backpropagation." << std::endl;); + TRACE("str", tout << "Resuming search due to axioms added by backpropagation." << std::endl;); return FC_CONTINUE; } @@ -8782,7 +8782,7 @@ final_check_status theory_str::final_check_eh() { bool length_propagation_occurred = propagate_length(varSet, concatSet, exprLenMap); if (length_propagation_occurred) { - TRACE("t_str", tout << "Resuming search due to axioms added by length propagation." << std::endl;); + TRACE("str", tout << "Resuming search due to axioms added by length propagation." << std::endl;); return FC_CONTINUE; } } @@ -8801,19 +8801,19 @@ final_check_status theory_str::final_check_eh() { if (internal_variable_set.find(itor->first) != internal_variable_set.end() || regex_variable_set.find(itor->first) != regex_variable_set.end()) { // this can be ignored, I think - TRACE("t_str_detail", tout << "free internal variable " << mk_pp(itor->first, m) << " ignored" << std::endl;); + TRACE("str", tout << "free internal variable " << mk_pp(itor->first, m) << " ignored" << std::endl;); continue; } bool hasEqcValue = false; expr * eqcString = get_eqc_value(itor->first, hasEqcValue); if (!hasEqcValue) { - TRACE("t_str_detail", tout << "found free variable " << mk_pp(itor->first, m) << std::endl;); + TRACE("str", tout << "found free variable " << mk_pp(itor->first, m) << std::endl;); needToAssignFreeVars = true; free_variables.insert(itor->first); // break; } else { // debug - TRACE("t_str_detail", tout << "variable " << mk_pp(itor->first, m) << " = " << mk_pp(eqcString, m) << std::endl;); + TRACE("str", tout << "variable " << mk_pp(itor->first, m) << " = " << mk_pp(eqcString, m) << std::endl;); } } } @@ -8839,15 +8839,15 @@ final_check_status theory_str::final_check_eh() { } } if (addedStrIntAxioms) { - TRACE("t_str", tout << "Resuming search due to addition of string-integer conversion axioms." << std::endl;); + TRACE("str", tout << "Resuming search due to addition of string-integer conversion axioms." << std::endl;); return FC_CONTINUE; } if (unused_internal_variables.empty()) { - TRACE("t_str", tout << "All variables are assigned. Done!" << std::endl;); + TRACE("str", tout << "All variables are assigned. Done!" << std::endl;); return FC_DONE; } else { - TRACE("t_str", tout << "Assigning decoy values to free internal variables." << std::endl;); + TRACE("str", tout << "Assigning decoy values to free internal variables." << std::endl;); for (std::set::iterator it = unused_internal_variables.begin(); it != unused_internal_variables.end(); ++it) { expr * var = *it; expr_ref assignment(m.mk_eq(var, mk_string("**unused**")), m); @@ -8857,7 +8857,7 @@ final_check_status theory_str::final_check_eh() { } } - CTRACE("t_str", needToAssignFreeVars, + CTRACE("str", needToAssignFreeVars, tout << "Need to assign values to the following free variables:" << std::endl; for (std::set::iterator itx = free_variables.begin(); itx != free_variables.end(); ++itx) { tout << mk_ismt2_pp(*itx, m) << std::endl; @@ -8890,7 +8890,7 @@ final_check_status theory_str::final_check_eh() { for (std::map >::iterator fvIt3 = fv_unrolls_map.begin(); fvIt3 != fv_unrolls_map.end(); fvIt3++) { expr * var = fvIt3->first; - TRACE("t_str_detail", tout << "erase free variable " << mk_pp(var, m) << " from freeVar_map, it is bounded by an Unroll" << std::endl;); + TRACE("str", tout << "erase free variable " << mk_pp(var, m) << " from freeVar_map, it is bounded by an Unroll" << std::endl;); freeVar_map.erase(var); } @@ -8954,7 +8954,7 @@ final_check_status theory_str::final_check_eh() { } } for (std::set::iterator vItor = fvUnrollSet.begin(); vItor != fvUnrollSet.end(); vItor++) { - TRACE("t_str_detail", tout << "remove " << mk_pp(*vItor, m) << " from freeVar_map" << std::endl;); + TRACE("str", tout << "remove " << mk_pp(*vItor, m) << " from freeVar_map" << std::endl;); freeVar_map.erase(*vItor); } @@ -8964,7 +8964,7 @@ final_check_status theory_str::final_check_eh() { constValue = NULL; { - TRACE("t_str_detail", tout << "free var map (#" << freeVar_map.size() << "):" << std::endl; + TRACE("str", tout << "free var map (#" << freeVar_map.size() << "):" << std::endl; for (std::map::iterator freeVarItor1 = freeVar_map.begin(); freeVarItor1 != freeVar_map.end(); freeVarItor1++) { expr * freeVar = freeVarItor1->first; rational lenValue; @@ -9010,7 +9010,7 @@ final_check_status theory_str::final_check_eh() { // experimental free variable assignment - end // now deal with removed free variables that are bounded by an unroll - TRACE("t_str", tout << "fv_unrolls_map (#" << fv_unrolls_map.size() << "):" << std::endl;); + TRACE("str", tout << "fv_unrolls_map (#" << fv_unrolls_map.size() << "):" << std::endl;); for (std::map >::iterator fvIt1 = fv_unrolls_map.begin(); fvIt1 != fv_unrolls_map.end(); fvIt1++) { expr * var = fvIt1->first; @@ -9027,7 +9027,7 @@ final_check_status theory_str::final_check_eh() { } if (opt_VerifyFinalCheckProgress && !finalCheckProgressIndicator) { - TRACE("t_str", tout << "BUG: no progress in final check, giving up!!" << std::endl;); + TRACE("str", tout << "BUG: no progress in final check, giving up!!" << std::endl;); m.raise_exception("no progress in theory_str final check"); } @@ -9049,7 +9049,7 @@ inline std::string longlong_to_string(long long i) { void theory_str::print_value_tester_list(svector > & testerList) { ast_manager & m = get_manager(); - TRACE("t_str_detail", + TRACE("str", int ss = testerList.size(); tout << "valueTesterList = {"; for (int i = 0; i < ss; ++i) { @@ -9084,7 +9084,7 @@ zstring theory_str::gen_val_string(int len, int_vector & encoding) { bool theory_str::get_next_val_encode(int_vector & base, int_vector & next) { SASSERT(charSetSize > 0); - TRACE("t_str_value_test_bug", tout << "base vector: [ "; + TRACE("str", tout << "base vector: [ "; for (unsigned i = 0; i < base.size(); ++i) { tout << base[i] << " "; } @@ -9140,7 +9140,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * svector options; int_vector base; - TRACE("t_str_detail", tout + TRACE("str", tout << "freeVar = " << mk_ismt2_pp(freeVar, m) << std::endl << "len_indicator = " << mk_ismt2_pp(len_indicator, m) << std::endl << "val_indicator = " << mk_ismt2_pp(val_indicator, m) << std::endl @@ -9156,7 +9156,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * coverAll = false; } else { expr * lastestValIndi = fvar_valueTester_map[freeVar][len][tries - 1].second; - TRACE("t_str_detail", tout << "last value tester = " << mk_ismt2_pp(lastestValIndi, m) << std::endl;); + TRACE("str", tout << "last value tester = " << mk_ismt2_pp(lastestValIndi, m) << std::endl;); coverAll = get_next_val_encode(val_range_map[lastestValIndi], base); } @@ -9171,7 +9171,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * } val_range_map[val_indicator] = options[options.size() - 1]; - TRACE("t_str_detail", + TRACE("str", tout << "value tester encoding " << "{" << std::endl; int_vector vec = val_range_map[val_indicator]; @@ -9266,7 +9266,7 @@ expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, int len = atoi(len_valueStr.encode().c_str()); // check whether any value tester is actually in scope - TRACE("t_str_detail", tout << "checking scope of previous value testers" << std::endl;); + TRACE("str", tout << "checking scope of previous value testers" << std::endl;); bool map_effectively_empty = true; if (fvar_valueTester_map[freeVar].find(len) != fvar_valueTester_map[freeVar].end()) { // there's *something* in the map, but check its scope @@ -9275,9 +9275,9 @@ expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, std::pair entry = *it; expr * aTester = entry.second; if (internal_variable_set.find(aTester) == internal_variable_set.end()) { - TRACE("t_str_detail", tout << mk_pp(aTester, m) << " out of scope" << std::endl;); + TRACE("str", tout << mk_pp(aTester, m) << " out of scope" << std::endl;); } else { - TRACE("t_str_detail", tout << mk_pp(aTester, m) << " in scope" << std::endl;); + TRACE("str", tout << mk_pp(aTester, m) << " in scope" << std::endl;); map_effectively_empty = false; break; } @@ -9285,7 +9285,7 @@ expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, } if (map_effectively_empty) { - TRACE("t_str_detail", tout << "no previous value testers, or none of them were in scope" << std::endl;); + TRACE("str", tout << "no previous value testers, or none of them were in scope" << std::endl;); int tries = 0; expr * val_indicator = mk_internal_valTest_var(freeVar, len, tries); valueTester_fvar_map[val_indicator] = freeVar; @@ -9293,7 +9293,7 @@ expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, print_value_tester_list(fvar_valueTester_map[freeVar][len]); return gen_val_options(freeVar, len_indicator, val_indicator, len_valueStr, tries); } else { - TRACE("t_str_detail", tout << "checking previous value testers" << std::endl;); + TRACE("str", tout << "checking previous value testers" << std::endl;); print_value_tester_list(fvar_valueTester_map[freeVar][len]); // go through all previous value testers @@ -9305,7 +9305,7 @@ expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, // it's probably worth checking scope here, actually if (internal_variable_set.find(aTester) == internal_variable_set.end()) { - TRACE("t_str_detail", tout << "value tester " << mk_pp(aTester, m) << " out of scope, skipping" << std::endl;); + TRACE("str", tout << "value tester " << mk_pp(aTester, m) << " out of scope, skipping" << std::endl;); continue; } @@ -9317,17 +9317,17 @@ expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, // Z3_ast anEqc = get_eqc_value(t, aTester, anEqcHasValue); expr * aTester_eqc_value = get_eqc_value(aTester, anEqcHasValue); if (!anEqcHasValue) { - TRACE("t_str_detail", tout << "value tester " << mk_ismt2_pp(aTester, m) + TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) << " doesn't have an equivalence class value." << std::endl;); refresh_theory_var(aTester); expr * makeupAssert = gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i); - TRACE("t_str_detail", tout << "var: " << mk_ismt2_pp(freeVar, m) << std::endl + TRACE("str", tout << "var: " << mk_ismt2_pp(freeVar, m) << std::endl << mk_ismt2_pp(makeupAssert, m) << std::endl;); assert_axiom(makeupAssert); } else { - TRACE("t_str_detail", tout << "value tester " << mk_ismt2_pp(aTester, m) + TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m) << " == " << mk_ismt2_pp(aTester_eqc_value, m) << std::endl;); } } @@ -9355,7 +9355,7 @@ void theory_str::reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vect context & ctx = get_context(); ast_manager & mgr = get_manager(); - TRACE("t_str_detail", tout << "reduce regex " << mk_pp(regex, mgr) << " with respect to variable " << mk_pp(var, mgr) << std::endl;); + TRACE("str", tout << "reduce regex " << mk_pp(regex, mgr) << " with respect to variable " << mk_pp(var, mgr) << std::endl;); app * regexFuncDecl = to_app(regex); if (u.re.is_to_re(regexFuncDecl)) { @@ -9443,7 +9443,7 @@ void theory_str::gen_assign_unroll_reg(std::set & unrolls) { expr_ref_vector items(mgr); for (std::set::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) { expr * unrFunc = *itor; - TRACE("t_str_detail", tout << "generating assignment for unroll " << mk_pp(unrFunc, mgr) << std::endl;); + TRACE("str", tout << "generating assignment for unroll " << mk_pp(unrFunc, mgr) << std::endl;); expr * regexInUnr = to_app(unrFunc)->get_arg(0); expr * cntInUnr = to_app(unrFunc)->get_arg(1); @@ -9453,7 +9453,7 @@ void theory_str::gen_assign_unroll_reg(std::set & unrolls) { bool low_exists = lower_bound(cntInUnr, low); bool high_exists = upper_bound(cntInUnr, high); - TRACE("t_str_detail", + TRACE("str", tout << "unroll " << mk_pp(unrFunc, mgr) << std::endl; rational unrLenValue; bool unrLenValue_exists = get_len_value(unrFunc, unrLenValue); @@ -9599,7 +9599,7 @@ expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & expr_ref moreAst(mk_string("more"), mgr); for (std::set::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) { expr_ref item(ctx.mk_eq_atom(var, *itor), mgr); - TRACE("t_str_detail", tout << "considering unroll " << mk_pp(item, mgr) << std::endl;); + TRACE("str", tout << "considering unroll " << mk_pp(item, mgr) << std::endl;); litems.push_back(item); } @@ -9611,7 +9611,7 @@ expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & it != unroll_tries_map[var][unrolls].end(); ++it) { expr * tester = *it; bool inScope = (internal_unrollTest_vars.find(tester) != internal_unrollTest_vars.end()); - TRACE("t_str_detail", tout << "unroll test var " << mk_pp(tester, mgr) + TRACE("str", tout << "unroll test var " << mk_pp(tester, mgr) << (inScope ? " in scope" : " out of scope") << std::endl;); if (!inScope) { @@ -9644,13 +9644,13 @@ expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & expr_ref rImp(gen_unroll_assign(var, lcmStr, tester, l, h), mgr); SASSERT(lImp); - TRACE("t_str_detail", tout << "lImp = " << mk_pp(lImp, mgr) << std::endl;); + TRACE("str", tout << "lImp = " << mk_pp(lImp, mgr) << std::endl;); SASSERT(rImp); - TRACE("t_str_detail", tout << "rImp = " << mk_pp(rImp, mgr) << std::endl;); + TRACE("str", tout << "rImp = " << mk_pp(rImp, mgr) << std::endl;); expr_ref toAssert(mgr.mk_or(mgr.mk_not(lImp), rImp), mgr); SASSERT(toAssert); - TRACE("t_str_detail", tout << "Making up assignments for variable which is equal to unbounded Unroll" << std::endl;); + TRACE("str", tout << "Making up assignments for variable which is equal to unbounded Unroll" << std::endl;); m_trail.push_back(toAssert); return toAssert; @@ -9662,7 +9662,7 @@ expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & } else { zstring testerStr; u.str.is_string(testerVal, testerStr); - TRACE("t_str_detail", tout << "Tester [" << mk_pp(tester, mgr) << "] = " << testerStr << "\n";); + TRACE("str", tout << "Tester [" << mk_pp(tester, mgr) << "] = " << testerStr << "\n";); if (testerStr == "more") { litems.push_back(ctx.mk_eq_atom(tester, moreAst)); } @@ -9678,7 +9678,7 @@ expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & SASSERT(rImp); expr_ref toAssert(mgr.mk_or(mgr.mk_not(lImp), rImp), mgr); SASSERT(toAssert); - TRACE("t_str_detail", tout << "Generating assignment for variable which is equal to unbounded Unroll" << std::endl;); + TRACE("str", tout << "Generating assignment for variable which is equal to unbounded Unroll" << std::endl;); m_trail.push_back(toAssert); return toAssert; } @@ -9687,11 +9687,11 @@ expr * theory_str::gen_unroll_assign(expr * var, zstring lcmStr, expr * testerVa context & ctx = get_context(); ast_manager & mgr = get_manager(); - TRACE("t_str_detail", tout << "entry: var = " << mk_pp(var, mgr) << ", lcmStr = " << lcmStr + TRACE("str", tout << "entry: var = " << mk_pp(var, mgr) << ", lcmStr = " << lcmStr << ", l = " << l << ", h = " << h << "\n";); if (m_params.m_AggressiveUnrollTesting) { - TRACE("t_str_detail", tout << "note: aggressive unroll testing is active" << std::endl;); + TRACE("str", tout << "note: aggressive unroll testing is active" << std::endl;); } expr_ref_vector orItems(mgr); @@ -9700,7 +9700,7 @@ expr * theory_str::gen_unroll_assign(expr * var, zstring lcmStr, expr * testerVa for (int i = l; i < h; i++) { zstring iStr = int_to_string(i); expr_ref testerEqAst(ctx.mk_eq_atom(testerVar, mk_string(iStr)), mgr); - TRACE("t_str_detail", tout << "testerEqAst = " << mk_pp(testerEqAst, mgr) << std::endl;); + TRACE("str", tout << "testerEqAst = " << mk_pp(testerEqAst, mgr) << std::endl;); if (m_params.m_AggressiveUnrollTesting) { literal l = mk_eq(testerVar, mk_string(iStr), false); ctx.mark_as_relevant(l); @@ -9711,15 +9711,15 @@ expr * theory_str::gen_unroll_assign(expr * var, zstring lcmStr, expr * testerVa zstring unrollStrInstance = get_unrolled_string(lcmStr, i); expr_ref x1(ctx.mk_eq_atom(testerEqAst, ctx.mk_eq_atom(var, mk_string(unrollStrInstance))), mgr); - TRACE("t_str_detail", tout << "x1 = " << mk_pp(x1, mgr) << std::endl;); + TRACE("str", tout << "x1 = " << mk_pp(x1, mgr) << std::endl;); andItems.push_back(x1); expr_ref x2(ctx.mk_eq_atom(testerEqAst, ctx.mk_eq_atom(mk_strlen(var), mk_int(i * lcmStr.length()))), mgr); - TRACE("t_str_detail", tout << "x2 = " << mk_pp(x2, mgr) << std::endl;); + TRACE("str", tout << "x2 = " << mk_pp(x2, mgr) << std::endl;); andItems.push_back(x2); } expr_ref testerEqMore(ctx.mk_eq_atom(testerVar, mk_string("more")), mgr); - TRACE("t_str_detail", tout << "testerEqMore = " << mk_pp(testerEqMore, mgr) << std::endl;); + TRACE("str", tout << "testerEqMore = " << mk_pp(testerEqMore, mgr) << std::endl;); if (m_params.m_AggressiveUnrollTesting) { literal l = mk_eq(testerVar, mk_string("more"), false); ctx.mark_as_relevant(l); @@ -9732,15 +9732,15 @@ expr * theory_str::gen_unroll_assign(expr * var, zstring lcmStr, expr * testerVa //Z3_mk_ge(mk_length(t, var), mk_int(ctx, nextLowerLenBound)) m_autil.mk_ge(m_autil.mk_add(mk_strlen(var), mk_int(-1 * nextLowerLenBound)), mk_int(0)) ), mgr); - TRACE("t_str_detail", tout << "more2 = " << mk_pp(more2, mgr) << std::endl;); + TRACE("str", tout << "more2 = " << mk_pp(more2, mgr) << std::endl;); andItems.push_back(more2); expr_ref finalOR(mgr.mk_or(orItems.size(), orItems.c_ptr()), mgr); - TRACE("t_str_detail", tout << "finalOR = " << mk_pp(finalOR, mgr) << std::endl;); + TRACE("str", tout << "finalOR = " << mk_pp(finalOR, mgr) << std::endl;); andItems.push_back(mk_or(orItems)); expr_ref finalAND(mgr.mk_and(andItems.size(), andItems.c_ptr()), mgr); - TRACE("t_str_detail", tout << "finalAND = " << mk_pp(finalAND, mgr) << std::endl;); + TRACE("str", tout << "finalAND = " << mk_pp(finalAND, mgr) << std::endl;); // doing the following avoids a segmentation fault m_trail.push_back(finalAND); @@ -9761,7 +9761,7 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr int l = (tries - 1) * distance; int h = tries * distance; - TRACE("t_str_detail", + TRACE("str", tout << "building andList and orList" << std::endl; if (m_params.m_AggressiveLengthTesting) { tout << "note: aggressive length testing is active" << std::endl; @@ -9848,11 +9848,11 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr and_items.push_back(andList.get(i)); } - TRACE("t_str_detail", tout << "check: " << mk_pp(mk_and(and_items), m) << std::endl;); + TRACE("str", tout << "check: " << mk_pp(mk_and(and_items), m) << std::endl;); expr_ref lenTestAssert = mk_and(and_items); SASSERT(lenTestAssert); - TRACE("t_str_detail", tout << "crash avoidance lenTestAssert: " << mk_pp(lenTestAssert, m) << std::endl;); + TRACE("str", tout << "crash avoidance lenTestAssert: " << mk_pp(lenTestAssert, m) << std::endl;); int testerCount = tries - 1; if (testerCount > 0) { @@ -9861,10 +9861,10 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr for (int i = 0; i < testerCount; ++i) { expr * indicator = fvar_lenTester_map[freeVar][i]; if (internal_variable_set.find(indicator) == internal_variable_set.end()) { - TRACE("t_str_detail", tout << "indicator " << mk_pp(indicator, m) << " out of scope; continuing" << std::endl;); + TRACE("str", tout << "indicator " << mk_pp(indicator, m) << " out of scope; continuing" << std::endl;); continue; } else { - TRACE("t_str_detail", tout << "indicator " << mk_pp(indicator, m) << " in scope" << std::endl;); + TRACE("str", tout << "indicator " << mk_pp(indicator, m) << " in scope" << std::endl;); and_items_LHS.push_back(ctx.mk_eq_atom(indicator, moreAst)); } } @@ -9872,10 +9872,10 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr SASSERT(assertL); expr * finalAxiom = m.mk_or(m.mk_not(assertL), lenTestAssert.get()); SASSERT(finalAxiom != NULL); - TRACE("t_str_detail", tout << "crash avoidance finalAxiom: " << mk_pp(finalAxiom, m) << std::endl;); + TRACE("str", tout << "crash avoidance finalAxiom: " << mk_pp(finalAxiom, m) << std::endl;); return finalAxiom; } else { - TRACE("t_str_detail", tout << "crash avoidance lenTestAssert.get(): " << mk_pp(lenTestAssert.get(), m) << std::endl;); + TRACE("str", tout << "crash avoidance lenTestAssert.get(): " << mk_pp(lenTestAssert.get(), m) << std::endl;); m_trail.push_back(lenTestAssert.get()); return lenTestAssert.get(); } @@ -9892,7 +9892,7 @@ expr_ref theory_str::binary_search_case_split(expr * freeVar, expr * tester, bin rational N_plus_one = N + rational::one(); expr_ref lenFreeVar(mk_strlen(freeVar), m); - TRACE("t_str_binary_search", tout << "create case split for free var " << mk_pp(freeVar, m) + TRACE("str", tout << "create case split for free var " << mk_pp(freeVar, m) << " over " << mk_pp(tester, m) << " with midpoint " << N << std::endl;); expr_ref_vector combinedCaseSplit(m); @@ -9924,7 +9924,7 @@ expr_ref theory_str::binary_search_case_split(expr * freeVar, expr * tester, bin expr_ref final_term(mk_and(combinedCaseSplit), m); SASSERT(final_term); - TRACE("t_str_binary_search", tout << "final term: " << mk_pp(final_term, m) << std::endl;); + TRACE("str", tout << "final term: " << mk_pp(final_term, m) << std::endl;); return final_term; } @@ -9933,7 +9933,7 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT context & ctx = get_context(); if (binary_search_len_tester_stack.contains(freeVar) && !binary_search_len_tester_stack[freeVar].empty()) { - TRACE("t_str_binary_search", tout << "checking existing length testers for " << mk_pp(freeVar, m) << std::endl; + TRACE("str", tout << "checking existing length testers for " << mk_pp(freeVar, m) << std::endl; for (ptr_vector::const_iterator it = binary_search_len_tester_stack[freeVar].begin(); it != binary_search_len_tester_stack[freeVar].end(); ++it) { expr * tester = *it; @@ -9959,35 +9959,35 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT expr * lastTesterValue = get_eqc_value(lastTester, lastTesterHasEqcValue); zstring lastTesterConstant; if (!lastTesterHasEqcValue) { - TRACE("t_str_binary_search", tout << "length tester " << mk_pp(lastTester, m) << " at top of stack doesn't have an EQC value yet" << std::endl;); + TRACE("str", tout << "length tester " << mk_pp(lastTester, m) << " at top of stack doesn't have an EQC value yet" << std::endl;); // check previousLenTester if (previousLenTester == lastTester) { lastTesterConstant = previousLenTesterValue; - TRACE("t_str_binary_search", tout << "invoked with previousLenTester info matching top of stack" << std::endl;); + TRACE("str", tout << "invoked with previousLenTester info matching top of stack" << std::endl;); } else { - TRACE("t_str_binary_search", tout << "WARNING: unexpected reordering of length testers!" << std::endl;); + TRACE("str", tout << "WARNING: unexpected reordering of length testers!" << std::endl;); UNREACHABLE(); return NULL; } } else { u.str.is_string(lastTesterValue, lastTesterConstant); } - TRACE("t_str_binary_search", tout << "last length tester is assigned \"" << lastTesterConstant << "\"" << "\n";); + TRACE("str", tout << "last length tester is assigned \"" << lastTesterConstant << "\"" << "\n";); if (lastTesterConstant == "more" || lastTesterConstant == "less") { // use the previous bounds info to generate a new midpoint binary_search_info lastBounds; if (!binary_search_len_tester_info.find(lastTester, lastBounds)) { // unexpected - TRACE("t_str_binary_search", tout << "WARNING: no bounds information available for last tester!" << std::endl;); + TRACE("str", tout << "WARNING: no bounds information available for last tester!" << std::endl;); UNREACHABLE(); } - TRACE("t_str_binary_search", tout << "last bounds are [" << lastBounds.lowerBound << " | " << lastBounds.midPoint << " | " << lastBounds.upperBound << "]!" << lastBounds.windowSize << std::endl;); + TRACE("str", tout << "last bounds are [" << lastBounds.lowerBound << " | " << lastBounds.midPoint << " | " << lastBounds.upperBound << "]!" << lastBounds.windowSize << std::endl;); binary_search_info newBounds; expr * newTester; if (lastTesterConstant == "more") { // special case: if the midpoint, upper bound, and window size are all equal, // we double the window size and adjust the bounds if (lastBounds.midPoint == lastBounds.upperBound && lastBounds.upperBound == lastBounds.windowSize) { - TRACE("t_str_binary_search", tout << "search hit window size; expanding" << std::endl;); + TRACE("str", tout << "search hit window size; expanding" << std::endl;); newBounds.lowerBound = lastBounds.windowSize + rational::one(); newBounds.windowSize = lastBounds.windowSize * rational(2); newBounds.upperBound = newBounds.windowSize; @@ -10024,7 +10024,7 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT } refresh_theory_var(newTester); } - TRACE("t_str_binary_search", tout << "new bounds are [" << newBounds.lowerBound << " | " << newBounds.midPoint << " | " << newBounds.upperBound << "]!" << newBounds.windowSize << std::endl;); + TRACE("str", tout << "new bounds are [" << newBounds.lowerBound << " | " << newBounds.midPoint << " | " << newBounds.upperBound << "]!" << newBounds.windowSize << std::endl;); binary_search_len_tester_stack[freeVar].push_back(newTester); m_trail_stack.push(binary_search_trail(binary_search_len_tester_stack, freeVar)); binary_search_len_tester_info.insert(newTester, newBounds); @@ -10036,16 +10036,16 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT // ctx.mk_th_case_split(case_split_literals.size(), case_split_literals.c_ptr()); return next_case_split; } else { // lastTesterConstant is a concrete value - TRACE("t_str", tout << "length is fixed; generating models for free var" << std::endl;); + TRACE("str", tout << "length is fixed; generating models for free var" << std::endl;); // defensive check that this length did not converge on a negative value. binary_search_info lastBounds; if (!binary_search_len_tester_info.find(lastTester, lastBounds)) { // unexpected - TRACE("t_str_binary_search", tout << "WARNING: no bounds information available for last tester!" << std::endl;); + TRACE("str", tout << "WARNING: no bounds information available for last tester!" << std::endl;); UNREACHABLE(); } if (lastBounds.midPoint.is_neg()) { - TRACE("t_str_binary_search", tout << "WARNING: length search converged on a negative value. Negating this constraint." << std::endl;); + TRACE("str", tout << "WARNING: length search converged on a negative value. Negating this constraint." << std::endl;); expr_ref axiom(m_autil.mk_ge(mk_strlen(freeVar), m_autil.mk_numeral(rational::zero(), true)), m); return axiom; } @@ -10055,7 +10055,7 @@ expr * theory_str::binary_search_length_test(expr * freeVar, expr * previousLenT } } else { // no length testers yet - TRACE("t_str_binary_search", tout << "no length testers for " << mk_pp(freeVar, m) << std::endl;); + TRACE("str", tout << "no length testers for " << mk_pp(freeVar, m) << std::endl;); binary_search_len_tester_stack.insert(freeVar, ptr_vector()); expr * firstTester; @@ -10098,15 +10098,15 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe ast_manager & m = get_manager(); - TRACE("t_str_detail", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;); + TRACE("str", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;); if (m_params.m_UseBinarySearch) { - TRACE("t_str_detail", tout << "using binary search heuristic" << std::endl;); + TRACE("str", tout << "using binary search heuristic" << std::endl;); return binary_search_length_test(freeVar, lenTesterInCbEq, lenTesterValue); } else { bool map_effectively_empty = false; if (!fvar_len_count_map.contains(freeVar)) { - TRACE("t_str_detail", tout << "fvar_len_count_map is empty" << std::endl;); + TRACE("str", tout << "fvar_len_count_map is empty" << std::endl;); map_effectively_empty = true; } @@ -10120,18 +10120,18 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe for (ptr_vector::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) { expr * indicator = *it; if (internal_variable_set.find(indicator) != internal_variable_set.end()) { - TRACE("t_str_detail", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m) + TRACE("str", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m) << " in fvar_lenTester_map[freeVar]" << std::endl;); map_effectively_empty = false; break; } } - CTRACE("t_str_detail", map_effectively_empty, tout << "all variables in fvar_lenTester_map[freeVar] out of scope" << std::endl;); + CTRACE("str", map_effectively_empty, tout << "all variables in fvar_lenTester_map[freeVar] out of scope" << std::endl;); } if (map_effectively_empty) { // no length assertions for this free variable have ever been added. - TRACE("t_str_detail", tout << "no length assertions yet" << std::endl;); + TRACE("str", tout << "no length assertions yet" << std::endl;); fvar_len_count_map.insert(freeVar, 1); unsigned int testNum = fvar_len_count_map[freeVar]; @@ -10148,13 +10148,13 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe SASSERT(lenTestAssert != NULL); return lenTestAssert; } else { - TRACE("t_str_detail", tout << "found previous in-scope length assertions" << std::endl;); + TRACE("str", tout << "found previous in-scope length assertions" << std::endl;); expr * effectiveLenInd = NULL; zstring effectiveLenIndiStr(""); int lenTesterCount = (int) fvar_lenTester_map[freeVar].size(); - TRACE("t_str_detail", + TRACE("str", tout << lenTesterCount << " length testers in fvar_lenTester_map[" << mk_pp(freeVar, m) << "]:" << std::endl; for (int i = 0; i < lenTesterCount; ++i) { expr * len_indicator = fvar_lenTester_map[freeVar][i]; @@ -10170,13 +10170,13 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe expr * len_indicator_pre = fvar_lenTester_map[freeVar][i]; // check whether this is in scope as well if (internal_variable_set.find(len_indicator_pre) == internal_variable_set.end()) { - TRACE("t_str_detail", tout << "length indicator " << mk_pp(len_indicator_pre, m) << " not in scope" << std::endl;); + TRACE("str", tout << "length indicator " << mk_pp(len_indicator_pre, m) << " not in scope" << std::endl;); continue; } bool indicatorHasEqcValue = false; expr * len_indicator_value = get_eqc_value(len_indicator_pre, indicatorHasEqcValue); - TRACE("t_str_detail", tout << "length indicator " << mk_ismt2_pp(len_indicator_pre, m) << + TRACE("str", tout << "length indicator " << mk_ismt2_pp(len_indicator_pre, m) << " = " << mk_ismt2_pp(len_indicator_value, m) << std::endl;); if (indicatorHasEqcValue) { zstring len_pIndiStr; @@ -10188,7 +10188,7 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe } } else { if (lenTesterInCbEq != len_indicator_pre) { - TRACE("t_str", tout << "WARNING: length indicator " << mk_ismt2_pp(len_indicator_pre, m) + TRACE("str", tout << "WARNING: length indicator " << mk_ismt2_pp(len_indicator_pre, m) << " does not have an equivalence class value." << " i = " << i << ", lenTesterCount = " << lenTesterCount << std::endl;); if (i > 0) { @@ -10196,7 +10196,7 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe bool effectiveHasEqcValue; expr * effective_eqc_value = get_eqc_value(effectiveLenInd, effectiveHasEqcValue); bool effectiveInScope = (internal_variable_set.find(effectiveLenInd) != internal_variable_set.end()); - TRACE("t_str_detail", tout << "checking effective length indicator " << mk_pp(effectiveLenInd, m) << ": " + TRACE("str", tout << "checking effective length indicator " << mk_pp(effectiveLenInd, m) << ": " << (effectiveInScope ? "in scope" : "NOT in scope") << ", "; if (effectiveHasEqcValue) { tout << "~= " << mk_pp(effective_eqc_value, m); @@ -10227,11 +10227,11 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe } // !indicatorHasEqcValue } // for (i : [0..lenTesterCount-1]) if (effectiveLenIndiStr == "more" || effectiveLenIndiStr == "") { - TRACE("t_str", tout << "length is not fixed; generating length tester options for free var" << std::endl;); + TRACE("str", tout << "length is not fixed; generating length tester options for free var" << std::endl;); expr_ref indicator(m); unsigned int testNum = 0; - TRACE("t_str", tout << "effectiveLenIndiStr = " << effectiveLenIndiStr + TRACE("str", tout << "effectiveLenIndiStr = " << effectiveLenIndiStr << ", i = " << i << ", lenTesterCount = " << lenTesterCount << "\n";); if (i == lenTesterCount) { @@ -10249,7 +10249,7 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe SASSERT(lenTestAssert != NULL); return lenTestAssert; } else { - TRACE("t_str", tout << "length is fixed; generating models for free var" << std::endl;); + TRACE("str", tout << "length is fixed; generating models for free var" << std::endl;); // length is fixed expr * valueAssert = gen_free_var_options(freeVar, effectiveLenInd, effectiveLenIndiStr, NULL, zstring("")); return valueAssert; @@ -10318,7 +10318,7 @@ void theory_str::process_free_var(std::map & freeVar_map) { } } if (duplicated && dupVar != NULL) { - TRACE("t_str_detail", tout << "Duplicated free variable found:" << mk_ismt2_pp(freeVar, m) + TRACE("str", tout << "Duplicated free variable found:" << mk_ismt2_pp(freeVar, m) << " = " << mk_ismt2_pp(dupVar, m) << " (SKIP)" << std::endl;); continue; } else { @@ -10428,7 +10428,7 @@ void theory_str::get_eqc_simpleUnroll(expr * n, expr * &constStr, std::setget_owner(), get_manager()) << + TRACE("str", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")" << std::endl;); ast_manager & m = get_manager(); context & ctx = get_context(); @@ -10489,7 +10489,7 @@ model_value_proc * theory_str::mk_value(enode * n, model_generator & mg) { if (val != NULL) { return alloc(expr_wrapper_proc, val); } else { - TRACE("t_str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;); + TRACE("str", tout << "WARNING: failed to find a concrete value, falling back" << std::endl;); return alloc(expr_wrapper_proc, to_app(mk_string("**UNUSED**"))); } }