diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h index 6313d637e..c70eb18d9 100644 --- a/src/ast/euf/euf_snode.h +++ b/src/ast/euf/euf_snode.h @@ -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; } diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 279e066af..0819e5d88 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -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> 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; diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 237815cb6..cd53d4f2e 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -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 m_subst; - vector m_char_subst; // character-level substitutions (mirrors ZIPT's SubstC) vector 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 const& subst() const { return m_subst; } void add_subst(nielsen_subst const& s) { m_subst.push_back(s); } - vector 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 const& side_constraints() const { return m_side_constraints; } @@ -580,7 +577,7 @@ namespace seq { void add_constraint(constraint const &ic); vector const& constraints() const { return m_constraints; } - vector& constraints() { return m_constraints; } + vector& constraints() { return m_constraints; } // Query current bounds for a variable from the arithmetic subsolver. // Falls der Subsolver keinen Bound liefert, werden konservative Defaults diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 04e4327ab..4701e0619 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -618,12 +618,6 @@ namespace seq { << " → " // mapping arrow << snode_label_html(s.m_replacement, m); } - for (auto const& cs : e->char_substs()) { - if (!first) out << "
"; - first = false; - out << "?" << cs.m_var->id() - << " → ?" << cs.m_val->id(); - } // side constraints: integer equalities/inequalities for (auto const& ic : e->side_constraints()) { if (!first) out << "
"; diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 1be2587c9..7bbc63b66 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -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 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() << diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index cdfcd8698..7fa5ac06a 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -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; vector m_prop_queue; @@ -63,6 +64,7 @@ namespace smt { unsigned m_next_mem_id = 0; // monotone counter for tracked_str_mem ids obj_hashtable m_axiom_set; // dedup guard for axiom_item enqueues obj_hashtable 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;