mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

Revert "remove std::cout debugging for PR"

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

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

@ -2132,10 +2132,14 @@ 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;
}
@ -2462,10 +2466,13 @@ 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;
@ -2542,6 +2549,7 @@ 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;

9
src/smt/seq_regex.cpp
View file

@ -101,6 +101,8 @@ 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
@ -144,6 +146,7 @@ namespace smt {
}
void seq_regex::propagate_accept(literal lit) {
std::cout << "PA ";
if (!propagate(lit))
m_to_propagate.push_back(lit);
}
@ -197,6 +200,9 @@ 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;
@ -314,6 +320,7 @@ 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
@ -354,6 +361,7 @@ 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);
@ -394,6 +402,7 @@ 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);