mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-20 03:53:10 +00:00
Code Activity

Create dummy sat-node to avoid problems in case the preprocessor solves the problem entirely

Browse source
This commit is contained in:
CEisenhofer 2026-03-19 16:02:51 +01:00
parent 9f4e823c8b
commit 51f3996464
3 changed files with 32 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -573,8 +573,8 @@ namespace seq {
}
void nielsen_graph::add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r) {
if (!m_root)
m_root = mk_node();
if (!root())
create_root();
dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r));
str_eq eq(lhs, rhs, dep);
eq.sort();
@ -582,8 +582,8 @@ namespace seq {
}
void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l) {
if (!m_root)
m_root = mk_node();
if (!root())
create_root();
dep_tracker dep = m_dep_mgr.mk_leaf(l);
euf::snode* history = m_sg.mk_empty_seq(str->get_sort());
unsigned id = next_mem_id();
@ -592,8 +592,8 @@ namespace seq {
// test-friendly overloads (no external dependency tracking)
void nielsen_graph::add_str_eq(euf::snode* lhs, euf::snode* rhs) {
if (!m_root)
m_root = mk_node();
if (root())
create_root();
dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr));
str_eq eq(lhs, rhs, dep);
eq.sort();
@ -601,8 +601,8 @@ namespace seq {
}
void nielsen_graph::add_str_mem(euf::snode* str, euf::snode* regex) {
if (!m_root)
m_root = mk_node();
if (!root())
create_root();
dep_tracker dep = nullptr;
euf::snode* history = m_sg.mk_empty_seq(str->get_sort());
unsigned id = next_mem_id();

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

@ -835,11 +835,24 @@ namespace seq {
// root node access
nielsen_node* root() const { return m_root; }
void set_root(nielsen_node* n) { m_root = n; }
void set_root(nielsen_node* n) {
SASSERT(n);
m_root = n;
}
// satisfying leaf node (set by solve() when result is sat)
nielsen_node* sat_node() const { return m_sat_node; }
void set_sat_node(nielsen_node* n) { m_sat_node = n; }
void set_sat_node(nielsen_node* n) {
SASSERT(n);
m_sat_node = n;
}
// creates a new root for the graph
void create_root() {
SASSERT(!root());
set_root(mk_node());
}
// path of edges from root to sat_node (set when sat_node is set)
svector<nielsen_edge*> const& sat_path() const { return m_sat_path; }
@ -935,9 +948,10 @@ namespace seq {
bool solve_sat_path_ints(model_ref& mdl);
// accessor for the seq_regex module
seq::seq_regex* seq_regex_module() const { return m_seq_regex; }
seq_regex* seq_regex_module() const { return m_seq_regex; }
private:
search_result search_dfs(nielsen_node* node, unsigned depth, svector<nielsen_edge*>& cur_path);
// Regex widening: overapproximate `str` by replacing variables with

7
src/smt/theory_nseq.cpp
View file

@ -371,8 +371,12 @@ namespace smt {
return FC_CONTINUE;
}
// there is nothing to do for the string solver, as there are no string constraints
if (m_state.empty() && m_ho_terms.empty() && !has_unhandled_preds()) {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: empty state+ho, FC_DONE (no solve)\n";);
m_nielsen.reset();
m_nielsen.create_root();
m_nielsen.set_sat_node(m_nielsen.root());
return FC_DONE;
}
@ -384,6 +388,9 @@ namespace smt {
if (m_state.empty() && !has_unhandled_preds()) {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: empty state (after ho), FC_DONE (no solve)\n";);
m_nielsen.reset();
m_nielsen.create_root();
m_nielsen.set_sat_node(m_nielsen.root());
return FC_DONE;
}