mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

[WIP] Try to replace "recursive reusage" of variables by seq.slice

Browse source
This commit is contained in:
CEisenhofer 2026-05-20 17:24:57 +02:00
parent dd00dd7362
commit 315a09aea8
7 changed files with 88 additions and 156 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -321,7 +321,7 @@ namespace seq {
// We have to add all - even if some of it conflict // We have to add all - even if some of it conflict
// [otw. we would leave the node partially initialized] // [otw. we would leave the node partially initialized]
for (const auto f : *to_app(c.fml)) { for (const auto f : *to_app(c.fml)) {
add_constraint(constraint(f, c.dep, m)); add_constraint(constraint(f, c.dep, c.internal, m));
} }
return; return;
} }
@ -371,8 +371,7 @@ namespace seq {
expr* var_c_expr = s.m_var->arg(0)->get_expr(); expr* var_c_expr = s.m_var->arg(0)->get_expr();
expr* repl_c_expr = s.m_replacement->arg(0)->get_expr(); expr* repl_c_expr = s.m_replacement->arg(0)->get_expr();
add_constraint( add_constraint(
constraint( constraint(m.mk_eq(var_c_expr, repl_c_expr), s.m_dep, false, m));
m.mk_eq(var_c_expr, repl_c_expr), s.m_dep, m));
if (m_char_ranges.contains(var_id)) { if (m_char_ranges.contains(var_id)) {
const auto range = m_char_ranges.find(var_id); // copy exactly const auto range = m_char_ranges.find(var_id); // copy exactly
@ -426,7 +425,7 @@ namespace seq {
seq.mk_le(seq.mk_char(ranges[i].m_lo), var), seq.mk_le(seq.mk_char(ranges[i].m_lo), var),
seq.mk_le(var, seq.mk_char(ranges[i].m_hi - 1))); seq.mk_le(var, seq.mk_char(ranges[i].m_hi - 1)));
} }
add_constraint(constraint(m.mk_or(cases), dep, m)); add_constraint(constraint(m.mk_or(cases), dep, false, m));
} }
// ----------------------------------------------- // -----------------------------------------------
// nielsen_graph // nielsen_graph
@ -519,16 +518,6 @@ namespace seq {
m_root->add_str_mem(str_mem(str, regex, dep)); m_root->add_str_mem(str_mem(str, regex, dep));
} }
void nielsen_graph::inc_run_idx() {
if (m_run_idx == UINT_MAX) {
for (nielsen_node* n : m_nodes)
n->reset_counter();
m_run_idx = 1;
}
else
++m_run_idx;
}
void nielsen_graph::reset() { void nielsen_graph::reset() {
for (nielsen_node* n : m_nodes) for (nielsen_node* n : m_nodes)
dealloc(n); dealloc(n);
@ -539,7 +528,6 @@ namespace seq {
m_root = nullptr; m_root = nullptr;
m_sat_node = nullptr; m_sat_node = nullptr;
m_sat_path.reset(); m_sat_path.reset();
m_run_idx = 0;
m_depth_bound = 0; m_depth_bound = 0;
m_fresh_cnt = 0; m_fresh_cnt = 0;
m_root_constraints_asserted = false; m_root_constraints_asserted = false;
@ -567,7 +555,7 @@ namespace seq {
// just assume it to be correct // just assume it to be correct
// Just add the constraint - we do not have to recompute it // Just add the constraint - we do not have to recompute it
// [also it is on the set of side-conditions if we assert a satisfied node] // [also it is on the set of side-conditions if we assert a satisfied node]
n->add_constraint(constraint(le, dep, m)); n->add_constraint(constraint(le, dep, false, m));
} }
// ----------------------------------------------------------------------- // -----------------------------------------------------------------------
@ -1708,7 +1696,6 @@ namespace seq {
} }
if (m_max_search_depth > 0 && m_depth_bound > m_max_search_depth) if (m_max_search_depth > 0 && m_depth_bound > m_max_search_depth)
break; break;
inc_run_idx();
ptr_vector<nielsen_edge> cur_path; ptr_vector<nielsen_edge> cur_path;
// scoped_push _scoped_push(m_dep_mgr); // gc dependencies after search // scoped_push _scoped_push(m_dep_mgr); // gc dependencies after search
const search_result r = search_dfs(m_root, cur_path); // the main search loop const search_result r = search_dfs(m_root, cur_path); // the main search loop
@ -1783,29 +1770,17 @@ namespace seq {
if (m_max_nodes > 0 && m_stats.m_num_dfs_nodes > m_max_nodes) if (m_max_nodes > 0 && m_stats.m_num_dfs_nodes > m_max_nodes)
return search_result::unknown; return search_result::unknown;
// revisit detection: if already visited this run (e.g., iterative deepening), return cached status. if (node->is_satisfied()) {
// mirrors ZIPT's NielsenNode.GraphExpansion() evalIdx check. m_sat_node = node;
const unsigned eval_idx = node->eval_idx(); m_sat_path = cur_path;
if (eval_idx == m_run_idx) { return search_result::sat;
if (node->is_satisfied()) {
m_sat_node = node;
m_sat_path = cur_path;
return search_result::sat;
}
if (node->is_currently_conflict())
return search_result::unsat;
return search_result::unknown;
} }
node->set_eval_idx(m_run_idx); if (node->is_currently_conflict())
SASSERT(!node->is_general_conflict()); return search_result::unsat;
if (eval_idx > 0)
// adding the side-conditions from the edge
// when generating this node might trigger a local conflict
node->clear_local_conflict(); // clear local conflicts from previous runs
// we might need to tell the SAT solver about the new integer inequalities // we might need to tell the SAT solver about the new integer inequalities
// that might have been added by an extension step // that might have been added by an extension step
assert_node_new_int_constraints(node); assert_node_side_constraints(node);
if (node->is_currently_conflict()) { if (node->is_currently_conflict()) {
++m_stats.m_num_simplify_conflict; ++m_stats.m_num_simplify_conflict;
@ -1841,7 +1816,7 @@ namespace seq {
// Also generate per-node |LHS| = |RHS| length constraints for descendant // Also generate per-node |LHS| = |RHS| length constraints for descendant
// equations (root constraints are already at the base level). // equations (root constraints are already at the base level).
generate_node_length_constraints(node); generate_node_length_constraints(node);
assert_node_new_int_constraints(node); assert_node_side_constraints(node);
if (node->is_currently_conflict()) { if (node->is_currently_conflict()) {
++m_stats.m_num_simplify_conflict; ++m_stats.m_num_simplify_conflict;
@ -1873,7 +1848,7 @@ namespace seq {
node->set_conflict(backtrack_reason::regex, dep); node->set_conflict(backtrack_reason::regex, dep);
return search_result::unsat; return search_result::unsat;
} }
assert_node_new_int_constraints(node); assert_node_side_constraints(node);
// We need to have everything asserted before reporting SAT // We need to have everything asserted before reporting SAT
// (otw. the outer solver might assume false-assigned literals to be true) // (otw. the outer solver might assume false-assigned literals to be true)
if (node->is_currently_conflict()) { if (node->is_currently_conflict()) {
@ -3971,7 +3946,7 @@ namespace seq {
nielsen_node *child = mk_child(node); nielsen_node *child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true); nielsen_edge* e = mk_edge(node, child, true);
for (const auto f : cs) { for (const auto f : cs) {
e->add_side_constraint(constraint(f, mem.m_dep, m)); e->add_side_constraint(constraint(f, mem.m_dep, false, m));
} }
for (str_mem &cm : child->str_mems()) { for (str_mem &cm : child->str_mems()) {
if (cm == mem) { if (cm == mem) {
@ -4281,11 +4256,21 @@ namespace seq {
dep_tracker nielsen_graph::collect_conflict_deps() const { dep_tracker nielsen_graph::collect_conflict_deps() const {
dep_tracker deps = nullptr; dep_tracker deps = nullptr;
// We enumerate all nodes rather than having a "todo"-list, as // todo: Add visit set if the graph could contain cycles in the future
// hypothetically the graph could contain cycles in the future // enumerating all nodes would not work due to hot-restarts having created
for (nielsen_node const* n : m_nodes) { // children that are currently not relevant
vector<nielsen_node const*> to_visit;
to_visit.push_back(m_root);
while (!to_visit.empty()) {
nielsen_node const* n = to_visit.back();
to_visit.pop_back();
if (n->reason() == backtrack_reason::children_failed) { if (n->reason() == backtrack_reason::children_failed) {
SASSERT(n->m_conflict_external_literal == sat::null_literal); SASSERT(n->m_conflict_external_literal == sat::null_literal);
SASSERT(!n->m_conflict_internal);
for (unsigned i = n->outgoing().size(); i > 0; i--) {
nielsen_edge const* e = n->outgoing()[i - 1];
to_visit.push_back(e->tgt());
}
continue; continue;
} }
// not true anymore since we might have done a hot-restart where we previously created the child: // not true anymore since we might have done a hot-restart where we previously created the child:
@ -4362,7 +4347,7 @@ namespace seq {
tout << "Length constraint from LHS " << snode_label_html(eq.m_lhs, m) << " to " << len_lhs << ":\n"; tout << "Length constraint from LHS " << snode_label_html(eq.m_lhs, m) << " to " << len_lhs << ":\n";
tout << "Length constraint from RHS " << snode_label_html(eq.m_rhs, m) << " to " << len_rhs << "\n"); tout << "Length constraint from RHS " << snode_label_html(eq.m_rhs, m) << " to " << len_rhs << "\n");
expr_ref len_eq(m.mk_eq(len_lhs, len_rhs), m); expr_ref len_eq(m.mk_eq(len_lhs, len_rhs), m);
constraints.push_back(length_constraint(len_eq, eq.m_dep, length_kind::eq, m)); constraints.push_back(length_constraint(len_eq, eq.m_dep, length_kind::eq, true, m));
// collect variables for non-negativity constraints // collect variables for non-negativity constraints
euf::snode_vector tokens; euf::snode_vector tokens;
@ -4374,7 +4359,7 @@ namespace seq {
expr_ref len_var(seq.str.mk_length(tok->get_expr()), m); expr_ref len_var(seq.str.mk_length(tok->get_expr()), m);
expr_ref ge_zero(a.mk_ge(len_var, a.mk_int(0)), m); expr_ref ge_zero(a.mk_ge(len_var, a.mk_int(0)), m);
TRACE(seq, tout << "non-negative length " << ge_zero << "\n"); TRACE(seq, tout << "non-negative length " << ge_zero << "\n");
constraints.push_back(length_constraint(ge_zero, eq.m_dep, length_kind::nonneg, m)); constraints.push_back(length_constraint(ge_zero, eq.m_dep, length_kind::nonneg, true, m));
} }
} }
} }
@ -4393,14 +4378,14 @@ namespace seq {
if (min_len > 0) { if (min_len > 0) {
expr_ref bound(a.mk_ge(len_str, a.mk_int(min_len)), m); expr_ref bound(a.mk_ge(len_str, a.mk_int(min_len)), m);
TRACE(seq, tout << "Parikh " << mk_pp(re_expr, m) << " bound: " << bound << "\n"); TRACE(seq, tout << "Parikh " << mk_pp(re_expr, m) << " bound: " << bound << "\n");
constraints.push_back(length_constraint(bound, mem.m_dep, length_kind::bound, m)); constraints.push_back(length_constraint(bound, mem.m_dep, length_kind::bound, false, m));
} }
// generate len(str) <= max_len when bounded // generate len(str) <= max_len when bounded
if (max_len < UINT_MAX) { if (max_len < UINT_MAX) {
expr_ref bound(a.mk_le(len_str, a.mk_int(max_len)), m); expr_ref bound(a.mk_le(len_str, a.mk_int(max_len)), m);
TRACE(seq, tout << "Parikh " << mk_pp(re_expr, m) << " bound: " << bound << "\n"); TRACE(seq, tout << "Parikh " << mk_pp(re_expr, m) << " bound: " << bound << "\n");
constraints.push_back(length_constraint(bound, mem.m_dep, length_kind::bound, m)); constraints.push_back(length_constraint(bound, mem.m_dep, length_kind::bound, false, m));
} }
} }
} }
@ -4482,7 +4467,7 @@ namespace seq {
continue; continue;
has_non_elim = true; has_non_elim = true;
// Assert LHS >= 0 // Assert LHS >= 0
e->add_side_constraint(mk_constraint(a.mk_ge(lhs, a.mk_int(0)), s.m_dep)); e->add_side_constraint(mk_constraint(a.mk_ge(lhs, a.mk_int(0)), s.m_dep, true));
} }
// Step 2: Bump mod counts for all non-eliminating variables at once. // Step 2: Bump mod counts for all non-eliminating variables at once.
@ -4494,7 +4479,13 @@ namespace seq {
for (auto const &[idx, lhs] : lhs_exprs) { for (auto const &[idx, lhs] : lhs_exprs) {
auto const& s = substs[idx]; auto const& s = substs[idx];
expr_ref rhs = compute_length_expr(s.m_replacement); expr_ref rhs = compute_length_expr(s.m_replacement);
e->add_side_constraint(mk_constraint(m.mk_eq(lhs, rhs), s.m_dep)); e->add_side_constraint(mk_constraint(m.mk_eq(lhs, rhs), s.m_dep, true));
// otw. we have equality as a side-constraint in the Nielsen node
// and adding the Nielsen assumption will force the phase of the equality to true
// however the arith.-solver will axiomatize it as <= && >= which do not have a phase
// hence it might get assigned false by decision which is a performance problem
// e->add_side_constraint(mk_constraint(a.mk_le(lhs, rhs), s.m_dep));
// e->add_side_constraint(mk_constraint(a.mk_ge(lhs, rhs), s.m_dep));
} }
// Step 4: Restore mod counts (temporary bump for computing RHS only). // Step 4: Restore mod counts (temporary bump for computing RHS only).
@ -4547,7 +4538,7 @@ namespace seq {
m_length_solver.assert_expr(e); m_length_solver.assert_expr(e);
} }
void nielsen_graph::assert_node_new_int_constraints(nielsen_node* node) const { void nielsen_graph::assert_node_side_constraints(nielsen_node* node) const {
// Assert only the constraints that are new to this node (beyond those // Assert only the constraints that are new to this node (beyond those
// inherited from its parent via clone_from). The parent's constraints are // inherited from its parent via clone_from). The parent's constraints are
// already present in the enclosing solver scope; asserting them again would // already present in the enclosing solver scope; asserting them again would
@ -4585,7 +4576,7 @@ namespace seq {
expr_ref len_lhs = compute_length_expr(eq.m_lhs); expr_ref len_lhs = compute_length_expr(eq.m_lhs);
expr_ref len_rhs = compute_length_expr(eq.m_rhs); expr_ref len_rhs = compute_length_expr(eq.m_rhs);
node->add_constraint(mk_constraint(m.mk_eq(len_lhs, len_rhs), eq.m_dep)); node->add_constraint(mk_constraint(m.mk_eq(len_lhs, len_rhs), eq.m_dep, true));
// non-negativity for each variable (mod-count-aware) // non-negativity for each variable (mod-count-aware)
euf::snode_vector tokens; euf::snode_vector tokens;
@ -4595,7 +4586,7 @@ namespace seq {
if (tok->is_var() && !seen_vars.contains(tok->id())) { if (tok->is_var() && !seen_vars.contains(tok->id())) {
seen_vars.insert(tok->id()); seen_vars.insert(tok->id());
expr_ref len_var = compute_length_expr(tok); expr_ref len_var = compute_length_expr(tok);
node->add_constraint(mk_constraint(a.mk_ge(len_var, a.mk_int(0)), eq.m_dep)); node->add_constraint(mk_constraint(a.mk_ge(len_var, a.mk_int(0)), eq.m_dep, true));
} }
} }
} }
@ -4611,9 +4602,9 @@ namespace seq {
expr_ref len_str = compute_length_expr(mem.m_str); expr_ref len_str = compute_length_expr(mem.m_str);
if (min_len > 0) if (min_len > 0)
node->add_constraint(mk_constraint(a.mk_ge(len_str, a.mk_int(min_len)), mem.m_dep)); node->add_constraint(mk_constraint(a.mk_ge(len_str, a.mk_int(min_len)), mem.m_dep, true));
if (max_len < UINT_MAX) if (max_len < UINT_MAX)
node->add_constraint(mk_constraint(a.mk_le(len_str, a.mk_int(max_len)), mem.m_dep)); node->add_constraint(mk_constraint(a.mk_le(len_str, a.mk_int(max_len)), mem.m_dep, true));
} }
} }
@ -4674,14 +4665,14 @@ namespace seq {
dep = m_length_solver.core(); dep = m_length_solver.core();
m_length_solver.pop(1); m_length_solver.pop(1);
if (result == l_false) { if (result == l_false) {
n->add_constraint(constraint(a.mk_le(lhs, rhs), dep, m)); n->add_constraint(constraint(a.mk_le(lhs, rhs), dep, false, m));
return true; return true;
} }
return false; return false;
} }
constraint nielsen_graph::mk_constraint(expr* fml, dep_tracker const& dep) const { constraint nielsen_graph::mk_constraint(expr* fml, dep_tracker const& dep, bool internal) const {
return constraint(fml, dep, m); return constraint(fml, dep, internal, m);
} }
expr* nielsen_graph::get_power_exponent(euf::snode* power) { expr* nielsen_graph::get_power_exponent(euf::snode* power) {

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

@ -499,6 +499,7 @@ namespace seq {
struct constraint { struct constraint {
expr_ref fml; // the formula (eq, le, or ge, unit-diseq expression) expr_ref fml; // the formula (eq, le, or ge, unit-diseq expression)
dep_tracker dep; // tracks which input constraints contributed dep_tracker dep; // tracks which input constraints contributed
bool internal; // don't push back to the outer solver (helpful if not necessary and it would reveal internal variables)
static expr_ref simplify(expr* f, ast_manager& m) { static expr_ref simplify(expr* f, ast_manager& m) {
//th_rewriter th(m); //th_rewriter th(m);
@ -508,9 +509,10 @@ namespace seq {
} }
constraint(ast_manager& m): constraint(ast_manager& m):
fml(m), dep(nullptr) {} fml(m), dep(nullptr), internal(true) {}
constraint(expr* f, dep_tracker const& d, ast_manager& m):
fml(simplify(f, m)), dep(d) {} constraint(expr* f, dep_tracker const& d, const bool internal, ast_manager& m):
fml(simplify(f, m)), dep(d), internal(internal) {}
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
}; };
@ -527,13 +529,14 @@ namespace seq {
expr_ref m_expr; // arithmetic expression (e.g., len(x) + len(y) = len(a) + 1) expr_ref m_expr; // arithmetic expression (e.g., len(x) + len(y) = len(a) + 1)
dep_tracker m_dep; // tracks which input constraints contributed dep_tracker m_dep; // tracks which input constraints contributed
length_kind m_kind; // determines propagation strategy length_kind m_kind; // determines propagation strategy
bool m_internal;
length_constraint(ast_manager& m): m_expr(m), m_dep(nullptr), m_kind(length_kind::nonneg) {} length_constraint(ast_manager& m): m_expr(m), m_dep(nullptr), m_kind(length_kind::nonneg), m_internal(true) {}
length_constraint(expr* e, dep_tracker const& dep, length_kind kind, ast_manager& m): length_constraint(expr* e, dep_tracker const& dep, length_kind kind, const bool internal, ast_manager& m):
m_expr(e, m), m_dep(dep), m_kind(kind) {} m_expr(e, m), m_dep(dep), m_kind(kind), m_internal(internal) {}
constraint to_constraint() const { constraint to_constraint() const {
return constraint(m_expr, m_dep, m_expr.get_manager()); return constraint(m_expr, m_dep, m_internal, m_expr.get_manager());
} }
}; };
@ -603,9 +606,6 @@ namespace seq {
bool m_is_progress = false; bool m_is_progress = false;
bool m_node_len_constraints_generated = false; // true after generate_node_length_constraints runs bool m_node_len_constraints_generated = false; // true after generate_node_length_constraints runs
// evaluation index for run tracking
unsigned m_eval_idx = 0;
// Parikh filter: set to true once apply_parikh_to_node has been applied // Parikh filter: set to true once apply_parikh_to_node has been applied
// to this node. Prevents duplicate constraint generation across DFS runs. // to this node. Prevents duplicate constraint generation across DFS runs.
bool m_parikh_applied = false; bool m_parikh_applied = false;
@ -724,10 +724,6 @@ namespace seq {
bool is_progress() const { return m_is_progress; } bool is_progress() const { return m_is_progress; }
unsigned eval_idx() const { return m_eval_idx; }
void set_eval_idx(unsigned idx) { m_eval_idx = idx; }
void reset_counter() { m_eval_idx = 0; }
// clone constraints from a parent node // clone constraints from a parent node
void clone_from(nielsen_node const& parent); void clone_from(nielsen_node const& parent);
@ -849,7 +845,6 @@ namespace seq {
nielsen_node* m_root = nullptr; nielsen_node* m_root = nullptr;
nielsen_node* m_sat_node = nullptr; nielsen_node* m_sat_node = nullptr;
ptr_vector<nielsen_edge> m_sat_path; ptr_vector<nielsen_edge> m_sat_path;
unsigned m_run_idx = 0;
unsigned m_depth_bound = 0; unsigned m_depth_bound = 0;
unsigned m_max_search_depth = 0; unsigned m_max_search_depth = 0;
unsigned m_max_nodes = 0; // 0 = unlimited unsigned m_max_nodes = 0; // 0 = unlimited
@ -969,10 +964,6 @@ namespace seq {
void add_str_eq(euf::snode* lhs, euf::snode* rhs); void add_str_eq(euf::snode* lhs, euf::snode* rhs);
void add_str_mem(euf::snode* str, euf::snode* regex); void add_str_mem(euf::snode* str, euf::snode* regex);
// run management
unsigned run_idx() const { return m_run_idx; }
void inc_run_idx();
// access all nodes // access all nodes
ptr_vector<nielsen_node> const& nodes() const { return m_nodes; } ptr_vector<nielsen_node> const& nodes() const { return m_nodes; }
unsigned num_nodes() const { return m_nodes.size(); } unsigned num_nodes() const { return m_nodes.size(); }
@ -1065,7 +1056,7 @@ namespace seq {
// parent (indices [m_parent_ic_count..end)) into the current solver scope. // parent (indices [m_parent_ic_count..end)) into the current solver scope.
// Called by search_dfs after simplify_and_init so that the newly derived // Called by search_dfs after simplify_and_init so that the newly derived
// bounds become visible to subsequent check() and check_lp_le() calls. // bounds become visible to subsequent check() and check_lp_le() calls.
void assert_node_new_int_constraints(nielsen_node* node) const; void assert_node_side_constraints(nielsen_node* node) const;
private: private:
@ -1316,7 +1307,7 @@ namespace seq {
bool check_lp_le(expr* lhs, expr* rhs, nielsen_node* n, dep_tracker& dep); bool check_lp_le(expr* lhs, expr* rhs, nielsen_node* n, dep_tracker& dep);
// create an integer constraint: lhs <kind> rhs // create an integer constraint: lhs <kind> rhs
constraint mk_constraint(expr* fml, dep_tracker const& dep) const; constraint mk_constraint(expr* fml, dep_tracker const& dep, bool internal = false) const;
// get the exponent expression from a power snode (arg(1)) // get the exponent expression from a power snode (arg(1))
static expr * get_power_exponent(euf::snode* power); static expr * get_power_exponent(euf::snode* power);

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

@ -537,9 +537,10 @@ namespace seq {
out << "<br/>"; out << "<br/>";
} }
// integer constraints // integer constraints
std::vector<std::string> int_constraints(m_constraints.size()); std::vector<std::string> int_constraints;
for (auto const& ic : m_constraints) { for (auto const& ic : m_constraints) {
int_constraints.push_back(constraint_html(ic, names, next_id, m)); int_constraints.push_back(
(ic.internal ? "[I] " : "") + constraint_html(ic, names, next_id, m));
} }
if (!int_constraints.empty()) { if (!int_constraints.empty()) {
// eliminate duplicates // eliminate duplicates
@ -635,8 +636,6 @@ namespace seq {
out << ", color=darkred"; out << ", color=darkred";
else if (n->is_currently_conflict()) else if (n->is_currently_conflict())
out << ", color=red"; out << ", color=red";
else if (n->eval_idx() != m_run_idx) // inactive, not visited this run
out << ", color=blue";
out << "];\n"; out << "];\n";
} }
@ -669,8 +668,6 @@ namespace seq {
nielsen_edge* ep = const_cast<nielsen_edge*>(e); nielsen_edge* ep = const_cast<nielsen_edge*>(e);
if (sat_edges.contains(ep)) if (sat_edges.contains(ep))
out << ", color=green"; out << ", color=green";
else if (e->tgt()->eval_idx() != m_run_idx)
out << ", color=blue";
else if (e->tgt()->is_currently_conflict()) else if (e->tgt()->is_currently_conflict())
out << ", color=red"; out << ", color=red";

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

@ -210,11 +210,11 @@ namespace seq {
expr_ref stride_expr(a.mk_int(stride), m); expr_ref stride_expr(a.mk_int(stride), m);
expr_ref stride_k(a.mk_mul(stride_expr, k_var), m); expr_ref stride_k(a.mk_mul(stride_expr, k_var), m);
expr_ref rhs(a.mk_add(min_expr, stride_k), m); expr_ref rhs(a.mk_add(min_expr, stride_k), m);
out.push_back(constraint(m.mk_eq(len_str, rhs), mem.m_dep, m)); out.push_back(constraint(m.mk_eq(len_str, rhs), mem.m_dep, false, m));
// Constraint 2: k ≥ 0 // Constraint 2: k ≥ 0
expr_ref zero(a.mk_int(0), m); expr_ref zero(a.mk_int(0), m);
out.push_back(constraint(a.mk_ge(k_var, zero), mem.m_dep, m)); out.push_back(constraint(a.mk_ge(k_var, zero), mem.m_dep, false, m));
// Constraint 3 (optional): k ≤ max_k when max_len is bounded. // Constraint 3 (optional): k ≤ max_k when max_len is bounded.
// max_k = floor((max_len - min_len) / stride) // max_k = floor((max_len - min_len) / stride)
@ -226,7 +226,7 @@ namespace seq {
unsigned range = max_len - min_len; unsigned range = max_len - min_len;
unsigned max_k = range / stride; unsigned max_k = range / stride;
expr_ref max_k_expr(a.mk_int(max_k), m); expr_ref max_k_expr(a.mk_int(max_k), m);
out.push_back(constraint(a.mk_le(k_var, max_k_expr), mem.m_dep, m)); out.push_back(constraint(a.mk_le(k_var, max_k_expr), mem.m_dep, false, m));
} }
} }

33
src/smt/theory_nseq.cpp
View file

@ -225,7 +225,8 @@ namespace smt {
seq::dep_tracker dep = nullptr; seq::dep_tracker dep = nullptr;
ctx.push_trail(restore_vector(m_prop_queue)); ctx.push_trail(restore_vector(m_prop_queue));
m_prop_queue.push_back(eq_item(s1, s2, get_enode(v1), get_enode(v2), dep)); m_prop_queue.push_back(eq_item(s1, s2, get_enode(v1), get_enode(v2), dep));
++m_constraint_gen; m_last_constraint_added = ctx.get_scope_level();
m_can_hot_restart = false;
} }
catch(const std::exception&) { catch(const std::exception&) {
#ifdef Z3DEBUG #ifdef Z3DEBUG
@ -285,7 +286,8 @@ namespace smt {
if (is_true) { if (is_true) {
ctx.push_trail(restore_vector(m_prop_queue)); ctx.push_trail(restore_vector(m_prop_queue));
m_prop_queue.push_back(mem_item(sn_str, sn_re, lit, dep)); m_prop_queue.push_back(mem_item(sn_str, sn_re, lit, dep));
++m_constraint_gen; m_last_constraint_added = ctx.get_scope_level();
m_can_hot_restart = false;
} }
else { else {
// ¬(str ∈ R) ≡ str ∈ complement(R): store as a positive membership // ¬(str ∈ R) ≡ str ∈ complement(R): store as a positive membership
@ -295,7 +297,8 @@ namespace smt {
euf::snode* sn_re_compl = get_snode(re_compl.get()); euf::snode* sn_re_compl = get_snode(re_compl.get());
ctx.push_trail(restore_vector(m_prop_queue)); ctx.push_trail(restore_vector(m_prop_queue));
m_prop_queue.push_back(mem_item(sn_str, sn_re_compl, lit, dep)); m_prop_queue.push_back(mem_item(sn_str, sn_re_compl, lit, dep));
++m_constraint_gen; m_last_constraint_added = ctx.get_scope_level();
m_can_hot_restart = false;
} }
} }
else if (m_seq.str.is_prefix(e)) { else if (m_seq.str.is_prefix(e)) {
@ -371,7 +374,9 @@ namespace smt {
m_sgraph.pop(num_scopes); m_sgraph.pop(num_scopes);
// A pop may remove constraints and/or unassign forced Nielsen // A pop may remove constraints and/or unassign forced Nielsen
// literals; conservatively invalidate the cached SAT path. // literals; conservatively invalidate the cached SAT path.
++m_constraint_gen; if (m_can_hot_restart && ctx.get_scope_level() - num_scopes < m_last_constraint_added)
// we popped one of the constraints used to build the Nielsen graph
m_can_hot_restart = false;
} }
catch(const std::exception&) { catch(const std::exception&) {
#ifdef Z3DEBUG #ifdef Z3DEBUG
@ -584,6 +589,7 @@ namespace smt {
void theory_nseq::populate_nielsen_graph() { void theory_nseq::populate_nielsen_graph() {
m_nielsen.reset(); m_nielsen.reset();
m_can_hot_restart = true;
unsigned num_eqs = 0, num_mems = 0; unsigned num_eqs = 0, num_mems = 0;
@ -686,7 +692,7 @@ namespace smt {
// Fast path: if no new string eq/mem arrived and no scope was popped // Fast path: if no new string eq/mem arrived and no scope was popped
// since the last successful solve, the Nielsen graph can be (at least) // since the last successful solve, the Nielsen graph can be (at least)
// partially be reused // partially be reused
if (m_solved_gen == m_constraint_gen) { if (m_can_hot_restart) {
// SAT leaf are identical to what we would rebuild. All of the leaf's // SAT leaf are identical to what we would rebuild. All of the leaf's
// arithmetic side-constraints are already assigned true by the outer // arithmetic side-constraints are already assigned true by the outer
// solver, so the model is valid — skip the rebuild and re-solve. // solver, so the model is valid — skip the rebuild and re-solve.
@ -703,8 +709,6 @@ namespace smt {
// fall through - no reason to rebuild the Nielsen graph // fall through - no reason to rebuild the Nielsen graph
// everything that is not a general conflict needs to be recomputed // everything that is not a general conflict needs to be recomputed
// but we can keep the general conflicts (which can be a lot!) // but we can keep the general conflicts (which can be a lot!)
1 == 1;
0 == 0;
std::stack<seq::nielsen_node*> to_visit; std::stack<seq::nielsen_node*> to_visit;
to_visit.push(m_nielsen.root()); to_visit.push(m_nielsen.root());
while (!to_visit.empty()) { while (!to_visit.empty()) {
@ -726,6 +730,7 @@ namespace smt {
} }
} }
m_nielsen.clear_sat_node(); m_nielsen.clear_sat_node();
m_length_solver.reset();
} }
else { else {
// let's rebuild the whole Nielsen graph // let's rebuild the whole Nielsen graph
@ -739,7 +744,7 @@ namespace smt {
SASSERT(m_nielsen.root()); SASSERT(m_nielsen.root());
m_nielsen.assert_node_new_int_constraints(m_nielsen.root()); m_nielsen.assert_node_side_constraints(m_nielsen.root());
++m_num_final_checks; ++m_num_final_checks;
@ -789,10 +794,6 @@ namespace smt {
// std::cout << "Got: " << (result == seq::nielsen_graph::search_result::sat ? "sat" : (result == seq::nielsen_graph::search_result::unsat ? "unsat" : "unknown")) << std::endl; // std::cout << "Got: " << (result == seq::nielsen_graph::search_result::sat ? "sat" : (result == seq::nielsen_graph::search_result::unsat ? "unsat" : "unknown")) << std::endl;
#endif #endif
// Snapshot generation so the fast path can skip a full rebuild
// on the next call if no new constraints arrive in the meantime.
m_solved_gen = m_constraint_gen;
if (result == seq::nielsen_graph::search_result::unsat) { if (result == seq::nielsen_graph::search_result::unsat) {
IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve UNSAT\n";); IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve UNSAT\n";);
TRACE(seq, tout << "nseq final_check: solve UNSAT\n"); TRACE(seq, tout << "nseq final_check: solve UNSAT\n");
@ -850,7 +851,11 @@ namespace smt {
bool all_sat = true; bool all_sat = true;
ctx.push_trail(reset_vector(m_nielsen_literals)); ctx.push_trail(reset_vector(m_nielsen_literals));
for (auto const& c : m_nielsen.sat_node()->constraints()) { for (auto const& c : m_nielsen.sat_node()->constraints()) {
// std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl; if (c.internal) {
std::cout << "Skipping internall assumption: "<< mk_pp(c.fml, m) << std::endl;
continue;
}
std::cout << "Assumption: " << mk_pp(c.fml, m) << std::endl;
auto lit = mk_literal(c.fml); auto lit = mk_literal(c.fml);
m_nielsen_literals.push_back(lit); m_nielsen_literals.push_back(lit);
// Ensure Nielsen assumptions participate in SAT search instead of // Ensure Nielsen assumptions participate in SAT search instead of
@ -904,7 +909,7 @@ namespace smt {
set_conflict(eqs, lits); set_conflict(eqs, lits);
#ifdef Z3DEBUG #ifdef Z3DEBUG
#if 1 #if 0
// Pass constraints to a subsolver to check correctness modulo legacy solver // Pass constraints to a subsolver to check correctness modulo legacy solver
{ {
smt_params p; smt_params p;

4
src/smt/theory_nseq.h
View file

@ -73,8 +73,8 @@ namespace smt {
// Nielsen-relevant constraint set changes (new str eq/mem, or a pop). // Nielsen-relevant constraint set changes (new str eq/mem, or a pop).
// m_solved_gen is the generation at the last successful SAT solve; // m_solved_gen is the generation at the last successful SAT solve;
// when it still equals m_constraint_gen the cached sat path is reusable. // when it still equals m_constraint_gen the cached sat path is reusable.
unsigned m_constraint_gen = 0; unsigned m_last_constraint_added = 0;
unsigned m_solved_gen = UINT_MAX; bool m_can_hot_restart = false;
// statistics // statistics
unsigned m_num_conflicts = 0; unsigned m_num_conflicts = 0;

56
src/test/seq_nielsen.cpp
View file

@ -409,26 +409,6 @@ static void test_nielsen_expansion() {
ng.display(std::cout); ng.display(std::cout);
} }
// test run index management
static void test_run_idx() {
std::cout << "test_run_idx\n";
ast_manager m;
reg_decl_plugins(m);
euf::egraph eg(m);
euf::sgraph sg(m, eg);
dummy_simple_solver solver;
seq::context_solver_i context_solver;
seq::nielsen_graph ng(sg, solver, context_solver);
SASSERT(ng.run_idx() == 0);
ng.inc_run_idx();
SASSERT(ng.run_idx() == 1);
ng.inc_run_idx();
SASSERT(ng.run_idx() == 2);
}
// test multiple regex memberships // test multiple regex memberships
static void test_multiple_memberships() { static void test_multiple_memberships() {
std::cout << "test_multiple_memberships\n"; std::cout << "test_multiple_memberships\n";
@ -1661,36 +1641,6 @@ static void test_solve_children_failed_reason() {
SASSERT(result == seq::nielsen_graph::search_result::unsat); SASSERT(result == seq::nielsen_graph::search_result::unsat);
} }
// test that eval_idx is set during solve
static void test_solve_eval_idx_tracking() {
std::cout << "test_solve_eval_idx_tracking\n";
ast_manager m;
reg_decl_plugins(m);
euf::egraph eg(m);
euf::sgraph sg(m, eg);
dummy_simple_solver solver;
seq::context_solver_i context_solver;
seq::nielsen_graph ng(sg, solver, context_solver);
euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
euf::snode* a = sg.mk_char('A');
// x = A·x would be infinite without depth bound, but
// x = A is simple and satisfiable
ng.add_str_eq(x, a);
unsigned run_before = ng.run_idx();
auto result = ng.solve();
SASSERT(result == seq::nielsen_graph::search_result::sat);
// run_idx should have been incremented
SASSERT(ng.run_idx() > run_before);
// root's eval_idx should match current run_idx
seq::nielsen_node* root = ng.root();
SASSERT(root->eval_idx() == ng.run_idx());
}
// ----------------------------------------------------------------------- // -----------------------------------------------------------------------
// Direct simplify_and_init tests // Direct simplify_and_init tests
// ----------------------------------------------------------------------- // -----------------------------------------------------------------------
@ -3438,14 +3388,14 @@ static void add_len_ge(seq::nielsen_graph& ng, seq::nielsen_node* node, euf::sno
ast_manager& m = ng.get_manager(); ast_manager& m = ng.get_manager();
arith_util arith(m); arith_util arith(m);
expr_ref len(ng.seq().str.mk_length(var->get_expr()), m); expr_ref len(ng.seq().str.mk_length(var->get_expr()), m);
node->add_constraint(seq::constraint(arith.mk_ge(len, arith.mk_int(lb)), dep, m)); node->add_constraint(seq::constraint(arith.mk_ge(len, arith.mk_int(lb)), dep, false, m));
} }
static void add_len_le(seq::nielsen_graph& ng, seq::nielsen_node* node, euf::snode* var, unsigned ub, seq::dep_tracker dep) { static void add_len_le(seq::nielsen_graph& ng, seq::nielsen_node* node, euf::snode* var, unsigned ub, seq::dep_tracker dep) {
ast_manager& m = ng.get_manager(); ast_manager& m = ng.get_manager();
arith_util arith(m); arith_util arith(m);
expr_ref len(ng.seq().str.mk_length(var->get_expr()), m); expr_ref len(ng.seq().str.mk_length(var->get_expr()), m);
node->add_constraint(seq::constraint(arith.mk_le(len, arith.mk_int(ub)), dep, m)); node->add_constraint(seq::constraint(arith.mk_le(len, arith.mk_int(ub)), dep, false, m));
} }
static unsigned queried_lb(seq::nielsen_node* node, euf::snode* var) { static unsigned queried_lb(seq::nielsen_node* node, euf::snode* var) {
@ -3959,7 +3909,6 @@ void tst_seq_nielsen() {
test_nielsen_subst_apply(); test_nielsen_subst_apply();
test_nielsen_graph_reset(); test_nielsen_graph_reset();
test_nielsen_expansion(); test_nielsen_expansion();
test_run_idx();
test_multiple_memberships(); test_multiple_memberships();
test_backedge(); test_backedge();
test_eq_split_basic(); test_eq_split_basic();
@ -4004,7 +3953,6 @@ void tst_seq_nielsen() {
test_solve_node_extended_flag(); test_solve_node_extended_flag();
test_solve_mixed_eq_mem_sat(); test_solve_mixed_eq_mem_sat();
test_solve_children_failed_reason(); test_solve_children_failed_reason();
test_solve_eval_idx_tracking();
test_simplify_prefix_cancel(); test_simplify_prefix_cancel();
test_simplify_suffix_cancel_rtl(); test_simplify_suffix_cancel_rtl();
test_simplify_symbol_clash(); test_simplify_symbol_clash();