dejavu
Fast probabilistic symmetry detection.
Loading...
Searching...
No Matches
trace.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_TRACE_H
6#define DEJAVU_TRACE_H
7
8#include <vector>
9#include <cassert>
10#include <cstdint>
11
12namespace dejavu {
13 namespace ir {
14#define TRACE_MARKER_INDIVIDUALIZE (INT32_MAX-7)
15#define TRACE_MARKER_REFINE_START (INT32_MAX-2)
16#define TRACE_MARKER_REFINE_END (INT32_MAX-3)
17#define TRACE_MARKER_REFINE_CELL_START (INT32_MAX-4)
18#define TRACE_MARKER_REFINE_CELL_END (INT32_MAX-5)
19
33 class trace {
34 private:
35 // the trace
36 std::vector<int> data;
38 trace *compare_trace = nullptr;
39 unsigned long hash = 0;
41 // mode
42 bool compare = false;
43 bool record = false;
45 // housekeeping
46 // int cell_act_spot = -1;
47 // int cell_old_color = -1;
48 bool assert_cell_act = false;
49 bool assert_refine_act = false;
50
51 // comparison variables
52 int position = 0;
53 bool comp = true;
54
55 void inline add_to_hash(int d) {
56 unsigned long ho = hash & 0xff00000000000000; // extract high-order 8 bits from hash
57 hash = hash << 8; // shift hash left by 5 bits
58 hash = hash ^ (ho >> 56); // move the highorder 5 bits to the low-order
59 hash = hash ^ d; // XOR into hash
60 }
61
62 void write_compare(int d) {
63 d = std::min(INT32_MAX-10,d);
65 write_compare_no_limit(d);
66 dej_assert(record?static_cast<int>(data.size())==position:true);
67 }
68
69 void write_compare_no_limit(int d) {
70 add_to_hash(d);
71 if (record) data.push_back(d);
72 if (compare) comp = comp && (position < ((int) compare_trace->data.size()))
73 && (compare_trace->data[position] == d);
74 ++position;
75 }
76
77 /*void write_skip_compare(int d) {
78 d = std::min(INT32_MAX-10,d);
79 dej_assert(d != TRACE_MARKER_INDIVIDUALIZE && d != TRACE_MARKER_REFINE_START);
80 if (record) data.push_back(d);
81 ++position;
82 }*/
83
84 public:
85
87 return compare_trace;
88 }
89
94 void op_individualize(const int ind_color) {
95 dej_assert(ind_color >= 0);
96 write_compare_no_limit(TRACE_MARKER_INDIVIDUALIZE);
97 write_compare(ind_color);
98 }
99
104 dej_assert(!comp || !assert_refine_act);
105 write_compare_no_limit(TRACE_MARKER_REFINE_START);
106 assert_refine_act = true;
107 }
108
114 dej_assert(!comp || !assert_cell_act);
115 write_compare_no_limit(TRACE_MARKER_REFINE_CELL_START);
116 //write_compare(color);
117 // cell_old_color = color;
118 //cell_act_spot = (int) data.size();
119 //write_skip_compare(false);
120 assert_cell_act = true;
121 }
122
127 void op_refine_cell_record(int new_color) {
128 dej_assert(!comp || assert_cell_act);
129 write_compare(new_color);
130 //if (new_color != cell_old_color && record) data[cell_act_spot] = true;
131 }
132
133 void op_additional_info(int d) {
134 write_compare(d);
135 }
136
141 dej_assert(!comp || assert_cell_act);
142 assert_cell_act = false;
143 //
144 write_compare_no_limit(TRACE_MARKER_REFINE_CELL_END);
145 }
146
151 dej_assert(!comp || !assert_cell_act);
152 dej_assert(assert_refine_act);
153 assert_refine_act = false;
154 write_compare_no_limit(TRACE_MARKER_REFINE_END);
155 }
156
164 if (!compare || !comp || position > static_cast<int>(compare_trace->data.size())) return true;
165
166 dej_assert(compare_trace);
167 size_t read_pt = position;
168 dej_assert(compare_trace->data.size() > read_pt);
169 for(; read_pt > 0 && compare_trace->data[read_pt] != TRACE_MARKER_REFINE_CELL_START; --read_pt);
170 dej_assert(compare_trace->data[read_pt] == TRACE_MARKER_REFINE_CELL_START);
171 ++read_pt;
172
173 dej_assert(compare_trace->data.size() > read_pt);
174 dej_assert((compare_trace->data[read_pt] == false) || (compare_trace->data[read_pt] == true));
175 return compare_trace->data[read_pt];
176 }
177
185 while (position < static_cast<int>(compare_trace->data.size()) &&
186 compare_trace->data[position] != TRACE_MARKER_REFINE_CELL_END) {
187 dej_assert(compare_trace->data.size() > (size_t) position);
188 ++position;
189 }
190 ++position;
191 assert_cell_act = false;
192 }
193
198 assert_cell_act = false;
199 assert_refine_act = false;
200 if (record) {
201 int read_pt = std::max((int) data.size() - 1, 0);
202 while (read_pt > 0 && data[read_pt] != TRACE_MARKER_INDIVIDUALIZE) {
203 --read_pt;
204 }
205 data.resize(read_pt);
206 position = read_pt;
207 }
208 if (compare) {
209 int read_pt = std::max(position - 1, 0);
210 while (read_pt > 0 && compare_trace->data[read_pt] != TRACE_MARKER_INDIVIDUALIZE) {
211 --read_pt;
212 }
213 position = read_pt;
214 }
215 }
216
223 assert_cell_act = false;
224 assert_refine_act = false;
225 if (compare) {
226 int read_pt = position - 1;
227 while ((size_t) read_pt < compare_trace->data.size() &&
228 compare_trace->data[read_pt] != TRACE_MARKER_INDIVIDUALIZE) {
229 ++read_pt;
230 }
231 position = read_pt;
232 }
233 }
234
240 void set_compare_trace(trace *new_compare_trace) {
241 this->compare_trace = new_compare_trace;
242 }
243
250 void set_compare(bool new_compare) {
251 this->compare = new_compare;
252 }
253
257 dej_nodiscard unsigned long get_hash() const {
258 return hash;
259 }
260
265 void set_hash(unsigned long new_hash) {
266 this->hash = new_hash;
267 }
268
273 return comp;
274 }
275
280 comp = true;
281 }
286 comp = false;
287 }
288
289 void reset() {
290 data.clear();
291 compare_trace = nullptr;
292 position = 0;
293 hash = 0;
294 dej_assert(record?static_cast<int>(data.size())==position:true);
296 }
297
298 // record to trace
299 void set_record(bool new_record) {
300 this->record = new_record;
301 }
302
303 void reserve(const int n) {
304 data.reserve(n);
305 }
306
307 // position the trace
308 void set_position(int new_position) {
309 assert_cell_act = false;
310 assert_refine_act = false;
311 this->position = new_position;
312 if(record) data.resize(position);
313 dej_assert(record?static_cast<int>(data.size())==position:true);
314 }
315
317 return position;
318 }
319 };
320 }
321}
322
323
324#endif //DEJAVU_TRACE_H
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 reset_trace_unequal()
Definition: trace.h:285
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 blueprint_skip_to_next_cell()
Definition: trace.h:184
void op_refine_cell_record(int new_color)
Definition: trace.h:127
dej_nodiscard bool blueprint_is_next_cell_active()
Definition: trace.h:163
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
void rewind_to_individualization()
Definition: trace.h:197
Definition: bfs.h:10
#define TRACE_MARKER_REFINE_START
Definition: trace.h:15
#define TRACE_MARKER_REFINE_CELL_END
Definition: trace.h:18
#define TRACE_MARKER_REFINE_END
Definition: trace.h:16
#define TRACE_MARKER_REFINE_CELL_START
Definition: trace.h:17
#define TRACE_MARKER_INDIVIDUALIZE
Definition: trace.h:14
#define dej_assert(expr)
Definition: utility.h:40
#define dej_nodiscard
Definition: utility.h:46