diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h index 1f8d3903b..1efeaebc5 100644 --- a/src/ast/euf/euf_snode.h +++ b/src/ast/euf/euf_snode.h @@ -26,6 +26,7 @@ Author: #include "util/vector.h" #include "util/region.h" #include "ast/ast.h" +#include "ast/ast_pp.h" #include "ast/seq_decl_plugin.h" #include "ast/rewriter/seq_axioms.h" @@ -57,34 +58,34 @@ namespace euf { }; class snode { - expr* m_expr = nullptr; - snode_kind m_kind = snode_kind::s_var; - unsigned m_id = UINT_MAX; - unsigned m_num_args = 0; + expr *m_expr = nullptr; + snode_kind m_kind = snode_kind::s_var; + unsigned m_id = UINT_MAX; + unsigned m_num_args = 0; // metadata flags, analogous to ZIPT's Str/StrToken properties - bool m_ground = true; // no uninterpreted string variables - bool m_regex_free = true; // no regex constructs - bool m_nullable = false; // accepts the empty string - bool m_is_classical = true; // classical regular expression - unsigned m_level = 0; // tree depth/level (0 for empty, 1 for singletons) - unsigned m_length = 0; // token count, number of leaf tokens in the tree + bool m_ground = true; // no uninterpreted string variables + bool m_regex_free = true; // no regex constructs + bool m_nullable = false; // accepts the empty string + bool m_is_classical = true; // classical regular expression + unsigned m_level = 0; // tree depth/level (0 for empty, 1 for singletons) + unsigned m_length = 0; // token count, number of leaf tokens in the tree // hash matrix for associativity-respecting hashing (2x2 polynomial hash matrix) // all zeros means not cached, non-zero means cached - unsigned m_hash_matrix[2][2] = {{0,0},{0,0}}; + unsigned m_hash_matrix[2][2] = {{0, 0}, {0, 0}}; - snode* m_args[0]; // variable-length array, allocated via get_snode_size(num_args) + snode *m_args[0]; // variable-length array, allocated via get_snode_size(num_args) friend class sgraph; static unsigned get_snode_size(unsigned num_args) { - return sizeof(snode) + num_args * sizeof(snode*); + return sizeof(snode) + num_args * sizeof(snode *); } - static snode* mk(region& r, expr* e, snode_kind k, unsigned id, unsigned num_args, snode* const* args) { - void* mem = r.allocate(get_snode_size(num_args)); - snode* n = new (mem) snode(); + static snode *mk(region &r, expr *e, snode_kind k, unsigned id, unsigned num_args, snode *const *args) { + void *mem = r.allocate(get_snode_size(num_args)); + snode *n = new (mem) snode(); n->m_expr = e; n->m_kind = k; n->m_id = id; @@ -96,55 +97,114 @@ namespace euf { } public: - expr* get_expr() const { return m_expr; } - snode_kind kind() const { return m_kind; } - unsigned id() const { return m_id; } - unsigned num_args() const { return m_num_args; } - snode* arg(unsigned i) const { SASSERT(i < m_num_args); return m_args[i]; } + expr *get_expr() const { + return m_expr; + } + snode_kind kind() const { + return m_kind; + } + unsigned id() const { + return m_id; + } + unsigned num_args() const { + return m_num_args; + } + snode *arg(unsigned i) const { + SASSERT(i < m_num_args); + return m_args[i]; + } // TODO: Track regex being "classical" (no complement, intersection, fail) - bool is_ground() const { return m_ground; } - bool is_regex_free() const { return m_regex_free; } - bool is_nullable() const { return m_nullable; } - bool is_classical() const { return m_is_classical; } - unsigned level() const { return m_level; } - unsigned length() const { return m_length; } + bool is_ground() const { + return m_ground; + } + bool is_regex_free() const { + return m_regex_free; + } + bool is_nullable() const { + return m_nullable; + } + bool is_classical() const { + return m_is_classical; + } + unsigned level() const { + return m_level; + } + unsigned length() const { + return m_length; + } // associativity-respecting hash: cached if the 2x2 matrix is non-zero. // M[0][0] = HASH_BASE^(num_leaves) which is always nonzero since HASH_BASE // is odd and gcd(odd, 2^32) = 1, so the check is safe. - bool has_cached_hash() const { return m_hash_matrix[0][0] != 0; } - unsigned assoc_hash() const { return m_hash_matrix[0][1]; } + bool has_cached_hash() const { + return m_hash_matrix[0][0] != 0; + } + unsigned assoc_hash() const { + return m_hash_matrix[0][1]; + } - bool is_empty() const { return m_kind == snode_kind::s_empty; } - bool is_char() const { return m_kind == snode_kind::s_char; } - bool is_var() const { return m_kind == snode_kind::s_var; } - bool is_unit() const { return m_kind == snode_kind::s_unit; } + bool is_empty() const { + return m_kind == snode_kind::s_empty; + } + bool is_char() const { + return m_kind == snode_kind::s_char; + } + bool is_var() const { + return m_kind == snode_kind::s_var; + } + bool is_unit() const { + return m_kind == snode_kind::s_unit; + } bool is_char_or_unit() const { return m_kind == snode_kind::s_char || m_kind == snode_kind::s_unit; } - bool is_concat() const { return m_kind == snode_kind::s_concat; } - bool is_power() const { return m_kind == snode_kind::s_power; } - bool is_star() const { return m_kind == snode_kind::s_star; } - bool is_loop() const { return m_kind == snode_kind::s_loop; } - bool is_union() const { return m_kind == snode_kind::s_union; } - bool is_intersect() const { return m_kind == snode_kind::s_intersect; } - bool is_complement() const { return m_kind == snode_kind::s_complement; } - bool is_fail() const { return m_kind == snode_kind::s_fail; } - bool is_full_char() const { return m_kind == snode_kind::s_full_char; } - bool is_full_seq() const { return m_kind == snode_kind::s_full_seq; } - bool is_range() const { return m_kind == snode_kind::s_range; } - bool is_to_re() const { return m_kind == snode_kind::s_to_re; } - bool is_in_re() const { return m_kind == snode_kind::s_in_re; } + bool is_concat() const { + return m_kind == snode_kind::s_concat; + } + bool is_power() const { + return m_kind == snode_kind::s_power; + } + bool is_star() const { + return m_kind == snode_kind::s_star; + } + bool is_loop() const { + return m_kind == snode_kind::s_loop; + } + bool is_union() const { + return m_kind == snode_kind::s_union; + } + bool is_intersect() const { + return m_kind == snode_kind::s_intersect; + } + bool is_complement() const { + return m_kind == snode_kind::s_complement; + } + bool is_fail() const { + return m_kind == snode_kind::s_fail; + } + bool is_full_char() const { + return m_kind == snode_kind::s_full_char; + } + bool is_full_seq() const { + return m_kind == snode_kind::s_full_seq; + } + bool is_range() const { + return m_kind == snode_kind::s_range; + } + bool is_to_re() const { + return m_kind == snode_kind::s_to_re; + } + bool is_in_re() const { + return m_kind == snode_kind::s_in_re; + } // is this a leaf token (analogous to ZIPT's StrToken as opposed to Str) bool is_token() const { switch (m_kind) { case snode_kind::s_empty: - case snode_kind::s_concat: - return false; - default: - return true; + case snode_kind::s_concat: return false; + default: return true; } } @@ -153,47 +213,47 @@ namespace euf { } // analogous to ZIPT's Str.First / Str.Last - snode const* first() const { - snode const* s = this; + snode const *first() const { + snode const *s = this; while (s->is_concat()) s = s->arg(0); return s; } - snode const* last() const { - snode const* s = this; + snode const *last() const { + snode const *s = this; while (s->is_concat()) s = s->arg(1); return s; } - snode* first() { - snode* s = this; + snode *first() { + snode *s = this; while (s->is_concat()) s = s->arg(0); return s; } - snode* last() { - snode* s = this; + snode *last() { + snode *s = this; while (s->is_concat()) s = s->arg(1); return s; } // collect all leaf tokens in left-to-right order - void collect_tokens(snode_vector& tokens) const { + void collect_tokens(snode_vector &tokens) const { if (is_concat()) { arg(0)->collect_tokens(tokens); arg(1)->collect_tokens(tokens); } else if (!is_empty()) - tokens.push_back(const_cast(this)); + tokens.push_back(const_cast(this)); } // access the i-th token (0-based, left-to-right order) // returns nullptr if i >= length() - snode* at(unsigned i) const { + snode *at(unsigned i) const { if (is_concat()) { unsigned left_len = arg(0)->length(); if (i < left_len) @@ -202,9 +262,19 @@ namespace euf { } if (is_empty()) return nullptr; - return i == 0 ? const_cast(this) : nullptr; + return i == 0 ? const_cast(this) : nullptr; } }; } +struct spp { + euf::snode *n; + ast_manager &m; + spp(euf::snode *n, ast_manager &m) : n(n), m(m) {} +}; + +inline std::ostream &operator<<(std::ostream &out, spp const&p) { + return out << mk_pp(p.n->get_expr(), p.m); +} + diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 95b65086e..4fa6004e4 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -1085,7 +1085,7 @@ namespace seq { euf::snode* deriv = fwd ? sg.brzozowski_deriv(mem.m_regex, tok) : reverse_brzozowski_deriv(sg, mem.m_regex, tok); - TRACE(seq, tout << mem_pp(m, mem) << " d: " << mk_pp(deriv->get_expr(), m) << "\n"); + TRACE(seq, tout << mem_pp(m, mem) << " d: " << spp(deriv, m) << "\n"); if (!deriv) break; if (deriv->is_fail()) { @@ -1129,7 +1129,7 @@ namespace seq { auto next = sg.mk(d); if (next->is_fail()) { - TRACE(seq, tout << "empty regex" << mk_pp(mem.m_regex->get_expr(), m) << " d: " << d << "\n"); + TRACE(seq, tout << "empty regex" << spp(mem.m_regex, m) << " d: " << d << "\n"); set_general_conflict(); set_conflict(backtrack_reason::regex, mem.m_dep); return simplify_result::conflict; @@ -3444,7 +3444,7 @@ namespace seq { VERIFY(!minterms.empty()); bool created = false; - // std::cout << "Considering regex: " << mk_pp(mem.m_regex->get_expr(), m) << std::endl; + // std::cout << "Considering regex: " << spp(mem.m_regex, m) << std::endl; // Branch 1: x → ε (progress) { @@ -3464,7 +3464,7 @@ namespace seq { // Branch 2+: for each minterm m_i, x → ?c · x // where ?c is a symbolic char constrained by the minterm for (euf::snode* mt : minterms) { - // std::cout << "Processing minterm: " << mk_pp(mt->get_expr(), m) << std::endl; + // std::cout << "Processing minterm: " << spp(mt, m) << std::endl; SASSERT(mt); SASSERT(mt->get_expr()); SASSERT(!mt->is_fail()); @@ -3475,7 +3475,7 @@ namespace seq { SASSERT(deriv); if (deriv->is_fail()) continue; - // std::cout << "Result: " << mk_pp(deriv->get_expr(), m) << std::endl; + // std::cout << "Result: " << spp(deriv, m) << std::endl; SASSERT(m_seq_regex); char_set cs = m_seq_regex->minterm_to_char_set(mt->get_expr()); @@ -4172,8 +4172,8 @@ namespace seq { expr_ref all_re(m_seq.re.mk_full_seq(m_seq.re.mk_re(str_sort)), m); tok_re = m_sg.mk(all_re); } - TRACE(seq, tout << "intersection-collection\n" << mk_pp(tok->get_expr(), m) - << "\n" << mk_pp(tok_re->get_expr(), m) << "\n"); + TRACE(seq, tout << "intersection-collection\n" << spp(tok, m) + << "\n" << spp(tok_re, m) << "\n"); } else if (tok->is_unit()) { // Symbolic char — try to get char_range diff --git a/src/smt/seq/seq_regex.cpp b/src/smt/seq/seq_regex.cpp index 4c03d3f3b..d9024fadf 100644 --- a/src/smt/seq/seq_regex.cpp +++ b/src/smt/seq/seq_regex.cpp @@ -672,7 +672,7 @@ namespace seq { SASSERT(first); if (first != var) continue; - TRACE(seq, tout << mk_pp(first->get_expr(), m) << " " << mem_pp(m, mem) << " dep: " << mem.m_dep << "\n"); + TRACE(seq, tout << mk_pp(first->get_expr(), m) << " " << mem_pp(m, mem) << "\n"); if (!result) { result = mem.m_regex;