mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 18:08:57 +00:00
Code Activity

Bug fixing with unit replacement

Browse source
This commit is contained in:
CEisenhofer 2026-03-26 15:56:58 +01:00
parent 17ca44b351
commit 3b5b53126e
6 changed files with 33 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/euf/euf_snode.h
View file

@ -99,6 +99,7 @@ namespace euf {
unsigned num_args() const { return m_num_args; }
snode* arg(unsigned i) const { SASSERT(i < m_num_args); return m_args[i]; }
// TODO: Track regex being "classical" (no complement, intersection, fail)
bool is_ground() const { return m_ground; }
bool is_regex_free() const { return m_regex_free; }
bool is_nullable() const { return m_nullable; }

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

@ -196,6 +196,12 @@ namespace seq {
return true;
}
bool nielsen_subst::is_char_subst() const {
SASSERT(m_var && m_replacement);
SASSERT(!m_var->is_unit() || m_replacement->is_char_or_unit());
return m_var->is_unit();
}
// -----------------------------------------------
// nielsen_edge
// -----------------------------------------------
@ -275,6 +281,13 @@ namespace seq {
mem.m_dep = m_graph.dep_mgr().mk_join(mem.m_dep, s.m_dep);
}
}
if (s.m_var->is_unit()) {
SASSERT(s.m_replacement->is_char_or_unit());
expr* v = s.m_var->arg(0)->get_expr();
expr* repl = s.m_replacement->arg(0)->get_expr();
expr* eq = sg.get_manager().mk_eq(v, repl);
m_constraints.push_back(constraint(eq, s.m_dep, sg.get_manager()));
}
}
void nielsen_node::add_char_range(euf::snode* sym_char, char_set const& range) {
@ -1601,14 +1614,12 @@ namespace seq {
eqs[eq_idx] = eqs.back();
eqs.pop_back();
nielsen_subst subst(lt->arg(0), rt->arg(0), eq.m_dep);
nielsen_subst subst(lt, rt, eq.m_dep);
e->add_subst(subst);
child->apply_subst(m_sg, subst);
if (!lhs_rest->is_empty() && !rhs_rest->is_empty())
eqs.push_back(str_eq(lhs_rest, rhs_rest, eq.m_dep));
// NSB review: lt->arg(0) == rt->arg(0) should also be a side constraint
return true;
}
else
@ -3657,6 +3668,8 @@ namespace seq {
svector<std::pair<unsigned, expr*>> lhs_exprs;
for (unsigned i = 0; i < substs.size(); ++i) {
auto const& s = substs[i];
if (s.is_char_subst())
continue;
SASSERT(s.m_var && s.m_var->is_var());
if (!m_seq.is_seq(s.m_var->get_expr()))
continue;

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

@ -425,12 +425,13 @@ namespace seq {
SASSERT(repl != nullptr);
// var may be s_var or s_power; sgraph::subst uses pointer identity matching
SASSERT(var->is_var() || var->is_power() || var->is_unit());
SASSERT(!var->is_unit());
}
// an eliminating substitution does not contain the variable in the replacement
bool is_eliminating() const;
bool is_char_subst() const;
bool operator==(nielsen_subst const& other) const {
return m_var == other.m_var && m_replacement == other.m_replacement;
}
@ -463,7 +464,7 @@ namespace seq {
// relationships between length variables and power exponents.
// mirrors ZIPT's IntEq / IntLe over Presburger arithmetic polynomials.
struct constraint {
expr_ref fml; // the formula (eq, le, or ge expression)
expr_ref fml; // the formula (eq, le, or ge, unit-diseq expression)
dep_tracker dep; // tracks which input constraints contributed
constraint(ast_manager& m):
@ -479,7 +480,6 @@ namespace seq {
nielsen_node* m_src;
nielsen_node* m_tgt;
vector<nielsen_subst> m_subst;
vector<char_subst> m_char_subst; // character-level substitutions (mirrors ZIPT's SubstC)
vector<constraint> m_side_constraints; // side constraints: integer equalities/inequalities
bool m_is_progress; // does this edge represent progress?
bool m_len_constraints_computed = false; // lazily computed substitution length constraints
@ -496,9 +496,6 @@ namespace seq {
vector<nielsen_subst> const& subst() const { return m_subst; }
void add_subst(nielsen_subst const& s) { m_subst.push_back(s); }
vector<char_subst> const& char_substs() const { return m_char_subst; }
void add_char_subst(char_subst const& s) { m_char_subst.push_back(s); }
void add_side_constraint(constraint const& ic) { m_side_constraints.push_back(ic); }
vector<constraint> const& side_constraints() const { return m_side_constraints; }
@ -580,7 +577,7 @@ namespace seq {
void add_constraint(constraint const &ic);
vector<constraint> const& constraints() const { return m_constraints; }
vector<constraint>& constraints() { return m_constraints; }
vector<constraint>& constraints() { return m_constraints; }
// Query current bounds for a variable from the arithmetic subsolver.
// Falls der Subsolver keinen Bound liefert, werden konservative Defaults

6
src/smt/seq/seq_nielsen_pp.cpp
View file

@ -618,12 +618,6 @@ namespace seq {
<< " &#8594; " // mapping arrow
<< snode_label_html(s.m_replacement, m);
}
for (auto const& cs : e->char_substs()) {
if (!first) out << "<br/>";
first = false;
out << "?" << cs.m_var->id()
<< " &#8594; ?" << cs.m_val->id();
}
// side constraints: integer equalities/inequalities
for (auto const& ic : e->side_constraints()) {
if (!first) out << "<br/>";

14
src/smt/theory_nseq.cpp
View file

@ -37,7 +37,8 @@ namespace smt {
m_nielsen(m_sgraph, m_context_solver),
m_axioms(m_th_rewriter),
m_regex(m_sgraph),
m_model(m, m_seq, m_rewriter, m_sgraph)
m_model(m, m_seq, m_rewriter, m_sgraph),
m_relevant_lengths(m)
{
std::function<void(expr_ref_vector const&)> add_clause =
[&](expr_ref_vector const &clause) {
@ -112,7 +113,7 @@ namespace smt {
// -----------------------------------------------------------------------
bool theory_nseq::internalize_atom(app* atom, bool /*gate_ctx*/) {
std::cout << "internalize_atom: " << mk_pp(atom, m) << std::endl;
// std::cout << "internalize_atom: " << mk_pp(atom, m) << std::endl;
// str.in_re atoms are boolean predicates: register as bool_var
// so that assign_eh fires when the SAT solver assigns them.
// Following theory_seq: create a bool_var directly without an enode
@ -144,7 +145,7 @@ namespace smt {
}
bool theory_nseq::internalize_term(app* term) {
std::cout << "internalize_term: " << mk_pp(term, m) << std::endl;
// std::cout << "internalize_term: " << mk_pp(term, m) << std::endl;
// ensure ALL children are internalized (following theory_seq pattern)
for (auto arg : *term) {
mk_var(ensure_enode(arg));
@ -181,6 +182,11 @@ namespace smt {
m_ho_terms.push_back(term);
ensure_length_var(ho_s);
}
expr* v;
if (m_seq.str.is_length(term, v)) {
ctx.push_trail(restore_vector(m_relevant_lengths));
m_relevant_lengths.push_back(term);
}
return true;
}
@ -605,7 +611,7 @@ namespace smt {
auto lit = mk_literal(c.fml);
switch (ctx.get_assignment(lit)) {
case l_true: break;
case l_undef:
case l_undef:
has_undef = true;
ctx.force_phase(lit);
IF_VERBOSE(2, verbose_stream() <<

2
src/smt/theory_nseq.h
View file

@ -56,6 +56,7 @@ namespace smt {
using mem_item = tracked_str_mem; // regex membership
struct axiom_item { expr* e; }; // structural axiom for term e
// TODO: Track unit disequalities and add them to Nielsen graph
using prop_item = std::variant<eq_item, mem_item, axiom_item>;
vector<prop_item> m_prop_queue;
@ -63,6 +64,7 @@ namespace smt {
unsigned m_next_mem_id = 0; // monotone counter for tracked_str_mem ids
obj_hashtable<expr> m_axiom_set; // dedup guard for axiom_item enqueues
obj_hashtable<expr> m_no_diseq_set; // track expressions that should not trigger new disequality axioms
expr_ref_vector m_relevant_lengths; // track variables whose lengths are relevant
// statistics
unsigned m_num_conflicts = 0;