From 2b7204b07c5447a5f5fa9b2af5b865e3fadbcd22 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Fri, 10 Apr 2026 17:59:16 +0200 Subject: [PATCH] Does model construction work properly now? --- src/smt/seq/seq_nielsen.cpp | 8 +- src/smt/seq_model.cpp | 199 +++++++++++++++++++++++++++++++++--- src/smt/seq_model.h | 16 ++- src/smt/theory_nseq.cpp | 3 +- 4 files changed, 204 insertions(+), 22 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 7ae8c5793..ef26b120b 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -4155,15 +4155,11 @@ nielsen_graph::generate_length_constraints(vector& constraint // 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(); - for (nielsen_edge* e : m_sat_path) { - for (auto const& ic : e->side_constraints()) { + if (m_sat_node) { + for (auto const& ic : m_sat_node->constraints()) { m_solver.assert_expr(ic.fml); } } - 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) { diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp index ac3529d53..609772ded 100644 --- a/src/smt/seq_model.cpp +++ b/src/smt/seq_model.cpp @@ -24,9 +24,107 @@ Author: namespace smt { - seq_model::seq_model(ast_manager& m, seq_util& seq, + static void collect_expr_dependencies(context& ctx, expr* e, obj_hashtable& seen, ptr_vector& deps) { + if (!e) + return; + ptr_vector todo; + obj_hashtable seen_expr; + todo.push_back(e); + while (!todo.empty()) { + expr* cur = todo.back(); + todo.pop_back(); + if (seen_expr.contains(cur)) + continue; + seen_expr.insert(cur); + + if (ctx.e_internalized(cur)) { + enode* dep = ctx.get_enode(cur)->get_root(); + if (!seen.contains(dep)) { + seen.insert(dep); + deps.push_back(dep); + } + } + + if (!is_app(cur)) + continue; + for (expr* arg : *to_app(cur)) + todo.push_back(arg); + } + } + + static expr_ref substitute_dependency_values(ast_manager& m, context& ctx, expr* e, obj_map const& dep_values) { + if (!e) + return expr_ref(m); + + expr* cur = e; + if (ctx.e_internalized(e)) { + expr* dval = nullptr; + enode* dep = ctx.get_enode(e)->get_root(); + if (dep_values.find(dep, dval) && dval) { + if (m.is_value(dval)) + return expr_ref(dval, m); + cur = dval; + } + } + + if (!is_app(cur)) + return expr_ref(cur, m); + + app* a = to_app(cur); + expr_ref_vector args(m); + bool changed = false; + for (expr* arg : *a) { + expr_ref new_arg = substitute_dependency_values(m, ctx, arg, dep_values); + changed = changed || (new_arg != arg); + args.push_back(new_arg); + } + if (!changed) + return expr_ref(cur, m); + return expr_ref(m.mk_app(a->get_decl(), args.size(), args.data()), m); + } + + class seq_snode_value_proc : public model_value_proc { + seq_model& m_owner; + enode* m_node; + euf::snode* m_snode; + ptr_vector m_dependencies; + + public: + seq_snode_value_proc(seq_model& owner, enode* node, euf::snode* snode) + : m_owner(owner), m_node(node), m_snode(snode) { + obj_hashtable seen; + if (m_node) + seen.insert(m_node->get_root()); + m_owner.collect_dependencies(m_snode, seen, m_dependencies); + } + + void get_dependencies(buffer& result) override { + for (enode* d : m_dependencies) + result.push_back(model_value_dependency(d)); + } + + app* mk_value(model_generator& mg, expr_ref_vector const& values) override { + SASSERT(values.size() == m_dependencies.size()); + obj_map dep_values; + for (unsigned i = 0; i < m_dependencies.size(); ++i) + dep_values.insert(m_dependencies[i]->get_root(), values[i]); + + expr_ref val = m_owner.snode_to_value(m_snode, mg, &dep_values); + if (!val) + val = m_owner.snode_to_value(m_snode, mg); + if (!val) + val = m_owner.m_seq.str.mk_empty(m_node->get_expr()->get_sort()); + + m_owner.m_trail.push_back(val); + m_owner.m_factory->add_trail(val); + TRACE(seq, tout << "nseq seq_snode_value_proc: " << mk_pp(m_node->get_expr(), m_owner.m) << " -> " << mk_pp(val, m_owner.m) << "\n";); + return to_app(val); + } + }; + + seq_model::seq_model(ast_manager& m, context& ctx, seq_util& seq, seq_rewriter& rw, euf::sgraph& sg) - : m(m), m_seq(seq), m_rewriter(rw), m_sg(sg), m_trail(m) + : m(m), m_ctx(ctx), m_seq(seq), m_rewriter(rw), m_sg(sg), m_trail(m) {} void seq_model::init(model_generator& mg, seq::nielsen_graph& nielsen) { @@ -48,7 +146,7 @@ namespace smt { // solve integer constraints from the sat_path FIRST so that // m_int_model is available when snode_to_value evaluates power exponents - VERIFY(nielsen.solve_sat_path_raw(m_int_model)); + // VERIFY(nielsen.solve_sat_path_raw(m_int_model)); // extract variable assignments from the satisfying leaf's substitution path extract_assignments(nielsen.sat_path()); @@ -88,7 +186,7 @@ namespace smt { }); expr_ref val(m); if (sn) - val = snode_to_value(sn); + return alloc(seq_snode_value_proc, *this, n, sn); if (!val) { // no assignment found — default to empty string @@ -143,7 +241,7 @@ namespace smt { unsigned id = b.first->first()->id(); if (m_var_values.contains(id)) continue; - expr_ref val = snode_to_value(b.second); + expr_ref val = snode_to_value(b.second, *m_mg); IF_VERBOSE(1, { verbose_stream() << " var snode[" << id << "]"; if (b.first->get_expr()) verbose_stream() << "=" << mk_bounded_pp(b.first->get_expr(), m, 2); @@ -158,7 +256,11 @@ namespace smt { } } - expr_ref seq_model::snode_to_value(euf::snode* n) { + expr_ref seq_model::snode_to_value(euf::snode* n, model_generator& mg) { + return snode_to_value(n, mg, nullptr); + } + + expr_ref seq_model::snode_to_value(euf::snode* n, model_generator& mg, obj_map const* dep_values) { if (!n) return expr_ref(m); @@ -173,14 +275,38 @@ namespace smt { expr* e = n->get_expr(); SASSERT(m_seq.str.is_unit(e)); e = to_app(e)->get_arg(0); + + unsigned c; + if (dep_values && e && m_ctx.e_internalized(e)) { + expr* dval = nullptr; + enode* dep = m_ctx.get_enode(e)->get_root(); + if (dep_values->find(dep, dval) && dval && m_seq.is_const_char(dval, c)) + return expr_ref(m_seq.str.mk_string(zstring(c)), m); + } + + if (dep_values && e && m_mg) { + expr_ref e_sub = substitute_dependency_values(m, m_ctx, e, *dep_values); + expr_ref val_sub(m); + if (m_mg->get_model().eval(e_sub, val_sub, true) && val_sub && m_seq.is_const_char(val_sub, c)) + return expr_ref(m_seq.str.mk_string(zstring(c)), m); + } + expr_ref val(m); - if (e && m_int_model) { - unsigned c; - m_int_model->eval_expr(e, val, true); + if (e && m_mg && m_mg->get_model().eval(e, val, true)) { if (val && m_seq.is_const_char(val, c)) return expr_ref(m_seq.str.mk_string(zstring(c)), m); } - return e ? expr_ref(e, m) : expr_ref(m); + + if (e && m_seq.is_char(e)) { + return expr_ref(m_seq.str.mk_string("0"), m); + } + + if (m_mg && e) { + expr* some = m_mg->get_model().get_some_value(e->get_sort()); + if (some) + return expr_ref(m_seq.str.mk_unit(some), m); + } + return expr_ref(m_seq.str.mk_unit(e), m); } if (n->is_var()) @@ -188,8 +314,8 @@ namespace smt { if (n->is_concat()) { SASSERT(n->get_sort() && m_seq.is_seq(n->get_sort())); - expr_ref lhs = snode_to_value(n->arg(0)); - expr_ref rhs = snode_to_value(n->arg(1)); + expr_ref lhs = snode_to_value(n->arg(0), mg, dep_values); + expr_ref rhs = snode_to_value(n->arg(1), mg, dep_values); if (lhs && rhs) return expr_ref(m_seq.str.mk_concat(lhs, rhs), m); if (lhs) @@ -204,7 +330,7 @@ namespace smt { // Evaluate the base and exponent to produce a concrete string. // The base is a string snode; the exponent is an integer expression // whose value comes from the sat_path integer model. - expr_ref base_val = snode_to_value(n->arg(0)); + expr_ref base_val = snode_to_value(n->arg(0), mg, dep_values); if (!base_val) return expr_ref(m); @@ -219,6 +345,21 @@ namespace smt { if (exp_expr && arith.is_numeral(exp_expr, exp_val)) { // already concrete } + else if (dep_values && exp_expr && m_ctx.e_internalized(exp_expr)) { + expr* dval = nullptr; + enode* dep = m_ctx.get_enode(exp_expr)->get_root(); + if (dep_values->find(dep, dval) && dval && arith.is_numeral(dval, exp_val)) { + // evaluated from dependency values + } + else if (m_mg) { + expr_ref sub_exp = substitute_dependency_values(m, m_ctx, exp_expr, *dep_values); + expr_ref result(m); + if (!(m_mg->get_model().eval(sub_exp, result, true) && arith.is_numeral(result, exp_val))) + exp_val = rational(0); + } + 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)) { @@ -277,6 +418,38 @@ namespace smt { return e ? expr_ref(e, m) : expr_ref(m); } + void seq_model::collect_dependencies(euf::snode* n, obj_hashtable& seen, ptr_vector& deps) const { + if (!n) + return; + + if (n->is_char() || n->is_unit()) { + expr* e = n->get_expr(); + if (e && m_seq.str.is_unit(e)) { + expr* ch = to_app(e)->get_arg(0); + collect_expr_dependencies(m_ctx, ch, seen, deps); + } + return; + } + + if (n->is_concat()) { + collect_dependencies(n->arg(0), seen, deps); + collect_dependencies(n->arg(1), seen, deps); + return; + } + + if (n->is_power()) { + collect_dependencies(n->arg(0), seen, deps); + if (n->num_args() == 2) { + euf::snode* exp_snode = n->arg(1); + expr* exp_expr = exp_snode ? exp_snode->get_expr() : nullptr; + rational exp_val; + arith_util arith(m); + if (exp_expr && !arith.is_numeral(exp_expr, exp_val)) + collect_expr_dependencies(m_ctx, exp_expr, seen, deps); + } + } + } + void seq_model::register_existing_values(seq::nielsen_graph& nielsen) { seq::nielsen_node const* root = nielsen.root(); if (!root) diff --git a/src/smt/seq_model.h b/src/smt/seq_model.h index d047b7fac..e9328fb97 100644 --- a/src/smt/seq_model.h +++ b/src/smt/seq_model.h @@ -28,6 +28,7 @@ Author: --*/ #pragma once +#include "smt_context.h" #include "ast/seq_decl_plugin.h" #include "ast/rewriter/seq_rewriter.h" #include "ast/euf/euf_sgraph.h" @@ -43,9 +44,13 @@ namespace smt { class model_generator; struct tracked_str_mem; class model_value_proc; + class seq_snode_value_proc; class seq_model { + friend class seq_snode_value_proc; + ast_manager& m; + context& m_ctx; seq_util& m_seq; seq_rewriter& m_rewriter; euf::sgraph& m_sg; @@ -69,7 +74,7 @@ namespace smt { u_map m_var_regex; public: - seq_model(ast_manager& m, seq_util& seq, + seq_model(ast_manager& m, context& ctx, seq_util& seq, seq_rewriter& rw, euf::sgraph& sg); // Phase 1: initialize model construction. @@ -97,7 +102,14 @@ namespace smt { // recursively substitute known variable assignments into an snode tree. // Returns a concrete Z3 expression. - expr_ref snode_to_value(euf::snode* n); + expr_ref snode_to_value(euf::snode* n, model_generator& mg); + + // Same as above, but optionally uses pre-evaluated model values for + // enode dependencies (provided by model_generator). + expr_ref snode_to_value(euf::snode* n, model_generator& mg, obj_map const* dep_values); + + // Collect enode dependencies required to evaluate an snode value. + void collect_dependencies(euf::snode* n, obj_hashtable& seen, ptr_vector& deps) const; // register all string literals appearing in the constraint store // with the factory to avoid collisions with fresh values. diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 0ad11f3f1..b80c0bf97 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -38,7 +38,7 @@ namespace smt { m_nielsen(m_sgraph, m_context_solver, m_core_solver), m_axioms(m_th_rewriter), m_regex(m_sgraph), - m_model(m, m_seq, m_rewriter, m_sgraph), + m_model(m, ctx, m_seq, m_rewriter, m_sgraph), m_relevant_lengths(m) { std::function add_clause = @@ -733,6 +733,7 @@ namespace smt { 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; switch (ctx.get_assignment(lit)) { case l_true: break;