mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

Z3 arguments got ignored in the Nielsen graph

Browse source
This commit is contained in:
CEisenhofer 2026-06-05 19:19:08 +02:00
parent c20bc0e631
commit 8ac7a242eb
2 changed files with 16 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1074,18 +1074,18 @@ namespace seq {
unsigned num_nodes() const { return m_nodes.size(); }
// maximum overall search depth (0 = unlimited)
void set_max_search_depth(unsigned d) { m_max_search_depth = d; }
void set_max_search_depth(const unsigned d) { m_max_search_depth = d; }
// maximum total DFS nodes per solve() call (0 = unlimited)
void set_max_nodes(unsigned n) { m_max_nodes = n; }
void set_max_nodes(const unsigned n) { m_max_nodes = n; }
// enable/disable Parikh image verification constraints
void set_parikh_enabled(bool e) { m_parikh_enabled = e; }
void set_parikh_enabled(const bool e) { m_parikh_enabled = e; }
void set_signature_split(bool e) { m_signature_split = e; }
void set_signature_split(const bool e) { m_signature_split = e; }
void set_regex_factorization_threshold(unsigned max) { m_regex_factorization_threshold = max; }
void set_regex_factorization_eager(bool e) { m_regex_factorization_eager = e; }
void set_regex_factorization_threshold(const unsigned max) { m_regex_factorization_threshold = max; }
void set_regex_factorization_eager(const bool e) { m_regex_factorization_eager = e; }
// display for debugging
std::ostream& display(std::ostream& out) const;

22
src/smt/theory_nseq.cpp
View file

@ -829,26 +829,24 @@ namespace smt {
// let's rebuild the whole Nielsen graph
populate_nielsen_graph();
// assert length constraints derived from string equalities
if (assert_length_constraints()) {
TRACE(seq, tout << "nseq final_check: length constraints asserted, FC_CONTINUE\n");
return FC_CONTINUE;
}
SASSERT(m_nielsen.root());
m_nielsen.assert_node_side_constraints(m_nielsen.root());
++m_num_final_checks;
m_nielsen.set_max_search_depth(get_fparams().m_nseq_max_depth);
m_nielsen.set_max_nodes(get_fparams().m_nseq_max_nodes);
m_nielsen.set_parikh_enabled(get_fparams().m_nseq_parikh);
m_nielsen.set_signature_split(get_fparams().m_nseq_signature);
m_nielsen.set_regex_factorization_threshold(get_fparams().m_nseq_regex_factorization_threshold);
m_nielsen.set_regex_factorization_eager(get_fparams().m_nseq_regex_factorization_eager);
// assert length constraints derived from string equalities
if (assert_length_constraints()) {
TRACE(seq, tout << "nseq final_check: length constraints asserted, FC_CONTINUE\n");
return FC_CONTINUE;
}
SASSERT(m_nielsen.root());
m_nielsen.assert_node_side_constraints(m_nielsen.root());
}
++m_num_final_checks;
SASSERT(!m_nielsen.root()->is_currently_conflict());
// Regex membership pre-check: before running DFS, check intersection