mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

Character ranges must be passed back to the solver

Browse source
This commit is contained in:
CEisenhofer 2026-04-09 15:21:12 +02:00
parent aafb704cf8
commit 09572b20ed
2 changed files with 22 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -351,6 +351,22 @@ namespace seq {
}
else
m_char_ranges.insert(id, std::make_pair(range.clone(), dep));
auto& ranges = range.ranges();
auto& m = graph().get_manager();
auto& seq = graph().seq();
expr* var = sym_char->get_expr();
SASSERT(seq.str.is_unit(var));
var = to_app(var)->get_arg(0);
ptr_vector<expr> cases;
cases.reserve(ranges.size());
for (unsigned i = 0; i < ranges.size(); ++i) {
cases[i] = m.mk_and(
seq.mk_le(seq.mk_char(ranges[i].m_lo), var),
seq.mk_le(var, seq.mk_char(ranges[i].m_hi - 1)));
}
add_constraint(constraint(m.mk_or(cases), dep, m));
}
bool nielsen_node::lower_bound(expr* e, rational& lo) const {
@ -4145,21 +4161,6 @@ nielsen_graph::generate_length_constraints(vector<length_constraint>& constraint
if (m_sat_node) {
for (auto const& ic : m_sat_node->constraints())
m_solver.assert_expr(ic.fml);
for (auto const& kvp : m_sat_node->char_ranges()) {
expr_ref_vector cases(m);
auto var = m_sg.nodes()[kvp.m_key]->get_expr();
SASSERT(seq().str.is_unit(var));
var = to_app(var)->get_arg(0);
const auto& ranges = kvp.m_value.first.ranges();
cases.reserve(ranges.size());
for (unsigned i = 0; i < ranges.size(); ++i) {
cases[i] = m.mk_and(
seq().mk_le(seq().mk_char(ranges[i].m_lo), var),
seq().mk_le(var, seq().mk_char(ranges[i].m_hi - 1)));
}
m_solver.assert_expr(m.mk_or(cases));
}
}
lbool result = m_solver.check();
IF_VERBOSE(1, verbose_stream() << "solve_sat_path_ints result: " << result << "\n";);

9
src/smt/seq_model.cpp
View file

@ -48,7 +48,7 @@ namespace smt {
// solve integer constraints from the sat_path FIRST so that
// m_int_model is available when snode_to_value evaluates power exponents
nielsen.solve_sat_path_raw(m_int_model);
VERIFY(nielsen.solve_sat_path_raw(m_int_model));
// extract variable assignments from the satisfying leaf's substitution path
extract_assignments(nielsen.sat_path());
@ -171,11 +171,14 @@ namespace smt {
if (n->is_char() || n->is_unit()) {
expr* e = n->get_expr();
SASSERT(m_seq.str.is_unit(e));
e = to_app(e)->get_arg(0);
expr_ref val(m);
if (e && m_int_model) {
unsigned c;
m_int_model->eval_expr(e, val, true);
if (val)
return val;
if (val && m_seq.is_const_char(val, c))
return expr_ref(m_seq.str.mk_string(zstring(c)), m);
}
return e ? expr_ref(e, m) : expr_ref(m);
}