mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-17 07:29:28 +00:00
Code Activity

Push substitutions back to base solver

Browse source
This commit is contained in:
CEisenhofer 2026-04-21 18:29:27 +02:00
parent 4446705eae
commit 03c990e0e1
2 changed files with 54 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -39,6 +39,7 @@ NSB review:
#include <algorithm>
#include <complex>
#include <cstdlib>
#include <stack>
#include <unordered_map>
namespace seq {
@ -315,8 +316,9 @@ namespace seq {
const unsigned var_id = s.m_var->id();
ast_manager& m = graph().get_manager();
if (s.is_char_subst()) {
ast_manager& m = graph().get_manager();
expr* var_c_expr = s.m_var->arg(0)->get_expr();
expr* repl_c_expr = s.m_replacement->arg(0)->get_expr();
add_constraint(
@ -329,6 +331,18 @@ namespace seq {
add_char_range(s.m_replacement, range.first, m_graph.dep_mgr().mk_join(range.second, s.m_dep));
}
}
else {
expr_ref v = graph().get_current_skolem(s.m_var);
// temporarily bump counter for the substituted variable
unsigned prev = 0;
graph().m_mod_cnt.find(s.m_var->id(), prev);
graph().m_mod_cnt.insert(s.m_var->id(), prev + 1);
expr_ref str = graph().get_current_skolem_str(s.m_replacement);
graph().m_mod_cnt.insert(s.m_var->id(), prev);
add_constraint(
constraint(m.mk_eq(v, str), s.m_dep, m));
}
}
void nielsen_node::add_char_range(euf::snode* sym_char, char_set const& range, dep_tracker dep) {
@ -1347,7 +1361,7 @@ namespace seq {
++m_stats.m_num_unknown;
return search_result::unknown;
}
catch(const std::exception&) {
catch(const std::exception& e) {
#ifdef Z3DEBUG
std::string dot = to_dot();
#endif
@ -3859,6 +3873,42 @@ namespace seq {
return e;
}
expr_ref nielsen_graph::get_current_skolem_str(euf::snode* s) {
std::stack<euf::snode*> stack;
stack.push(s);
expr_ref e(m);
while (!stack.empty()) {
euf::snode* n = stack.top();
stack.pop();
SASSERT(n);
if (n->is_concat()) {
stack.push(n->arg(1));
stack.push(n->arg(0));
continue;
}
expr_ref add(m);
if (n->is_var())
add = get_current_skolem(n);
else if (n->is_empty())
continue;
else if (n->is_char_or_unit())
add = n->get_expr();
else if (n->is_power())
add = m_seq.str.mk_power(get_current_skolem_str(n->arg(0)), n->arg(1)->get_expr());
else {
UNREACHABLE();
}
if (e)
e = seq().str.mk_concat(e, add);
else
e = add;
}
if (!e)
e = seq().str.mk_empty(s->get_sort());
return e;
}
expr_ref nielsen_graph::get_or_create_char_var(euf::snode* var) {
SASSERT(var && var->is_var());
th_rewriter rw(m);

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

@ -1201,6 +1201,8 @@ namespace seq {
// Gets the expression representing the variable with respect to its current mod-count
expr_ref get_current_skolem(euf::snode* var);
expr_ref get_current_skolem_str(euf::snode* s);
// Get or create a fresh symbolic character variable for the given variable
expr_ref get_or_create_char_var(euf::snode* var);