mirror of
https://github.com/Z3Prover/z3
synced 2026-03-20 03:53:10 +00:00
theory_nseq: dispatch assign_eh on all seq predicate cases via m_axioms, add enqueue/dequeue_axiom with variant prop_item (#9040)
* dispatch assign_eh cases via m_axioms: add prefix/suffix/contains true axioms Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * fix build: remove stale snode_label_html declaration from seq_nielsen.h Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * theory_nseq: add enqueue/dequeue_axiom + std::variant prop_item + relevant_eh Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Copilot
GitHub
parent
109ab7d098
commit
8795bf06fb
5 changed files with 179 additions and 49 deletions
|
|
@ -1274,6 +1274,40 @@ namespace seq {
|
|||
}
|
||||
|
||||
|
||||
// prefix(s, t) => t = s ++ prefix_inv(s, t)
|
||||
void axioms::prefix_true_axiom(expr* e) {
|
||||
expr* _s = nullptr, *_t = nullptr;
|
||||
VERIFY(seq.str.is_prefix(e, _s, _t));
|
||||
auto s = purify(_s);
|
||||
auto t = purify(_t);
|
||||
expr_ref inv = m_sk.mk_prefix_inv(s, t);
|
||||
expr_ref lit(e, m);
|
||||
add_clause(~lit, mk_seq_eq(t, mk_concat(s, inv)));
|
||||
}
|
||||
|
||||
// suffix(s, t) => t = suffix_inv(s, t) ++ s
|
||||
void axioms::suffix_true_axiom(expr* e) {
|
||||
expr* _s = nullptr, *_t = nullptr;
|
||||
VERIFY(seq.str.is_suffix(e, _s, _t));
|
||||
auto s = purify(_s);
|
||||
auto t = purify(_t);
|
||||
expr_ref inv = m_sk.mk_suffix_inv(s, t);
|
||||
expr_ref lit(e, m);
|
||||
add_clause(~lit, mk_seq_eq(t, mk_concat(inv, s)));
|
||||
}
|
||||
|
||||
// contains(t, s) => t = contains_left(t, s) ++ s ++ contains_right(t, s)
|
||||
void axioms::contains_true_axiom(expr* e) {
|
||||
expr* _t = nullptr, *_s = nullptr;
|
||||
VERIFY(seq.str.is_contains(e, _t, _s));
|
||||
auto t = purify(_t);
|
||||
auto s = purify(_s);
|
||||
expr_ref f1 = m_sk.mk_contains_left(t, s);
|
||||
expr_ref f2 = m_sk.mk_contains_right(t, s);
|
||||
expr_ref lit(e, m);
|
||||
add_clause(~lit, mk_seq_eq(t, mk_concat(f1, s, f2)));
|
||||
}
|
||||
|
||||
/**
|
||||
~contains(a, b) => ~prefix(b, a)
|
||||
~contains(a, b) => ~contains(tail(a), b)
|
||||
|
|
|
|||
|
|
@ -84,6 +84,9 @@ namespace seq {
|
|||
|
||||
void suffix_axiom(expr* n);
|
||||
void prefix_axiom(expr* n);
|
||||
void prefix_true_axiom(expr* n);
|
||||
void suffix_true_axiom(expr* n);
|
||||
void contains_true_axiom(expr* n);
|
||||
void extract_axiom(expr* n);
|
||||
void indexof_axiom(expr* n);
|
||||
void last_indexof_axiom(expr* n);
|
||||
|
|
|
|||
|
|
@ -515,8 +515,6 @@ namespace seq {
|
|||
}
|
||||
};
|
||||
|
||||
static std::string snode_label_html(euf::snode const* n, ast_manager& m);
|
||||
|
||||
// node in the Nielsen graph
|
||||
// mirrors ZIPT's NielsenNode
|
||||
class nielsen_node {
|
||||
|
|
|
|||
|
|
@ -172,7 +172,7 @@ namespace smt {
|
|||
unsigned idx = m_state.str_eqs().size();
|
||||
m_state.add_str_eq(s1, s2, get_enode(v1), get_enode(v2));
|
||||
ctx.push_trail(restore_vector(m_prop_queue));
|
||||
m_prop_queue.push_back({prop_item::eq_prop, idx});
|
||||
m_prop_queue.push_back(eq_item{idx});
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -196,39 +196,60 @@ namespace smt {
|
|||
|
||||
void theory_nseq::assign_eh(bool_var v, bool is_true) {
|
||||
expr* e = ctx.bool_var2expr(v);
|
||||
expr* s = nullptr;
|
||||
expr* re = nullptr;
|
||||
if (!m_seq.str.is_in_re(e, s, re)) {
|
||||
// Track unhandled boolean string predicates (prefixof, contains, etc.)
|
||||
if (is_app(e) && to_app(e)->get_family_id() == m_seq.get_family_id())
|
||||
push_unhandled_pred();
|
||||
return;
|
||||
expr* s = nullptr, *re = nullptr;
|
||||
TRACE(seq, tout << (is_true ? "" : "¬") << mk_bounded_pp(e, m, 3) << "\n";);
|
||||
if (m_seq.str.is_in_re(e, s, re)) {
|
||||
euf::snode* sn_str = get_snode(s);
|
||||
euf::snode* sn_re = get_snode(re);
|
||||
if (!sn_str || !sn_re)
|
||||
return;
|
||||
unsigned idx = m_state.str_mems().size();
|
||||
literal lit(v, !is_true);
|
||||
if (is_true) {
|
||||
m_state.add_str_mem(sn_str, sn_re, lit);
|
||||
}
|
||||
else {
|
||||
// ¬(str ∈ R) ≡ str ∈ complement(R): store as a positive membership
|
||||
// so the Nielsen graph sees it uniformly; the original negative literal
|
||||
// is kept in mem_source for conflict reporting.
|
||||
expr_ref re_compl(m_seq.re.mk_complement(re), m);
|
||||
euf::snode* sn_re_compl = get_snode(re_compl.get());
|
||||
m_state.add_str_mem(sn_str, sn_re_compl, lit);
|
||||
}
|
||||
ctx.push_trail(restore_vector(m_prop_queue));
|
||||
m_prop_queue.push_back(mem_item{idx});
|
||||
}
|
||||
euf::snode* sn_str = get_snode(s);
|
||||
euf::snode* sn_re = get_snode(re);
|
||||
if (!sn_str || !sn_re)
|
||||
return;
|
||||
|
||||
unsigned idx = m_state.str_mems().size();
|
||||
literal lit(v, !is_true);
|
||||
if (is_true) {
|
||||
m_state.add_str_mem(sn_str, sn_re, lit);
|
||||
else if (m_seq.str.is_prefix(e)) {
|
||||
if (is_true)
|
||||
m_axioms.prefix_true_axiom(e);
|
||||
else
|
||||
m_axioms.prefix_axiom(e);
|
||||
}
|
||||
else {
|
||||
// ¬(str ∈ R) ≡ str ∈ complement(R): store as a positive membership
|
||||
// so the Nielsen graph sees it uniformly; the original negative literal
|
||||
// is kept in mem_source for conflict reporting.
|
||||
expr_ref re_compl(m_seq.re.mk_complement(re), m);
|
||||
euf::snode* sn_re_compl = get_snode(re_compl.get());
|
||||
m_state.add_str_mem(sn_str, sn_re_compl, lit);
|
||||
else if (m_seq.str.is_suffix(e)) {
|
||||
if (is_true)
|
||||
m_axioms.suffix_true_axiom(e);
|
||||
else
|
||||
m_axioms.suffix_axiom(e);
|
||||
}
|
||||
ctx.push_trail(restore_vector(m_prop_queue));
|
||||
m_prop_queue.push_back({prop_item::pos_mem_prop, idx});
|
||||
|
||||
TRACE(seq, tout << "nseq assign_eh: " << (is_true ? "" : "¬")
|
||||
<< "str.in_re "
|
||||
<< mk_bounded_pp(s, m, 3) << " in "
|
||||
<< mk_bounded_pp(re, m, 3) << "\n";);
|
||||
else if (m_seq.str.is_contains(e)) {
|
||||
if (is_true)
|
||||
m_axioms.contains_true_axiom(e);
|
||||
else
|
||||
m_axioms.unroll_not_contains(e);
|
||||
}
|
||||
else if (m_seq.str.is_lt(e) || m_seq.str.is_le(e)) {
|
||||
// axioms added via relevant_eh → dequeue_axiom
|
||||
}
|
||||
else if (m_seq.is_skolem(e) ||
|
||||
m_seq.str.is_nth_i(e) ||
|
||||
m_seq.str.is_nth_u(e) ||
|
||||
m_seq.str.is_is_digit(e) ||
|
||||
m_seq.str.is_foldl(e) ||
|
||||
m_seq.str.is_foldli(e)) {
|
||||
// no-op: handled by other mechanisms
|
||||
}
|
||||
else if (is_app(e) && to_app(e)->get_family_id() == m_seq.get_family_id())
|
||||
push_unhandled_pred();
|
||||
}
|
||||
|
||||
// -----------------------------------------------------------------------
|
||||
|
|
@ -266,15 +287,13 @@ namespace smt {
|
|||
return;
|
||||
ctx.push_trail(value_trail(m_prop_qhead));
|
||||
while (m_prop_qhead < m_prop_queue.size() && !ctx.inconsistent()) {
|
||||
auto [k, idx] = m_prop_queue[m_prop_qhead++];
|
||||
switch (k) {
|
||||
case prop_item::eq_prop:
|
||||
propagate_eq(idx);
|
||||
break;
|
||||
case prop_item::pos_mem_prop:
|
||||
propagate_pos_mem(idx);
|
||||
break;
|
||||
}
|
||||
auto const& item = m_prop_queue[m_prop_qhead++];
|
||||
if (std::holds_alternative<eq_item>(item))
|
||||
propagate_eq(std::get<eq_item>(item).idx);
|
||||
else if (std::holds_alternative<mem_item>(item))
|
||||
propagate_pos_mem(std::get<mem_item>(item).idx);
|
||||
else if (std::holds_alternative<axiom_item>(item))
|
||||
dequeue_axiom(std::get<axiom_item>(item).e);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -324,6 +343,75 @@ namespace smt {
|
|||
ctx.internalize(len, false);
|
||||
}
|
||||
|
||||
// -----------------------------------------------------------------------
|
||||
// Axiom enqueue / dequeue (follows theory_seq::enque_axiom / deque_axiom)
|
||||
// -----------------------------------------------------------------------
|
||||
|
||||
void theory_nseq::enqueue_axiom(expr* e) {
|
||||
if (m_axiom_set.contains(e))
|
||||
return;
|
||||
m_axiom_set.insert(e);
|
||||
ctx.push_trail(insert_obj_trail<expr>(m_axiom_set, e));
|
||||
ctx.push_trail(restore_vector(m_prop_queue));
|
||||
m_prop_queue.push_back(axiom_item{e});
|
||||
}
|
||||
|
||||
void theory_nseq::dequeue_axiom(expr* n) {
|
||||
TRACE(seq, tout << "dequeue_axiom: " << mk_bounded_pp(n, m, 2) << "\n";);
|
||||
if (m_seq.str.is_length(n))
|
||||
m_axioms.length_axiom(n);
|
||||
else if (m_seq.str.is_index(n))
|
||||
m_axioms.indexof_axiom(n);
|
||||
else if (m_seq.str.is_last_index(n))
|
||||
m_axioms.last_indexof_axiom(n);
|
||||
else if (m_seq.str.is_replace(n))
|
||||
m_axioms.replace_axiom(n);
|
||||
else if (m_seq.str.is_replace_all(n))
|
||||
m_axioms.replace_all_axiom(n);
|
||||
else if (m_seq.str.is_extract(n))
|
||||
m_axioms.extract_axiom(n);
|
||||
else if (m_seq.str.is_at(n))
|
||||
m_axioms.at_axiom(n);
|
||||
else if (m_seq.str.is_nth_i(n))
|
||||
m_axioms.nth_axiom(n);
|
||||
else if (m_seq.str.is_itos(n))
|
||||
m_axioms.itos_axiom(n);
|
||||
else if (m_seq.str.is_stoi(n))
|
||||
m_axioms.stoi_axiom(n);
|
||||
else if (m_seq.str.is_lt(n))
|
||||
m_axioms.lt_axiom(n);
|
||||
else if (m_seq.str.is_le(n))
|
||||
m_axioms.le_axiom(n);
|
||||
else if (m_seq.str.is_unit(n))
|
||||
m_axioms.unit_axiom(n);
|
||||
else if (m_seq.str.is_is_digit(n))
|
||||
m_axioms.is_digit_axiom(n);
|
||||
else if (m_seq.str.is_from_code(n))
|
||||
m_axioms.str_from_code_axiom(n);
|
||||
else if (m_seq.str.is_to_code(n))
|
||||
m_axioms.str_to_code_axiom(n);
|
||||
}
|
||||
|
||||
void theory_nseq::relevant_eh(app* n) {
|
||||
if (m_seq.str.is_length(n) ||
|
||||
m_seq.str.is_index(n) ||
|
||||
m_seq.str.is_last_index(n) ||
|
||||
m_seq.str.is_replace(n) ||
|
||||
m_seq.str.is_replace_all(n)||
|
||||
m_seq.str.is_extract(n) ||
|
||||
m_seq.str.is_at(n) ||
|
||||
m_seq.str.is_nth_i(n) ||
|
||||
m_seq.str.is_itos(n) ||
|
||||
m_seq.str.is_stoi(n) ||
|
||||
m_seq.str.is_lt(n) ||
|
||||
m_seq.str.is_le(n) ||
|
||||
m_seq.str.is_unit(n) ||
|
||||
m_seq.str.is_is_digit(n) ||
|
||||
m_seq.str.is_from_code(n) ||
|
||||
m_seq.str.is_to_code(n))
|
||||
enqueue_axiom(n);
|
||||
}
|
||||
|
||||
// -----------------------------------------------------------------------
|
||||
// Final check: build Nielsen graph and search
|
||||
// -----------------------------------------------------------------------
|
||||
|
|
|
|||
|
|
@ -19,6 +19,7 @@ Author:
|
|||
--*/
|
||||
#pragma once
|
||||
|
||||
#include <variant>
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
#include "ast/rewriter/seq_rewriter.h"
|
||||
#include "ast/rewriter/seq_axioms.h"
|
||||
|
|
@ -51,13 +52,16 @@ namespace smt {
|
|||
seq::seq_regex m_regex; // regex membership pre-processing
|
||||
seq_model m_model; // model construction helper
|
||||
|
||||
// propagation queue
|
||||
struct prop_item {
|
||||
enum kind_t { eq_prop, pos_mem_prop } m_kind;
|
||||
unsigned m_idx;
|
||||
};
|
||||
svector<prop_item> m_prop_queue;
|
||||
unsigned m_prop_qhead = 0;
|
||||
// propagation queue items (variant over the distinct propagation cases)
|
||||
struct eq_item { unsigned idx; }; // string equality at index idx in str_eqs
|
||||
struct mem_item { unsigned idx; }; // regex membership at index idx in str_mems
|
||||
struct axiom_item { expr* e; }; // structural axiom for term e
|
||||
|
||||
using prop_item = std::variant<eq_item, mem_item, axiom_item>;
|
||||
|
||||
vector<prop_item> m_prop_queue;
|
||||
unsigned m_prop_qhead = 0;
|
||||
obj_hashtable<expr> m_axiom_set; // dedup guard for axiom_item enqueues
|
||||
|
||||
// statistics
|
||||
unsigned m_num_conflicts = 0;
|
||||
|
|
@ -92,6 +96,7 @@ namespace smt {
|
|||
void propagate() override;
|
||||
void init() override;
|
||||
void assign_eh(bool_var v, bool is_true) override;
|
||||
void relevant_eh(app* n) override;
|
||||
final_check_status final_check_eh(unsigned) override;
|
||||
void push_scope_eh() override;
|
||||
void pop_scope_eh(unsigned num_scopes) override;
|
||||
|
|
@ -114,6 +119,8 @@ namespace smt {
|
|||
// propagation dispatch helpers
|
||||
void propagate_eq(unsigned idx);
|
||||
void propagate_pos_mem(unsigned idx);
|
||||
void enqueue_axiom(expr* e);
|
||||
void dequeue_axiom(expr* e);
|
||||
void ensure_length_var(expr* e);
|
||||
|
||||
// higher-order term unfolding
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue