mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 05:44:51 +00:00
Code Activity

A bit cleanup

Browse source
This commit is contained in:
CEisenhofer 2026-03-05 17:14:54 +01:00
parent c5e7cbc29d
commit 7dcebcdb0a
3 changed files with 1 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/euf/euf_sgraph.cpp
View file

@ -575,7 +575,7 @@ namespace euf {
if (!re || !re->get_expr())
return;
expr* e = re->get_expr();
expr* ch = nullptr, *lo = nullptr, *hi = nullptr;
expr* lo = nullptr, *hi = nullptr;
// leaf regex predicates: character ranges and single characters
if (m_seq.re.is_range(e, lo, hi)) {
preds.push_back(e);

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

@ -868,10 +868,6 @@ namespace seq {
return search_result::unknown;
}
simplify_result nielsen_graph::simplify_node(nielsen_node* node) {
return node->simplify_and_init(*this);
}
bool nielsen_graph::apply_det_modifier(nielsen_node* node) {
for (str_eq const& eq : node->str_eqs()) {
if (eq.is_trivial())

8
src/smt/seq/seq_nielsen.h
View file

@ -594,12 +594,7 @@ namespace seq {
ptr_vector<nielsen_node> const& nodes() const { return m_nodes; }
unsigned num_nodes() const { return m_nodes.size(); }
// depth bound for iterative deepening
unsigned depth_bound() const { return m_depth_bound; }
void set_depth_bound(unsigned d) { m_depth_bound = d; }
// maximum overall search depth (0 = unlimited)
unsigned max_search_depth() const { return m_max_search_depth; }
void set_max_search_depth(unsigned d) { m_max_search_depth = d; }
// generate next unique regex membership id
@ -626,9 +621,6 @@ namespace seq {
// main search entry point: iterative deepening DFS
search_result solve();
// simplify a node's constraints (delegate to node)
simplify_result simplify_node(nielsen_node* node);
// generate child nodes by applying modifier rules
// returns true if at least one child was generated
bool generate_extensions(nielsen_node *node);