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

remove std::cout debugging for PR

Browse source
This commit is contained in:
calebstanford-msr 2020-06-05 15:07:15 -04:00
parent fdc6df1b17
commit c7bdc44d31
2 changed files with 0 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/rewriter/seq_rewriter.cpp
View file

@ -2132,14 +2132,10 @@ expr_ref seq_rewriter::re_predicate(expr* cond, sort* seq_sort) {
} }
expr_ref seq_rewriter::is_nullable_rec(expr* r) { 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()); expr_ref result(m_op_cache.find(_OP_RE_IS_NULLABLE, r, nullptr, nullptr), m());
if (!result) { if (!result) {
std::cout << "(m) ";
result = is_nullable(r); result = is_nullable(r);
m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, nullptr, result); m_op_cache.insert(_OP_RE_IS_NULLABLE, r, nullptr, nullptr, result);
} else {
std::cout << "(h) ";
} }
return result; return result;
} }
@ -2466,13 +2462,10 @@ br_status seq_rewriter::mk_re_derivative(expr* ele, expr* r, expr_ref& result) {
pair of pointers. pair of pointers.
*/ */
expr_ref seq_rewriter::combine_ites(decl_kind k, expr* a, expr* b, expr* cond) { 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()); expr_ref result(m_op_cache.find(k, a, b, cond), m());
if (result) { if (result) {
std::cout << "(h) ";
return result; return result;
} }
std::cout << "(m) ";
SASSERT((k == OP_ITE) == (cond != nullptr)); SASSERT((k == OP_ITE) == (cond != nullptr));
expr *acond = nullptr, *a1 = nullptr, *a2 = nullptr, expr *acond = nullptr, *a1 = nullptr, *a2 = nullptr,
*bcond = nullptr, *b1 = nullptr, *b2 = 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. representation in unfolding string in regex constraints.
*/ */
expr_ref seq_rewriter::lift_ites(expr* r, bool lift_over_union, bool lift_over_inter) { 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(); decl_kind k = to_app(r)->get_decl_kind();
family_id fid = get_fid(); family_id fid = get_fid();
expr *r1 = nullptr, *r2 = nullptr, *cond = nullptr, *ele = nullptr; expr *r1 = nullptr, *r2 = nullptr, *cond = nullptr, *ele = nullptr;

9
src/smt/seq_regex.cpp
View file

@ -101,8 +101,6 @@ namespace smt {
expr* e = ctx.bool_var2expr(lit.var()); expr* e = ctx.bool_var2expr(lit.var());
VERIFY(str().is_in_re(e, s, r)); VERIFY(str().is_in_re(e, s, r));
std::cout << "PI ";
TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";); TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
// convert negative negative membership literals to positive // convert negative negative membership literals to positive
@ -146,7 +144,6 @@ namespace smt {
} }
void seq_regex::propagate_accept(literal lit) { void seq_regex::propagate_accept(literal lit) {
std::cout << "PA ";
if (!propagate(lit)) if (!propagate(lit))
m_to_propagate.push_back(lit); m_to_propagate.push_back(lit);
} }
@ -200,9 +197,6 @@ namespace smt {
TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";); TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
std::cout << "P ";
// << mk_pp(e, m) << std::endl;
if (block_unfolding(lit, idx)) if (block_unfolding(lit, idx))
return true; return true;
@ -320,7 +314,6 @@ namespace smt {
with optimizations for if-then-else expressions involving the head. with optimizations for if-then-else expressions involving the head.
*/ */
expr_ref seq_regex::derivative_wrapper(expr* hd, expr* r) { expr_ref seq_regex::derivative_wrapper(expr* hd, expr* r) {
std::cout << "D ";
expr_ref result = expr_ref(re().mk_derivative(hd, r), m); expr_ref result = expr_ref(re().mk_derivative(hd, r), m);
rewrite(result); rewrite(result);
// don't lift over unions // don't lift over unions
@ -361,7 +354,6 @@ namespace smt {
* *
*/ */
void seq_regex::propagate_is_non_empty(literal lit) { void seq_regex::propagate_is_non_empty(literal lit) {
std::cout << "PN ";
expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr; expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr;
VERIFY(sk().is_is_non_empty(e, r, u)); VERIFY(sk().is_is_non_empty(e, r, u));
expr_ref is_nullable = seq_rw().is_nullable(r); 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 is_empty(r, u) is true if r is a member of u
*/ */
void seq_regex::propagate_is_empty(literal lit) { void seq_regex::propagate_is_empty(literal lit) {
std::cout << "PE ";
expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr; expr* e = ctx.bool_var2expr(lit.var()), *r = nullptr, *u = nullptr;
VERIFY(sk().is_is_empty(e, r, u)); VERIFY(sk().is_is_empty(e, r, u));
expr_ref is_nullable = seq_rw().is_nullable(r); expr_ref is_nullable = seq_rw().is_nullable(r);