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

remove debugging statements for PR

Browse source
This commit is contained in:
calebstanford-msr 2020-06-08 13:18:40 -04:00
parent 766e979641
commit 38e85a7288
2 changed files with 0 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2155,14 +2155,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;
} }

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
@ -144,7 +142,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);
} }
@ -172,8 +169,6 @@ namespace smt {
TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";); TRACE("seq", tout << "propagate " << mk_pp(e, m) << "\n";);
std::cout << "P ";
if (re().is_empty(r)) { if (re().is_empty(r)) {
th.add_axiom(~lit); th.add_axiom(~lit);
return true; return true;
@ -361,10 +356,8 @@ 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);
std::cout << std::endl << "Derivative result: " << result << std::endl;
return result; return result;
} }
@ -400,7 +393,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);
@ -456,7 +448,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);