aboutsummaryrefslogtreecommitdiff
path: root/src/solvers/h48
diff options
context:
space:
mode:
Diffstat (limited to 'src/solvers/h48')
-rw-r--r--src/solvers/h48/checkdata.h234
-rw-r--r--src/solvers/h48/gendata_eoesep.h4
-rw-r--r--src/solvers/h48/gendata_h48.h90
-rw-r--r--src/solvers/h48/h48.h1
4 files changed, 237 insertions, 92 deletions
diff --git a/src/solvers/h48/checkdata.h b/src/solvers/h48/checkdata.h
new file mode 100644
index 0000000..53e616b
--- /dev/null
+++ b/src/solvers/h48/checkdata.h
@@ -0,0 +1,234 @@
1STATIC long long checkdata_h48(
2 const char *, unsigned long long n, const unsigned char [n]);
3
4/*
5Currently unused.
6TODO: re-introduce check on cocsep table
7*/
8uint64_t expected_cocsep[21] = {
9 [0] = 1,
10 [1] = 6,
11 [2] = 63,
12 [3] = 468,
13 [4] = 3068,
14 [5] = 15438,
15 [6] = 53814,
16 [7] = 71352,
17 [8] = 8784,
18 [9] = 96
19};
20
21struct {
22 uint8_t max;
23 uint64_t table[21];
24} expected_h48[12][9] = {
25 [0] = {
26 [2] = {
27 .max = 3,
28 .table = {
29 [0] = 5473562,
30 [1] = 34776317,
31 [2] = 68566704,
32 [3] = 8750867,
33 },
34 },
35 [4] = {
36 .max = 12,
37 .table = {
38 [0] = 1,
39 [1] = 1,
40 [2] = 4,
41 [3] = 34,
42 [4] = 331,
43 [5] = 3612,
44 [6] = 41605,
45 [7] = 474128,
46 [8] = 4953846,
47 [9] = 34776317,
48 [10] = 68566704,
49 [11] = 8749194,
50 [12] = 1673,
51 },
52 },
53 },
54 [1] = {
55 [2] = {
56 .max = 3,
57 .table = {
58 [0] = 6012079,
59 [1] = 45822302,
60 [2] = 142018732,
61 [3] = 41281787,
62 },
63 },
64 },
65 [2] = {
66 [2] = {
67 .max = 3,
68 .table = {
69 [0] = 6391286,
70 [1] = 55494785,
71 [2] = 252389935,
72 [3] = 155993794,
73 },
74 },
75 },
76 [3] = {
77 [2] = {
78 .max = 3,
79 .table = {
80 [0] = 6686828,
81 [1] = 63867852,
82 [2] = 392789689,
83 [3] = 477195231,
84 },
85 },
86 },
87 [4] = {
88 [2] = {
89 .max = 3,
90 .table = {
91 [0] = 77147213,
92 [1] = 543379415,
93 [2] = 1139570251,
94 [3] = 120982321,
95 },
96 },
97 },
98 [5] = {
99 [2] = {
100 .max = 3,
101 .table = {
102 [0] = 82471284,
103 [1] = 687850732,
104 [2] = 2345840746,
105 [3] = 645995638,
106 },
107 },
108 },
109 [6] = {
110 [2] = {
111 .max = 3,
112 .table = {
113 [0] = 85941099,
114 [1] = 804752968,
115 [2] = 4077248182,
116 [3] = 2556374551,
117 },
118 },
119 },
120 [7] = {
121 [2] = {
122 .max = 3,
123 .table = {
124 [0] = 88529761,
125 [1] = 897323475,
126 [2] = 6126260791,
127 [3] = 7936519573,
128 },
129 },
130 },
131 [8] = {
132 [2] = {
133 .max = 3,
134 .table = {
135 [0] = 1051579940,
136 [1] = 8136021316,
137 [2] = 19024479822,
138 [3] = 18851861220,
139 },
140 },
141 },
142 [9] = {
143 [2] = {
144 .max = 3,
145 .table = {
146 [0] = 1102038189,
147 [1] = 9888265242,
148 [2] = 38299375805,
149 [3] = 10904855164,
150 },
151 },
152 },
153 [10] = {
154 [2] = {
155 .max = 3,
156 .table = {
157 [0] = 1133240039,
158 [1] = 11196285614,
159 [2] = 64164702961,
160 [3] = 43894840186,
161 },
162 },
163 },
164 [11] = {
165 [2] = {
166 .max = 3,
167 .table = {
168 [0] = 1150763161,
169 [1] = 12045845660,
170 [2] = 91163433330,
171 [3] = 136418095449,
172 },
173 },
174 },
175};
176
177STATIC long long
178checkdata_h48(
179 const char *solver,
180 unsigned long long data_size,
181 const unsigned char data[data_size]
182)
183{
184 const unsigned char *table;
185 tableinfo_t info;
186 int64_t err;
187 uint64_t actual_distribution[INFO_DISTRIBUTION_LEN];
188 uint8_t em;
189 uint64_t *ed;
190
191 if ((size_t)data % 8 != 0) {
192 LOG("[checkdata] Error: buffer is not 8-byte aligned\n");
193 return NISSY_ERROR_DATA;
194 }
195
196 do {
197 err = readtableinfo(data_size, data, &info);
198 if (err != NISSY_OK) {
199 LOG("[checkdata] Data is corrupt\n");
200 return NISSY_ERROR_DATA;
201 }
202
203 table = data + INFOSIZE;
204 data += info.next;
205 data_size -= info.next;
206
207 if (info.type != TABLETYPE_PRUNING) {
208 LOG("[checkdata] Skipping '%s'\n", info.solver);
209 continue;
210 }
211
212 ed = expected_h48[info.h48h][info.bits].table;
213 em = expected_h48[info.h48h][info.bits].max;
214
215 LOG("[checkdata] Checking distribution for '%s' from "
216 "table preamble\n", info.solver);
217 if (!distribution_equal(ed, info.distribution, em)) {
218 LOG("[checkdata] Distribution from the table preamble "
219 "does not matche the expected one\n");
220 return NISSY_ERROR_DATA;
221 }
222
223 LOG("[checkdata] Checking distribution for '%s' from "
224 "actual table\n", info.solver);
225 getdistribution(table, actual_distribution, &info);
226 if (!distribution_equal(ed, actual_distribution, em)) {
227 LOG("[checkdata] Distribution from the actual table "
228 "does not match the expected one\n");
229 return NISSY_ERROR_DATA;
230 }
231 } while (info.next != 0);
232
233 return NISSY_OK;
234}
diff --git a/src/solvers/h48/gendata_eoesep.h b/src/solvers/h48/gendata_eoesep.h
index f1e3d4c..52e2b8b 100644
--- a/src/solvers/h48/gendata_eoesep.h
+++ b/src/solvers/h48/gendata_eoesep.h
@@ -79,7 +79,7 @@ gendata_eoesep(unsigned char *buf, uint8_t maxdepth)
79 if (buf == NULL) 79 if (buf == NULL)
80 goto gendata_eoesep_return_size; 80 goto gendata_eoesep_return_size;
81 81
82 LOG("Computing eoesep data\n"); 82 LOG("[H48 gendata] Computing eoesep data\n");
83 memset(buf, 0xFF, EOESEP_FULLSIZE); 83 memset(buf, 0xFF, EOESEP_FULLSIZE);
84 esep_classes = (uint32_t *)(buf + INFOSIZE); 84 esep_classes = (uint32_t *)(buf + INFOSIZE);
85 buf8 = buf + INFOSIZE + 4*ESEP_MAX; 85 buf8 = buf + INFOSIZE + 4*ESEP_MAX;
@@ -111,7 +111,7 @@ gendata_eoesep(unsigned char *buf, uint8_t maxdepth)
111 111
112 writetableinfo(&info, EOESEP_FULLSIZE, buf); 112 writetableinfo(&info, EOESEP_FULLSIZE, buf);
113 113
114 LOG("eoesep data computed\n"); 114 LOG("[H48 gendata] eoesep data computed\n");
115 115
116gendata_eoesep_return_size: 116gendata_eoesep_return_size:
117 return EOESEP_FULLSIZE; 117 return EOESEP_FULLSIZE;
diff --git a/src/solvers/h48/gendata_h48.h b/src/solvers/h48/gendata_h48.h
index 644ddc2..d1ab3bd 100644
--- a/src/solvers/h48/gendata_h48.h
+++ b/src/solvers/h48/gendata_h48.h
@@ -25,8 +25,6 @@ STATIC_INLINE uint8_t get_h48_pval_atomic(
25STATIC_INLINE void set_h48_pval_atomic( 25STATIC_INLINE void set_h48_pval_atomic(
26 _Atomic unsigned char *, int64_t, uint8_t, uint8_t); 26 _Atomic unsigned char *, int64_t, uint8_t, uint8_t);
27 27
28size_t gendata_h48_derive(uint8_t, const unsigned char *, unsigned char *);
29
30STATIC long long 28STATIC long long
31gendata_h48_dispatch( 29gendata_h48_dispatch(
32 const char *solver, 30 const char *solver,
@@ -711,91 +709,3 @@ set_h48_pval_atomic(
711 table[H48_INDEX(i, k)] = (table[H48_INDEX(i, k)] & (~H48_MASK(i, k))) 709 table[H48_INDEX(i, k)] = (table[H48_INDEX(i, k)] & (~H48_MASK(i, k)))
712 | (val << H48_SHIFT(i, k)); 710 | (val << H48_SHIFT(i, k));
713} 711}
714
715size_t
716gendata_h48_derive(uint8_t h, const unsigned char *fulltable, unsigned char *buf)
717{
718 size_t cocsepsize, h48size;
719 uint8_t val_full, val_derive;
720 const unsigned char *h48full;
721 unsigned char *h48derive;
722 int64_t i, j, h48max;
723 uint64_t bufsize;
724 gendata_h48_arg_t arg;
725 tableinfo_t cocsepinfo, fulltableinfo;
726
727 /* Initializing values in case of error */
728 /* TODO cleanup this */
729 fulltableinfo.h48h = 11;
730 fulltableinfo.bits = 2;
731 fulltableinfo.base = 8;
732
733 int64_t TODOlarge = 999999999999; /* TODO: cleanup here */
734
735 readtableinfo_n(TODOlarge, fulltable, 2, &fulltableinfo);
736 arg.h = h;
737 arg.k = fulltableinfo.bits;
738 arg.maxdepth = 20;
739 arg.buf = buf;
740 arg.cocsepdata = (uint32_t *)(buf + INFOSIZE);
741 arg.base = fulltableinfo.base;
742 arg.info = makeinfo_h48k2(&arg);
743
744 /* Technically this step is redundant, except that we
745 need selfsim and crep */
746 cocsepsize = gendata_cocsep(buf, arg.selfsim, arg.crep);
747 arg.h48buf = (_Atomic unsigned char *)buf + cocsepsize;
748 h48size = H48_TABLESIZE(h, arg.k) + INFOSIZE;
749
750 if (buf == NULL)
751 goto gendata_h48_derive_return_size;
752
753 bufsize = COCSEP_FULLSIZE + INFOSIZE;
754 if (readtableinfo(bufsize, buf, &cocsepinfo) != NISSY_OK) {
755 LOG("[H48 derive gendata] Error: could not read info for "
756 "cocsep table\n");
757 goto gendata_h48_derive_error;
758 }
759
760 cocsepinfo.next = cocsepsize;
761 bufsize = COCSEP_FULLSIZE + INFOSIZE;
762 if (writetableinfo(&cocsepinfo, bufsize, buf) != NISSY_OK) {
763 LOG("[H48 derive gendata] Error: could not write info for "
764 "cocsep table with updated 'next' value\n");
765 goto gendata_h48_derive_error;
766 }
767
768 h48full = fulltable + cocsepsize + INFOSIZE;
769 h48derive = (unsigned char *)arg.h48buf + INFOSIZE;
770 memset(h48derive, 0xFF, H48_TABLESIZE(h, arg.k));
771 memset(arg.info.distribution, 0,
772 INFO_DISTRIBUTION_LEN * sizeof(uint64_t));
773
774 h48max = H48_COORDMAX(fulltableinfo.h48h);
775 for (i = 0; i < h48max; i++) {
776 if (i % INT64_C(1000000000) == 0 && i > 0)
777 LOG("[H48 derive gendata] Processing %" PRId64
778 "th coordinate\n", i);
779 j = i >> (int64_t)(fulltableinfo.h48h - h);
780 val_full = get_h48_pval(h48full, i, arg.k);
781 val_derive = get_h48_pval(h48derive, j, arg.k);
782 set_h48_pval(
783 h48derive, j, arg.k, MIN(val_full, val_derive));
784 }
785
786 getdistribution(h48derive, arg.info.distribution, &arg.info);
787
788 bufsize = arg.buf_size - COCSEP_FULLSIZE - INFOSIZE;
789 if (writetableinfo(&arg.info, bufsize, (unsigned char *)arg.h48buf)
790 != NISSY_OK) {
791 LOG("H48 derive gendata] Error: could not write info "
792 "for table\n");
793 goto gendata_h48_derive_error;
794 }
795
796gendata_h48_derive_return_size:
797 return cocsepsize + h48size;
798
799gendata_h48_derive_error:
800 return 0;
801}
diff --git a/src/solvers/h48/h48.h b/src/solvers/h48/h48.h
index 79d2583..44fdb59 100644
--- a/src/solvers/h48/h48.h
+++ b/src/solvers/h48/h48.h
@@ -7,4 +7,5 @@
7#include "gendata_cocsep.h" 7#include "gendata_cocsep.h"
8#include "gendata_eoesep.h" 8#include "gendata_eoesep.h"
9#include "gendata_h48.h" 9#include "gendata_h48.h"
10#include "checkdata.h"
10#include "solve.h" 11#include "solve.h"

Generated with cgit - Back to sebastiano.tronto.net