From c7bdc44d319ea02735c7d8f1076c01acb29ddc91 Mon Sep 17 00:00:00 2001 From: calebstanford-msr Date: Fri, 5 Jun 2020 15:07:15 -0400 Subject: [PATCH] remove std::cout debugging for PR --- src/ast/rewriter/seq_rewriter.cpp | 8 -------- src/smt/seq_regex.cpp | 9 --------- 2 files changed, 17 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index f4d010632..fb66bb9a1 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2132,14 +2132,10 @@ expr_ref seq_rewriter::re_predicate(expr* cond, sort* seq_sort) { } expr_ref seq_rewriter::is_nullable_rec(expr* r) { - std::cout << "n"; expr_ref result(m_op_cache.find(_OP_RE_IS_NULLABLE, r, nullptr, nullptr), m()); if (!result) { - std::cout << "(m) "; result = is_nullable(r); m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, nullptr, result); - } else { - std::cout << "(h) "; } return result; } @@ -2466,13 +2462,10 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) { pair of pointers. */ expr_ref seq_rewriter::combine_ites(decl_kind k, expr* a, expr* b, expr* cond) { - std::cout << "c"; expr_ref result(m_op_cache.find(k, a, b, cond), m()); if (result) { - std::cout << "(h) "; return result; } - std::cout << "(m) "; SASSERT((k == OP_ITE) == (cond != nullptr)); expr *acond = nullptr, *a1 = nullptr, *a2 = nullptr, *bcond = nullptr, *b1 = nullptr, *b2 = nullptr; @@ -2549,7 +2542,6 @@ expr_ref seq_rewriter::combine_ites(decl_kind k, expr* a, expr* b, expr* cond) { representation in unfolding string in regex constraints. */ expr_ref seq_rewriter::lift_ites(expr* r, bool lift_over_union, bool lift_over_inter) { - std::cout << "l "; decl_kind k = to_app(r)->get_decl_kind(); family_id fid = get_fid(); expr *r1 = nullptr, *r2 = nullptr, *cond = nullptr, *ele = nullptr; diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 675893381..ee1484125 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -101,8 +101,6 @@ namespace smt { expr* e = ctx.bool_var2expr(lit.var()); VERIFY(str().is_in_re(e, s, r)); - std::cout << "PI "; - TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";); // convert negative negative membership literals to positive @@ -146,7 +144,6 @@ namespace smt { } void seq_regex::propagate_accept(literal lit) { - std::cout << "PA "; if (!propagate(lit)) m_to_propagate.push_back(lit); } @@ -200,9 +197,6 @@ namespace smt { TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";); - std::cout << "P "; - // << mk_pp(e, m) << std::endl; - if (block_unfolding(lit, idx)) return true; @@ -320,7 +314,6 @@ namespace smt { with optimizations for if-then-else expressions involving the head. */ expr_ref seq_regex::derivative_wrapper(expr* hd, expr* r) { - std::cout << "D "; expr_ref result = expr_ref(re().mk_derivative(hd, r), m); rewrite(result); // don't lift over unions @@ -361,7 +354,6 @@ namespace smt { * */ void seq_regex::propagate_is_non_empty(literal lit) { - std::cout << "PN "; expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr; VERIFY(sk().is_is_non_empty(e, r, u)); expr_ref is_nullable = seq_rw().is_nullable(r); @@ -402,7 +394,6 @@ namespace smt { is_empty(r, u) is true if r is a member of u */ void seq_regex::propagate_is_empty(literal lit) { - std::cout << "PE "; expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr; VERIFY(sk().is_is_empty(e, r, u)); expr_ref is_nullable = seq_rw().is_nullable(r);