mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-03 04:33:28 +00:00
Code Activity

use definition of is_var from theory_seq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-08-01 14:41:05 -07:00
parent 068edf6a46
commit 1e507cd11e
3 changed files with 18 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/rewriter/seq_monadic.cpp
View file

@ -273,16 +273,13 @@ bool seq_monadic::parse_term(expr* t, vector<atom>& atoms, expr*& the_var) {
}
return true;
}
if (u().str.is_unit(t)) { // seq.unit of a constant element
expr* elem = to_app(t)->get_arg(0);
if (m.is_value(elem)) {
atoms.push_back(atom(m, false, nullptr, elem));
return true;
}
return false; // symbolic (non-constant) unit: unsupported
expr *elem = nullptr;
if (u().str.is_unit(t, elem) && m.is_value(elem)) { // seq.unit of a constant element
atoms.push_back(atom(m, false, nullptr, elem));
return true;
}
// uninterpreted 0-ary constant of sequence sort => a sequence variable
if (is_uninterp_const(t)) {
// uninterpreted constant of sequence sort => a sequence variable
if (is_var(t)) {
the_var = t; // mark that at least one variable occurs
atoms.push_back(atom(m, true, t, nullptr));
return true;

9
src/ast/rewriter/seq_monadic.h
View file

@ -88,6 +88,7 @@ private:
using membership_vec = vector<std::tuple<expr_ref, expr_ref, void*>>;
membership_vec m_memberships; // asserted (term in regex, dep) for check()
ptr_vector<void> m_core; // dependencies of an unsat subset, filled by check() on l_false
std::function<bool(expr *)> m_is_var; // predicate for whether a term is a sequence variable
seq_util& u() const { return m_rw.u(); }
seq_util::rex& re() const { return m_rw.u().re; }
@ -162,6 +163,10 @@ private:
// deletion and collect the (non-null) dependencies of its members into m_core.
void minimize_core(membership_vec const& memberships);
bool is_var(expr *term) const {
return m_is_var ? m_is_var(term) : is_uninterp(term);
}
public:
seq_monadic(seq_rewriter& rw, trail_stack& undo_trail,
transition_mode mode = transition_mode::light_antimirov) :
@ -191,6 +196,10 @@ public:
// returns the dependencies of all asserted memberships (no deletion-based shrinking).
void set_min_core(bool b) { m_min_core = b; }
void set_is_var(std::function<bool(expr *)> const &is_var) {
m_is_var = is_var;
}
// Assert a membership (term in regex) to be decided jointly by the next check().
// `d` carries the dependency used for unsat-core tracking and may be nullptr.
// Memberships remain asserted until the constructor-provided trail is popped.

4
src/smt/seq_regex.cpp
View file

@ -32,7 +32,9 @@ namespace smt {
m(th.get_manager()),
m_monadic(seq_rw(), ctx.get_trail_stack()),
m_state_to_expr(m),
m_state_graph(state_graph::state_pp(this, pp_state)) { }
m_state_graph(state_graph::state_pp(this, pp_state)) {
m_monadic.set_is_var([&th](expr *e) { return th.is_var(e); });
}
seq_util& seq_regex::u() { return th.m_util; }
class seq_util::rex& seq_regex::re() { return th.m_util.re; }