dejavu
Fast probabilistic symmetry detection.
Loading...
Searching...
No Matches
ir.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_IR_H
6#define DEJAVU_IR_H
7
8#include <unordered_map>
9#include "refinement.h"
10#include "coloring.h"
11#include "graph.h"
12#include "trace.h"
13#include "groups.h"
14
15namespace dejavu {
16
23 namespace ir {
31 enum ir_mode {
33 };
34
38 typedef int type_selector_hook(const coloring *, const int);
39
48 // TODO enable a "compressed state" only consisting of base (but code outside should be oblivious to it)
49 // TODO this is only supposed to be an "incomplete" state -- should there be complete states?
50
51 std::vector<int> base_vertex;
52 coloring c;
53 unsigned long invariant = 0;
54 int trace_position = 0;
55 int base_position = 0;
56 public:
57 void save(std::vector<int>& s_base_vertex, coloring &s_c, unsigned long s_invariant, int s_trace_position,
58 int s_base_position) {
59 this->base_vertex = s_base_vertex;
60 this->c.copy_any(&s_c);
61 this->invariant = s_invariant;
62 this->trace_position = s_trace_position;
63 this->base_position = s_base_position;
64 }
65
70 return &c;
71 }
72
76 dej_nodiscard unsigned long get_invariant_hash() const {
77 return invariant;
78 }
79
84 return trace_position;
85 }
86
91 return base_position;
92 }
93
97 std::vector<int>& get_base() {
98 return base_vertex;
99 }
100 };
101
105 struct base_info {
106 int color;
108 int cells;
113 unsigned long trace_hash;
115 base_info(int selColor, int colorSz, int cellNum, int touchedColorListPt, int singletonPt, int tracePos,
116 unsigned long traceHash) :
117 color(selColor), color_sz(colorSz), cells(cellNum), touched_color_list_pt(touchedColorListPt),
118 singleton_pt(singletonPt), trace_pos(tracePos), trace_hash(traceHash) {}
119 };
120
130 struct controller {
131 public:
132 coloring *c = nullptr;
133 trace *T = nullptr;
135 std::vector<int> singletons;
136 std::vector<int>* compare_singletons = nullptr;
138 std::vector<int> base_vertex;
139 std::vector<base_info> base;
141 std::vector<int>* compare_base_vertex = nullptr;
142 std::vector<base_info>*compare_base = nullptr;
150 // statistics
151 int s_base_pos = 0;
152 private:
153 refinement* R;
154 trace *cT = nullptr;
155 trace internal_T1;
156 trace internal_T2;
158 std::vector<int> internal_compare_singletons;
159 std::vector<int> internal_compare_base_vertex;
160 std::vector<base_info> internal_compare_base;
162 // the following workspaces are only used for the paired color dfs (AKA the saucy-style dfs) -- not needed
163 // for normal bfs, dfs, or random search operation
164 markset diff_tester;
165 markset diff_vertices;
166 markset diff_is_singleton;
167 worklist diff_vertices_list;
168 worklist diff_vertices_list_pt;
170 markset diff_updated_color;
171 workspace diff_previous_color;
172 workspace diff_original_size;
173 bool diff_diverge = false;
175 int singleton_pt_start = 0;
177 // hooks for color refinement -- this controller hooks into the color refinement algorithm to gather
178 // necessary information
179 std::function<type_split_color_hook> my_split_hook;
180 std::function<type_worklist_color_hook> my_worklist_hook;
182 // settings
185 // internal flags for heuristics
186 bool s_cell_active = false;
187 bool s_individualize = false;
189 bool h_trace_early_out = false;
190 bool h_deviation_inc_active = false;
191 int s_deviation_inc_current = 0;
192 int h_deviation_inc = 48;
195 bool h_use_split_limit = false;
196 int h_split_limit = 0;
197
198 int s_splits = 0;
199
204 void touch_initial_colors() {
205 int i = 0;
206 while (i < c->domain_size) {
208 i += c->ptn[i] + 1;
209 }
210 }
211
215 void reset_touched() {
219 touch_initial_colors();
220 }
221
225 void flip_trace() {
226 trace* t_flip = T;
227 T = cT;
228 cT = t_flip;
229 }
230
235 bool split_hook(const int old_color, const int new_color, const int new_color_sz) {
237 // write singletons to singleton list
238 if (new_color_sz == 1) singletons.push_back(c->lab[new_color]);
239
240 // record colors that were changed
241 if (!touched_color.get(new_color)) {
242 touched_color.set(new_color);
243 prev_color_list.push_back(old_color);
244 touched_color_list.push_back(new_color);
245 }
246 }
247
248 // record split into trace invariant, unless we are individualizing
249 if (!s_individualize && old_color != new_color) T->op_refine_cell_record(new_color);
250
251 const bool cont = !h_trace_early_out || T->trace_equal();
252 s_deviation_inc_current += (!cont);
253 const bool deviation_override = h_deviation_inc_active && (s_deviation_inc_current <= h_deviation_inc);
254
255 const bool continue_cell_limit = !((mode != IR_MODE_RECORD_TRACE) && T->trace_equal()
256 && s_base_pos - 1 < static_cast<int>(compare_base->size())
257 && (*compare_base)[s_base_pos - 1].cells == c->cells);
258 ++s_splits;
259 const bool continue_split_limit = !h_use_split_limit || (s_splits < h_split_limit);
260 return continue_split_limit && continue_cell_limit && (cont || deviation_override);
261 }
262
263 std::function<type_split_color_hook> self_split_hook() {
264 #ifndef dej_nolambda
265 return [this](auto && PH1, auto && PH2, auto && PH3) { return
266 this->split_hook(std::forward<decltype(PH1)>(PH1), std::forward<decltype(PH2)>(PH2),
267 std::forward<decltype(PH3)>(PH3));
268 };
269 #else
270 return std::bind(&controller::split_hook, this, std::placeholders::_1, std::placeholders::_2,
271 std::placeholders::_3);
272 #endif
273 }
274
275
279 bool worklist_hook(const int color, const int color_sz) {
280 if (s_cell_active) {
282 s_cell_active = false;
283 }
284
285 T->op_refine_cell_start(color);
286 if (!s_individualize) T->op_additional_info(color_sz);
287
288 // blueprints
289 /*if (T->trace_equal() && !T->blueprint_is_next_cell_active()) {
290 s_cell_active = false;
291 T->blueprint_skip_to_next_cell();
292 return false;
293 }*/
294
295 s_cell_active = true;
296 return true;
297 }
298
299 std::function<type_worklist_color_hook> self_worklist_hook() {
300 #ifndef dej_nolambda
301 return [this](auto && PH1, auto && PH2) {
302 return this->worklist_hook(std::forward<decltype(PH1)>(PH1), std::forward<decltype(PH2)>(PH2));
303 };
304 #else
305 return std::bind(&controller::worklist_hook, this, std::placeholders::_1, std::placeholders::_2);
306 #endif
307 }
308
313 void add_diff_vertex(int v) {
314 //assert(trace || (!diff_vertices.get(v) && !diff_is_singleton.get(v)));
315 if(!diff_vertices.get(v) && !diff_is_singleton.get(v)) {
316 diff_vertices.set(v);
317 diff_vertices_list.push_back(v);
318 diff_vertices_list_pt[v] = diff_vertices_list.cur_pos - 1;
319 }
320 }
321
326 void remove_diff_vertex(int v) {
327 //assert(trace || (diff_vertices.get(v)));
328 if(diff_vertices.get(v)) {
329 const int pt = diff_vertices_list_pt[v];
330 dej_assert(diff_vertices_list[pt] == v);
331
332 // which element is in the back?
333 const int back_pt = diff_vertices_list.cur_pos-1;
334 const int back_v = diff_vertices_list[back_pt];
335
336 // now swap back_col to col
337 diff_vertices_list[pt] = back_v;
338 dej_assert(diff_vertices.get(back_v));
339 dej_assert(diff_vertices_list_pt[back_v] == back_pt);
340 diff_vertices_list_pt[back_v] = pt;
341 diff_vertices_list_pt[v] = -1; // I don't trust myself
342
343 diff_vertices.unset(v);
344 --diff_vertices_list.cur_pos;
345 }
346 }
347
353 void color_fix_difference(const controller& state, int col) {
354 const int col_sz = c->ptn[col] + 1;
355
356 if(col_sz == 1) {
357 add_diff_vertex(state.c->lab[col]);
358 const int v = c->lab[col];
359 remove_diff_vertex(v);
360 if(!diff_is_singleton.get(v)) {
361 diff_is_singleton.set(v);
362 }
363 return;
364 }
365
366 diff_tester.reset();
367 for(int i = 0; i < col_sz; ++i) diff_tester.set(state.c->lab[col + i]);
368 for(int i = 0; i < col_sz; ++i)
369 if(!diff_tester.get(c->lab[col + i])) add_diff_vertex(c->lab[col + i]);
370
371 diff_tester.reset();
372 for(int i = 0; i < col_sz; ++i) diff_tester.set(c->lab[col + i]);
373 for(int i = 0; i < col_sz; ++i)
374 if(!diff_tester.get(state.c->lab[col + i])) add_diff_vertex(state.c->lab[col + i]);
375 }
376
377 public:
385 this->c = col;
386 this->R = ref;
387
388 T = &internal_T1;
389 cT = &internal_T2;
390
394
395 touch_initial_colors();
396
397 my_split_hook = self_split_hook();
398 my_worklist_hook = self_worklist_hook();
399
400 diff_tester.initialize(col->domain_size);
401
402 diff_vertices.initialize(col->domain_size);
403 diff_vertices_list.resize(col->domain_size);
404 diff_vertices_list_pt.resize(col->domain_size);
405 diff_is_singleton.initialize(col->domain_size);
406
407 diff_updated_color.initialize(col->domain_size);
408 diff_previous_color.resize(col->domain_size);
409 diff_original_size.resize(col->domain_size);
410
411 singleton_pt_start = 0;
412 singletons.reserve(col->domain_size);
413 }
414
416 return s_splits;
417 }
418
425 T->reset();
426 cT->reset();
427
428 reset_touched();
430 T->set_compare(false);
431 T->set_record(true);
432
433 internal_compare_base.clear();
434 internal_compare_base_vertex.clear();
435 internal_compare_singletons.clear();
436 }
437
444 }
445
453 for(int i = 0; i < c->domain_size;) {
454 const int col = i;
455 const int col_sz = c->ptn[col] + 1;
456 i += col_sz;
457 if(col_sz == 1) continue;
458
459 diff_tester.reset();
460 for(int j = col; j < col + col_sz; ++j) {
461 const int v = c->lab[j];
462 diff_tester.set(v);
463 }
464 for(int j = col; j < col + col_sz; ++j) {
465 const int v = leaf_color.lab[j];
466 if(!diff_tester.get(v)) return true;
467 }
468 }
469 return false;
470 }
471
479 automorphism->reset();
480
481 for(int i = 0; i < c->domain_size;) {
482 const int col_sz = c->ptn[i] + 1;
483
484 if(col_sz == 1 && c->lab[i] != leaf_color.lab[i]) {
485 automorphism->write_single_map(c->lab[i], leaf_color.lab[i]);
486 }
487 i += col_sz;
488 }
489 }
490
492 automorphism->reset();
493
494 for(int i = 0; i < c->domain_size; ++i) {
495
496 const int v1 = i;
497 const int col = c->vertex_to_lab[i];
498 const int v2 = leaf_color.lab[col];
499
500 if(v1 != v2) {
501 automorphism->write_single_map(v1, v2);
502 }
503 }
504 }
505
506
514 for(int i = 0; i < domain_size;) {
515 const int col = i;
516 const int col_sz = c->ptn[col] + 1;
517 i += col_sz;
518
519 diff_tester.reset();
520 for(int j = col; j < col + col_sz; ++j) {
521 const int v = c->lab[j];
522 diff_tester.set(v);
523 }
524 for(int j = col; j < col + col_sz; ++j) {
525 const int v = leaf_color.lab[j];
526 if(!diff_tester.get(v)) return true;
527 }
528 }
529 return false;
530 }
531
539 std::pair<int, int> diff_pair(const controller& state) {
540 dej_assert(diff_vertices_list.cur_pos > 0);
541
542 // pick a vertex from the difference list
543 const int right = diff_vertices_list[0];
544 const int right_col = c->vertex_to_col[right];
545
546 // find a corresponding counterpart in the other coloring
547 //const int left = state.c->lab[right_col];
548 const int right_col_sz = c->ptn[right_col] + 1;
549 int left = -1;
550 for (int i = 0; i < right_col_sz; ++i) {
551 const int candidate = state.c->lab[right_col + i];
552 if(diff_vertices.get(candidate)) {
553 left = candidate;
554 break;
555 }
556 }
557 if(left == -1) left = state.c->lab[right_col];
558
559
560 return {left, right};
561 }
562
566 void reset_diff() {
567 diff_vertices.reset();
568 diff_vertices_list.reset();
569 diff_is_singleton.reset();
570
571 diff_tester.reset();
572 singleton_pt_start = singletons.size();
573
574 diff_diverge = false;
575 }
576
585 automorphism.reset();
586 for(int i = singleton_pt_start; i < static_cast<int>(singletons.size()); ++i) {
587 automorphism.write_single_map(singletons[i], state.singletons[i]);
588 }
589 }
590
598 return diff_diverge;
599 }
600
601
612 int i;
614 diff_diverge = true;
615 return true;
616 }
617
618 diff_updated_color.reset();
619
620 // reconstruct color prior to individualization for each new color
621 for(i = base.back().touched_color_list_pt; i < touched_color_list.cur_pos; ++i) {
622 const int old_color = prev_color_list[i];
623 const int new_color = touched_color_list[i];
624 diff_original_size[old_color] = 0;
625 if(!diff_updated_color.get(old_color)) {
626 diff_updated_color.set(old_color);
627 diff_previous_color[old_color] = old_color;
628 }
629 while(diff_previous_color[old_color] != diff_previous_color[diff_previous_color[old_color]])
630 diff_previous_color[old_color] = diff_previous_color[diff_previous_color[old_color]];
631 diff_updated_color.set(new_color);
632 diff_previous_color[new_color] = diff_previous_color[old_color];
633 }
634
635 // determine size of the original color classes
636 for(i = base.back().touched_color_list_pt; i < touched_color_list.cur_pos; ++i) {
637 const int new_color = touched_color_list[i];
638 const int old_color = diff_previous_color[new_color];
639 diff_original_size[old_color] = std::max(diff_original_size[old_color],
640 new_color + c->ptn[new_color] + 1);
641 }
642
643 diff_updated_color.reset();
644
645 // now fix colors according to fragments of original color classes
646 for(i = base.back().touched_color_list_pt; i < touched_color_list.cur_pos; ++i) {
647 const int old_color = prev_color_list[i];
648 if(diff_updated_color.get(old_color)) {
649 dej_assert(diff_updated_color.get(touched_color_list[i]));
650 continue;
651 }
652 int old_color_end_pt = std::max(old_color + c->ptn[old_color] + 1, diff_original_size[old_color]);
653
654
655 // let's update diff for all the fragments of old_color
656 const int old_color_sz = c->ptn[old_color] + 1;
657 const int old_color_sz_other = other_state.c->ptn[old_color] + 1;
658 diff_diverge = diff_diverge || (old_color_sz != old_color_sz_other);
659 if(diff_diverge) break;
660
661 // determine the largest fragment
662 int largest_fragment = -1;
663 int largest_fragment_sz = -1;
664
665 for(int j = old_color; j < old_color_end_pt;) {
666 const int next_color = j;
667 const int next_color_sz = c->ptn[next_color] + 1;
668 const int next_color_sz_other = other_state.c->ptn[next_color] + 1;
669 diff_diverge = diff_diverge || (next_color_sz != next_color_sz_other);
670 if(next_color_sz > largest_fragment_sz) {
671 largest_fragment = next_color;
672 largest_fragment_sz = next_color_sz;
673 }
674
675 diff_updated_color.set(next_color);
676 j += next_color_sz;
677 }
678
679 if(diff_diverge) break;
680
681 // update all but the largest of those fragments
682 for(int j = old_color; j < old_color_end_pt;) {
683 const int next_color = j;
684 const int next_color_sz = c->ptn[next_color] + 1;
685 if(j != largest_fragment) color_fix_difference(other_state, next_color);
686 j += next_color_sz;
687 }
688
689 // unless the largest fragment is a singleton, in that case we want to record the singleton
690 if(largest_fragment_sz == 1) color_fix_difference(other_state, largest_fragment);
691 }
692 return (diff_vertices_list.cur_pos != 0) || diff_diverge; // there is a diff!
693 }
694
695
704 this->c->copy_any(state->c);
705
706 T->set_compare(true);
707 T->set_record(false);
709 T->set_position(state->T->get_position());
710 T->set_hash(state->T->get_hash());
711
712 base_vertex = state->base_vertex;
713 base = state->base;
714
716 compare_base = state->compare_base;
717
719 mode = state->mode;
720
724
725 //singletons = state->singletons;
727
728 s_base_pos = state->s_base_pos;
729
730 this->R = state->R;
731 }
732
740 void link(controller* state) {
741 this->c->copy_any(state->c);
742
743 T->set_compare(true);
744 T->set_record(false);
745 T->set_compare_trace(state->T);
746 T->set_position(state->T->get_position());
747 T->set_hash(state->T->get_hash());
748
749 base_vertex = state->base_vertex;
750 base = state->base;
751
753 compare_base = &state->base;
754
756 mode = state->mode;
757
761 singletons = state->singletons;
763
764 s_base_pos = state->s_base_pos;
765
766 this->R = state->R;
767 }
768
769 int diff_num() {
770 return diff_vertices_list.cur_pos;
771 };
772
780
781 cT->set_compare(true);
782 cT->set_record(false);
783 cT->set_compare_trace(T);
785 flip_trace();
786
787 internal_compare_base = base;
788 internal_compare_base_vertex = base_vertex;
789 internal_compare_singletons = singletons;
790
791 compare_base = &internal_compare_base;
792 compare_base_vertex = &internal_compare_base_vertex;
793 compare_singletons = &internal_compare_singletons;
794
795
798 }
799
800 void reserve() {
801 const int domain_size = sqrt(c->domain_size);
802 int sqrt_domain = sqrt(domain_size);
803 base.reserve(sqrt_domain);
804 base_vertex.reserve(sqrt_domain);
805 T->reserve(2*domain_size);
806 }
807
816 void use_reversible(const bool reversible) {
817 if(mode == IR_MODE_RECORD_TRACE) return;
818 if(reversible) {
819 reset_touched();
821 } else {
823 }
824 }
825
831 void use_trace_early_out(bool trace_early_out) {
832 this->h_trace_early_out = trace_early_out;
833 if(!trace_early_out) use_increase_deviation(false);
834 }
835
843 void use_increase_deviation(bool deviation_inc_active) {
844 h_deviation_inc_active = deviation_inc_active;
845 }
846
854 void set_increase_deviation(int deviation_inc = 48) {
855 h_deviation_inc = deviation_inc;
856 }
857
865 void use_split_limit(bool use_split_limit, int limit = 0) {
866 h_use_split_limit = use_split_limit;
867 h_split_limit = limit;
868 }
869
875 s_deviation_inc_current = 0;
876 }
877
884 state.save(base_vertex, *c, T->get_hash(), T->get_position(),
885 s_base_pos);
886 }
887
894 c->copy_any(state.get_coloring());
895
896 T->set_hash(state.get_invariant_hash());
899 T->set_compare(true);
901 base_vertex = state.get_base();
902
903 // these become meaningless, so clear them out
904 base.clear();
905
906 // if reversible, need to reset touched colors
907 if(mode == IR_MODE_COMPARE_TRACE_REVERSIBLE) reset_touched();
908 }
909
911 T->set_hash(state.get_invariant_hash());
914 T->set_compare(true);
916 base_vertex = state.get_base();
917
918 // becomes meaningless
919 base.clear();
920
921 // deactivate reversability
923 }
924
926 return c;
927 }
928
930 return s_base_pos;
931 }
932
939 void write_to_trace(const int d) const {
941 }
942
948 void write_strong_invariant(const sgraph* g) const {
949 for(int l = 0; l < g->v_size; ++l) {
950 const int v = c->lab[l];
951 unsigned int inv1 = 0;
952 const int start_pt = g->v[v];
953 const int end_pt = start_pt + g->d[v];
954 for(int pt = start_pt; pt < end_pt; ++pt) {
955 const int other_v = g->e[pt];
956 inv1 += hash((unsigned int) c->vertex_to_col[other_v]);
957 }
958 T->op_additional_info((int) inv1);
959 }
960 }
961
969 for(int l = 0; l < g->v_size; l += 4) {
970 const int v = c->lab[l];
971 unsigned int inv1 = 0;
972 const int start_pt = g->v[v];
973 const int end_pt = start_pt + g->d[v];
974 for(int pt = start_pt; pt < end_pt; ++pt) {
975 const int other_v = g->e[pt];
976 inv1 += hash((unsigned int) c->vertex_to_col[other_v]);
977 }
978 T->op_additional_info((int) inv1);
979 }
980 }
981
989 void move_to_child(sgraph *g, int v) {
990 // always keep track of vertex base
991 ++s_base_pos;
992 s_splits = 0;
993 base_vertex.push_back(v);
994
995 dej_assert(!s_cell_active);
996
997 // some info maybe needed later
998 const int singleton_pt = (int) singletons.size();
999 const int touched_color_pt = touched_color_list.cur_pos;
1000 const int trace_pos = T->get_position();
1001 const unsigned long trace_hash = T->get_hash();
1002
1003 // determine color
1004 const int prev_col = c->vertex_to_col[v];
1005 const int prev_col_sz = c->ptn[prev_col] + 1;
1006
1007 // individualize vertex
1008 s_individualize = true;
1009 const int init_color_class = refinement::individualize_vertex(c, v, my_split_hook);
1011 s_individualize = false;
1012
1013 // refine coloring
1014 T->op_refine_start();
1015 if (mode == IR_MODE_RECORD_TRACE) {
1016 R->refine_coloring(g, c, init_color_class, -1, &my_split_hook, &my_worklist_hook);
1017 if (s_cell_active) T->op_refine_cell_end();
1018 T->op_refine_end();
1019 } else {
1020 R->refine_coloring(g, c, init_color_class, -1, &my_split_hook, &my_worklist_hook);
1021 if (T->trace_equal() && c->cells==(*compare_base)[s_base_pos - 1].cells && !h_use_split_limit) {
1023 }
1024 }
1025
1026 s_cell_active = false;
1027
1029 base.emplace_back(prev_col, prev_col_sz, c->cells, touched_color_pt, singleton_pt, trace_pos,
1030 trace_hash);
1031 }
1032
1041 const int init_color_class = R->individualize_vertex(c, v);
1042 R->refine_coloring_first(g, c, init_color_class);
1043 }
1044
1050 void refine(sgraph *g) {
1051 R->refine_coloring_first(g, c);
1052 }
1053
1059 dej_assert(base.size() > 0);
1060
1061 // unwind invariant
1062 T->set_position(base.back().trace_pos);
1063 T->set_hash(base.back().trace_hash);
1064
1065 // unwind colors introduced on this level of the tree
1066 --s_base_pos;
1067 while (prev_color_list.cur_pos > base.back().touched_color_list_pt) {
1068 const int old_color = prev_color_list.pop_back();
1069 const int new_color = touched_color_list.pop_back();
1070
1071 touched_color.unset(new_color);
1072
1073 const int new_color_sz = c->ptn[new_color] + 1;
1074 c->ptn[old_color] += new_color_sz;
1075 c->ptn[new_color] = 1;
1076
1077 for (int j = 0; j < new_color_sz; ++j) {
1078 const int v = c->lab[new_color + j];
1079 c->vertex_to_col[v] = old_color;
1080 dej_assert(c->vertex_to_lab[v] == new_color + j);
1081 }
1082
1083 --c->cells;
1084 }
1085 // unwind singletons
1086 int const new_singleton_pos = base.back().singleton_pt;
1087 singletons.resize(new_singleton_pos);
1088
1089 // remove base information
1090 base_vertex.pop_back();
1091 base.pop_back();
1092
1094 }
1095
1104 void walk(sgraph *g, ir::limited_save &start_from, std::vector<int>& vertices) {
1105 load_reduced_state(start_from);
1106
1107 while (s_base_pos < (int) vertices.size()) {
1108 int v = vertices[s_base_pos];
1109 move_to_child(g, v);
1110 }
1111 }
1112
1124 if(automorphism.nsupp() == 0) return true;
1125 if(automorphism.nsupp() > g->v_size / 4) {
1126 return R->certify_automorphism(g, automorphism.p());
1127 } else {
1128 return R->certify_automorphism_sparse(g, automorphism.p(), automorphism.nsupp(),
1129 automorphism.supp());
1130 }
1131 }
1132 };
1133
1141 const int locked_lim = 512;
1142
1143 std::vector<int> saved_color_base;
1144 std::vector<int> saved_color_sizes;
1145 std::function<type_selector_hook> dynamic_seletor;
1146 markset test_set;
1147 std::vector<int> candidates;
1148 big_number ir_tree_size_estimate;
1149
1150 int color_score(sgraph *g, controller *state, int color) {
1151 test_set.reset();
1152 const int v = state->get_coloring()->lab[color];
1153 const int d = g->d[v];
1154 const int ept_st = g->v[v];
1155 const int ept_end = ept_st + d;
1156 int non_triv_col_d = 1;
1157 for (int i = ept_st; i < ept_end; ++i) {
1158 const int test_col = state->get_coloring()->vertex_to_col[g->e[i]];
1159 if (!test_set.get(test_col)) {
1160 non_triv_col_d += 1;
1161 test_set.set(test_col);
1162 }
1163 }
1164 return state->get_coloring()->ptn[color] * non_triv_col_d;
1165 }
1166
1167 static int color_score_size(controller *state, int color) {
1168 return state->get_coloring()->ptn[color];
1169 }
1170
1171 static int color_score_anti_size(controller *state, int color) {
1172 return INT32_MAX - state->get_coloring()->ptn[color];
1173 }
1174
1175 public:
1177
1185 int cell_selector(const coloring *c, const int base_pos) {
1186 if (base_pos >= 0 && base_pos < (int) saved_color_base.size() && c->ptn[saved_color_base[base_pos]] > 0 &&
1187 c->vertex_to_col[c->lab[saved_color_base[base_pos]]] == saved_color_base[base_pos] &&
1188 c->ptn[saved_color_base[base_pos]] + 1 == saved_color_sizes[base_pos]) {
1189 return saved_color_base[base_pos];
1190 }
1191 int best_score = -1;
1192 int best_color = -1;
1193 for (int i = 0; i < c->domain_size;) {
1194 if (c->ptn[i] > best_score && c->ptn[i] > 0) {
1195 best_score = c->ptn[i];
1196 best_color = i;
1197 }
1198 if(best_color >= 0) break;
1199 i += c->ptn[i] + 1;
1200 }
1201 return best_color;
1202 }
1203
1207 std::function<type_selector_hook> *get_selector_hook() {
1208 dynamic_seletor = std::bind(&cell_selector_factory::cell_selector, this, std::placeholders::_1,
1209 std::placeholders::_2);
1210 return &dynamic_seletor;
1211 }
1212
1217 return ir_tree_size_estimate;
1218 }
1219
1229 void make_cell_selector(sgraph *g, controller *state, controller *state_probe, const selector_style style,
1230 const int h_seed, const int h_budget) {
1231 int perturbe = 0;
1232 if(h_seed > 6) {
1233 perturbe = (int) (hash(h_seed) % 256);
1234 }
1235 switch(style) {
1236 case 0:
1237 //find_combinatorial_optimized_base_recurse(g, state, perturbe);
1239 //find_first_base(g, state);
1240 break;
1241 case 1:
1243 break;
1244 case 2:
1245 find_small_optimized_base(g, state, perturbe);
1246 break;
1247 case 3:
1248 if(h_budget > 32) {
1249 // hail mary selector... seems to be very good for some classes, but is very expensive and
1250 // its use must be limited somehow... probing is only used for a fixed number of levels and
1251 // then switches to find_combinatorial_optimized_base
1252 // idea is to create trace deviations "higher up" in the tree, such that bfs may succeed
1253 // earlier
1254 find_early_trace_deviation_base(g, state, state_probe, perturbe);
1255 } else find_combinatorial_optimized_base(g, state);
1256 break;
1257 }
1258
1259 // now save the selector and make some estimates
1260 ir_tree_size_estimate.mantissa = 1.0;
1261 ir_tree_size_estimate.exponent = 0;
1262
1263 saved_color_base.clear();
1264 saved_color_base.reserve(state->base.size());
1265 for(auto& bi : state->base) {
1266 saved_color_base.push_back(bi.color);
1267 }
1268
1269 saved_color_sizes.clear();
1270 saved_color_sizes.reserve(state->base.size());
1271 for(auto& bi : state->base) {
1272 ir_tree_size_estimate.multiply(bi.color_sz);
1273 saved_color_sizes.push_back(bi.color_sz);
1274 }
1275 }
1285 // some settings for heuristics
1286 constexpr int base_lim = 1000;
1287 constexpr int test_lim_pre = 512;
1288 constexpr int test_lim_post = 1;
1289
1290 state->mode_write_base();
1291
1292 int prev_color = -1;
1293 dej_assert(state->s_base_pos == 0);
1294 test_set.initialize(g->v_size);
1295
1296 int start_test_from = 0;
1297 int start_test_from_inside = 0;
1298
1299 int buffered_col = -1;
1300 int buffered_col_score = -1;
1301
1302 while (state->get_coloring()->cells != g->v_size) {
1303 int best_color = -1;
1304 int test_lim = state->s_base_pos <= base_lim?test_lim_pre:test_lim_post;
1305
1306 // pick previous color if possible
1307 if (prev_color >= 0 && state->get_coloring()->ptn[prev_color] > 0) {
1308 best_color = prev_color;
1309 } else if (prev_color >= 0) { // pick neighbour of previous color if possible
1310 const int test_vertex = state->get_coloring()->lab[prev_color];
1311 int i = g->v[test_vertex] + start_test_from_inside;
1312 const int end_pt = g->v[test_vertex] + g->d[test_vertex];
1313 for (; i < end_pt; ++i) {
1314 const int other_vertex = g->e[i];
1315 const int other_color = state->get_coloring()->vertex_to_col[other_vertex];
1316 if (state->get_coloring()->ptn[other_color] > 0) {
1317 best_color = other_color;
1318 break;
1319 } else {
1320 ++start_test_from_inside;
1321 }
1322 }
1323 }
1324
1325 start_test_from_inside = 0;
1326
1327 // use buffered color if possible
1328 if(best_color == -1 && buffered_col >= 0 && state->get_coloring()->ptn[buffered_col] > 0 &&
1329 color_score(g, state, buffered_col) >= buffered_col_score) {
1330 best_color = buffered_col;
1331 buffered_col = -1;
1332 buffered_col_score = -1;
1333 }
1334
1335 // same color, neighbour of color and buffer failed, so now we try to pick a "good" color
1336 if (best_color == -1) {
1337 int best_score = -1;
1338
1339 for (int i = start_test_from; i < state->get_coloring()->domain_size && test_lim >= 0;) {
1340 const int col_sz = state->get_coloring()->ptn[i];
1341
1342 if (col_sz > 0) {
1343 --test_lim;
1344 const int test_score = color_score(g, state, i);
1345 if (test_score > best_score) {
1346 best_color = i;
1347 best_score = test_score;
1348 buffered_col = -1;
1349 buffered_col_score = -1;
1350 } else if (test_score == best_score) {
1351 buffered_col = i;
1352 buffered_col_score = test_score;
1353 }
1354 }
1355
1356 if(col_sz == 0 && start_test_from == i) start_test_from += col_sz + 1;
1357 i += col_sz + 1;
1358 }
1359 }
1360
1361 dej_assert(best_color >= 0);
1362 dej_assert(best_color < g->v_size);
1363 prev_color = best_color;
1364 state->move_to_child(g, state->get_coloring()->lab[best_color]);
1365 }
1366 }
1367
1369 state->mode_write_base();
1370 dej_assert(state->s_base_pos == 0);
1371
1372 test_set.initialize(g->v_size);
1373
1374 int start_test_from = 0;
1375
1376 while (state->get_coloring()->cells != g->v_size) {
1377 int best_color = -1;
1378 int test_lim = 512;
1379
1380
1381 for (int i = start_test_from; i < state->get_coloring()->domain_size && test_lim >= 0;) {
1382 const int col_sz = state->get_coloring()->ptn[i];
1383
1384 if (col_sz > 0) {
1385 best_color = i;
1386 break;
1387 }
1388
1389 if(col_sz == 0 && start_test_from == i) start_test_from += col_sz + 1;
1390 i += col_sz + 1;
1391 }
1392
1393 dej_assert(best_color >= 0);
1394 dej_assert(best_color < g->v_size);
1395 state->move_to_child(g, state->get_coloring()->lab[best_color]);
1396 }
1397 }
1398
1408 state->mode_write_base();
1409
1410 test_set.initialize(g->v_size);
1411 int prev_color = -1;
1412 int prev_color_sz = 0;
1413
1414 dej_assert(state->s_base_pos == 0);
1415
1416 while (state->get_coloring()->cells != g->v_size) {
1417 int best_color = -1;
1418 int test_lim = 512;
1419
1420 // recurse into previous color if possible
1421 if(prev_color >= 0) {
1422 for (int i = 0; i < prev_color + prev_color_sz;) {
1423 if (state->get_coloring()->ptn[i] > 0) {
1424 best_color = i;
1425 break;
1426 }
1427 i += state->get_coloring()->ptn[i] + 1;
1428 }
1429 }
1430
1431 if (prev_color >= 0 && best_color == -1) { // pick neighbour of previous color if possible
1432 const int test_vertex = state->get_coloring()->lab[prev_color];
1433 for (int i = 0; i < g->d[test_vertex]; ++i) {
1434 const int other_vertex = g->e[g->v[test_vertex] + i];
1435 const int other_color = state->get_coloring()->vertex_to_col[other_vertex];
1436 if (state->get_coloring()->ptn[other_color] > 0) {
1437 best_color = other_color;
1438 }
1439 }
1440 }
1441
1442 // heuristic, try to pick "good" color
1443 if (best_color == -1) {
1444 int best_score = -1;
1445
1446 for (int i = 0; i < state->get_coloring()->domain_size && test_lim >= 0;) {
1447 if (state->get_coloring()->ptn[i] > 0) {
1448 int test_score = color_score(g, state, i);
1449 if (test_score > best_score) {
1450 best_color = i;
1451 best_score = test_score;
1452 }
1453 --test_lim;
1454 }
1455
1456 i += state->get_coloring()->ptn[i] + 1;
1457 }
1458 }
1459
1460 dej_assert(best_color >= 0);
1461 dej_assert(best_color < g->v_size);
1462 prev_color = best_color;
1463 prev_color_sz = state->get_coloring()->ptn[best_color] + 1;
1464 state->move_to_child(g, state->get_coloring()->lab[(best_color +
1465 (perturbe%state->get_coloring()->ptn[best_color]))]);
1466 }
1467 }
1468
1477 void find_small_optimized_base(sgraph *g, controller *state, int perturbe) {
1478 state->mode_write_base();
1479
1480 while (state->get_coloring()->cells != g->v_size) {
1481 int best_color = -1;
1482 int test_lim = 256;
1483
1484 // heuristic, try to pick "good" color
1485 int best_score = INT32_MIN;
1486 for (int i = 0; i < state->get_coloring()->domain_size && test_lim >= 0;) {
1487 if (state->get_coloring()->ptn[i] > 0) {
1488 int test_score = color_score_anti_size(state, i);
1489 if (test_score > best_score || best_color == -1) {
1490 best_color = i;
1491 best_score = test_score;
1492 --test_lim;
1493 if(best_score == INT32_MAX - 1) break;
1494 }
1495 }
1496
1497 i += state->get_coloring()->ptn[i] + 1;
1498 }
1499
1500 dej_assert(best_color >= 0);
1501 dej_assert(best_color < g->v_size);
1502 state->move_to_child(g, state->get_coloring()->lab[(best_color +
1503 (perturbe%state->get_coloring()->ptn[best_color]))]);
1504 }
1505 }
1506
1508 state->mode_write_base();
1509
1510 test_set.initialize(g->v_size);
1511 candidates.clear();
1512 candidates.reserve(locked_lim);
1513
1514 markset neighbour_color;
1515 neighbour_color.initialize(g->v_size);
1516
1517 while (state->get_coloring()->cells != g->v_size) {
1518 int best_color = -1;
1519
1520 // heuristic, try to pick "good" color
1521 candidates.clear();
1522 int best_score = -1;
1523 for (int i = 0; i < state->get_coloring()->domain_size;) {
1524 if (state->get_coloring()->ptn[i] > 0) {
1525 candidates.push_back(i);
1526 }
1527 i += state->get_coloring()->ptn[i] + 1;
1528 }
1529 while (!candidates.empty()) {
1530 const int test_color = candidates.back();
1531 candidates.pop_back();
1532
1533 int test_score = color_score_size(state, test_color);
1534 if (neighbour_color.get(test_color)) {
1535 test_score *= 10;
1536 }
1537 if (test_score >= best_score) {
1538 best_color = test_color;
1539 best_score = test_score;
1540 }
1541 }
1542
1543 dej_assert(best_color >= 0);
1544 dej_assert(best_color < g->v_size);
1545 state->move_to_child(g, state->get_coloring()->lab[best_color]);
1546 }
1547 }
1548
1549
1550
1560 state->mode_write_base();
1561
1562 int prev_color = -1;
1563 int prev_color_sz = 0;
1564
1565 const bool perturbe_flip = perturbe % 2;
1566
1567 while (state->get_coloring()->cells != g->v_size) {
1568 int best_color = -1;
1569 int best_score = -1;
1570
1571 // recurse into previous color if possible
1572 if(prev_color >= 0) {
1573 for (int i = 0; i < prev_color + prev_color_sz;) {
1574 const int col_sz = state->get_coloring()->ptn[i];
1575 int test_score = color_score_size(state, i);
1576 if (((test_score > best_score) || (perturbe_flip && (test_score >= best_score))) && col_sz > 0) {
1577 best_color = i;
1578 best_score = test_score;
1579 }
1580 i += state->get_coloring()->ptn[i] + 1;
1581 }
1582 }
1583
1584 if(best_color == -1) {
1585 // heuristic, pick first largest color
1586 for (int i = 0; i < state->get_coloring()->domain_size;) {
1587 const int col_sz = state->get_coloring()->ptn[i];
1588 int test_score = color_score_size(state, i);
1589 if (test_score > best_score && col_sz > 0) {
1590 best_color = i;
1591 best_score = test_score;
1592 }
1593
1594 i += col_sz + 1;
1595 }
1596 }
1597
1598 dej_assert(best_color >= 0);
1599 dej_assert(best_color < g->v_size);
1600 prev_color = best_color;
1601 prev_color_sz = state->get_coloring()->ptn[best_color] + 1;
1602 state->move_to_child(g, state->get_coloring()->lab[(best_color + (perturbe% prev_color_sz))]);
1603 }
1604
1605 }
1606
1615 void find_early_trace_deviation_base(sgraph *g, controller* state, controller* state_probe, int perturbe) {
1616 state->mode_write_base();
1617 constexpr int probe_limit = 5;
1618
1619 state_probe->link(state);
1620 state_probe->mode_compare_base();
1621 state_probe->use_reversible(true);
1622 candidates.clear();
1623
1624 int probe_limit_candidates = 8;
1625
1626 bool use_probing = true;
1627
1628 while (state->get_coloring()->cells != g->v_size) {
1629 int best_color = -1;
1630 int best_score_deviate = -1;
1631 int best_score_cells = -1;
1632 int best_score_size = -1;
1633 int best_test_v = -1;
1634
1635 probe_limit_candidates = std::max(probe_limit_candidates, 2);
1636
1637 if(use_probing) {
1638 candidates.clear();
1639 for (int i = 0; i < state->c->domain_size;) {
1640 const int col_sz = state->c->ptn[i] + 1;
1641 if (col_sz >= 2) {
1642 candidates.push_back(i);
1643 }
1644 if (static_cast<int>(candidates.size()) >= probe_limit_candidates) break;
1645 i += col_sz;
1646 }
1647
1648 // now, probe and score the candidates... we are trying to find the color with most trace deviations
1649 for (int i = 0; i < static_cast<int>(candidates.size()); ++i) {
1650 const int col = candidates[i];
1651 const int col_sz = state->c->ptn[col] + 1;
1652 dej_assert(col_sz >= 2);
1653 const int probe_lim_col = std::min(probe_limit, col_sz);
1654
1655 const int v_base = state->get_coloring()->lab[(col + (perturbe % col_sz))];
1656 dej_assert(state->s_base_pos == state_probe->s_base_pos);
1657 dej_assert(state->T->get_position() == state_probe->T->get_position());
1658 dej_assert(state->c->cells == state_probe->c->cells);
1659 #if defined(DEJDEBUG) && !defined(NDEBUG)
1660 const int cells_pre = state->c->cells;
1661 const int previous_pos = state->T->get_position();
1662 #endif
1663
1664 state->move_to_child(g, v_base);
1665 const int cells = state->c->cells;
1666
1667 int deviated = 0;
1668 for (int j = 0; j < probe_lim_col; ++j) {
1669 // pick random vertex
1670 const int v = state_probe->c->lab[col + ((j + perturbe) % col_sz)];
1671 // individualize in state_probe
1672 state_probe->reset_trace_equal();
1673 state_probe->use_trace_early_out(true);
1674 dej_assert(state_probe->c->vertex_to_col[v] == state_probe->c->vertex_to_col[v_base]);
1675 state_probe->move_to_child(g, v);
1676 deviated += !state_probe->T->trace_equal();
1677 dej_assert(v == v_base ? state_probe->T->trace_equal() : true);
1678 state_probe->move_to_parent();
1679 dej_assert(state_probe->c->cells == cells_pre);
1680 dej_assert(state_probe->T->get_position() == previous_pos);
1681 }
1682
1683 state->move_to_parent();
1684 dej_assert(state->T->get_position() == previous_pos);
1685 dej_assert(cells_pre == state->c->cells);
1686 dej_assert(state->s_base_pos == state_probe->s_base_pos);
1687 dej_assert(state->T->get_position() == state_probe->T->get_position());
1688 dej_assert(state->c->cells == state_probe->c->cells);
1689
1690 if (deviated > best_score_deviate ||
1691 ((deviated == best_score_deviate) && (cells > best_score_cells)) ||
1692 ((deviated == best_score_deviate) && (cells == best_score_cells) &&
1693 (col_sz > best_score_size))) {
1694 best_color = col;
1695 best_score_deviate = deviated;
1696 best_score_cells = cells;
1697 best_score_size = col_sz;
1698 best_test_v = v_base;
1699 if (deviated > 0) break;
1700 }
1701 }
1702
1703 if (best_score_deviate > 0) --probe_limit_candidates;
1704 } else {
1705 // heuristic, try to pick "good" color
1706 candidates.clear();
1707 int best_score = -1;
1708 for (int i = 0; i < state->get_coloring()->domain_size;) {
1709 if (state->get_coloring()->ptn[i] > 0) {
1710 candidates.push_back(i);
1711 }
1712 i += state->get_coloring()->ptn[i] + 1;
1713 }
1714 while (!candidates.empty()) {
1715 const int test_color = candidates.back();
1716 candidates.pop_back();
1717
1718 int test_score = color_score_size(state, test_color);
1719 if (test_score >= best_score) {
1720 best_color = test_color;
1721 best_score = test_score;
1722 }
1723 }
1724 }
1725
1726 if(probe_limit_candidates < 2 || state->s_base_pos > 5) use_probing = false;
1727
1728 dej_assert(best_color >= 0);
1729 dej_assert(best_color < g->v_size);
1730 dej_assert(!use_probing || state->s_base_pos == state_probe->s_base_pos);
1731 dej_assert(!use_probing || state->T->get_position() == state_probe->T->get_position());
1732 //assert(state->T->get_hash() == state_probe->T->get_hash());
1733 dej_assert(!use_probing || state->c->cells == state_probe->c->cells);
1734 const int col_sz = state->get_coloring()->ptn[best_color] + 1;
1735 int v = best_test_v;
1736 if(v == -1) v = state->get_coloring()->lab[(best_color + (perturbe% col_sz))];
1737
1738 dej_assert(!use_probing || state->c->vertex_to_col[v] == state_probe->c->vertex_to_col[v]);
1739
1740 state_probe->reset_trace_equal();
1741 state->move_to_child(g, v);
1742 if(use_probing) state_probe->move_to_child(g, v);
1743
1744 dej_assert(!use_probing || state->s_base_pos == state_probe->s_base_pos);
1745 dej_assert(!use_probing || state_probe->T->trace_equal());
1746 dej_assert(!use_probing || state->c->cells == state_probe->c->cells);
1747 dej_assert(!use_probing || state->T->get_position() == state_probe->T->get_position());
1748 }
1749 }
1750 };
1751
1756 private:
1757 std::unordered_set<unsigned long> map;
1758 int computed_for_base = 0;
1759 int expected_for_base = 0;
1760 bool deviation_done = false;
1761
1762 void check_finished() {
1763 if(computed_for_base == expected_for_base) deviation_done = true;
1764 dej_assert(computed_for_base <= expected_for_base);
1765 }
1766
1767 public:
1768 void start(const int h_expected_for_base) {
1769 computed_for_base = 0;
1770 expected_for_base = h_expected_for_base;
1771
1772 map.clear();
1773 deviation_done = false;
1774 }
1775
1776 void record_deviation(unsigned long deviation) {
1777 map.insert(deviation);
1778 ++computed_for_base;
1779 dej_assert(computed_for_base <= expected_for_base);
1780 check_finished();
1781 }
1782
1784 ++computed_for_base;
1785 dej_assert(computed_for_base <= expected_for_base);
1786 check_finished();
1787 }
1788
1789 bool check_deviation(unsigned long deviation) {
1790 return !deviation_done || map.find(deviation) != map.end();
1791 }
1792 };
1793
1801 public:
1803 STORE_BASE
1805
1806 stored_leaf(int* arr, int arr_sz, stored_leaf_type storetype) : store_type(storetype) {
1807 lab_or_base.allocate(arr_sz);
1808 memcpy(lab_or_base.get_array(), arr, arr_sz * sizeof(int));
1809 lab_or_base.set_size(arr_sz);
1810 }
1811
1812 stored_leaf(std::vector<int>& arr, stored_leaf_type storetype) : store_type(storetype) {
1813 lab_or_base.allocate((int) arr.size());
1814 std::copy(arr.begin(), arr.end(), lab_or_base.get_array());
1815 lab_or_base.set_size((int) arr.size());
1816 }
1817
1818 const int* get_lab_or_base() {
1819 return lab_or_base.get_array();
1820 }
1821
1823 return lab_or_base.size();
1824 }
1825
1827 return store_type;
1828 }
1829
1830 private:
1831 worklist lab_or_base;
1832 stored_leaf_type store_type;
1833 };
1834
1842 std::unordered_multimap<unsigned long, stored_leaf*> leaf_store;
1843 std::vector<stored_leaf*> garbage_collector;
1844
1845 public:
1846 int s_leaves = 0;
1850 leaf_store.reserve(20);
1851 }
1852
1857 for(auto & l : garbage_collector) {
1858 delete l;
1859 }
1860 }
1861
1868 stored_leaf* lookup_leaf(unsigned long hash) {
1869 auto find = leaf_store.find(hash);
1870 if(find != leaf_store.end()) {
1871 return find->second;
1872 } else {
1873 return nullptr;
1874 }
1875 }
1876
1883 void add_leaf(unsigned long hash, coloring& c, std::vector<int>& base) {
1884 // check whether hash already exists
1885 //if(leaf_store.contains(hash)) return;
1886 if(leaf_store.find(hash) != leaf_store.end()) return;
1887
1888 // if not, add the leaf
1889 const bool full_save = s_leaves < h_full_save_limit;
1890 auto type
1892 auto new_leaf
1893 = full_save?new stored_leaf(c.lab,c.domain_size, type):new stored_leaf(base, type);
1894 leaf_store.insert(std::pair<unsigned long, stored_leaf*>(hash, new_leaf));
1895 garbage_collector.push_back(new_leaf);
1896 ++s_leaves;
1897 }
1898
1902 void clear() {
1903 s_leaves = 0;
1904 leaf_store.clear();
1905 // TODO clear garbage collector?
1906 }
1907 };
1908
1913 limited_save* data = nullptr;
1914 bool owns_data = true;
1915 tree_node* next;
1916 tree_node* parent;
1917 bool is_base = false;
1918 bool is_pruned = false;
1919 unsigned long hash = 0;
1920 public:
1921
1924
1925 tree_node(limited_save* _data, tree_node* _next, tree_node* _parent, bool ownsdata) {
1926 this->data = _data;
1927 this->next = _next;
1928 this->owns_data = ownsdata;
1929 this->parent = _parent;
1930 }
1931
1933 return next;
1934 }
1936 return parent;
1937 }
1938 void set_next(tree_node* new_next) {
1939 this->next = new_next;
1940 }
1942 return data;
1943 }
1944
1945 void prune() {
1946 is_pruned = true;
1947 }
1949 return is_pruned;
1950 }
1951 void add_hash(unsigned long add) {
1952 this->hash += add;
1953 }
1954
1955 dej_nodiscard unsigned long get_hash() const {
1956 return hash;
1957 }
1958
1959 void base() {
1960 is_base = true;
1961 }
1962
1964 return is_base;
1965 }
1966
1968 if(owns_data) delete data;
1969 }
1970 };
1971
1972 typedef std::pair<ir::tree_node*, int> missing_node;
1973
1983 stack_t<missing_node> missing_nodes;
1984 std::vector<tree_node*> tree_data;
1985 std::vector<std::vector<tree_node*>> tree_data_jump_map;
1986 std::vector<int> tree_level_size;
1987 std::vector<tree_node*> garbage_collector;
1988 int finished_up_to = 0;
1989
1990 std::vector<int> current_base;
1991
1992 std::vector<unsigned long> node_invariant; // TODO: move this to inprocessor?
1993
1994 bool init = false;
1995 public:
2001 explicit shared_tree(int domain_size) {
2002 h_bfs_top_level_orbit.initialize(domain_size);
2003 };
2004
2005 // TODO: move this to inprocessor?
2007 if(finished_up_to > 1) {
2008 for(int j = finished_up_to; j >= 1; --j) {
2009 finish_level(j);
2010 for(auto node : tree_data_jump_map[j]) {
2011 const int v = node->get_save()->get_base()[0];
2012 unsigned long add_hash = 1;
2013 add_hash = add_to_hash(add_hash, node->get_hash());
2014 add_hash = add_to_hash(add_hash, hash(j));
2015
2016 if(j == finished_up_to) {
2017 int cnt = 0;
2018 for (auto v_pre: node->get_save()->get_base()) {
2019 node_invariant[v_pre] += add_hash * hash(cnt);
2020 ++cnt;
2021 }
2022 }
2023
2024 node_invariant[node->get_save()->get_base()[j-1]] += add_hash;
2025 node_invariant[v] += add_hash + 1;
2026 }
2027 }
2028 }
2029 }
2030
2032 /*for(int j = finished_up_to; j >= 1; --j) {
2033 finish_level(j);
2034 for(auto node : tree_data_jump_map[j]) {
2035 node->nodes_below = 0;
2036 }
2037 }
2038
2039 for(int j = finished_up_to; j >= 1; --j) {
2040 for(auto node : tree_data_jump_map[j]) {
2041 node->get_parent()->nodes_below += node->nodes_below + 1;
2042 }
2043 }
2044
2045 for(int j = 1; j <= finished_up_to; ++j) {
2046 int nodes_below_compare = 0;
2047 for(auto node : tree_data_jump_map[j]) {
2048 if(node->get_base()) {
2049 nodes_below_compare = node->nodes_below;
2050 break;
2051 }
2052 }
2053 int could_prune = 0;
2054 for(auto node : tree_data_jump_map[j]) {
2055 if(nodes_below_compare != node->nodes_below) {
2056 ++could_prune;
2057 }
2058 }
2059 std::cout << could_prune << "@" << j << std::endl;
2060 }*/
2061 }
2062
2063 std::vector<unsigned long>* get_node_invariant() {
2064 return &node_invariant;
2065 }
2066
2067 void initialize(std::vector<int> &base, ir::limited_save* root) {
2068 tree_data.resize(base.size() + 1);
2069 tree_level_size.resize(base.size() + 1);
2070 tree_data_jump_map.resize(base.size() + 1);
2071 add_node(0, root, nullptr, true);
2072 node_invariant.resize(root->get_coloring()->domain_size);
2073 current_base = base;
2074 init = true;
2075 }
2076
2079 }
2080
2084 int stat_leaves() const {
2085 return stored_leaves.s_leaves;
2086 }
2087
2088 bool reset(std::vector<int> &new_base, ir::limited_save* root, bool keep_old) {
2089 if(!init) {
2090 initialize(new_base, root);
2091 return false;
2092 }
2093
2094 for(int i = 0; i < root->get_coloring()->domain_size; ++i) node_invariant[i] = 0;
2095
2096 const int old_size = (int) current_base.size();
2097 const int new_size = (int) new_base.size();
2098
2099 // compare with stored base, keep whatever is possible
2100 int keep_until = 0;
2101 if(keep_old) {
2102 for (; keep_until < old_size && keep_until < new_size; ++keep_until) {
2103 if (current_base[keep_until] != new_base[keep_until]) break;
2104 }
2105 }
2106
2107 if(keep_until == 0) {
2108 for(auto t : garbage_collector) delete t;
2109 garbage_collector.clear();
2110 }
2111
2112
2113 if(keep_until == new_size && new_size == old_size) return false;
2114
2115 finished_up_to = std::min(keep_until, finished_up_to);
2116
2118 tree_data.resize(new_size + 1);
2119 tree_level_size.resize(new_size + 1);
2120 tree_data_jump_map.resize(new_size + 1);
2121
2122 for (int i = keep_until+1; i < new_size+1; ++i) {
2123 tree_data[i] = nullptr;
2124 tree_level_size[i] = 0;
2125 tree_data_jump_map[i].clear();
2126 }
2127
2128 if(keep_until == 0) {
2129 tree_level_size[0] = 0;
2130 tree_data_jump_map[0].clear();
2131 tree_data[0] = nullptr;
2132 add_node(0, root, nullptr, true);
2133 }
2134 dej_assert(missing_nodes.empty());
2135
2136 current_base = new_base;
2137
2138 return true;
2139 }
2140
2141
2142 void queue_reserve(const int n) {
2143 missing_nodes.reserve(n);
2144 }
2145
2147 missing_nodes.add(node);
2148 }
2149
2151 return missing_nodes.empty();
2152 }
2153
2155 return missing_nodes.pop();
2156 }
2157
2159 if(tree_data[1] == nullptr) return;
2160
2161 marks.reset();
2162
2163 tree_node * first = tree_data[1];
2164 tree_node * next = first;
2165 do {
2166 marks.set(next->get_save()->get_base()[0]);
2167 next = next->get_next();
2168 } while (next != first);
2169 }
2170
2171 void record_invariant(int v, unsigned long inv) {
2172 node_invariant[v] = inv;
2173 }
2174
2175 void record_add_invariant(int v, unsigned long inv) {
2176 node_invariant[v] += inv;
2177 }
2178
2179 void add_node(int level, limited_save* data, tree_node* parent, bool is_base = false) {
2180 dej_assert(data != nullptr);
2181 if(tree_data[level] == nullptr) {
2182 tree_level_size[level] = 0;
2183 tree_data[level] = new tree_node(data, nullptr, parent, level != 0);
2184 tree_data[level]->set_next(tree_data[level]);
2185
2186 garbage_collector.push_back( tree_data[level]);
2187 if(is_base) tree_data[level]->base();
2188 } else {
2189 tree_node* a_node = tree_data[level];
2190 tree_node* next_node = a_node->get_next();
2191 auto new_node = new tree_node(data, next_node, parent, level != 0);
2192 garbage_collector.push_back(new_node);
2193 if(is_base) new_node->base();
2194 a_node->set_next(new_node);
2195 tree_data[level] = new_node;
2196 }
2197 ++tree_level_size[level];
2198 }
2199
2200 void finish_level(int level) {
2201 if(tree_data_jump_map[level].empty()) {
2202 tree_node * first = tree_data[level];
2203 tree_data_jump_map[level].reserve(tree_level_size[level]);
2204 tree_node * next = first;
2205 do {
2206 if(next->get_parent() == nullptr || !next->get_parent()->get_prune()) {
2207 tree_data_jump_map[level].push_back(next);
2208 }
2209 next = next->get_next();
2210 } while (next != first);
2211 tree_level_size[level] = tree_data_jump_map[level].size();
2212 dej_assert(static_cast<int>(tree_data_jump_map[level].size()) == tree_level_size[level]);
2213 }
2214 }
2215
2216 ir::tree_node* pick_node_from_level(const int level, int num) {
2217 finish_level(level);
2218 num = num % tree_level_size[level];
2219 return tree_data_jump_map[level][num];
2220 }
2221
2223 return finished_up_to;
2224 }
2225
2226 void set_finished_up_to(const int new_finished_up_to) {
2227 this->finished_up_to = new_finished_up_to;
2228 }
2229
2230 tree_node* get_level(int level) {
2231 return tree_data[level];
2232 }
2233
2235 return tree_level_size[finished_up_to];
2236 }
2237
2239 return tree_data[finished_up_to]->get_save()->get_trace_position();
2240 }
2241
2242 int get_level_size(int level) {
2243 return tree_level_size[level];
2244 }
2245
2247 for(auto & i : garbage_collector) delete i;
2248 };
2249 };
2250 }
2251}
2252
2253#endif //DEJAVU_IR_H
Stores big numbers.
Definition: utility.h:138
long double mantissa
Definition: utility.h:140
void multiply(int number)
Definition: utility.h:165
Vertex coloring for a graph.
Definition: coloring.h:23
void copy_any(coloring *c)
Definition: coloring.h:125
Set specialized for quick resets.
Definition: ds.h:546
void copy(const markset *other)
Definition: ds.h:651
bool get(int pos)
Definition: ds.h:605
void reset()
Definition: ds.h:634
void initialize(int size)
Definition: ds.h:588
void set(int pos)
Definition: ds.h:616
void unset(int pos)
Definition: ds.h:626
Stack datastructure.
Definition: ds.h:43
bool empty()
Definition: ds.h:66
void reserve(int n)
Definition: ds.h:59
void add(T &t)
Definition: ds.h:51
void copy(const worklist_t< T > *other)
Definition: ds.h:151
T * get_array() const
Definition: ds.h:280
void allocate(int size)
Definition: ds.h:166
void set_size(const int size)
Definition: ds.h:215
void resize(const int size)
Definition: ds.h:248
dej_nodiscard int size() const
Definition: ds.h:222
void push_back(T value)
Definition: ds.h:177
Fixed-size integer array, 0-initialized.
Definition: ds.h:326
void resize(const int size)
Definition: ds.h:413
Workspace for sparse automorphisms.
Definition: groups.h:68
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
void write_single_map(const int from, const int to)
Definition: groups.h:463
Orbit partition.
Definition: groups.h:507
void initialize(int domain_size)
Definition: groups.h:638
Creates cell selectors.
Definition: ir.h:1140
void find_sparse_optimized_base_recurse(sgraph *g, controller *state, int perturbe)
Definition: ir.h:1407
void find_combinatorial_optimized_base_recurse(sgraph *g, controller *state, int perturbe)
Definition: ir.h:1559
big_number get_ir_size_estimate()
Definition: ir.h:1216
void make_cell_selector(sgraph *g, controller *state, controller *state_probe, const selector_style style, const int h_seed, const int h_budget)
Definition: ir.h:1229
void find_sparse_optimized_base(sgraph *g, controller *state)
Definition: ir.h:1284
void find_first_base(sgraph *g, controller *state)
Definition: ir.h:1368
void find_combinatorial_optimized_base(sgraph *g, controller *state)
Definition: ir.h:1507
std::function< type_selector_hook > * get_selector_hook()
Definition: ir.h:1207
void find_early_trace_deviation_base(sgraph *g, controller *state, controller *state_probe, int perturbe)
Definition: ir.h:1615
void find_small_optimized_base(sgraph *g, controller *state, int perturbe)
Definition: ir.h:1477
int cell_selector(const coloring *c, const int base_pos)
Definition: ir.h:1185
Store deviations for a BFS level.
Definition: ir.h:1755
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
void save(std::vector< int > &s_base_vertex, coloring &s_c, unsigned long s_invariant, int s_trace_position, int s_base_position)
Definition: ir.h:57
std::vector< int > & get_base()
Definition: ir.h:97
coloring * get_coloring()
Definition: ir.h:69
dej_nodiscard int get_base_position() const
Definition: ir.h:90
dej_nodiscard int get_trace_position() const
Definition: ir.h:83
dej_nodiscard unsigned long get_invariant_hash() const
Definition: ir.h:76
Color refinement and related algorithms.
Definition: refinement.h:143
bool certify_automorphism(sgraph *g, const int *p)
Definition: refinement.h:362
static int individualize_vertex(coloring *c, int v, const std::function< type_split_color_hook > &split_hook=nullptr)
Definition: refinement.h:245
void refine_coloring_first(sgraph *g, coloring *c, int init_color_class=-1)
Definition: refinement.h:284
bool certify_automorphism_sparse(const sgraph *g, const int *p, int supp, const int *supp_arr)
Definition: refinement.h:379
void refine_coloring(sgraph *g, coloring *c, int init_color=-1, int color_limit=-1, const std::function< type_split_color_hook > *split_hook=nullptr, const std::function< type_worklist_color_hook > *worklist_hook=nullptr)
Definition: refinement.h:161
Collection of leaves.
Definition: ir.h:1841
stored_leaf * lookup_leaf(unsigned long hash)
Definition: ir.h:1868
void add_leaf(unsigned long hash, coloring &c, std::vector< int > &base)
Definition: ir.h:1883
IR tree structure.
Definition: ir.h:1982
int get_current_level_tracepos()
Definition: ir.h:2238
void record_invariant(int v, unsigned long inv)
Definition: ir.h:2171
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 make_node_invariant()
Definition: ir.h:2006
void queue_reserve(const int n)
Definition: ir.h:2142
int get_current_level_size()
Definition: ir.h:2234
int stat_leaves() const
Definition: ir.h:2084
void queue_missing_node(missing_node node)
Definition: ir.h:2146
int get_level_size(int level)
Definition: ir.h:2242
void initialize(std::vector< int > &base, ir::limited_save *root)
Definition: ir.h:2067
int h_bfs_automorphism_pw
Definition: ir.h:1997
void mark_first_level(markset &marks)
Definition: ir.h:2158
bool queue_missing_node_empty()
Definition: ir.h:2150
deviation_map stored_deviation
Definition: ir.h:1999
shared_tree(int domain_size)
Definition: ir.h:2001
groups::orbit h_bfs_top_level_orbit
Definition: ir.h:1996
bool reset(std::vector< int > &new_base, ir::limited_save *root, bool keep_old)
Definition: ir.h:2088
void set_finished_up_to(const int new_finished_up_to)
Definition: ir.h:2226
std::vector< unsigned long > * get_node_invariant()
Definition: ir.h:2063
void finish_level(int level)
Definition: ir.h:2200
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
void introspection()
Definition: ir.h:2031
ir::tree_node * pick_node_from_level(const int level, int num)
Definition: ir.h:2216
shared_leaves stored_leaves
Definition: ir.h:1998
void clear_leaves()
Definition: ir.h:2077
missing_node queue_missing_node_pop()
Definition: ir.h:2154
@ STORE_LAB
stores coloring of the leaf
Definition: ir.h:1802
@ STORE_BASE
stores only base of the leaf
Definition: ir.h:1803
int get_lab_or_base_size()
Definition: ir.h:1822
const int * get_lab_or_base()
Definition: ir.h:1818
stored_leaf(int *arr, int arr_sz, stored_leaf_type storetype)
Definition: ir.h:1806
stored_leaf(std::vector< int > &arr, stored_leaf_type storetype)
Definition: ir.h:1812
dej_nodiscard stored_leaf_type get_store_type() const
Definition: ir.h:1826
The trace invariant.
Definition: trace.h:33
dej_nodiscard int get_position() const
Definition: trace.h:316
dej_nodiscard unsigned long get_hash() const
Definition: trace.h:257
void set_record(bool new_record)
Definition: trace.h:299
void op_refine_cell_end()
Definition: trace.h:140
void set_position(int new_position)
Definition: trace.h:308
dej_nodiscard bool trace_equal() const
Definition: trace.h:272
void set_hash(unsigned long new_hash)
Definition: trace.h:265
void op_additional_info(int d)
Definition: trace.h:133
void op_refine_cell_start(int)
Definition: trace.h:113
void reset()
Definition: trace.h:289
void op_refine_start()
Definition: trace.h:103
void set_compare_trace(trace *new_compare_trace)
Definition: trace.h:240
void op_individualize(const int ind_color)
Definition: trace.h:94
void set_compare(bool new_compare)
Definition: trace.h:250
void op_refine_cell_record(int new_color)
Definition: trace.h:127
trace * get_compare_trace()
Definition: trace.h:86
void op_refine_end()
Definition: trace.h:150
void skip_to_individualization()
Definition: trace.h:222
void reserve(const int n)
Definition: trace.h:303
void reset_trace_equal()
Definition: trace.h:279
A node of an IR tree.
Definition: ir.h:1912
tree_node * get_next()
Definition: ir.h:1932
tree_node(limited_save *_data, tree_node *_next, tree_node *_parent, bool ownsdata)
Definition: ir.h:1925
dej_nodiscard bool get_prune() const
Definition: ir.h:1948
dej_nodiscard unsigned long get_hash() const
Definition: ir.h:1955
void set_next(tree_node *new_next)
Definition: ir.h:1938
void add_hash(unsigned long add)
Definition: ir.h:1951
dej_nodiscard bool get_base() const
Definition: ir.h:1963
limited_save * get_save()
Definition: ir.h:1941
tree_node * get_parent()
Definition: ir.h:1935
Internal graph data structure.
Definition: graph.h:19
int * e
Definition: graph.h:46
int v_size
Definition: graph.h:48
int * v
Definition: graph.h:44
int * d
Definition: graph.h:45
int type_selector_hook(const coloring *, const int)
Definition: ir.h:38
ir_mode
Mode of trace for IR search.
Definition: ir.h:31
@ IR_MODE_COMPARE_TRACE_REVERSIBLE
Definition: ir.h:32
@ IR_MODE_RECORD_TRACE
Definition: ir.h:32
@ IR_MODE_COMPARE_TRACE_IRREVERSIBLE
Definition: ir.h:32
std::pair< ir::tree_node *, int > missing_node
Definition: ir.h:1972
Definition: bfs.h:10
Tracks information for a base point.
Definition: ir.h:105
unsigned long trace_hash
Definition: ir.h:113
int touched_color_list_pt
Definition: ir.h:109
base_info(int selColor, int colorSz, int cellNum, int touchedColorListPt, int singletonPt, int tracePos, unsigned long traceHash)
Definition: ir.h:115
Controls movement in IR tree.
Definition: ir.h:130
std::vector< int > * compare_base_vertex
Definition: ir.h:141
std::vector< base_info > * compare_base
Definition: ir.h:142
void compare_to_this()
Definition: ir.h:778
std::vector< base_info > base
Definition: ir.h:139
void singleton_automorphism_base(groups::automorphism_workspace *automorphism)
Definition: ir.h:478
void link_compare(controller *state)
Definition: ir.h:703
bool there_is_difference_to_base()
Definition: ir.h:452
void use_increase_deviation(bool deviation_inc_active)
Definition: ir.h:843
dej_nodiscard coloring * get_coloring() const
Definition: ir.h:925
bool update_diff_vertices_last_individualization(const controller &other_state)
Definition: ir.h:611
coloring * c
Definition: ir.h:132
std::vector< int > singletons
Definition: ir.h:135
void mode_write_base()
Definition: ir.h:424
void link(controller *state)
Definition: ir.h:740
void mode_compare_base()
Definition: ir.h:442
void save_reduced_state(limited_save &state)
Definition: ir.h:883
void move_to_child(sgraph *g, int v)
Definition: ir.h:989
void walk(sgraph *g, ir::limited_save &start_from, std::vector< int > &vertices)
Definition: ir.h:1104
void use_split_limit(bool use_split_limit, int limit=0)
Definition: ir.h:865
void use_reversible(const bool reversible)
Definition: ir.h:816
dej_nodiscard int get_diff_diverge() const
Definition: ir.h:597
void set_increase_deviation(int deviation_inc=48)
Definition: ir.h:854
dej_nodiscard int get_base_pos() const
Definition: ir.h:929
void reserve()
Definition: ir.h:800
void singleton_automorphism(controller &state, groups::automorphism_workspace &automorphism)
Definition: ir.h:584
void use_trace_early_out(bool trace_early_out)
Definition: ir.h:831
worklist touched_color_list
Definition: ir.h:147
markset touched_color
Definition: ir.h:146
void load_reduced_state_without_coloring(limited_save &state)
Definition: ir.h:910
void move_to_child_no_trace(sgraph *g, int v)
Definition: ir.h:1040
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
worklist prev_color_list
Definition: ir.h:148
void color_diff_automorphism_base(groups::automorphism_workspace *automorphism)
Definition: ir.h:491
std::vector< int > * compare_singletons
Definition: ir.h:136
std::pair< int, int > diff_pair(const controller &state)
Definition: ir.h:539
void write_strong_invariant_quarter(const sgraph *g) const
Definition: ir.h:968
int get_number_of_splits()
Definition: ir.h:415
std::vector< int > base_vertex
Definition: ir.h:138
void write_strong_invariant(const sgraph *g) const
Definition: ir.h:948
void write_to_trace(const int d) const
Definition: ir.h:939
void reset_diff()
Definition: ir.h:566
controller(refinement *ref, coloring *col)
Definition: ir.h:384
void refine(sgraph *g)
Definition: ir.h:1050
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
#define dej_nodiscard
Definition: utility.h:46