mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 09:58:59 +00:00
Code Activity

fix insertions into subst.

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-03-25 09:00:37 -07:00
parent 46c76d89e0
commit 9d2244798d
4 changed files with 30 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1467,6 +1467,17 @@ namespace seq {
}
}
template<typename T> class scoped_push {
T &t;
public:
scoped_push(T& t) : t(t) {
t.push_scope();
}
~scoped_push() {
t.pop_scope(1);
}
};
nielsen_graph::search_result nielsen_graph::solve() {
SASSERT(m_root);
@ -1497,6 +1508,7 @@ namespace seq {
break;
inc_run_idx();
ptr_vector<nielsen_edge> cur_path;
// scoped_push _scoped_push(m_dep_mgr); // gc dependencies after search
search_result r = search_dfs(m_root, cur_path);
IF_VERBOSE(1, verbose_stream()
<< " depth_bound=" << m_depth_bound << " dfs_nodes=" << m_stats.m_num_dfs_nodes
@ -1517,9 +1529,8 @@ namespace seq {
return r;
}
if (r == search_result::unsat) {
++m_stats.m_num_unsat;
dep_tracker deps = m_dep_mgr.mk_empty();
collect_conflict_deps(deps);
++m_stats.m_num_unsat;
auto deps = collect_conflict_deps();
m_dep_mgr.linearize(deps, m_conflict_sources);
return r;
}
@ -1739,6 +1750,12 @@ namespace seq {
nielsen_node* child = mk_child(node);
nielsen_edge* e = mk_edge(node, child, true);
if (lt->is_char()) {
std::swap(lt, rt);
std::swap(l, r);
}
SASSERT(lt->is_unit());
euf::snode* lhs_rest = m_sg.drop_left(l, prefix + 1);
euf::snode* rhs_rest = m_sg.drop_left(r, prefix + 1);
@ -1746,12 +1763,14 @@ namespace seq {
eqs[eq_idx] = eqs.back();
eqs.pop_back();
nielsen_subst subst(lt, rt, eq.m_dep);
nielsen_subst subst(lt->arg(0), rt->arg(0), 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
@ -3608,7 +3627,8 @@ namespace seq {
return true;
}
void nielsen_graph::collect_conflict_deps(dep_tracker& deps) const {
dep_tracker nielsen_graph::collect_conflict_deps() const {
dep_tracker deps = nullptr;
for (nielsen_node const* n : m_nodes) {
if (n->eval_idx() != m_run_idx)
continue;
@ -3619,6 +3639,7 @@ namespace seq {
for (str_mem const& mem : n->str_mems())
deps = m_dep_mgr.mk_join(deps, mem.m_dep);
}
return deps;
}
@ -3626,8 +3647,7 @@ namespace seq {
void nielsen_graph::explain_conflict(svector<enode_pair>& eqs,
svector<sat::literal>& mem_literals) const {
SASSERT(m_root);
dep_tracker deps = m_dep_mgr.mk_empty();
collect_conflict_deps(deps);
auto deps = collect_conflict_deps();
vector<dep_source, false> vs;
m_dep_mgr.linearize(deps, vs);
for (dep_source const& d : vs) {

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

@ -246,15 +246,11 @@ Author:
#include <map>
#include "model/model.h"
namespace seq {
class seq_regex; // forward declaration (defined in smt/seq/seq_regex.h)
}
namespace smt {
class enode;
}
namespace seq {
// forward declarations
@ -262,6 +258,7 @@ namespace seq {
class nielsen_edge;
class nielsen_graph;
class seq_parikh;
class seq_regex; // forward declaration (defined in smt/seq/seq_regex.h)
std::string snode_label_html(euf::snode const* n, obj_map<expr, std::string>& names, uint64_t& next_id, ast_manager& m);
@ -426,6 +423,7 @@ 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
@ -855,7 +853,6 @@ namespace seq {
// path of edges from root to sat_node (set when sat_node is set)
ptr_vector<nielsen_edge> const& sat_path() const { return m_sat_path; }
// add constraints to the root node from external solver
void add_str_eq(euf::snode* lhs, euf::snode* rhs, smt::enode* l, smt::enode* r);
void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal l);
@ -960,7 +957,7 @@ namespace seq {
dep_manager const& dep_mgr() const { return m_dep_mgr; }
// collect dependency information from conflicting constraints
void collect_conflict_deps(dep_tracker& deps) const;
dep_tracker collect_conflict_deps() const;
search_result search_dfs(nielsen_node *node, ptr_vector<nielsen_edge>& path);

8
src/smt/theory_nseq.cpp
View file

@ -579,14 +579,6 @@ namespace smt {
// Conflict explanation
// -----------------------------------------------------------------------
void theory_nseq::add_conflict_clause(seq::dep_tracker const& deps) {
enode_pair_vector eqs;
literal_vector lits;
seq::deps_to_lits(deps, eqs, lits);
++m_num_conflicts;
set_conflict(eqs, lits);
}
void theory_nseq::explain_nielsen_conflict() {
enode_pair_vector eqs;
literal_vector lits;

1
src/smt/theory_nseq.h
View file

@ -113,7 +113,6 @@ namespace smt {
// private helpers
void populate_nielsen_graph();
void explain_nielsen_conflict();
void add_conflict_clause(seq::dep_tracker const& deps);
void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits);
euf::snode* get_snode(expr* e);