dejavu
Fast probabilistic symmetry detection.
Loading...
Searching...
No Matches
bfs.h
Go to the documentation of this file.
1// Copyright 2024 Markus Anders
2// This file is part of dejavu 2.0.
3// See LICENSE for extended copyright information.
4
5#ifndef DEJAVU_BFS_H
6#define DEJAVU_BFS_H
7
8#include "ir.h"
9
10namespace dejavu {
11 namespace search_strategy {
12
16 class bfs_ir {
17 timed_print& gl_printer;
18 groups::automorphism_workspace& gl_automorphism;
19
20 public:
23 // TODO some of this should go into shared_tree
24 // statistics
25 int s_total_prune = 0;
26 int s_total_kept = 0;
32 gl_printer(printer), gl_automorphism(automorphism) {}
33
34 void do_a_level(sgraph* g, dejavu_hook* hook, ir::shared_tree& ir_tree, ir::controller& local_state,
35 std::function<ir::type_selector_hook> *selector) {
36 int current_level = ir_tree.get_finished_up_to();
37
39 s_total_prune = 0;
40 s_total_kept = 0;
43
45
46 queue_up_level(selector, ir_tree, current_level);
47 work_on_todo(g, hook, &ir_tree, local_state);
48 ir_tree.set_finished_up_to(current_level + 1);
49 }
50
51 static int next_level_estimate(ir::shared_tree& ir_tree, std::function<ir::type_selector_hook> *selector) {
52 const int base_pos = ir_tree.get_finished_up_to();
53 const auto start_node = ir_tree.get_level(base_pos);
54 dej_assert(start_node != nullptr);
55 const auto level_size = ir_tree.get_level_size(base_pos);
56 auto next_node_save = start_node->get_save();
57 auto c = next_node_save->get_coloring();
58 auto base_pos_ = next_node_save->get_base_position();
59 int col = (*selector)(c, base_pos_);
60 return level_size * (c->ptn[col] + 1);
61 }
62
63 static void queue_up_level(std::function<ir::type_selector_hook> *selector, ir::shared_tree& ir_tree,
64 int base_pos) {
65 auto start_node = ir_tree.get_level(base_pos);
66 dej_assert(start_node != nullptr);
67 while(!start_node->get_base()) {
68 start_node = start_node->get_next();
69 }
70 start_node = start_node->get_next();
71
72 const auto level_size = ir_tree.get_level_size(base_pos);
73 auto next_node = start_node;
74 bool reserve = false;
75
76 do {
77 auto next_node_save = next_node->get_save();
78 auto c = next_node_save->get_coloring();
79 auto this_base_pos = next_node_save->get_base_position();
80 int col = (*selector)(c, this_base_pos);
81 if(!reserve && col >= 0) {
82 const int expected_for_base = c->ptn[col] + 1;
83 ir_tree.stored_deviation.start(expected_for_base);
84 ir_tree.queue_reserve(expected_for_base * level_size);
85 reserve = true;
86 }
87
88 if(col >= 0) {
89 for (int i = 0; i < c->ptn[col] + 1; ++i) {
90 ir_tree.queue_missing_node({next_node, c->lab[col + i]});
91 }
92 }
93 next_node = next_node->get_next();
94 } while(next_node != start_node);
95 }
96
97 void compute_node(sgraph* g, dejavu_hook* hook, ir::shared_tree* ir_tree, ir::controller& local_state,
98 ir::tree_node* node, const int v, ir::limited_save* last_load) {
99 auto next_node_save = node->get_save();
100
101 // node is already pruned
102 const bool is_pruned = node->get_prune();
103 if(is_pruned && h_use_deviation_pruning) {
106 dej_assert(!node->get_base());
107 return;
108 }
109
110 // special code for automorphism pruning on base size 2
111 const int parent_node_base_pos = node->get_save()->get_base_position()-1;
112 const int parent_node_base_vert = parent_node_base_pos>=0?
113 node->get_save()->get_base()[parent_node_base_pos]:-1;
114 const int vert_on_base = parent_node_base_pos>=0 ?
115 (*local_state.compare_base_vertex)[parent_node_base_pos] : -1;
116 const int vert_on_base_sl = parent_node_base_pos==-1 ?
117 (*local_state.compare_base_vertex)[0] : -1;
118 if(parent_node_base_pos == 0 && !ir_tree->h_bfs_top_level_orbit.represents_orbit(parent_node_base_vert)) {
120 return;
121 }
122
123 if(parent_node_base_pos == -1 && v != vert_on_base_sl &&
124 ir_tree->h_bfs_top_level_orbit.are_in_same_orbit(v, vert_on_base_sl)) {
126 return;
127 }
128
129 constexpr int size_threshold = 1000;
130
131 // do efficient loading if parent is the same as previous load
132 if(next_node_save != last_load || g->v_size < size_threshold) { // TODO heuristic to check how much has changed
133 local_state.use_reversible(false); // potentially loads more efficiently
134 local_state.load_reduced_state(*next_node_save);
135 } else {
136 local_state.move_to_parent();
137 local_state.load_reduced_state_without_coloring(*next_node_save);
138 }
139
140 if(local_state.s_base_pos > 0) local_state.use_increase_deviation(true);
141
142
144
145 // do computation
146 local_state.reset_trace_equal();
147 local_state.use_reversible(g->v_size >= size_threshold);
148 //local_state.use_reversible(false);
149 local_state.use_trace_early_out(true);
150 local_state.move_to_child(g, v);
151
152 // we want to keep track of whether we are on the base or not
153 const bool parent_is_base = node->get_base();
154 const bool is_base = parent_is_base && (v == (*local_state.compare_base_vertex)[local_state.s_base_pos - 1]);
155
157
158 bool cert = true;
159 if(g->v_size == local_state.c->cells && local_state.T->trace_equal()) {
160 gl_automorphism.write_color_diff(local_state.c->vertex_to_col, local_state.leaf_color.lab);
161 cert = local_state.certify(g, gl_automorphism);
162 if(cert) {
163 ir_tree->h_bfs_top_level_orbit.add_automorphism_to_orbit(gl_automorphism);
164
165 // Output automorphism
166 if (hook)
167 (*hook)(g->v_size, gl_automorphism.p(), gl_automorphism.nsupp(),
168 gl_automorphism.supp());
169 }
171 gl_automorphism.reset();
172
173 if(parent_node_base_pos == 0 && vert_on_base == parent_node_base_vert)
174 ++ir_tree->h_bfs_automorphism_pw;
175 }
176
177
178 // could check for matching OPP to base and prune based on that
179 // but that invalidates certain invariant applications that I use, so these strategies are somewhat
180 // incompatible
181 /*if(local_state.T->trace_equal() && cert && g->v_size != local_state.c->cells && !is_base) {
182 const bool there_is_diff = local_state.there_is_difference_to_base();
183 if (!there_is_diff) {
184 gl_automorphism.reset();
185 local_state.singleton_automorphism_base(&gl_automorphism);
186 const bool certify_sparse = local_state.certify(g, gl_automorphism);
187 if(certify_sparse) {
188 std::cout << "found here" << std::endl;
189 if (hook)
190 (*hook)(g->v_size, gl_automorphism.perm(), gl_automorphism.nsupport(),
191 gl_automorphism.support());
192 //sh_schreier->sift(*gl_schreier, *gl_automorphism, false);
193 }
194 }
195 }*/
196
197 if(local_state.T->trace_equal() && cert) {
198 ++s_total_kept;
199 auto new_save = new ir::limited_save();
200 local_state.save_reduced_state(*new_save);
201 ir_tree->add_node(local_state.s_base_pos, new_save, node, is_base);
202 if(local_state.s_base_pos > 1 && !h_use_deviation_pruning)
203 ir_tree->record_add_invariant(v, local_state.T->get_hash());
204 } else {
205 dej_assert(!is_base);
206 // deviation map
207 if(local_state.s_base_pos > 1) {
209 const int first_level_v = node->get_save()->get_base()[0];
210 ir_tree->record_add_invariant(first_level_v, local_state.T->get_hash());
211 ir_tree->record_add_invariant(v, local_state.T->get_hash());
212 }
214 if (parent_is_base) ir_tree->stored_deviation.record_deviation(local_state.T->get_hash());
215 else {
216 if (!ir_tree->stored_deviation.check_deviation(local_state.T->get_hash())) {
217 dej_assert(!parent_is_base);
218 node->prune();
219 }
220 }
221 } else {
222 ir_tree->record_add_invariant(v, local_state.T->get_hash());
223 }
224 }
225
226 // keep track how many we computed for deviation map
227 if(parent_is_base && local_state.s_base_pos > 1 && local_state.T->trace_equal()) {
229 }
230 }
231
232 void work_on_todo(sgraph* g, dejavu_hook* hook, ir::shared_tree* ir_tree, ir::controller& local_state) {
233 ir::limited_save* last_load = nullptr;
234 int s_count_nodes = 0;
235 while(!ir_tree->queue_missing_node_empty()) {
236 ++s_count_nodes;
237 if((s_count_nodes & 0x00000FFF) == 0)
238 gl_printer.progress_current_method("bfs nodes=" +std::to_string(s_count_nodes)+
239 ", nodes_kept="+std::to_string(s_total_kept));
240 const auto todo = ir_tree->queue_missing_node_pop();
241 compute_node(g, hook, ir_tree, local_state, todo.first, todo.second, last_load);
242 last_load = todo.first->get_save();
243 }
244 }
245 };
246 }
247}
248
249#endif //DEJAVU_BFS_H
Workspace for sparse automorphisms.
Definition: groups.h:68
void write_color_diff(const int *vertex_to_col, const int *col_to_vertex)
Definition: groups.h:160
dej_nodiscard int nsupp() const
Definition: groups.h:497
dej_nodiscard int * p() const
Definition: groups.h:483
dej_nodiscard int * supp() const
Definition: groups.h:490
bool are_in_same_orbit(const int v1, const int v2)
Definition: groups.h:586
dej_nodiscard bool represents_orbit(const int v) const
Definition: groups.h:550
void add_automorphism_to_orbit(const int *p, const int nsupp, const int *supp)
Definition: groups.h:613
void record_no_deviation()
Definition: ir.h:1783
bool check_deviation(unsigned long deviation)
Definition: ir.h:1789
void start(const int h_expected_for_base)
Definition: ir.h:1768
void record_deviation(unsigned long deviation)
Definition: ir.h:1776
Reduced IR save state.
Definition: ir.h:47
std::vector< int > & get_base()
Definition: ir.h:97
dej_nodiscard int get_base_position() const
Definition: ir.h:90
IR tree structure.
Definition: ir.h:1982
tree_node * get_level(int level)
Definition: ir.h:2230
void add_node(int level, limited_save *data, tree_node *parent, bool is_base=false)
Definition: ir.h:2179
void queue_reserve(const int n)
Definition: ir.h:2142
int get_current_level_size()
Definition: ir.h:2234
void queue_missing_node(missing_node node)
Definition: ir.h:2146
int get_level_size(int level)
Definition: ir.h:2242
int h_bfs_automorphism_pw
Definition: ir.h:1997
bool queue_missing_node_empty()
Definition: ir.h:2150
deviation_map stored_deviation
Definition: ir.h:1999
groups::orbit h_bfs_top_level_orbit
Definition: ir.h:1996
void set_finished_up_to(const int new_finished_up_to)
Definition: ir.h:2226
void record_add_invariant(int v, unsigned long inv)
Definition: ir.h:2175
dej_nodiscard int get_finished_up_to() const
Definition: ir.h:2222
missing_node queue_missing_node_pop()
Definition: ir.h:2154
dej_nodiscard unsigned long get_hash() const
Definition: trace.h:257
dej_nodiscard bool trace_equal() const
Definition: trace.h:272
A node of an IR tree.
Definition: ir.h:1912
dej_nodiscard bool get_prune() const
Definition: ir.h:1948
dej_nodiscard bool get_base() const
Definition: ir.h:1963
limited_save * get_save()
Definition: ir.h:1941
Breadth-first search.
Definition: bfs.h:16
bfs_ir(timed_print &printer, groups::automorphism_workspace &automorphism)
Definition: bfs.h:31
static void queue_up_level(std::function< ir::type_selector_hook > *selector, ir::shared_tree &ir_tree, int base_pos)
Definition: bfs.h:63
void work_on_todo(sgraph *g, dejavu_hook *hook, ir::shared_tree *ir_tree, ir::controller &local_state)
Definition: bfs.h:232
void do_a_level(sgraph *g, dejavu_hook *hook, ir::shared_tree &ir_tree, ir::controller &local_state, std::function< ir::type_selector_hook > *selector)
Definition: bfs.h:34
void compute_node(sgraph *g, dejavu_hook *hook, ir::shared_tree *ir_tree, ir::controller &local_state, ir::tree_node *node, const int v, ir::limited_save *last_load)
Definition: bfs.h:97
static int next_level_estimate(ir::shared_tree &ir_tree, std::function< ir::type_selector_hook > *selector)
Definition: bfs.h:51
Internal graph data structure.
Definition: graph.h:19
int v_size
Definition: graph.h:48
Prints information to the console.
Definition: utility.h:237
void progress_current_method(const std::string &print) const
Definition: utility.h:301
Definition: bfs.h:10
Controls movement in IR tree.
Definition: ir.h:130
std::vector< int > * compare_base_vertex
Definition: ir.h:141
void use_increase_deviation(bool deviation_inc_active)
Definition: ir.h:843
coloring * c
Definition: ir.h:132
void save_reduced_state(limited_save &state)
Definition: ir.h:883
void move_to_child(sgraph *g, int v)
Definition: ir.h:989
void use_reversible(const bool reversible)
Definition: ir.h:816
void use_trace_early_out(bool trace_early_out)
Definition: ir.h:831
void load_reduced_state_without_coloring(limited_save &state)
Definition: ir.h:910
void load_reduced_state(limited_save &state)
Definition: ir.h:893
void reset_trace_equal()
Definition: ir.h:873
void move_to_parent()
Definition: ir.h:1057
bool certify(sgraph *g, groups::automorphism_workspace &automorphism)
Definition: ir.h:1123
bool there_is_difference_to_base_including_singles(int domain_size)
Definition: ir.h:513
coloring leaf_color
Definition: ir.h:144
#define dej_assert(expr)
Definition: utility.h:40
std::function< void(int, const int *, int, const int *)> dejavu_hook
Definition: utility.h:95