mirror of
https://github.com/Z3Prover/z3
synced 2026-07-12 01:56:22 +00:00
Better caching/hashing
First try for reintroducting subsumption
This commit is contained in:
CEisenhofer
parent
cc42304f60
commit
6f1eafaa5c
9 changed files with 486 additions and 351 deletions
|
|
@ -123,6 +123,36 @@ namespace euf {
|
|||
return arg(0);
|
||||
}
|
||||
|
||||
// equal modulo slicing
|
||||
bool similar(const snode* str, ast_manager& m) const {
|
||||
if (m_length != str->m_length)
|
||||
return false;
|
||||
auto it1 = begin();
|
||||
auto it2 = str->begin();
|
||||
for (; it1 != end() && it2 != str->end(); it1++, it2++) {
|
||||
if ((*it1)->kind() != (*it2)->kind())
|
||||
return false;
|
||||
if ((*it1)->is_var()) {
|
||||
expr* e1 = (*it1)->get_expr();
|
||||
expr* e2 = (*it2)->get_expr();
|
||||
th_rewriter th(m);
|
||||
seq::skolem sk(m, th);
|
||||
while (sk.is_slice(e1)) {
|
||||
e1 = to_app(e1)->get_arg(0);
|
||||
}
|
||||
while (sk.is_slice(e2)) {
|
||||
e2 = to_app(e2)->get_arg(0);
|
||||
}
|
||||
if (e1 != e2)
|
||||
return false;
|
||||
continue;
|
||||
}
|
||||
if (*it1 != *it2)
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
// Iterator over the leaf tokens of this snode, modulo concatenation
|
||||
// (analogous to first()/last()/at()): an s_concat tree is flattened to
|
||||
// its leaf tokens in left-to-right order, empty nodes are skipped, and
|
||||
|
|
|
|||
|
|
@ -363,12 +363,11 @@ namespace seq {
|
|||
SASSERT(m_constraints.size() == parent.m_constraints.size());
|
||||
}
|
||||
|
||||
void nielsen_node::add_str_eq(str_eq& eq) {
|
||||
void nielsen_node::add_str_eq(const str_eq& eq) {
|
||||
SASSERT(eq.m_lhs != nullptr);
|
||||
SASSERT(eq.m_rhs != nullptr);
|
||||
if (eq.is_trivial())
|
||||
return;
|
||||
eq.sort();
|
||||
// check if root node contains this equation already
|
||||
if (std::ranges::any_of(str_eqs(),
|
||||
[&](const str_eq &e) { return e.m_lhs == eq.m_lhs && e.m_rhs == eq.m_rhs; }))
|
||||
|
|
@ -377,10 +376,9 @@ namespace seq {
|
|||
m_str_eq.push_back(eq);
|
||||
}
|
||||
|
||||
void nielsen_node::add_str_deq(str_deq& deq) {
|
||||
void nielsen_node::add_str_deq(const str_deq& deq) {
|
||||
SASSERT(deq.m_lhs != nullptr);
|
||||
SASSERT(deq.m_rhs != nullptr);
|
||||
deq.sort();
|
||||
// check if root node contains this equation already
|
||||
if (std::ranges::any_of(str_deqs(),
|
||||
[&](const str_deq &e) { return e.m_lhs == deq.m_lhs && e.m_rhs == deq.m_rhs; }))
|
||||
|
|
@ -507,6 +505,59 @@ namespace seq {
|
|||
}
|
||||
}
|
||||
|
||||
unsigned nielsen_node::canonize_and_compute_node_hash() {
|
||||
unsigned hash = 457260179;
|
||||
std::sort(str_eqs().begin(), str_eqs().end());
|
||||
for (auto const& e : str_eqs()) {
|
||||
hash += 433867097 * e.hash();
|
||||
}
|
||||
std::sort(str_deqs().begin(), str_deqs().end());
|
||||
for (auto const& e : str_deqs()) {
|
||||
hash += 982048589 * e.hash();
|
||||
}
|
||||
std::sort(str_mems().begin(), str_mems().end());
|
||||
for (auto const& e : str_mems()) {
|
||||
hash += 736051237 * e.hash();
|
||||
}
|
||||
|
||||
for (auto const& [uid, cr] : char_ranges()) {
|
||||
// not sorted; computation needs to be commutative
|
||||
for (auto const& rg : cr.first.ranges()) {
|
||||
hash += 473672767 * (750753749 * rg.m_lo + rg.m_hi) + uid;
|
||||
}
|
||||
}
|
||||
return hash;
|
||||
}
|
||||
|
||||
bool nielsen_node::is_node_sibling(nielsen_node const* n) {
|
||||
if (n->str_eqs().size() != str_eqs().size())
|
||||
return false;
|
||||
if (n->str_deqs().size() != str_deqs().size())
|
||||
return false;
|
||||
if (n->str_mems().size() != str_mems().size())
|
||||
return false;
|
||||
if (n->char_ranges().size() != char_ranges().size())
|
||||
return false;
|
||||
for (unsigned i = 0; i < str_eqs().size(); i++) {
|
||||
if (str_eqs()[i] != n->str_eqs()[i])
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < str_deqs().size(); i++) {
|
||||
if (str_deqs()[i] != n->str_deqs()[i])
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < str_mems().size(); i++) {
|
||||
if (str_mems()[i] != n->str_mems()[i])
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < char_ranges().size(); i++) {
|
||||
// TODO: Check once more
|
||||
if (char_ranges()[i] != n->char_ranges()[i])
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
void nielsen_node::add_char_range(euf::snode const* sym_char, char_set const& range, dep_tracker dep) {
|
||||
if (sym_char->is_char()) {
|
||||
// for a concrete character just check if it matches
|
||||
|
|
@ -558,8 +609,8 @@ namespace seq {
|
|||
// -----------------------------------------------
|
||||
|
||||
nielsen_graph::nielsen_graph(euf::sgraph &sg, sub_solver_i &solver, context_solver_i &ctx_solver) :
|
||||
m(sg.get_manager()), a(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_rw(m), m_sk(m, m_rw),
|
||||
m_length_solver(solver), m_context_solver(ctx_solver), m_parikh(alloc(seq_parikh, sg)),
|
||||
m(sg.get_manager()), a(sg.get_manager()), m_seq(sg.get_seq_util()), m_sg(sg), m_rw(m), m_a_rw(m),
|
||||
m_sk(m, m_rw), m_length_solver(solver), m_context_solver(ctx_solver), m_parikh(alloc(seq_parikh, sg)),
|
||||
m_seq_regex(alloc(seq::seq_regex, sg)), m_partial_dfa_pin(sg.get_manager()) {
|
||||
}
|
||||
|
||||
|
|
@ -619,38 +670,37 @@ namespace seq {
|
|||
|
||||
void nielsen_graph::add_str_eq(euf::snode const* lhs, euf::snode const* rhs, smt::enode *l, smt::enode *r) const {
|
||||
const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r));
|
||||
str_eq eq(lhs, rhs, dep);
|
||||
str_eq eq(m, lhs, rhs, dep);
|
||||
m_root->add_str_eq(eq);
|
||||
}
|
||||
|
||||
void nielsen_graph::add_str_deq(euf::snode const* lhs, euf::snode const* rhs, sat::literal l) const {
|
||||
const dep_tracker dep = m_dep_mgr.mk_leaf(l);
|
||||
str_deq deq(lhs, rhs, dep);
|
||||
str_deq deq(m, lhs, rhs, dep);
|
||||
m_root->add_str_deq(deq);
|
||||
}
|
||||
|
||||
void nielsen_graph::add_str_mem(euf::snode const* str, euf::snode const* regex, sat::literal l) const {
|
||||
const dep_tracker dep = m_dep_mgr.mk_leaf(l);
|
||||
m_root->add_str_mem(str_mem(str, regex, dep));
|
||||
m_root->add_str_mem(str_mem(m, str, regex, dep));
|
||||
}
|
||||
|
||||
// test-friendly overloads (no external dependency tracking)
|
||||
void nielsen_graph::add_str_eq(euf::snode const* lhs, euf::snode const* rhs) const {
|
||||
const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr));
|
||||
str_eq eq(lhs, rhs, dep);
|
||||
eq.sort();
|
||||
const str_eq eq(m, lhs, rhs, dep);
|
||||
m_root->add_str_eq(eq);
|
||||
}
|
||||
|
||||
void nielsen_graph::add_str_deq(euf::snode const* lhs, euf::snode const* rhs) const {
|
||||
const dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(nullptr, nullptr));
|
||||
str_deq deq(lhs, rhs, dep);
|
||||
const str_deq deq(m, lhs, rhs, dep);
|
||||
m_root->add_str_deq(deq);
|
||||
}
|
||||
|
||||
void nielsen_graph::add_str_mem(euf::snode const* str, euf::snode const* regex) const {
|
||||
const dep_tracker dep = nullptr;
|
||||
str_mem mem(str, regex, dep);
|
||||
const str_mem mem(m, str, regex, dep);
|
||||
m_root->add_str_mem(mem);
|
||||
}
|
||||
|
||||
|
|
@ -678,6 +728,7 @@ namespace seq {
|
|||
m_projection_extract_idx = 0;
|
||||
m_explored_automaton.reset();
|
||||
m_unsat_node_cache.clear();
|
||||
m_siblings.clear();
|
||||
m_num_cache_hits = 0;
|
||||
m_eager_active = false;
|
||||
m_eager_leaf = nullptr;
|
||||
|
|
@ -1616,7 +1667,7 @@ namespace seq {
|
|||
euf::snode const* deriv = fwd
|
||||
? sg.brzozowski_deriv(mem.m_regex, tok)
|
||||
: reverse_brzozowski_deriv(sg, mem.m_regex, tok);
|
||||
TRACE(seq, tout << mem_pp(mem, m) << " d: " << spp(deriv, m) << "\n");
|
||||
TRACE(seq, tout << mem_pp(mem) << " d: " << spp(deriv, m) << "\n");
|
||||
if (!deriv)
|
||||
break;
|
||||
if (deriv->is_fail()) {
|
||||
|
|
@ -1721,7 +1772,7 @@ namespace seq {
|
|||
// check for regex memberships that are immediately infeasible
|
||||
for (str_mem& mem : m_str_mem) {
|
||||
if (mem.is_contradiction(this)) {
|
||||
TRACE(seq, tout << "contradiction " << mem_pp(mem, m) << "\n");
|
||||
TRACE(seq, tout << "contradiction " << mem_pp(mem) << "\n");
|
||||
set_general_conflict();
|
||||
set_conflict(backtrack_reason::regex, mem.m_dep);
|
||||
return simplify_result::conflict;
|
||||
|
|
@ -1949,6 +2000,9 @@ namespace seq {
|
|||
if (m_max_search_depth > 0 && m_depth_bound > m_max_search_depth)
|
||||
break;
|
||||
ptr_vector<nielsen_edge> cur_path;
|
||||
// The active-path index is per-traversal; clear it so a sat-aborted
|
||||
// previous iteration cannot leave stale ancestors behind.
|
||||
m_siblings.clear();
|
||||
// scoped_push _scoped_push(m_dep_mgr); // gc dependencies after search
|
||||
SASSERT(!m_root->is_currently_conflict());
|
||||
const search_result r = search_dfs(m_root, cur_path); // the main search loop
|
||||
|
|
@ -2014,7 +2068,7 @@ namespace seq {
|
|||
dep_tracker dep = m_dep_mgr.mk_leaf(enode_pair(l, r));
|
||||
lhs = eager_rewrite(lhs, dep);
|
||||
rhs = eager_rewrite(rhs, dep);
|
||||
str_eq eq(lhs, rhs, dep);
|
||||
str_eq eq(m, lhs, rhs, dep);
|
||||
eq.sort();
|
||||
m_eager_leaf->add_str_eq(eq);
|
||||
}
|
||||
|
|
@ -2024,7 +2078,7 @@ namespace seq {
|
|||
dep_tracker dep = m_dep_mgr.mk_leaf(lit);
|
||||
lhs = eager_rewrite(lhs, dep);
|
||||
rhs = eager_rewrite(rhs, dep);
|
||||
str_deq deq(lhs, rhs, dep);
|
||||
str_deq deq(m, lhs, rhs, dep);
|
||||
m_eager_leaf->add_str_deq(deq);
|
||||
}
|
||||
|
||||
|
|
@ -2033,7 +2087,7 @@ namespace seq {
|
|||
dep_tracker dep = m_dep_mgr.mk_leaf(lit);
|
||||
str = eager_rewrite(str, dep);
|
||||
regex = eager_rewrite(regex, dep);
|
||||
m_eager_leaf->add_str_mem(str_mem(str, regex, dep));
|
||||
m_eager_leaf->add_str_mem(str_mem(m, str, regex, dep));
|
||||
}
|
||||
|
||||
// Drive the deterministic chain from the current leaf to a fixpoint. Each step
|
||||
|
|
@ -2044,7 +2098,7 @@ namespace seq {
|
|||
nielsen_graph::search_result nielsen_graph::eager_close() {
|
||||
SASSERT(m_eager_active && m_eager_leaf);
|
||||
++m_stats.m_num_eager_calls;
|
||||
ptr_vector<nielsen_edge> empty_path;
|
||||
const ptr_vector<nielsen_edge> empty_path;
|
||||
|
||||
// Rigid defined ops (str.replace_all, …) must never be Nielsen-substituted;
|
||||
// a rigid term is inherited down the whole chain, so a single check on the
|
||||
|
|
@ -2111,6 +2165,12 @@ namespace seq {
|
|||
case backtrack_reason::regex_widening:
|
||||
case backtrack_reason::symbol_clash:
|
||||
case backtrack_reason::character_range:
|
||||
// a sibling (subsumption / loop-cut) conflict depends only on the node's
|
||||
// string signature: a cut equates two nodes by their string constraints,
|
||||
// and a sibling closure is reached only when every leaf below is itself a
|
||||
// string-only conflict or a cut. (Whether the closure is *cacheable* is a
|
||||
// separate, stronger question handled via the lowlink in search_dfs.)
|
||||
case backtrack_reason::sibling:
|
||||
return true;
|
||||
default:
|
||||
// arithmetic, parikh_image, external, children_failed, unevaluated
|
||||
|
|
@ -2124,71 +2184,6 @@ namespace seq {
|
|||
return reason_is_string_only(n->m_reason);
|
||||
}
|
||||
|
||||
std::vector<unsigned> nielsen_graph::compute_node_signature(nielsen_node const* n) {
|
||||
std::vector<unsigned> sig;
|
||||
// string equalities (order-independent)
|
||||
{
|
||||
std::vector<std::pair<unsigned,unsigned>> v;
|
||||
for (auto const& e : n->str_eqs()) {
|
||||
v.emplace_back(e.m_lhs->id(), e.m_rhs->id());
|
||||
}
|
||||
std::sort(v.begin(), v.end());
|
||||
sig.push_back(static_cast<unsigned>(v.size()));
|
||||
for (auto const& [a,b] : v) { sig.push_back(a); sig.push_back(b); }
|
||||
}
|
||||
sig.push_back(UINT_MAX); // section separator
|
||||
// string disequalities
|
||||
{
|
||||
std::vector<std::pair<unsigned,unsigned>> v;
|
||||
for (auto const& d : n->str_deqs()) {
|
||||
v.emplace_back(d.m_lhs->id(), d.m_rhs->id());
|
||||
}
|
||||
std::ranges::sort(v);
|
||||
sig.push_back(static_cast<unsigned>(v.size()));
|
||||
for (auto const& [a,b] : v) { sig.push_back(a); sig.push_back(b); }
|
||||
}
|
||||
sig.push_back(UINT_MAX);
|
||||
// regex memberships incl. view/guard metadata
|
||||
{
|
||||
std::vector<std::vector<unsigned>> v;
|
||||
for (auto const& mm : n->str_mems())
|
||||
v.push_back({ mm.m_str->id(), mm.m_regex->id(),
|
||||
static_cast<unsigned>(mm.m_kind),
|
||||
mm.m_root ? mm.m_root->id() : UINT_MAX,
|
||||
mm.m_nu, mm.m_discharged ? 1u : 0u });
|
||||
std::ranges::sort(v);
|
||||
sig.push_back(static_cast<unsigned>(v.size()));
|
||||
for (auto const& a : v) {
|
||||
for (unsigned x : a) {
|
||||
sig.push_back(x);
|
||||
}
|
||||
}
|
||||
}
|
||||
sig.push_back(UINT_MAX);
|
||||
// character-range constraints (per symbolic unit)
|
||||
{
|
||||
std::vector<std::vector<unsigned>> v;
|
||||
for (auto const& [uid, cr] : n->char_ranges()) {
|
||||
std::vector<unsigned> entry;
|
||||
entry.push_back(uid);
|
||||
for (auto const& rg : cr.first.ranges()) {
|
||||
entry.push_back(rg.m_lo);
|
||||
entry.push_back(rg.m_hi);
|
||||
}
|
||||
v.push_back(std::move(entry));
|
||||
}
|
||||
std::sort(v.begin(), v.end());
|
||||
sig.push_back(static_cast<unsigned>(v.size()));
|
||||
for (auto const& e : v) {
|
||||
sig.push_back(static_cast<unsigned>(e.size()));
|
||||
for (unsigned x : e) {
|
||||
sig.push_back(x);
|
||||
}
|
||||
}
|
||||
}
|
||||
return sig;
|
||||
}
|
||||
|
||||
dep_tracker nielsen_graph::node_all_deps(nielsen_node const* n) const {
|
||||
dep_tracker d = nullptr;
|
||||
for (auto const& e : n->str_eqs()) {
|
||||
|
|
@ -2217,6 +2212,11 @@ namespace seq {
|
|||
SASSERT(depth <= cur_path.size());
|
||||
m_stats.m_max_depth = std::max(m_stats.m_max_depth, depth);
|
||||
|
||||
// structural depth of this node on the current DFS path (counts ALL edges,
|
||||
// unlike `depth` which discounts progress edges). Used by the subsumption
|
||||
// rule to identify and compare ancestors.
|
||||
node->m_dfs_path_pos = cur_path.size();
|
||||
|
||||
if (node->is_general_conflict()) {
|
||||
++m_stats.m_num_simplify_conflict;
|
||||
return search_result::unsat;
|
||||
|
|
@ -2262,9 +2262,8 @@ namespace seq {
|
|||
// constraints — so we prune without re-exploring its subtree. We derive
|
||||
// the conflict from this node's own constraint deps (a sound over-approx).
|
||||
{
|
||||
const std::vector<unsigned> sig = compute_node_signature(node);
|
||||
if (m_unsat_node_cache.contains(sig)) {
|
||||
node->set_conflict(backtrack_reason::regex, node_all_deps(node));
|
||||
if (m_unsat_node_cache.contains(node)) {
|
||||
node->set_conflict(backtrack_reason::sibling, node_all_deps(node));
|
||||
node->set_general_conflict();
|
||||
node->m_unsat_cacheable = true;
|
||||
++m_stats.m_num_simplify_conflict;
|
||||
|
|
@ -2324,7 +2323,8 @@ namespace seq {
|
|||
node->set_conflict(backtrack_reason::regex, dep);
|
||||
// string-only conflict (empty intersection) → memoize.
|
||||
node->m_unsat_cacheable = true;
|
||||
m_unsat_node_cache.insert(compute_node_signature(node));
|
||||
node->canonize_and_compute_final_node_hash();
|
||||
m_unsat_node_cache.insert(node);
|
||||
return search_result::unsat;
|
||||
}
|
||||
assert_node_side_constraints(node);
|
||||
|
|
@ -2334,6 +2334,7 @@ namespace seq {
|
|||
++m_stats.m_num_simplify_conflict;
|
||||
return search_result::unsat;
|
||||
}
|
||||
node->canonize_and_compute_final_node_hash();
|
||||
m_sat_node = node;
|
||||
m_sat_path = cur_path;
|
||||
return search_result::sat;
|
||||
|
|
@ -2342,6 +2343,34 @@ namespace seq {
|
|||
if (node->is_currently_conflict())
|
||||
return search_result::unsat;
|
||||
|
||||
// -------------------------------------------------------------------
|
||||
// Subsumption rule (Nielsen loop-cut).
|
||||
// If this node has the SAME string constraints as a node further up the
|
||||
// current DFS path (an ancestor "sibling"), then every continuation from
|
||||
// here is already being explored from that ancestor. We must NOT report a
|
||||
// conflict: the arithmetic side-constraints accumulated along the two paths
|
||||
// differ, so a model may exist here that does not at the ancestor. Instead
|
||||
// we CUT — return unsat provisionally and remember (in m_subtree_lowlink)
|
||||
// the structural depth of the ancestor we defer to. A cut only hardens
|
||||
// into a genuine conflict at an enclosing node whose entire subtree closes
|
||||
// with string-only conflicts and self-contained cuts (see the epilogue).
|
||||
// -------------------------------------------------------------------
|
||||
node->canonize_and_compute_final_node_hash();
|
||||
{
|
||||
auto it = m_siblings.find(node);
|
||||
if (it != m_siblings.end() && !it->second.empty()) {
|
||||
nielsen_node* anc = it->second.back(); // deepest sibling still on the path
|
||||
SASSERT(anc != node);
|
||||
// deps are a sound over-approximation (the node's own constraint
|
||||
// sources); only used if a children_failed ancestor recurses here.
|
||||
node->set_conflict(backtrack_reason::sibling, node_all_deps(node));
|
||||
node->m_subtree_lowlink = anc->m_dfs_path_pos; // escape level
|
||||
node->m_subtree_has_cut = true;
|
||||
++m_stats.m_num_sibling_cut;
|
||||
return search_result::unsat;
|
||||
}
|
||||
}
|
||||
|
||||
// depth bound check
|
||||
if (depth >= m_depth_bound)
|
||||
return search_result::unknown;
|
||||
|
|
@ -2370,9 +2399,18 @@ namespace seq {
|
|||
++m_stats.m_num_extensions;
|
||||
}
|
||||
|
||||
// Register this node on the active path so descendants can detect a loop
|
||||
// back to it (the subsumption cut above). The hash/signature is already
|
||||
// computed (cut check) so the structural key is stable. Popped after the
|
||||
// child loop. A bucket holds at most one on-path node per signature
|
||||
// (a second equal node on the path would have been cut before reaching here).
|
||||
m_siblings[node].push_back(node);
|
||||
|
||||
// explore children
|
||||
bool any_unknown = false;
|
||||
bool all_general_conflict = true;
|
||||
bool subtree_has_cut = false; // a sibling loop-cut occurred below
|
||||
unsigned min_child_lowlink = UINT_MAX; // min depth any sibling cut below escapes to
|
||||
for (nielsen_edge *e : node->outgoing()) {
|
||||
cur_path.push_back(e);
|
||||
// Push a solver scope for this edge and assert its side integer
|
||||
|
|
@ -2397,25 +2435,39 @@ namespace seq {
|
|||
|
||||
m_length_solver.pop(1);
|
||||
if (r == search_result::sat)
|
||||
// m_siblings entry is left dangling; it is cleared at the start of
|
||||
// the next iteration (and the whole search returns sat now anyway).
|
||||
return search_result::sat;
|
||||
cur_path.pop_back();
|
||||
if (r == search_result::unknown)
|
||||
any_unknown = true;
|
||||
else { // unsat: fold the child's lowlink (cut escape level) into ours
|
||||
min_child_lowlink = std::min(min_child_lowlink, e->tgt()->m_subtree_lowlink);
|
||||
subtree_has_cut |= e->tgt()->m_subtree_has_cut;
|
||||
}
|
||||
if (!e->tgt()->is_general_conflict())
|
||||
all_general_conflict = false;
|
||||
}
|
||||
|
||||
// leave the active path (mirrors the push above)
|
||||
SASSERT(!m_siblings[node].empty() && m_siblings[node].back() == node);
|
||||
m_siblings[node].pop_back();
|
||||
|
||||
if (all_general_conflict) {
|
||||
SASSERT(!any_unknown);
|
||||
// mark it such that we do not have to reconsider it even after a hot-restart
|
||||
node->set_general_conflict();
|
||||
}
|
||||
node->m_subtree_has_cut = subtree_has_cut;
|
||||
if (!any_unknown) {
|
||||
node->set_child_conflict();
|
||||
// Memoize this internal UNSAT iff its whole subtree closed for
|
||||
// string/regex-only reasons (no child relied on arithmetic / Parikh /
|
||||
// external context). Then a same-signature node found via any other
|
||||
// path is pruned by the lookup above.
|
||||
// The subtree closed. Record our lowlink and decide how strong a
|
||||
// conflict we may claim. self_contained == no sibling cut below
|
||||
// escapes above this node, i.e. every loop is internal to our subtree.
|
||||
node->m_subtree_lowlink = min_child_lowlink;
|
||||
const bool self_contained = (min_child_lowlink >= node->m_dfs_path_pos);
|
||||
|
||||
// string-only closure: every leaf below is a string-only conflict or a
|
||||
// sibling cut (cuts count as string-only, see reason_is_string_only).
|
||||
bool all_string_only = true;
|
||||
for (nielsen_edge* e : node->outgoing()) {
|
||||
if (!node_unsat_string_only(e->tgt())) {
|
||||
|
|
@ -2423,9 +2475,40 @@ namespace seq {
|
|||
break;
|
||||
}
|
||||
}
|
||||
node->m_unsat_cacheable = all_string_only;
|
||||
if (all_string_only)
|
||||
m_unsat_node_cache.insert(compute_node_signature(node));
|
||||
|
||||
// Soundness of the subsumption rule: a loop-cut defers to an ancestor
|
||||
// whose arithmetic side-constraints differ from this path's, so a cut is
|
||||
// only a valid UNSAT witness when the WHOLE closure is string-only. If a
|
||||
// cut coexists with an arithmetic / Parikh / external conflict, the cut
|
||||
// may be hiding a model feasible under this node's distinct side
|
||||
// constraints — we cannot conclude UNSAT. Report unknown (the node is
|
||||
// left unmarked and re-explored at a larger depth bound).
|
||||
if (subtree_has_cut && !all_string_only)
|
||||
return search_result::unknown;
|
||||
|
||||
if (all_string_only) {
|
||||
// Subsumption rule: this node is a string-only conflict. Internal
|
||||
// (has children) closures carry no own deps — collect_conflict_deps
|
||||
// recurses through them to the genuine conflict / cut leaves below.
|
||||
node->set_conflict(backtrack_reason::sibling, nullptr);
|
||||
++m_stats.m_num_sibling_closure;
|
||||
if (self_contained) {
|
||||
// No cut escapes this subtree: the unsat is a property of the
|
||||
// node's string signature alone. Make it sticky (survives
|
||||
// hot-restart) and memoize it in the transposition table.
|
||||
node->set_general_conflict();
|
||||
node->m_unsat_cacheable = true;
|
||||
m_unsat_node_cache.insert(node);
|
||||
}
|
||||
else
|
||||
// Conditional on an ancestor above us; valid for this path only.
|
||||
node->m_unsat_cacheable = false;
|
||||
}
|
||||
else {
|
||||
// a child relied on arithmetic / Parikh / external context.
|
||||
node->set_child_conflict();
|
||||
node->m_unsat_cacheable = false;
|
||||
}
|
||||
return search_result::unsat;
|
||||
}
|
||||
return search_result::unknown;
|
||||
|
|
@ -2522,7 +2605,7 @@ namespace seq {
|
|||
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));
|
||||
eqs.push_back(str_eq(m, lhs_rest, rhs_rest, eq.m_dep));
|
||||
return true;
|
||||
}
|
||||
else
|
||||
|
|
@ -2557,7 +2640,7 @@ namespace seq {
|
|||
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));
|
||||
eqs.push_back(str_eq(m, lhs_rest, rhs_rest, eq.m_dep));
|
||||
return true;
|
||||
}
|
||||
else
|
||||
|
|
@ -2841,30 +2924,46 @@ namespace seq {
|
|||
e->add_subst(s);
|
||||
child->apply_subst(m_sg, s);
|
||||
}
|
||||
// child 2: y → ε (progress)
|
||||
// child 2: y → ε && |x| > 0 (progress)
|
||||
{
|
||||
nielsen_node* child = mk_child(node);
|
||||
nielsen_edge* e = mk_edge(node, child, "nielsen var =r", true);
|
||||
const nielsen_subst s(rhead, m_sg.mk_empty_seq(rhead->get_sort()), eq.m_dep);
|
||||
e->add_subst(s);
|
||||
e->add_side_constraint(mk_constraint(a.mk_ge(compute_length_expr(lhead), a.mk_int(0)), eq.m_dep));
|
||||
child->apply_subst(m_sg, s);
|
||||
}
|
||||
// child 3: x → y·x (no progress)
|
||||
// child 3: x → y && |x| > 0 (progress)
|
||||
{
|
||||
euf::snode const* replacement = dir_concat(m_sg, rhead, get_tail(lhead, compute_length_expr(rhead).get(), fwd), fwd);
|
||||
nielsen_node* child = mk_child(node);
|
||||
nielsen_edge* e = mk_edge(node, child, "nielsen var =", true);
|
||||
const nielsen_subst s(lhead, rhead, eq.m_dep);
|
||||
e->add_subst(s);
|
||||
e->add_side_constraint(mk_constraint(a.mk_ge(compute_length_expr(lhead), a.mk_int(0)), eq.m_dep));
|
||||
child->apply_subst(m_sg, s);
|
||||
}
|
||||
// child 4: x → y·x && |x| > 0 && |y| > 0 (no progress)
|
||||
{
|
||||
auto* tail = get_tail(lhead, compute_length_expr(rhead).get(), fwd);
|
||||
euf::snode const* replacement = dir_concat(m_sg, rhead, tail, fwd);
|
||||
nielsen_node* child = mk_child(node);
|
||||
nielsen_edge* e = mk_edge(node, child, "nielsen var >", false);
|
||||
const nielsen_subst s(lhead, replacement, eq.m_dep);
|
||||
e->add_subst(s);
|
||||
e->add_side_constraint(mk_constraint(a.mk_gt(compute_length_expr(rhead), a.mk_int(0)), eq.m_dep));
|
||||
e->add_side_constraint(mk_constraint(a.mk_gt(compute_length_expr(tail), a.mk_int(0)), eq.m_dep));
|
||||
child->apply_subst(m_sg, s);
|
||||
}
|
||||
// child 4: y → x·y (no progress)
|
||||
// child 5: y → x·y && |x| > 0 && |y| > 0 (no progress)
|
||||
{
|
||||
euf::snode const* replacement = dir_concat(m_sg, lhead, get_tail(rhead, compute_length_expr(lhead).get(), fwd), fwd);
|
||||
auto* tail = get_tail(rhead, compute_length_expr(lhead).get(), fwd);
|
||||
euf::snode const* replacement = dir_concat(m_sg, lhead, tail, fwd);
|
||||
nielsen_node* child = mk_child(node);
|
||||
nielsen_edge* e = mk_edge(node, child, "nielsen var <", false);
|
||||
const nielsen_subst s(rhead, replacement, eq.m_dep);
|
||||
e->add_subst(s);
|
||||
e->add_side_constraint(mk_constraint(a.mk_gt(compute_length_expr(lhead), a.mk_int(0)), eq.m_dep));
|
||||
e->add_side_constraint(mk_constraint(a.mk_gt(compute_length_expr(tail), a.mk_int(0)), eq.m_dep));
|
||||
child->apply_subst(m_sg, s);
|
||||
}
|
||||
return true;
|
||||
|
|
@ -2939,9 +3038,9 @@ namespace seq {
|
|||
bool rhs_has_symbolic = token_has_variable_length(rhs_toks[0]);
|
||||
int const_diff = 0;
|
||||
if (!lhs_has_symbolic)
|
||||
const_diff += (int)token_const_length(lhs_toks[0]);
|
||||
const_diff += token_const_length(lhs_toks[0]);
|
||||
if (!rhs_has_symbolic)
|
||||
const_diff -= (int)token_const_length(rhs_toks[0]);
|
||||
const_diff -= token_const_length(rhs_toks[0]);
|
||||
|
||||
bool seen_variable = lhs_has_symbolic || rhs_has_symbolic;
|
||||
|
||||
|
|
@ -3055,17 +3154,13 @@ namespace seq {
|
|||
for (unsigned eq_idx = 0; eq_idx < node->str_eqs().size(); ++eq_idx) {
|
||||
str_eq const& eq = node->str_eqs()[eq_idx];
|
||||
SASSERT(eq.well_formed());
|
||||
if (eq.is_trivial())
|
||||
continue;
|
||||
// EqSplit only applies to regex-free equations.
|
||||
if (!eq.m_lhs->is_regex_free() || !eq.m_rhs->is_regex_free())
|
||||
continue;
|
||||
SASSERT(!eq.is_trivial());
|
||||
|
||||
euf::snode_vector lhs_toks, rhs_toks;
|
||||
eq.m_lhs->collect_tokens(lhs_toks);
|
||||
eq.m_rhs->collect_tokens(rhs_toks);
|
||||
if (lhs_toks.empty() || rhs_toks.empty())
|
||||
continue;
|
||||
SASSERT(!lhs_toks.empty());
|
||||
SASSERT(!rhs_toks.empty());
|
||||
|
||||
unsigned split_lhs = 0, split_rhs = 0;
|
||||
int padding = 0;
|
||||
|
|
@ -3114,8 +3209,8 @@ namespace seq {
|
|||
auto& eqs = child->str_eqs();
|
||||
eqs[eq_idx] = eqs.back();
|
||||
eqs.pop_back();
|
||||
eqs.push_back(str_eq(eq1_lhs, eq1_rhs, eq.m_dep));
|
||||
eqs.push_back(str_eq(eq2_lhs, eq2_rhs, eq.m_dep));
|
||||
eqs.push_back(str_eq(m, eq1_lhs, eq1_rhs, eq.m_dep));
|
||||
eqs.push_back(str_eq(m, eq2_lhs, eq2_rhs, eq.m_dep));
|
||||
|
||||
// Int constraints on the edge.
|
||||
// 1) len(pad) = |padding| (if padding variable was created)
|
||||
|
|
@ -3342,7 +3437,7 @@ namespace seq {
|
|||
bool& fwd) {
|
||||
for (str_mem const& mem : node->str_mems()) {
|
||||
if (mem.is_trivial(node)) {
|
||||
std::cout << "Trivial mem: " << mem_pp(mem, node->graph().get_manager()) << std::endl;
|
||||
std::cout << "Trivial mem: " << mem_pp(mem) << std::endl;
|
||||
}
|
||||
SASSERT(mem.well_formed() && !mem.is_trivial(node));
|
||||
|
||||
|
|
@ -3806,10 +3901,10 @@ namespace seq {
|
|||
child->m_str_mem[mi].m_str = dir_drop(m_sg, child->m_str_mem[mi].m_str, 1, true);
|
||||
|
||||
// x' ∈ stab(R, Q_ν) (stabilizer view, F = {R}, current state = R)
|
||||
child->add_str_mem(str_mem::mk_view(xp, R, R, nu, mem.m_dep));
|
||||
child->add_str_mem(str_mem::mk_view(m, xp, R, R, nu, mem.m_dep));
|
||||
|
||||
// noloop(x'', R, Q_ν) (cycle guard, two-mode monitor, state = R)
|
||||
child->add_str_mem(str_mem::mk_guard(xpp, R, R, nu, mem.m_dep));
|
||||
child->add_str_mem(str_mem::mk_guard(m, xpp, R, R, nu, mem.m_dep));
|
||||
|
||||
TRACE(seq, tout << "cycle_decomp: x=" << mk_pp(x->get_expr(), m)
|
||||
<< " R=" << mk_pp(R->get_expr(), m) << " nu=" << nu << "\n");
|
||||
|
|
@ -3982,8 +4077,8 @@ namespace seq {
|
|||
}
|
||||
}
|
||||
|
||||
child->add_str_mem(str_mem(head, m_p, m_dep));
|
||||
child->add_str_mem(str_mem(tail, m_q, m_dep));
|
||||
child->add_str_mem(str_mem(m, head, m_p, m_dep));
|
||||
child->add_str_mem(str_mem(m, tail, m_q, m_dep));
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
@ -4269,12 +4364,12 @@ namespace seq {
|
|||
// (1) u1·x = v1 and u2 = x·v2
|
||||
// (2) u1 = v1·x and x·u2 = v2
|
||||
if (branch == 0) {
|
||||
child_eqs.push_back(str_eq(m_sg.mk_concat(u1, x), v1, eq.m_dep));
|
||||
child_eqs.push_back(str_eq(u2, m_sg.mk_concat(x, v2), eq.m_dep));
|
||||
child_eqs.push_back(str_eq(m, m_sg.mk_concat(u1, x), v1, eq.m_dep));
|
||||
child_eqs.push_back(str_eq(m, u2, m_sg.mk_concat(x, v2), eq.m_dep));
|
||||
}
|
||||
else {
|
||||
child_eqs.push_back(str_eq(u1, m_sg.mk_concat(v1, x), eq.m_dep));
|
||||
child_eqs.push_back(str_eq(m_sg.mk_concat(x, u2), v2, eq.m_dep));
|
||||
child_eqs.push_back(str_eq(m, u1, m_sg.mk_concat(v1, x), eq.m_dep));
|
||||
child_eqs.push_back(str_eq(m, m_sg.mk_concat(x, u2), v2, eq.m_dep));
|
||||
}
|
||||
}
|
||||
return true;
|
||||
|
|
@ -4683,7 +4778,6 @@ namespace seq {
|
|||
const expr_ref u_len(compute_length_expr(u), m);
|
||||
const expr_ref v_len(compute_length_expr(v), m);
|
||||
expr_ref len_eq(m.mk_eq(u_len, v_len), m);
|
||||
str_eq eq_uv(u, v, first.m_dep);
|
||||
sort *char_sort = nullptr;
|
||||
VERIFY(seq().is_seq(u->get_sort(), char_sort));
|
||||
euf::snode const* a = m_sg.mk(seq().str.mk_unit(m_sk.mk("diseq.a", u->get_expr(), v->get_expr(), char_sort).get()));
|
||||
|
|
@ -4695,8 +4789,8 @@ namespace seq {
|
|||
const expr_ref vp_len(compute_length_expr(vp), m);
|
||||
euf::snode const* wau = dir_concat(m_sg, dir_concat(m_sg, w, a, true), up, true);
|
||||
euf::snode const* wbv = dir_concat(m_sg, dir_concat(m_sg, w, b, true), vp, true);
|
||||
str_eq u_eq(u, wau, first.m_dep);
|
||||
str_eq v_eq(v, wbv, first.m_dep);
|
||||
str_eq u_eq(m, u, wau, first.m_dep);
|
||||
str_eq v_eq(m, v, wbv, first.m_dep);
|
||||
|
||||
// Branch 1: |u| < |v|
|
||||
{
|
||||
|
|
@ -4740,9 +4834,17 @@ namespace seq {
|
|||
while (!to_visit.empty()) {
|
||||
nielsen_node const* n = to_visit.back();
|
||||
to_visit.pop_back();
|
||||
if (n->reason() == backtrack_reason::children_failed) {
|
||||
SASSERT(n->m_conflict_external_literal == sat::null_literal);
|
||||
SASSERT(!n->m_conflict_internal);
|
||||
// Recurse through internal closures: children_failed nodes, and sibling
|
||||
// (subsumption) closures that have children. The latter carry no own
|
||||
// deps (m_conflict_internal == null) — their justification is the union
|
||||
// of the genuine conflict / cut leaves below them, gathered by recursing
|
||||
// (sound: collecting from all leaves never under-approximates). A sibling
|
||||
// LEAF (a loop cut, or a transposition-cache hit; no children) instead
|
||||
// contributes its own node_all_deps recorded in m_conflict_internal.
|
||||
const bool recurse =
|
||||
n->reason() == backtrack_reason::children_failed ||
|
||||
(n->reason() == backtrack_reason::sibling && !n->outgoing().empty());
|
||||
if (recurse) {
|
||||
for (unsigned i = n->outgoing().size(); i > 0; i--) {
|
||||
nielsen_edge const* e = n->outgoing()[i - 1];
|
||||
to_visit.push_back(e->tgt());
|
||||
|
|
@ -4794,13 +4896,17 @@ namespace seq {
|
|||
|
||||
if (n->is_power()) {
|
||||
const expr_ref base = compute_length_expr(n->arg0());
|
||||
return expr_ref(a.mk_mul(base.get(), n->arg(1)->get_expr()), m);
|
||||
expr_ref res(m);
|
||||
m_a_rw.mk_mul(base.get(), n->arg(1)->get_expr(), res);
|
||||
return res;
|
||||
}
|
||||
|
||||
if (n->is_concat()) {
|
||||
const expr_ref left = compute_length_expr(n->arg0());
|
||||
const expr_ref right = compute_length_expr(n->arg(1));
|
||||
return expr_ref(a.mk_add(left, right), m);
|
||||
expr_ref res(m);
|
||||
m_a_rw.mk_add(left, right, res);
|
||||
return res;
|
||||
}
|
||||
|
||||
//euf::snode const* length_term = nullptr;
|
||||
|
|
@ -5221,7 +5327,7 @@ namespace seq {
|
|||
// TODO: Minimize the conflict here
|
||||
const lbool result = m_seq_regex->is_empty_bfs(inter_sn, 5000);
|
||||
TRACE(seq, tout << "widen empty-intersect: " << result << " " << mk_pp(re, m)
|
||||
<< " <= " << mk_pp(ae, m) << "\n" << mem_pp(mem, m) << "\n";
|
||||
<< " <= " << mk_pp(ae, m) << "\n" << mem_pp(mem) << "\n";
|
||||
display(tout, &node) << "\n");
|
||||
return result == l_true;
|
||||
}
|
||||
|
|
@ -5452,6 +5558,8 @@ namespace seq {
|
|||
st.update("nseq mod axiomatized disequalities", m_stats.m_ax_diseq);
|
||||
st.update("nseq unsat-cache size", (unsigned) m_unsat_node_cache.size());
|
||||
st.update("nseq unsat-cache hits", m_num_cache_hits);
|
||||
st.update("nseq sibling cuts", m_stats.m_num_sibling_cut);
|
||||
st.update("nseq sibling closures", m_stats.m_num_sibling_closure);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -39,7 +39,9 @@ Author:
|
|||
#include "ast/ast.h"
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/euf/euf_mam.h"
|
||||
#include "ast/euf/euf_sgraph.h"
|
||||
#include "ast/rewriter/arith_rewriter.h"
|
||||
#include "model/model.h"
|
||||
#include "util/lbool.h"
|
||||
#include "util/dependency.h"
|
||||
|
|
@ -48,7 +50,7 @@ Author:
|
|||
#include "util/rational.h"
|
||||
#include "util/uint_set.h"
|
||||
#include "util/vector.h"
|
||||
#include <map>
|
||||
#include <unordered_set>
|
||||
#include <set>
|
||||
#include <vector>
|
||||
|
||||
|
|
@ -85,9 +87,9 @@ namespace seq {
|
|||
extended,
|
||||
symbol_clash,
|
||||
parikh_image,
|
||||
subsumption, // not used; retained for enum completeness
|
||||
arithmetic,
|
||||
regex,
|
||||
sibling,
|
||||
regex_widening,
|
||||
character_range,
|
||||
smt,
|
||||
|
|
@ -95,24 +97,6 @@ namespace seq {
|
|||
children_failed,
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, backtrack_reason r) {
|
||||
switch (r) {
|
||||
case backtrack_reason::unevaluated: return out << "unevaluated";
|
||||
case backtrack_reason::extended: return out << "extended";
|
||||
case backtrack_reason::symbol_clash: return out << "symbol_clash";
|
||||
case backtrack_reason::parikh_image: return out << "parikh_image";
|
||||
case backtrack_reason::subsumption: return out << "subsumption";
|
||||
case backtrack_reason::arithmetic: return out << "arithmetic";
|
||||
case backtrack_reason::regex: return out << "regex";
|
||||
case backtrack_reason::regex_widening: return out << "regex_widening";
|
||||
case backtrack_reason::character_range: return out << "char range";
|
||||
case backtrack_reason::children_failed: return out << "children_failed";
|
||||
case backtrack_reason::external: return out << "external";
|
||||
case backtrack_reason::smt: return out << "smt";
|
||||
default: return out << "<tbd reason>";
|
||||
}
|
||||
}
|
||||
|
||||
// source of a dependency: identifies an input constraint by kind and index.
|
||||
// kind::eq means a string equality, kind::mem means a regex membership.
|
||||
// index is the 0-based position in the input eq or mem list respectively.
|
||||
|
|
@ -194,17 +178,36 @@ namespace seq {
|
|||
// string equality constraint: lhs = rhs
|
||||
// mirrors ZIPT's StrEq (both sides are regex-free snode trees)
|
||||
struct str_eq {
|
||||
ast_manager& m;
|
||||
euf::snode const* m_lhs; // assumed to be non-null
|
||||
euf::snode const* m_rhs; // assumed to be non-null
|
||||
dep_tracker m_dep;
|
||||
|
||||
str_eq(euf::snode const* lhs, euf::snode const* rhs, dep_tracker const& dep):
|
||||
m_lhs(lhs), m_rhs(rhs), m_dep(dep) {
|
||||
str_eq(ast_manager& m, euf::snode const* lhs, euf::snode const* rhs, dep_tracker const& dep):
|
||||
m(m), m_lhs(lhs), m_rhs(rhs), m_dep(dep) {
|
||||
SASSERT(well_formed());
|
||||
sort();
|
||||
}
|
||||
|
||||
bool operator==(str_eq const& other) const {
|
||||
return m_lhs == other.m_lhs && m_rhs == other.m_rhs;
|
||||
str_eq& operator=(const str_eq & other) {
|
||||
m_lhs = other.m_lhs;
|
||||
m_rhs = other.m_rhs;
|
||||
m_dep = other.m_dep;
|
||||
return *this;
|
||||
}
|
||||
|
||||
bool operator==(const str_eq& other) const {
|
||||
return m_lhs->similar(other.m_lhs, m) && m_rhs->similar(other.m_rhs, m);
|
||||
}
|
||||
|
||||
bool operator<(const str_eq& other) const {
|
||||
if (m_lhs != other.m_lhs)
|
||||
return m_lhs < other.m_lhs;
|
||||
return m_rhs < other.m_rhs;
|
||||
}
|
||||
|
||||
unsigned hash() const {
|
||||
return 586947209 * m_lhs->assoc_hash() + m_rhs->assoc_hash();
|
||||
}
|
||||
|
||||
// sort so that lhs <= rhs by snode id
|
||||
|
|
@ -224,29 +227,47 @@ namespace seq {
|
|||
|
||||
struct eq_pp {
|
||||
str_eq const &eq;
|
||||
ast_manager &m;
|
||||
eq_pp(str_eq const &e, ast_manager &m) : eq(e), m(m) {}
|
||||
eq_pp(str_eq const &e) : eq(e) {}
|
||||
};
|
||||
|
||||
inline std::ostream &operator<<(std::ostream &out, eq_pp const &p) {
|
||||
return out << snode_label_html(p.eq.m_lhs, p.m, false)
|
||||
return out << snode_label_html(p.eq.m_lhs, p.eq.m, false)
|
||||
<< " == "
|
||||
<< snode_label_html(p.eq.m_rhs, p.m, false);
|
||||
<< snode_label_html(p.eq.m_rhs, p.eq.m, false);
|
||||
}
|
||||
|
||||
// string disequality constraint: lhs != rhs
|
||||
struct str_deq {
|
||||
ast_manager& m;
|
||||
euf::snode const* m_lhs; // assumed to be non-null
|
||||
euf::snode const* m_rhs; // assumed to be non-null
|
||||
dep_tracker m_dep;
|
||||
|
||||
str_deq(euf::snode const* lhs, euf::snode const* rhs, dep_tracker const& dep):
|
||||
m_lhs(lhs), m_rhs(rhs), m_dep(dep) {
|
||||
str_deq(ast_manager& m, euf::snode const* lhs, euf::snode const* rhs, dep_tracker const& dep):
|
||||
m(m), m_lhs(lhs), m_rhs(rhs), m_dep(dep) {
|
||||
SASSERT(well_formed());
|
||||
sort();
|
||||
}
|
||||
|
||||
bool operator==(str_deq const& other) const {
|
||||
return m_lhs == other.m_lhs && m_rhs == other.m_rhs;
|
||||
str_deq& operator=(const str_deq & other) {
|
||||
m_lhs = other.m_lhs;
|
||||
m_rhs = other.m_rhs;
|
||||
m_dep = other.m_dep;
|
||||
return *this;
|
||||
}
|
||||
|
||||
bool operator==(const str_deq& other) const {
|
||||
return m_lhs->similar(other.m_lhs, m) && m_rhs->similar(other.m_rhs, m);
|
||||
}
|
||||
|
||||
bool operator<(const str_deq& other) const {
|
||||
if (m_lhs != other.m_lhs)
|
||||
return m_lhs < other.m_lhs;
|
||||
return m_rhs < other.m_rhs;
|
||||
}
|
||||
|
||||
unsigned hash() const {
|
||||
return 891170543 * m_lhs->assoc_hash() + m_rhs->assoc_hash();
|
||||
}
|
||||
|
||||
void sort() {
|
||||
|
|
@ -267,14 +288,13 @@ namespace seq {
|
|||
|
||||
struct deq_pp {
|
||||
str_deq const &deq;
|
||||
ast_manager &m;
|
||||
deq_pp(str_deq const &e, ast_manager &m) : deq(e), m(m) {}
|
||||
deq_pp(str_deq const &e) : deq(e) {}
|
||||
};
|
||||
|
||||
inline std::ostream &operator<<(std::ostream &out, deq_pp const &p) {
|
||||
return out << snode_label_html(p.deq.m_lhs, p.m, false)
|
||||
return out << snode_label_html(p.deq.m_lhs, p.deq.m, false)
|
||||
<< " != "
|
||||
<< snode_label_html(p.deq.m_rhs, p.m, false);
|
||||
<< snode_label_html(p.deq.m_rhs, p.deq.m, false);
|
||||
}
|
||||
|
||||
// kind of a regex membership constraint (paper Section 3.3, "views"):
|
||||
|
|
@ -290,6 +310,7 @@ namespace seq {
|
|||
// regex membership constraint: str in regex
|
||||
// mirrors ZIPT's StrMem
|
||||
struct str_mem {
|
||||
ast_manager& m;
|
||||
euf::snode const* m_str; // assumed to be non-null
|
||||
euf::snode const* m_regex; // assumed to be non-null (plain regex = current run state)
|
||||
dep_tracker m_dep;
|
||||
|
|
@ -300,20 +321,31 @@ namespace seq {
|
|||
unsigned m_nu = 0; // ν: snapshot index identifying Q
|
||||
bool m_discharged = false; // guard monitor: false=watch, true=discharged
|
||||
|
||||
str_mem(euf::snode const* str, euf::snode const* regex, dep_tracker const& dep):
|
||||
m_str(str), m_regex(regex), m_dep(dep) {}
|
||||
str_mem(ast_manager& m, euf::snode const* str, euf::snode const* regex, dep_tracker const& dep):
|
||||
m(m), m_str(str), m_regex(regex), m_dep(dep) {}
|
||||
|
||||
str_mem& operator=(const str_mem& other) {
|
||||
m_str = other.m_str;
|
||||
m_regex = other.m_regex;
|
||||
m_dep = other.m_dep;
|
||||
m_kind = other.m_kind;
|
||||
m_root = other.m_root;
|
||||
m_nu = other.m_nu;
|
||||
m_discharged = other.m_discharged;
|
||||
return *this;
|
||||
}
|
||||
|
||||
// factory for a stabilizer view str ∈_{Q_ν,{root}} root (m_regex=state)
|
||||
static str_mem mk_view(euf::snode const* str, euf::snode const* state,
|
||||
static str_mem mk_view(ast_manager& m, euf::snode const* str, euf::snode const* state,
|
||||
euf::snode const* root, unsigned nu, dep_tracker const& dep) {
|
||||
str_mem r(str, state, dep);
|
||||
str_mem r(m, str, state, dep);
|
||||
r.m_kind = mem_kind::stab_view; r.m_root = root; r.m_nu = nu;
|
||||
return r;
|
||||
}
|
||||
// factory for a cycle guard noloop(str, root, Q_ν) (m_regex=state)
|
||||
static str_mem mk_guard(euf::snode const* str, euf::snode const* state,
|
||||
static str_mem mk_guard(ast_manager& m, euf::snode const* str, euf::snode const* state,
|
||||
euf::snode const* root, unsigned nu, dep_tracker const& dep) {
|
||||
str_mem r(str, state, dep);
|
||||
str_mem r(m, str, state, dep);
|
||||
r.m_kind = mem_kind::no_loop; r.m_root = root; r.m_nu = nu;
|
||||
return r;
|
||||
}
|
||||
|
|
@ -322,12 +354,22 @@ namespace seq {
|
|||
bool is_view() const { return m_kind == mem_kind::stab_view; }
|
||||
bool is_guard() const { return m_kind == mem_kind::no_loop; }
|
||||
|
||||
bool operator==(str_mem const& other) const {
|
||||
return m_str == other.m_str && m_regex == other.m_regex
|
||||
bool operator==(const str_mem& other) const {
|
||||
return m_str->similar(other.m_str, m) && m_regex == other.m_regex
|
||||
&& m_kind == other.m_kind && m_root == other.m_root
|
||||
&& m_nu == other.m_nu && m_discharged == other.m_discharged;
|
||||
}
|
||||
|
||||
bool operator<(const str_mem& other) const {
|
||||
if (m_str != other.m_str)
|
||||
return m_str < other.m_str;
|
||||
return m_regex < other.m_regex;
|
||||
}
|
||||
|
||||
unsigned hash() const {
|
||||
return 381416603 * m_str->assoc_hash() + m_regex->assoc_hash();
|
||||
}
|
||||
|
||||
// check if the constraint has the form x in R with x a single variable
|
||||
bool is_primitive() const;
|
||||
|
||||
|
|
@ -347,14 +389,13 @@ namespace seq {
|
|||
|
||||
struct mem_pp {
|
||||
str_mem const& mem;
|
||||
ast_manager &m;
|
||||
mem_pp(str_mem const& mem, ast_manager& m) : mem(mem), m(m) {}
|
||||
mem_pp(str_mem const& mem) : mem(mem) {}
|
||||
};
|
||||
inline std::ostream &operator<<(std::ostream &out, mem_pp const &p) {
|
||||
return out
|
||||
<< snode_label_html(p.mem.m_str, p.m, false)
|
||||
<< snode_label_html(p.mem.m_str, p.mem.m, false)
|
||||
<< " in "
|
||||
<< snode_label_html(p.mem.m_regex, p.m, false);
|
||||
<< snode_label_html(p.mem.m_regex, p.mem.m, false);
|
||||
}
|
||||
|
||||
// string variable substitution: var -> replacement
|
||||
|
|
@ -399,6 +440,7 @@ namespace seq {
|
|||
dep_tracker dep; // tracks which input constraints contributed
|
||||
|
||||
static expr_ref simplify(expr* f, ast_manager& m) {
|
||||
//arith_rewriter th(m);
|
||||
//th_rewriter th(m);
|
||||
expr_ref fml(f, m);
|
||||
//th(fml);
|
||||
|
|
@ -514,6 +556,30 @@ namespace seq {
|
|||
backtrack_reason m_reason = backtrack_reason::unevaluated;
|
||||
bool m_is_progress = false;
|
||||
bool m_node_len_constraints_generated = false; // true after generate_node_length_constraints runs
|
||||
|
||||
unsigned m_hash = 0; // 0 ... unset
|
||||
|
||||
nielsen_node* m_parent = this;
|
||||
|
||||
// DFS bookkeeping for the subsumption (loop-cut) rule.
|
||||
// m_dfs_path_pos: structural depth (= cur_path.size()) of this node while
|
||||
// it is on the active DFS path; read by a descendant that
|
||||
// loops back to it as a sibling.
|
||||
// m_subtree_lowlink: minimum structural depth that this node's UNSAT closure
|
||||
// escapes to via sibling cuts below it (Tarjan-style
|
||||
// lowlink). UINT_MAX means "no cut escapes" — the unsat
|
||||
// is self-contained. Only meaningful when the node's last
|
||||
// result was unsat.
|
||||
unsigned m_dfs_path_pos = 0;
|
||||
unsigned m_subtree_lowlink = UINT_MAX;
|
||||
// m_subtree_has_cut: a sibling loop-cut occurred somewhere in this node's
|
||||
// closed subtree. A cut defers to an ancestor whose ARITHMETIC side
|
||||
// constraints differ, so it is only a valid UNSAT witness inside a closure
|
||||
// that uses string-only reasons throughout. When a cut coexists with a
|
||||
// non-string-only (arithmetic / external) conflict the subtree result is
|
||||
// NOT a sound UNSAT — search_dfs reports unknown instead.
|
||||
bool m_subtree_has_cut = false;
|
||||
|
||||
// true once this node has been proven UNSAT for reasons that depend only
|
||||
// on its string/regex constraints (not on arithmetic / Parikh / external
|
||||
// context). Such an unsat is a property of the node's string signature
|
||||
|
|
@ -543,10 +609,10 @@ namespace seq {
|
|||
vector<str_mem> const& str_mems() const { return m_str_mem; }
|
||||
vector<str_mem>& str_mems() { return m_str_mem; }
|
||||
|
||||
void add_str_eq(str_eq& eq);
|
||||
void add_str_deq(str_deq& deq);
|
||||
void add_str_mem(str_mem const& mem);
|
||||
void add_constraint(constraint const &ic);
|
||||
void add_str_eq(const str_eq& eq);
|
||||
void add_str_deq(const str_deq& deq);
|
||||
void add_str_mem(const str_mem& mem);
|
||||
void add_constraint(const constraint &ic);
|
||||
|
||||
vector<constraint> const& constraints() const { return m_constraints; }
|
||||
vector<constraint>& constraints() { return m_constraints; }
|
||||
|
|
@ -578,6 +644,11 @@ namespace seq {
|
|||
nielsen_edge* parent_edge() const { return m_parent_edge; }
|
||||
void set_parent_edge(nielsen_edge* e) { m_parent_edge = e; }
|
||||
|
||||
// returns 0 if hash is unknown
|
||||
unsigned hash() const {
|
||||
return m_hash;
|
||||
}
|
||||
|
||||
// status
|
||||
bool is_general_conflict() const { return m_is_general_conflict; }
|
||||
void set_general_conflict() {
|
||||
|
|
@ -592,6 +663,9 @@ namespace seq {
|
|||
bool is_currently_conflict() const {
|
||||
return is_general_conflict() ||
|
||||
m_conflict_external_literal != sat::null_literal ||
|
||||
// a sibling (loop-cut / subsumption) conflict counts even when the
|
||||
// node was never extended (a cut leaf has no children).
|
||||
reason() == backtrack_reason::sibling ||
|
||||
(reason() != backtrack_reason::unevaluated && m_is_extended);
|
||||
}
|
||||
|
||||
|
|
@ -617,7 +691,7 @@ namespace seq {
|
|||
if (m_conflict_internal != nullptr && m_conflict_external_literal == sat::null_literal)
|
||||
return;
|
||||
// We prefer internal conflicts (we need it as a justification for general conflicts)
|
||||
TRACE(seq, tout << "internal conflict " << r << "\n");
|
||||
TRACE(seq, tout << "internal conflict " << (unsigned)r << "\n");
|
||||
m_reason = r;
|
||||
m_conflict_internal = confl;
|
||||
m_conflict_external_literal = sat::null_literal;
|
||||
|
|
@ -640,6 +714,22 @@ namespace seq {
|
|||
// apply a substitution to all constraints
|
||||
void apply_subst(euf::sgraph& sg, nielsen_subst const& s);
|
||||
|
||||
// Transposition table helpers (node memoization of string-only UNSAT).
|
||||
// after computing the signature we should not change the node anymore
|
||||
// the hash disregards length constraints on purpose for subsumption checks
|
||||
unsigned canonize_and_compute_node_hash();
|
||||
|
||||
unsigned canonize_and_compute_final_node_hash() {
|
||||
if (m_hash)
|
||||
return m_hash;
|
||||
m_hash = canonize_and_compute_node_hash();
|
||||
return m_hash;
|
||||
}
|
||||
|
||||
// check if two nodes are equivalent modulo side-constraints
|
||||
// (actually subset checks would be better but we currently do not track this)
|
||||
bool is_node_sibling(nielsen_node const* n);
|
||||
|
||||
// simplify all constraints at this node and initialize status.
|
||||
// Uses cur_path for LP solver queries during deterministic power cancellation.
|
||||
// Returns proceed, conflict, satisfied, or restart.
|
||||
|
|
@ -679,6 +769,22 @@ namespace seq {
|
|||
// Length bounds are queried from the arithmetic subsolver when needed.
|
||||
};
|
||||
|
||||
struct nielsen_node_hash {
|
||||
// outputs the hash without side-constraints
|
||||
unsigned operator()(nielsen_node* n) const {
|
||||
const unsigned h = n->hash();
|
||||
if (h == 0)
|
||||
return n->canonize_and_compute_node_hash();
|
||||
return h;
|
||||
}
|
||||
};
|
||||
|
||||
struct nielsen_node_eq {
|
||||
unsigned operator()(nielsen_node* n1, nielsen_node* n2) const {
|
||||
return n1->is_node_sibling(n2);
|
||||
}
|
||||
};
|
||||
|
||||
// search statistics collected during Nielsen graph solving
|
||||
struct nielsen_stats {
|
||||
unsigned m_num_solve_calls = 0;
|
||||
|
|
@ -712,6 +818,9 @@ namespace seq {
|
|||
unsigned m_mod_var_num_unwinding_eq = 0;
|
||||
unsigned m_mod_var_num_unwinding_mem = 0;
|
||||
unsigned m_ax_diseq = 0;
|
||||
// subsumption rule
|
||||
unsigned m_num_sibling_cut = 0; // loop-cut leaves (deferred to an ancestor)
|
||||
unsigned m_num_sibling_closure = 0; // subtrees closed as string-only sibling conflicts
|
||||
void reset() { memset(this, 0, sizeof(nielsen_stats)); }
|
||||
};
|
||||
|
||||
|
|
@ -750,7 +859,7 @@ namespace seq {
|
|||
|
||||
struct partial_dfa_edge_key_hash {
|
||||
size_t operator()(partial_dfa_edge_key const& k) const {
|
||||
size_t h = static_cast<size_t>(k.m_src);
|
||||
size_t h = k.m_src;
|
||||
h = (h * 1315423911u) ^ static_cast<size_t>(k.m_label + 0x9e3779b9u);
|
||||
h = (h * 2654435761u) ^ static_cast<size_t>(k.m_dst + 0x85ebca6bu);
|
||||
return h;
|
||||
|
|
@ -762,6 +871,7 @@ namespace seq {
|
|||
seq_util& m_seq;
|
||||
euf::sgraph& m_sg;
|
||||
th_rewriter m_rw;
|
||||
arith_rewriter m_a_rw;
|
||||
skolem m_sk;
|
||||
ptr_vector<nielsen_node> m_nodes;
|
||||
ptr_vector<nielsen_edge> m_edges;
|
||||
|
|
@ -835,12 +945,19 @@ namespace seq {
|
|||
// see ensure_automaton_explored).
|
||||
uint_set m_explored_automaton;
|
||||
|
||||
// Active-path index for the subsumption rule, keyed structurally (nodes
|
||||
// with identical string constraints share a bucket). While a node is on
|
||||
// the DFS path it is pushed onto its bucket and popped on leaving, so a
|
||||
// non-empty bucket for the current node holds exactly the ancestor(s) it
|
||||
// is a sibling of — i.e. a loop back up the Nielsen tree.
|
||||
std::unordered_map<nielsen_node*, vector<nielsen_node*>, nielsen_node_hash, nielsen_node_eq> m_siblings;
|
||||
|
||||
// Transposition table: structural signatures of nodes already proven
|
||||
// UNSAT for string/regex-only reasons. A node whose signature is present
|
||||
// is unsatisfiable regardless of how it was reached, so the DFS can prune
|
||||
// it without re-exploring its subtree (turns the search tree into the
|
||||
// finite DAG the termination proof bounds). See compute_node_signature.
|
||||
std::set<std::vector<unsigned>> m_unsat_node_cache;
|
||||
std::unordered_set<nielsen_node*, nielsen_node_hash, nielsen_node_eq> m_unsat_node_cache;
|
||||
unsigned m_num_cache_hits = 0;
|
||||
|
||||
// Incremental eager-closure chain state (see eager_begin / eager_close).
|
||||
|
|
@ -1062,11 +1179,6 @@ namespace seq {
|
|||
|
||||
search_result search_dfs(nielsen_node *node, ptr_vector<nielsen_edge>& path, unsigned depth = 0);
|
||||
|
||||
// Transposition table helpers (node memoization of string-only UNSAT).
|
||||
// Canonical structural signature of a node (string equalities,
|
||||
// disequalities, memberships incl. view/guard metadata, char ranges).
|
||||
// Two nodes with equal signatures have identical string constraints.
|
||||
static std::vector<unsigned> compute_node_signature(nielsen_node const* n);
|
||||
// Union of all constraint deps of a node (sound over-approx conflict).
|
||||
dep_tracker node_all_deps(nielsen_node const* n) const;
|
||||
// True iff the node's UNSAT depends only on string/regex constraints.
|
||||
|
|
@ -1356,3 +1468,21 @@ namespace seq {
|
|||
};
|
||||
|
||||
}
|
||||
|
||||
template <> struct std::hash<seq::str_eq> {
|
||||
unsigned operator()(seq::str_eq& eq) const noexcept {
|
||||
return eq.hash();
|
||||
}
|
||||
};
|
||||
|
||||
template <> struct std::hash<seq::str_deq> {
|
||||
unsigned operator()(seq::str_deq& deq) const noexcept {
|
||||
return deq.hash();
|
||||
}
|
||||
};
|
||||
|
||||
template <> struct std::hash<seq::str_mem> {
|
||||
unsigned operator()(seq::str_mem& mem) const noexcept {
|
||||
return mem.hash();
|
||||
}
|
||||
};
|
||||
|
|
@ -597,9 +597,9 @@ namespace seq {
|
|||
case backtrack_reason::extended: return "Extended";
|
||||
case backtrack_reason::symbol_clash: return "Symbol Clash";
|
||||
case backtrack_reason::parikh_image: return "Parikh Image";
|
||||
case backtrack_reason::subsumption: return "Subsumption";
|
||||
case backtrack_reason::arithmetic: return "Arithmetic";
|
||||
case backtrack_reason::regex: return "Regex";
|
||||
case backtrack_reason::sibling: return "Sibling";
|
||||
case backtrack_reason::regex_widening: return "RegexWidening";
|
||||
case backtrack_reason::character_range: return "Character Range";
|
||||
case backtrack_reason::smt: return "SMT";
|
||||
|
|
|
|||
|
|
@ -625,7 +625,7 @@ namespace seq {
|
|||
SASSERT(first);
|
||||
if (first != var)
|
||||
continue;
|
||||
TRACE(seq, tout << spp(first, m) << " " << mem_pp(mem, m) << "\n");
|
||||
TRACE(seq, tout << spp(first, m) << " " << mem_pp(mem) << "\n");
|
||||
|
||||
if (!result) {
|
||||
result = mem.m_regex;
|
||||
|
|
@ -644,14 +644,6 @@ namespace seq {
|
|||
return result;
|
||||
}
|
||||
|
||||
// -----------------------------------------------------------------------
|
||||
// Cycle detection
|
||||
// -----------------------------------------------------------------------
|
||||
|
||||
bool seq_regex::detect_cycle(seq::str_mem const& mem) const {
|
||||
return extract_cycle(mem) != nullptr;
|
||||
}
|
||||
|
||||
// -----------------------------------------------------------------------
|
||||
// Ground prefix consumption
|
||||
// -----------------------------------------------------------------------
|
||||
|
|
@ -784,55 +776,6 @@ namespace seq {
|
|||
return true;
|
||||
}
|
||||
|
||||
// -----------------------------------------------------------------------
|
||||
// History recording
|
||||
// -----------------------------------------------------------------------
|
||||
|
||||
seq::str_mem seq_regex::record_history(seq::str_mem const& mem, euf::snode const* history_re) {
|
||||
|
||||
return str_mem(mem.m_str, mem.m_regex, mem.m_dep);
|
||||
}
|
||||
|
||||
// -----------------------------------------------------------------------
|
||||
// Cycle detection
|
||||
// -----------------------------------------------------------------------
|
||||
|
||||
euf::snode const* seq_regex::extract_cycle(seq::str_mem const& mem) const {
|
||||
#if 0
|
||||
// Walk the history chain looking for a repeated regex.
|
||||
// A cycle exists when the current regex matches a regex in the history.
|
||||
if (!mem.m_regex || !mem.m_history)
|
||||
return nullptr;
|
||||
|
||||
euf::snode const* current = mem.m_regex;
|
||||
euf::snode const* hist = mem.m_history;
|
||||
|
||||
// Walk the history chain up to a bounded depth.
|
||||
// The history is structured as a chain of regex snapshots connected
|
||||
// via the sgraph's regex-concat: each level's arg(0) is a snapshot
|
||||
// and arg(1) is the tail. A leaf (non-concat) is a terminal entry.
|
||||
unsigned bound = 1000;
|
||||
while (hist && bound-- > 0) {
|
||||
euf::snode const* entry = hist;
|
||||
euf::snode const* tail = nullptr;
|
||||
|
||||
// If the history node is a regex concat, decompose it:
|
||||
// arg(0) is the regex snapshot, arg(1) is the rest of the chain
|
||||
if (hist->is_concat() && seq.re.is_concat(hist->get_expr())) {
|
||||
entry = hist->arg(0);
|
||||
tail = hist->arg(1);
|
||||
}
|
||||
|
||||
// Check pointer equality (fast, covers normalized regexes)
|
||||
if (entry == current)
|
||||
return entry;
|
||||
|
||||
hist = tail;
|
||||
}
|
||||
#endif
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
// -----------------------------------------------------------------------
|
||||
// Stabilizer from cycle
|
||||
// -----------------------------------------------------------------------
|
||||
|
|
|
|||
|
|
@ -251,7 +251,7 @@ namespace seq {
|
|||
if (deriv)
|
||||
propagate_self_stabilizing(parent_re, deriv);
|
||||
euf::snode const* new_str = m_sg.drop_first(mem.m_str);
|
||||
return str_mem(new_str, deriv, mem.m_dep);
|
||||
return str_mem(mem.m, new_str, deriv, mem.m_dep);
|
||||
}
|
||||
|
||||
// -----------------------------------------------------------------
|
||||
|
|
@ -321,21 +321,6 @@ namespace seq {
|
|||
// Cycle detection and stabilizers
|
||||
// -----------------------------------------------------------------
|
||||
|
||||
// record current regex in the derivation history of a str_mem.
|
||||
// the history tracks a chain of (regex, id) pairs for cycle detection.
|
||||
// returns the updated str_mem.
|
||||
str_mem record_history(str_mem const& mem, euf::snode const* history_re);
|
||||
|
||||
// check if the derivation history of mem contains a cycle, i.e.,
|
||||
// the same regex id appears twice in the history chain.
|
||||
// if found, returns the cycle entry point regex; nullptr otherwise.
|
||||
euf::snode const* extract_cycle(str_mem const& mem) const;
|
||||
|
||||
// check if the derivation history exhibits a cycle.
|
||||
// returns true when the current regex matches a previously seen regex
|
||||
// in the history chain. used to trigger stabilizer introduction.
|
||||
bool detect_cycle(str_mem const& mem) const;
|
||||
|
||||
// compute a Kleene star stabilizer from a cycle.
|
||||
// given the regex at the cycle point and the current regex,
|
||||
// builds r* that over-approximates any number of cycle iterations.
|
||||
|
|
|
|||
|
|
@ -29,20 +29,20 @@ namespace smt {
|
|||
|
||||
struct tracked_str_eq : seq::str_eq {
|
||||
enode *m_l, *m_r;
|
||||
tracked_str_eq(euf::snode const* lhs, euf::snode const* rhs, enode* l, enode* r, seq::dep_tracker const &dep)
|
||||
: str_eq(lhs, rhs, dep), m_l(l), m_r(r) {}
|
||||
tracked_str_eq(ast_manager& m, euf::snode const* lhs, euf::snode const* rhs, enode* l, enode* r, seq::dep_tracker const &dep)
|
||||
: str_eq(m, lhs, rhs, dep), m_l(l), m_r(r) {}
|
||||
};
|
||||
|
||||
struct tracked_str_deq : seq::str_deq {
|
||||
sat::literal lit;
|
||||
tracked_str_deq(euf::snode const* lhs, euf::snode const* rhs, const sat::literal lit, seq::dep_tracker const &dep)
|
||||
: str_deq(lhs, rhs, dep), lit(lit) {}
|
||||
tracked_str_deq(ast_manager& m, euf::snode const* lhs, euf::snode const* rhs, const sat::literal lit, seq::dep_tracker const &dep)
|
||||
: str_deq(m, lhs, rhs, dep), lit(lit) {}
|
||||
};
|
||||
|
||||
struct tracked_str_mem : seq::str_mem {
|
||||
sat::literal lit;
|
||||
tracked_str_mem(euf::snode const* str, euf::snode const* regex, const sat::literal lit, seq::dep_tracker const &dep)
|
||||
: str_mem(str, regex, dep), lit(lit) {}
|
||||
tracked_str_mem(ast_manager& m, euf::snode const* str, euf::snode const* regex, const sat::literal lit, seq::dep_tracker const &dep)
|
||||
: str_mem(m, str, regex, dep), lit(lit) {}
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -222,9 +222,8 @@ namespace smt {
|
|||
return;
|
||||
euf::snode const* s1 = get_snode(e1);
|
||||
euf::snode const* s2 = get_snode(e2);
|
||||
seq::dep_tracker dep = nullptr;
|
||||
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(m, s1, s2, get_enode(v1), get_enode(v2), nullptr));
|
||||
m_last_constraint_added = ctx.get_scope_level();
|
||||
m_can_hot_restart = false;
|
||||
++m_eager_dirty;
|
||||
|
|
@ -269,10 +268,9 @@ namespace smt {
|
|||
else {
|
||||
euf::snode const* s1 = get_snode(e1);
|
||||
euf::snode const* s2 = get_snode(e2);
|
||||
const seq::dep_tracker dep = nullptr;
|
||||
ctx.push_trail(restore_vector(m_prop_queue));
|
||||
const expr_ref eq_expr(m.mk_eq(e1, e2), m);
|
||||
m_prop_queue.push_back(deq_item(s1, s2, ~ctx.get_literal(eq_expr), dep));
|
||||
m_prop_queue.push_back(deq_item(m, s1, s2, ~ctx.get_literal(eq_expr), nullptr));
|
||||
m_last_constraint_added = ctx.get_scope_level();
|
||||
m_can_hot_restart = false;
|
||||
++m_eager_dirty;
|
||||
|
|
@ -296,10 +294,9 @@ namespace smt {
|
|||
if (m_seq.str.is_in_re(e, s, re)) {
|
||||
euf::snode const* sn_str = get_snode(s);
|
||||
euf::snode const* sn_re = get_snode(re);
|
||||
const seq::dep_tracker dep = nullptr;
|
||||
if (is_true) {
|
||||
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(m, sn_str, sn_re, lit, nullptr));
|
||||
m_last_constraint_added = ctx.get_scope_level();
|
||||
m_can_hot_restart = false;
|
||||
++m_eager_dirty;
|
||||
|
|
@ -311,7 +308,7 @@ namespace smt {
|
|||
const expr_ref re_compl(m_seq.re.mk_complement(re), m);
|
||||
euf::snode const* sn_re_compl = get_snode(re_compl.get());
|
||||
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(m, sn_str, sn_re_compl, lit, nullptr));
|
||||
m_last_constraint_added = ctx.get_scope_level();
|
||||
m_can_hot_restart = false;
|
||||
++m_eager_dirty;
|
||||
|
|
@ -973,6 +970,16 @@ namespace smt {
|
|||
SASSERT(!node->is_general_conflict());
|
||||
node->clear_reason();
|
||||
}
|
||||
else if (node->reason() == seq::backtrack_reason::sibling) {
|
||||
// A non-general sibling conflict (a loop cut, or a closure
|
||||
// that escaped to an ancestor) is valid only for the path it
|
||||
// was found on; the changed external context may now admit a
|
||||
// model. Clear it (and its recorded deps) for re-exploration.
|
||||
// Self-contained sibling closures are general and were skipped
|
||||
// above.
|
||||
SASSERT(!node->is_general_conflict());
|
||||
node->clear_local_conflict();
|
||||
}
|
||||
|
||||
if (node->is_external_conflict())
|
||||
node->clear_local_conflict();
|
||||
|
|
@ -1291,11 +1298,11 @@ namespace smt {
|
|||
std::cout << "The root node contained " << m_nielsen.root()->str_mems().size() << " memberships and " << m_nielsen.root()->str_eqs().size() << " equalities" << std::endl;
|
||||
unsigned idx = 0;
|
||||
for (auto& eq : m_nielsen.root()->str_eqs()) {
|
||||
std::cout << "[" << (idx++) << "]: " << seq::eq_pp(eq, m) << "\n";
|
||||
std::cout << "[" << (idx++) << "]: " << seq::eq_pp(eq) << "\n";
|
||||
}
|
||||
idx = 0;
|
||||
for (auto& mem : m_nielsen.root()->str_mems()) {
|
||||
std::cout << "[" << (idx++) << "]: " << seq::mem_pp(mem, m) << "\n";
|
||||
std::cout << "[" << (idx++) << "]: " << seq::mem_pp(mem) << "\n";
|
||||
}
|
||||
std::flush(std::cout);
|
||||
#endif
|
||||
|
|
@ -2033,7 +2040,7 @@ namespace smt {
|
|||
literal_vector dep_lits;
|
||||
|
||||
for (unsigned idx : mem_indices) {
|
||||
std::cout << seq::mem_pp(mems[idx], m) << std::endl;
|
||||
std::cout << seq::mem_pp(mems[idx]) << std::endl;
|
||||
seq::deps_to_lits(m_nielsen.dep_mgr(), mems[idx].m_dep, eqs, dep_lits);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -2194,72 +2194,6 @@ static void test_explain_conflict_mixed_eq_mem() {
|
|||
ng.test_aux_explain_conflict(eqs, mem_literals);
|
||||
}
|
||||
|
||||
// test subsumption pruning during solve: a node whose constraint set
|
||||
// is a superset of a known-unsat node is pruned
|
||||
static void test_subsumption_pruning_unsat() {
|
||||
std::cout << "test_subsumption_pruning_unsat\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 const* a = sg.mk_char('A');
|
||||
euf::snode const* b = sg.mk_char('B');
|
||||
|
||||
// A = B is an immediate conflict (symbol clash).
|
||||
// Any branch that inherits this equation should be pruned.
|
||||
ng.add_str_eq(a, b);
|
||||
const auto result = ng.solve();
|
||||
SASSERT(result == seq::nielsen_graph::search_result::unsat);
|
||||
|
||||
// root should have conflict set
|
||||
SASSERT(ng.root()->is_general_conflict());
|
||||
}
|
||||
|
||||
// test that subsumption sets backtrack_reason::subsumption
|
||||
static void test_subsumption_reason_set() {
|
||||
std::cout << "test_subsumption_reason_set\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 const* x = sg.mk_var(symbol("x"), sg.get_str_sort());
|
||||
euf::snode const* y = sg.mk_var(symbol("y"), sg.get_str_sort());
|
||||
euf::snode const* a = sg.mk_char('A');
|
||||
euf::snode const* b = sg.mk_char('B');
|
||||
|
||||
// x·A = y·B: after Nielsen splitting, children will have A=B
|
||||
// which is unsat. The subsumption pruning may fire on sibling
|
||||
// branches that inherit the same conflict.
|
||||
euf::snode const* xa = sg.mk_concat(x, a);
|
||||
euf::snode const* yb = sg.mk_concat(y, b);
|
||||
ng.add_str_eq(xa, yb);
|
||||
|
||||
const auto result = ng.solve();
|
||||
SASSERT(result == seq::nielsen_graph::search_result::unsat);
|
||||
|
||||
// check that at least one node has subsumption reason
|
||||
bool found_subsumption = false;
|
||||
for (const seq::nielsen_node* nd : ng.nodes()) {
|
||||
if (nd->reason() == seq::backtrack_reason::subsumption) {
|
||||
found_subsumption = true;
|
||||
SASSERT(nd->is_general_conflict());
|
||||
break;
|
||||
}
|
||||
}
|
||||
// subsumption may or may not fire depending on search order;
|
||||
// the important thing is the solve result is correct.
|
||||
// If it does fire, the reason must be subsumption.
|
||||
(void)found_subsumption;
|
||||
}
|
||||
|
||||
// test generate_length_constraints: basic equation x . y = A . B
|
||||
static void test_length_constraints_basic() {
|
||||
std::cout << "test_length_constraints_basic\n";
|
||||
|
|
@ -3971,8 +3905,6 @@ void tst_seq_nielsen() {
|
|||
test_var_nielsen_substitution_types();
|
||||
test_explain_conflict_mem_only();
|
||||
test_explain_conflict_mixed_eq_mem();
|
||||
test_subsumption_pruning_unsat();
|
||||
test_subsumption_reason_set();
|
||||
test_length_constraints_basic();
|
||||
test_length_constraints_trivial_skip();
|
||||
test_length_constraints_empty();
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue