mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-21 09:29:35 +00:00
Code Activity

Removed legacy code

Browse source
This commit is contained in:
CEisenhofer 2026-05-04 20:16:13 +02:00
parent 5b3d734ecb
commit e2e876c7a9
3 changed files with 4 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3043,19 +3043,16 @@ namespace seq {
// ----------------------------------------------------------------------- // -----------------------------------------------------------------------
bool nielsen_graph::apply_cycle_decomposition(nielsen_node* node) { bool nielsen_graph::apply_cycle_decomposition(nielsen_node* node) {
return false; // For now, disable return false;
if (!node->backedge())
return false;
// Look for a str_mem with a variable-headed string // Look for a str_mem with a variable-headed string
for (unsigned mi = 0; mi < node->str_mems().size(); ++mi) { for (unsigned mi = 0; mi < node->str_mems().size(); ++mi) {
str_mem const& mem = node->str_mems()[mi]; str_mem const& mem = node->str_mems()[mi];
if (!mem.m_str || !mem.m_regex) SASSERT(mem.well_formed());
continue;
if (mem.is_primitive()) if (mem.is_primitive())
continue; continue;
euf::snode* first = mem.m_str->first(); euf::snode* first = mem.m_str->first();
if (!first || !first->is_var()) SASSERT(first);
if (!first->is_var())
continue; continue;
euf::snode* x = first; euf::snode* x = first;

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

@ -584,7 +584,6 @@ namespace seq {
// edges // edges
ptr_vector<nielsen_edge> m_outgoing; ptr_vector<nielsen_edge> m_outgoing;
nielsen_node* m_backedge = nullptr;
nielsen_edge* m_parent_edge = nullptr; nielsen_edge* m_parent_edge = nullptr;
// status flags // status flags
@ -651,9 +650,6 @@ namespace seq {
ptr_vector<nielsen_edge> const& outgoing() const { return m_outgoing; } ptr_vector<nielsen_edge> const& outgoing() const { return m_outgoing; }
void add_outgoing(nielsen_edge* e) { m_outgoing.push_back(e); } void add_outgoing(nielsen_edge* e) { m_outgoing.push_back(e); }
nielsen_node* backedge() const { return m_backedge; }
void set_backedge(nielsen_node* n) { m_backedge = n; }
nielsen_edge* parent_edge() const { return m_parent_edge; } nielsen_edge* parent_edge() const { return m_parent_edge; }
void set_parent_edge(nielsen_edge* e) { m_parent_edge = e; } void set_parent_edge(nielsen_edge* e) { m_parent_edge = e; }

10
src/smt/seq/seq_nielsen_pp.cpp
View file

@ -19,7 +19,6 @@ Author:
#include "smt/seq/seq_nielsen.h" #include "smt/seq/seq_nielsen.h"
#include "ast/arith_decl_plugin.h" #include "ast/arith_decl_plugin.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/rewriter/seq_rewriter.h"
#include "util/obj_hashtable.h" #include "util/obj_hashtable.h"
#include <sstream> #include <sstream>
@ -86,9 +85,6 @@ namespace seq {
out << "\n"; out << "\n";
} }
if (n->backedge())
out << " backedge -> node[" << n->backedge()->id() << "]\n";
return out; return out;
} }
@ -634,13 +630,7 @@ namespace seq {
out << "];\n"; out << "];\n";
} }
// backedge as dotted arrow
if (n->backedge())
out << " " << n->id() << " -> " << n->backedge()->id()
<< " [style=dotted];\n";
} }
out << "}\n"; out << "}\n";
return out; return out;
} }