mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 23:25:36 +00:00
Code Activity

add spp for easier pretty printing snode

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-14 00:39:01 -07:00
parent 53cc320efa
commit acae332b13
3 changed files with 140 additions and 70 deletions
Download patch file Download diff file Expand all files Collapse all files

194
src/ast/euf/euf_snode.h
View file

@ -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<snode*>(this));
tokens.push_back(const_cast<snode *>(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<snode*>(this) : nullptr;
return i == 0 ? const_cast<snode *>(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);
}

14
src/smt/seq/seq_nielsen.cpp
View file

@ -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

2
src/smt/seq/seq_regex.cpp
View file

@ -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;