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

Simplify code

Browse source
This commit is contained in:
CEisenhofer 2026-04-13 14:06:06 +02:00
parent 276b9c38af
commit d620f20c63
4 changed files with 29 additions and 95 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1056,11 +1056,9 @@ namespace seq {
}
else {
// we only know for sure that one is smaller than the other
expr_ref d(m_graph.mk_fresh_int_var());
expr_ref zero_e(m_graph.a.mk_int(0), m);
expr_ref d_plus_smaller(m_graph.a.mk_add(d, smaller_exp), m);
add_constraint(m_graph.mk_constraint(m_graph.a.mk_ge(d, zero_e), eq.m_dep));
add_constraint(m_graph.mk_constraint(m.mk_eq(d_plus_smaller, larger_exp), eq.m_dep));
expr_ref d(m_graph.a.mk_sub(larger_exp, smaller_exp), m);
expr_ref zero(m_graph.a.mk_int(0), m);
add_constraint(m_graph.mk_constraint(m_graph.a.mk_ge(d, zero), eq.m_dep));
expr_ref pw(seq.str.mk_power(lb, d), m);
euf::snode*& larger_side = lp_le_rp ? eq.m_rhs : eq.m_lhs;
larger_side = dir_concat(sg, sg.mk(pw), larger_side, fwd);
@ -1082,7 +1080,7 @@ namespace seq {
bool fwd = od == 0;
while (!mem.m_str->is_empty()) {
euf::snode* tok = dir_token(mem.m_str, fwd);
if (!tok || !tok->is_char())
if (!tok || !tok->is_char_or_unit())
break;
euf::snode* deriv = fwd
? sg.brzozowski_deriv(mem.m_regex, tok)
@ -3003,8 +3001,6 @@ namespace seq {
if (mem.is_primitive() || !mem.m_regex->is_classical())
continue;
std::cout << "Factoring " << mk_pp(mem.m_str->get_expr(), m) << " ∈ " << mk_pp(mem.m_regex->get_expr(), m) << std::endl;
euf::snode* first = mem.m_str->first();
SASSERT(first);
euf::snode* tail = m_sg.drop_first(mem.m_str);
@ -3013,9 +3009,6 @@ namespace seq {
tau_pairs pairs;
compute_tau(m, m_seq, m_sg, mem.m_regex->get_expr(), pairs);
bool any_child = false;
dep_tracker conflict_dep = mem.m_dep;
for (auto const& pair : pairs) {
euf::snode* sn_p = m_sg.mk(pair.m_p);
euf::snode* sn_q = m_sg.mk(pair.m_q);
@ -3030,19 +3023,13 @@ namespace seq {
// Also check intersection with other primitive constraints on `first`
ptr_vector<euf::snode> regexes_p;
regexes_p.push_back(sn_p);
dep_tracker local_dep = nullptr;
for (auto const& prev_mem : node->str_mems()) {
if (prev_mem.m_str == first) {
if (prev_mem.m_str == first)
regexes_p.push_back(prev_mem.m_regex);
local_dep = m_dep_mgr.mk_join(local_dep, prev_mem.m_dep);
}
}
if (regexes_p.size() > 1 && m_seq_regex->check_intersection_emptiness(regexes_p, 100) == l_true) {
conflict_dep = m_dep_mgr.mk_join(conflict_dep, local_dep);
if (regexes_p.size() > 1 && m_seq_regex->check_intersection_emptiness(regexes_p, 100) == l_true)
continue;
}
any_child = true;
nielsen_node* child = mk_child(node);
mk_edge(node, child, true);
@ -3060,11 +3047,6 @@ namespace seq {
child->add_str_mem(str_mem(tail, sn_q, mem.m_history, next_mem_id(), mem.m_dep));
}
if (!any_child) {
node->set_conflict(backtrack_reason::regex, conflict_dep);
node->set_general_conflict();
}
return true;
}
return false;
@ -4107,8 +4089,8 @@ namespace seq {
return false; // definitely infeasible
}
rational rhs_lo, lhs_up;
if (m_solver.lower_bound(lhs, lhs_lo) &&
m_solver.upper_bound(rhs, rhs_up)) {
if (m_solver.upper_bound(lhs, lhs_up) &&
m_solver.lower_bound(rhs, rhs_lo)) {
if (lhs_up <= rhs_lo)
return true; // definitely feasible
@ -4148,41 +4130,6 @@ namespace seq {
return expr_ref(m.mk_fresh_const(name.c_str(), a.mk_int()), m);
}
bool nielsen_graph::solve_sat_path_raw(model_ref& mdl) {
mdl = nullptr;
if (m_sat_path.empty() && (!m_sat_node ||
(m_sat_node->constraints().empty() && m_sat_node->char_ranges().empty())))
return false;
// Re-assert the sat-path constraints into m_solver (which holds only root-level
// constraints at this point) and extract a model via the injected simple_solver.
// The sat path was found by DFS which verified feasibility at every step via
// check_int_feasibility, so all constraints along this path are jointly satisfiable
// and do not require incremental skipping.
IF_VERBOSE(1, verbose_stream() << "solve_sat_path_ints: sat_path length=" << m_sat_path.size() << "\n";);
m_solver.push();
if (m_sat_node) {
for (auto const& ic : m_sat_node->constraints()) {
m_solver.assert_expr(ic.fml);
}
}
lbool result = m_solver.check();
IF_VERBOSE(1, verbose_stream() << "solve_sat_path_ints result: " << result << "\n";);
if (result == l_true) {
m_solver.get_model(mdl);
IF_VERBOSE(1, if (mdl) {
verbose_stream() << " raw_model:\n";
for (unsigned i = 0; i < mdl->get_num_constants(); ++i) {
func_decl* fd = mdl->get_constant(i);
expr* val = mdl->get_const_interp(fd);
if (val) verbose_stream() << " " << fd->get_name() << " = " << mk_bounded_pp(val, m, 3) << "\n";
}
});
}
m_solver.pop(1);
return mdl.get() != nullptr;
}
// -----------------------------------------------------------------------
// Regex widening: overapproximate string and check intersection emptiness
// Mirrors ZIPT NielsenNode.CheckRegexWidening (NielsenNode.cs:1350-1380)

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

@ -933,13 +933,6 @@ namespace seq {
// max_len == UINT_MAX means unbounded.
void compute_regex_length_interval(euf::snode* regex, unsigned& min_len, unsigned& max_len);
// solve all integer constraints along the sat_path and return
// a model mapping integer variables to concrete values.
// Must be called after solve() returns sat.
// Returns true if a satisfying model was found.
// Caller takes ownership of the returned model pointer.
bool solve_sat_path_raw(model_ref& mdl);
// accessor for the seq_regex module
seq_regex* seq_regex_module() const { return m_seq_regex; }

18
src/smt/seq_model.cpp
View file

@ -147,7 +147,6 @@ namespace smt {
m_var_values.reset();
m_var_regex.reset();
m_trail.reset();
m_int_model = nullptr;
m_mg = &mg;
m_factory = alloc(seq_factory, m, m_seq.get_family_id(), mg.get_model());
@ -220,7 +219,6 @@ namespace smt {
m_var_values.reset();
m_var_regex.reset();
m_trail.reset();
m_int_model = nullptr;
m_mg = nullptr;
m_factory = nullptr;
}
@ -374,22 +372,6 @@ namespace smt {
else
exp_val = rational(0);
}
else if (exp_expr && m_int_model.get()) {
expr_ref result(m);
if (m_int_model->eval_expr(exp_expr, result, true) && arith.is_numeral(result, exp_val)) {
// evaluated from int model
}
else if (m_mg) {
proto_model& pm = m_mg->get_model();
if (pm.eval(exp_expr, result, true) && arith.is_numeral(result, exp_val)) {
// evaluated from proto_model
}
else
exp_val = rational(0);
}
else
exp_val = rational(0);
}
else if (exp_expr && m_mg) {
expr_ref result(m);
proto_model& pm = m_mg->get_model();

30
src/smt/theory_nseq.cpp
View file

@ -613,7 +613,9 @@ namespace smt {
if (!m_nielsen_literals.empty() && m_nielsen.sat_node() != nullptr &&
all_of(m_nielsen_literals, [&](auto lit) { return l_true == ctx.get_assignment(lit); })) {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: satifiable state revisited\n");
return FC_DONE;
// Re-run solving/model extraction instead of early exiting on a
// cached SAT node. This avoids stale sat paths after additional
// SAT assignments were introduced in prior FC_CONTINUE rounds.
}
// unfold higher-order terms when sequence structure is known
@ -693,8 +695,13 @@ namespace smt {
// Nielsen found a consistent assignment for positive constraints.
SASSERT(has_eq_or_mem); // we should have axiomatized them
if (!add_nielsen_assumptions())
return FC_CONTINUE;
if (!add_nielsen_assumptions()) {
// If assumptions remain undefined, returning SAT can yield
// unsound/invalid models because the chosen Nielsen branch
// is not yet committed in the outer SAT core.
IF_VERBOSE(1, verbose_stream() << "nseq final_check: unresolved assumptions, FC_GIVEUP\n";);
return FC_GIVEUP;
}
if (!check_length_coherence())
return FC_CONTINUE;
@ -730,17 +737,22 @@ namespace smt {
//std::cout << "Nielsen assumptions:\n";
ctx.push_trail(reset_vector(m_nielsen_literals));
for (auto const& c : m_nielsen.sat_node()->constraints()) {
bool was_internalized = ctx.e_internalized(c.fml);
auto lit = mk_literal(c.fml);
m_nielsen_literals.push_back(lit);
std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl;
// Ensure Nielsen assumptions participate in SAT search instead of
// remaining permanently undefined under pure phase hints.
ctx.mark_as_relevant(lit);
// std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl;
switch (ctx.get_assignment(lit)) {
case l_true:
break;
case l_undef:
//std::cout << "Undef [" << lit << "]: " << mk_pp(c.fml, m) << "\n";
std::cout << "Undef [" << lit << "]: " << mk_pp(c.fml, m) << std::endl;
has_undef = true;
ctx.force_phase(lit);
// Commit the chosen Nielsen assumption to the SAT core so it
// cannot remain permanently undefined in a partial model.
ctx.mk_th_axiom(get_id(), 1, &lit);
ctx.force_phase(lit);
IF_VERBOSE(2, verbose_stream() <<
"nseq final_check: adding nielsen assumption " << c.fml << "\n";);
TRACE(seq, tout << "assign: " << c.fml << "\n");
@ -749,10 +761,10 @@ namespace smt {
// this should not happen because nielsen checks for this before returning a satisfying path.
IF_VERBOSE(1, verbose_stream()
<< "nseq final_check: nielsen assumption " << c.fml << " is false\n";);
ctx.force_phase(lit);
has_undef = true;
ctx.mk_th_axiom(get_id(), 1, &lit);
ctx.force_phase(lit);
//std::cout << "False [" << lit << "]: " << mk_pp(c.fml, m) << std::endl;
std::cout << "False [" << lit << "]: " << mk_pp(c.fml, m) << std::endl;
break;
}
}