From ad50f6219456e87669500396b4ad48e102807144 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 19 Jan 2026 01:51:10 +0000 Subject: [PATCH 1/5] Initial plan From a051ba31f914efa1f7f91325d43f199ae9985d2f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 19 Jan 2026 02:16:55 +0000 Subject: [PATCH 2/5] Replace std::vector with Z3's vector/svector types in theory_finite_set_lattice_refutation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- .../theory_finite_set_lattice_refutation.cpp | 89 ++++++++----------- .../theory_finite_set_lattice_refutation.h | 15 ++-- 2 files changed, 43 insertions(+), 61 deletions(-) diff --git a/src/smt/theory_finite_set_lattice_refutation.cpp b/src/smt/theory_finite_set_lattice_refutation.cpp index 0f467aaa9..1b955938d 100644 --- a/src/smt/theory_finite_set_lattice_refutation.cpp +++ b/src/smt/theory_finite_set_lattice_refutation.cpp @@ -12,33 +12,31 @@ Module Name: #include "smt/smt_theory.h" #include "smt/theory_finite_set.h" #include "smt/smt_context.h" -#include "iostream" +#include "util/uint_set.h" -const int NUM_WORDS = 5; -// some example have shown, the introduction of large conflict clauses can severely slow down refutation +// some examples have shown, the introduction of large conflict clauses can severely slow down refutation const int MAX_DECISION_LITERALS = 10; +const int MAX_VARS = 320; namespace smt { reachability_matrix::reachability_matrix(context &ctx, theory_finite_set_lattice_refutation &t_lattice) - : reachable(NUM_WORDS * NUM_WORDS * 64, 0), links(NUM_WORDS * NUM_WORDS * 64 * 64, {nullptr, nullptr}), - link_dls(NUM_WORDS * NUM_WORDS * 64 * 64, 0), non_links(NUM_WORDS * NUM_WORDS * 64), - non_link_justifications(NUM_WORDS * NUM_WORDS * 64 * 64, {nullptr, nullptr}), largest_var(0), - max_size(NUM_WORDS * 64), ctx(ctx), t_lattice_refutation(t_lattice) {} + : reachable(MAX_VARS), links(MAX_VARS * MAX_VARS, {nullptr, nullptr}), + link_dls(MAX_VARS * MAX_VARS, 0u), non_links(MAX_VARS), + non_link_justifications(MAX_VARS * MAX_VARS, {nullptr, nullptr}), largest_var(0), + max_size(MAX_VARS), ctx(ctx), t_lattice_refutation(t_lattice) { + // Initialize the uint_sets for each row + for (int i = 0; i < MAX_VARS; i++) { + reachable[i].reset(); + non_links[i].reset(); + } + } int reachability_matrix::get_max_var() { return largest_var; } - inline int reachability_matrix::get_word_index(int row, int col) const { - return (row * NUM_WORDS) + (col / 64); - }; - - inline uint64_t reachability_matrix::get_bitmask(int col) const { - return 1ull << (col % 64); - }; - bool reachability_matrix::is_reachability_forbidden(theory_var source, theory_var dest) { - return non_links[get_word_index(source, dest)] & get_bitmask(dest); + return non_links[source].contains(dest); } bool reachability_matrix::in_bounds(theory_var source, theory_var dest) { @@ -46,7 +44,7 @@ namespace smt { } bool reachability_matrix::is_reachable(theory_var source, theory_var dest) { - return reachable[get_word_index(source, dest)] & get_bitmask(dest); + return reachable[source].contains(dest); } bool reachability_matrix::is_linked(theory_var source, theory_var dest) { @@ -54,17 +52,22 @@ namespace smt { } bool reachability_matrix::bitwise_or_rows(int source_dest, int source) { - bool changes = false; - for (int i = 0; i < NUM_WORDS; i++) { - uint64_t old_value = reachable[source_dest * NUM_WORDS + i]; - uint64_t new_value = reachable[source_dest * NUM_WORDS + i] | reachable[source * NUM_WORDS + i]; - if (old_value == new_value) { - continue; + // Save old state for potential rollback + uint_set old_reachable = reachable[source_dest]; + + // Compute union: reachable[source_dest] |= reachable[source] + reachable[source_dest] |= reachable[source]; + + // Check if anything changed + bool changes = !(old_reachable == reachable[source_dest]); + if (changes) { + ctx.push_trail(value_trail(reachable[source_dest])); + // Check for conflicts with newly added reachabilities + for (unsigned dest : reachable[source]) { + if (!old_reachable.contains(dest)) { + check_reachability_conflict(source_dest, dest); + } } - ctx.push_trail(value_trail(reachable[source_dest * NUM_WORDS + i])); - reachable[source_dest * NUM_WORDS + i] = new_value; - changes = true; - check_reachability_conflict_word(source_dest, i); } return changes; } @@ -76,9 +79,8 @@ namespace smt { ctx.push_trail(value_trail(largest_var)); largest_var = std::max({largest_var, source, dest}); - int word_idx = get_word_index(source, dest); - ctx.push_trail(value_trail(reachable[word_idx])); - reachable[word_idx] |= get_bitmask(dest); + ctx.push_trail(value_trail(reachable[source])); + reachable[source].insert(dest); ctx.push_trail(value_trail(links[source * max_size + dest])); links[source * max_size + dest] = reachability_witness; ctx.push_trail(value_trail(link_dls[source * max_size + dest])); @@ -95,13 +97,6 @@ namespace smt { } bitwise_or_rows(i, source); } - if (conflict_word >= 0 && conflict_row >= 0) { - for (int i = conflict_word * 64; i < conflict_word * 64 + 64; i++) { - check_reachability_conflict(conflict_row, i); - } - conflict_word = -1; - conflict_row = -1; - } return true; } @@ -112,8 +107,8 @@ namespace smt { } ctx.push_trail(value_trail(largest_var)); largest_var = std::max({largest_var, source, dest}); - ctx.push_trail(value_trail(non_links[get_word_index(source, dest)])); - non_links[get_word_index(source, dest)] |= get_bitmask(dest); + ctx.push_trail(value_trail(non_links[source])); + non_links[source].insert(dest); ctx.push_trail(value_trail(non_link_justifications[source * max_size + dest])); non_link_justifications[source * max_size + dest] = non_reachability_witness; check_reachability_conflict(source, dest); @@ -162,7 +157,7 @@ namespace smt { void reachability_matrix::get_path(theory_var source, theory_var dest, vector &path, int &num_decisions) { SASSERT(is_reachable(source, dest)); - vector visited(max_size, false); + bool_vector visited(max_size, false); if (source != dest) { visited[source] = true; } @@ -207,22 +202,12 @@ namespace smt { return false; } - bool reachability_matrix::check_reachability_conflict_word(int row, int word) { - if (reachable[row * NUM_WORDS + word] & non_links[row * NUM_WORDS + word]) { - // somewhere in this word there is a conflict - conflict_row = row; - conflict_word = word; - return true; - } - return false; - } - void reachability_matrix::print_relations() { TRACE(finite_set, tout << "largest_var: " << largest_var); for (size_t i = 0; i < max_size; i++) { for (size_t j = 0; j < max_size; j++) { - if ((reachable[get_word_index(i, j)] & get_bitmask(j)) || is_reachable(i, j)) { - TRACE(finite_set, tout << "reachable: " << i << "->" << j << " :" << is_reachable(i, j)); + if (is_reachable(i, j)) { + TRACE(finite_set, tout << "reachable: " << i << "->" << j); } } } diff --git a/src/smt/theory_finite_set_lattice_refutation.h b/src/smt/theory_finite_set_lattice_refutation.h index 22f726864..e33a9c7fa 100644 --- a/src/smt/theory_finite_set_lattice_refutation.h +++ b/src/smt/theory_finite_set_lattice_refutation.h @@ -12,6 +12,7 @@ Module Name: #include "ast/finite_set_decl_plugin.h" #include "ast/rewriter/finite_set_axioms.h" #include "smt/smt_theory.h" +#include "util/uint_set.h" namespace smt { class context; @@ -19,11 +20,11 @@ namespace smt { class theory_finite_set_lattice_refutation; class reachability_matrix { - std::vector reachable; - std::vector links; - std::vector link_dls; - std::vector non_links; - std::vector non_link_justifications; + vector reachable; + vector links; + vector link_dls; + vector non_links; + vector non_link_justifications; int largest_var; @@ -32,12 +33,9 @@ namespace smt { context &ctx; theory_finite_set_lattice_refutation &t_lattice_refutation; int conflict_row = -1; - int conflict_word = -1; // sets source_dest |= dest, and pushing the changed words to the trail bool bitwise_or_rows(int source_dest, int source); - inline int get_word_index(int row, int col) const; - inline uint64_t get_bitmask(int col) const; public: void get_path(theory_var source, theory_var dest, vector &path, int &num_decisions); @@ -48,7 +46,6 @@ namespace smt { bool is_linked(theory_var source, theory_var dest); bool check_reachability_conflict(theory_var source, theory_var dest); - bool check_reachability_conflict_word(int row, int word); bool set_reachability(theory_var source, theory_var dest, enode_pair reachability_witness); bool set_non_reachability(theory_var source, theory_var dest, enode_pair non_reachability_witness); From 4be6d1894ff8e4a2f43c0ec30df7784f8945d592 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 19 Jan 2026 02:20:15 +0000 Subject: [PATCH 3/5] Address code review feedback: fix conflict checking loop and constructor initialization Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/theory_finite_set_lattice_refutation.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_finite_set_lattice_refutation.cpp b/src/smt/theory_finite_set_lattice_refutation.cpp index 1b955938d..068f41ce2 100644 --- a/src/smt/theory_finite_set_lattice_refutation.cpp +++ b/src/smt/theory_finite_set_lattice_refutation.cpp @@ -21,10 +21,11 @@ const int MAX_VARS = 320; namespace smt { reachability_matrix::reachability_matrix(context &ctx, theory_finite_set_lattice_refutation &t_lattice) : reachable(MAX_VARS), links(MAX_VARS * MAX_VARS, {nullptr, nullptr}), - link_dls(MAX_VARS * MAX_VARS, 0u), non_links(MAX_VARS), + link_dls(), non_links(MAX_VARS), non_link_justifications(MAX_VARS * MAX_VARS, {nullptr, nullptr}), largest_var(0), max_size(MAX_VARS), ctx(ctx), t_lattice_refutation(t_lattice) { - // Initialize the uint_sets for each row + // Initialize the vectors + link_dls.resize(MAX_VARS * MAX_VARS, 0); for (int i = 0; i < MAX_VARS; i++) { reachable[i].reset(); non_links[i].reset(); @@ -63,7 +64,7 @@ namespace smt { if (changes) { ctx.push_trail(value_trail(reachable[source_dest])); // Check for conflicts with newly added reachabilities - for (unsigned dest : reachable[source]) { + for (unsigned dest : reachable[source_dest]) { if (!old_reachable.contains(dest)) { check_reachability_conflict(source_dest, dest); } From e3c1610335e41605b4fdb753dacecd2db10ca5cd Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 19 Jan 2026 02:22:55 +0000 Subject: [PATCH 4/5] Fix trail mechanism to capture state before modification Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/theory_finite_set_lattice_refutation.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_finite_set_lattice_refutation.cpp b/src/smt/theory_finite_set_lattice_refutation.cpp index 068f41ce2..4e046d34e 100644 --- a/src/smt/theory_finite_set_lattice_refutation.cpp +++ b/src/smt/theory_finite_set_lattice_refutation.cpp @@ -25,7 +25,7 @@ namespace smt { non_link_justifications(MAX_VARS * MAX_VARS, {nullptr, nullptr}), largest_var(0), max_size(MAX_VARS), ctx(ctx), t_lattice_refutation(t_lattice) { // Initialize the vectors - link_dls.resize(MAX_VARS * MAX_VARS, 0); + link_dls.resize(MAX_VARS * MAX_VARS, static_cast(0)); for (int i = 0; i < MAX_VARS; i++) { reachable[i].reset(); non_links[i].reset(); @@ -53,16 +53,18 @@ namespace smt { } bool reachability_matrix::bitwise_or_rows(int source_dest, int source) { - // Save old state for potential rollback + // Save old state before modification uint_set old_reachable = reachable[source_dest]; + // Push trail before modifying + ctx.push_trail(value_trail(reachable[source_dest])); + // Compute union: reachable[source_dest] |= reachable[source] reachable[source_dest] |= reachable[source]; // Check if anything changed bool changes = !(old_reachable == reachable[source_dest]); if (changes) { - ctx.push_trail(value_trail(reachable[source_dest])); // Check for conflicts with newly added reachabilities for (unsigned dest : reachable[source_dest]) { if (!old_reachable.contains(dest)) { From 1c6ffd2161cf82789bd1befa66c8065eb022f977 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 19 Jan 2026 02:25:02 +0000 Subject: [PATCH 5/5] Optimize bitwise_or_rows and simplify constructor initialization Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- .../theory_finite_set_lattice_refutation.cpp | 36 ++++++++++++------- 1 file changed, 23 insertions(+), 13 deletions(-) diff --git a/src/smt/theory_finite_set_lattice_refutation.cpp b/src/smt/theory_finite_set_lattice_refutation.cpp index 4e046d34e..c6e05a422 100644 --- a/src/smt/theory_finite_set_lattice_refutation.cpp +++ b/src/smt/theory_finite_set_lattice_refutation.cpp @@ -25,7 +25,7 @@ namespace smt { non_link_justifications(MAX_VARS * MAX_VARS, {nullptr, nullptr}), largest_var(0), max_size(MAX_VARS), ctx(ctx), t_lattice_refutation(t_lattice) { // Initialize the vectors - link_dls.resize(MAX_VARS * MAX_VARS, static_cast(0)); + link_dls.resize(MAX_VARS * MAX_VARS, 0); for (int i = 0; i < MAX_VARS; i++) { reachable[i].reset(); non_links[i].reset(); @@ -53,26 +53,36 @@ namespace smt { } bool reachability_matrix::bitwise_or_rows(int source_dest, int source) { - // Save old state before modification - uint_set old_reachable = reachable[source_dest]; + // Check if there's anything to add + bool has_new_elements = false; + for (unsigned dest : reachable[source]) { + if (!reachable[source_dest].contains(dest)) { + has_new_elements = true; + break; + } + } - // Push trail before modifying + if (!has_new_elements) { + return false; + } + + // Push trail before modifying (captures current state for undo) ctx.push_trail(value_trail(reachable[source_dest])); + // Save elements before modification for conflict checking + uint_set old_reachable = reachable[source_dest]; + // Compute union: reachable[source_dest] |= reachable[source] reachable[source_dest] |= reachable[source]; - // Check if anything changed - bool changes = !(old_reachable == reachable[source_dest]); - if (changes) { - // Check for conflicts with newly added reachabilities - for (unsigned dest : reachable[source_dest]) { - if (!old_reachable.contains(dest)) { - check_reachability_conflict(source_dest, dest); - } + // Check for conflicts with newly added reachabilities + for (unsigned dest : reachable[source_dest]) { + if (!old_reachable.contains(dest)) { + check_reachability_conflict(source_dest, dest); } } - return changes; + + return true; } bool reachability_matrix::set_reachability(theory_var source, theory_var dest, enode_pair reachability_witness) {