nissy-core

The "engine" of nissy, including the H48 optimal solver.
git clone https://git.tronto.net/nissy-core
Download | Log | Files | Refs | README | LICENSE

checkdata.h (3905B)


      1 STATIC long long checkdata_h48(
      2     const char *, unsigned long long, const unsigned char *);
      3 
      4 /* TODO: Currently unused, re-introduce check on cocsep table */
      5 uint64_t expected_cocsep[21] = {
      6 	[0] = 1,
      7 	[1] = 6,
      8 	[2] = 63,
      9 	[3] = 468,
     10 	[4] = 3068,
     11 	[5] = 15438,
     12 	[6] = 53814,
     13 	[7] = 71352,
     14 	[8] = 8784,
     15 	[9] = 96
     16 };
     17 
     18 struct {
     19 	uint8_t max;
     20 	uint64_t table[21];
     21 } expected_h48[12][9] = {
     22 	[0] = {
     23 		[2] = {
     24 			.max = 3,
     25 			.table = {
     26 				[0] = 5473562,
     27 				[1] = 34776317,
     28 				[2] = 68566704,
     29 				[3] = 8750867,
     30 			},
     31 		},
     32 		[4] = {
     33 			.max = 12,
     34 			.table = {
     35 				[0] = 1,
     36 				[1] = 1,
     37 				[2] = 4,
     38 				[3] = 34,
     39 				[4] = 331,
     40 				[5] = 3612,
     41 				[6] = 41605,
     42 				[7] = 474128,
     43 				[8] = 4953846,
     44 				[9] = 34776317,
     45 				[10] = 68566704,
     46 				[11] = 8749194,
     47 				[12] = 1673,
     48 			},
     49 		},
     50 	},
     51 	[1] = {
     52 		[2] = {
     53 			.max = 3,
     54 			.table = {
     55 				[0] = 6012079,
     56 				[1] = 45822302,
     57 				[2] = 142018732,
     58 				[3] = 41281787,
     59 			},
     60 		},
     61 	},
     62 	[2] = {
     63 		[2] = {
     64 			.max = 3,
     65 			.table = {
     66 				[0] = 6391286,
     67 				[1] = 55494785,
     68 				[2] = 252389935,
     69 				[3] = 155993794,
     70 			},
     71 		},
     72 	},
     73 	[3] = {
     74 		[2] = {
     75 			.max = 3,
     76 			.table = {
     77 				[0] = 6686828,
     78 				[1] = 63867852,
     79 				[2] = 392789689,
     80 				[3] = 477195231,
     81 			},
     82 		},
     83 	},
     84 	[4] = {
     85 		[2] = {
     86 			.max = 3,
     87 			.table = {
     88 				[0] = 77147213,
     89 				[1] = 543379415,
     90 				[2] = 1139570251,
     91 				[3] = 120982321,
     92 			},
     93 		},
     94 	},
     95 	[5] = {
     96 		[2] = {
     97 			.max = 3,
     98 			.table = {
     99 				[0] = 82471284,
    100 				[1] = 687850732,
    101 				[2] = 2345840746,
    102 				[3] = 645995638,
    103 			},
    104 		},
    105 	},
    106 	[6] = {
    107 		[2] = {
    108 			.max = 3,
    109 			.table = {
    110 				[0] = 85941099,
    111 				[1] = 804752968,
    112 				[2] = 4077248182,
    113 				[3] = 2556374551,
    114 			},
    115 		},
    116 	},
    117 	[7] = {
    118 		[2] = {
    119 			.max = 3,
    120 			.table = {
    121 				[0] = 88529761,
    122 				[1] = 897323475,
    123 				[2] = 6126260791,
    124 				[3] = 7936519573,
    125 			},
    126 		},
    127 	},
    128 	[8] = {
    129 		[2] = {
    130 			.max = 3,
    131 			.table = {
    132 				[0] = 1051579940,
    133 				[1] = 8136021316,
    134 				[2] = 19024479822,
    135 				[3] = 1885186122,
    136 			},
    137 		},
    138 	},
    139 	[9] = {
    140 		[2] = {
    141 			.max = 3,
    142 			.table = {
    143 				[0] = 1102038189,
    144 				[1] = 9888265242,
    145 				[2] = 38299375805,
    146 				[3] = 10904855164,
    147 			},
    148 		},
    149 	},
    150 	[10] = {
    151 		[2] = {
    152 			.max = 3,
    153 			.table = {
    154 				[0] = 1133240039,
    155 				[1] = 11196285614,
    156 				[2] = 64164702961,
    157 				[3] = 43894840186,
    158 			},
    159 		},
    160 	},
    161 	[11] = {
    162 		[2] = {
    163 			.max = 3,
    164 			.table = {
    165 				[0] = 1150763161,
    166 				[1] = 12045845660,
    167 				[2] = 91163433330,
    168 				[3] = 136418095449,
    169 			},
    170 		},
    171 	},
    172 };
    173 
    174 STATIC long long
    175 checkdata_h48(
    176 	const char *solver,
    177 	unsigned long long data_size,
    178 	const unsigned char *data
    179 )
    180 {
    181 	const unsigned char *table;
    182 	tableinfo_t info;
    183 	int64_t err;
    184 	uint64_t actual_distribution[INFO_DISTRIBUTION_LEN];
    185 	uint8_t em;
    186 	uint64_t *ed;
    187 
    188 	if ((size_t)data % 8 != 0) {
    189 		LOG("[checkdata] Error: buffer is not 8-byte aligned\n");
    190 		return NISSY_ERROR_DATA;
    191 	}
    192 
    193 	do {
    194 		err = readtableinfo(data_size, data, &info);
    195 		if (err != NISSY_OK) {
    196 			LOG("[checkdata] Data is corrupt\n");
    197 			return NISSY_ERROR_DATA;
    198 		}
    199 
    200 		table = data + INFOSIZE;
    201 		data += info.next;
    202 		data_size -= info.next;
    203 
    204 		if (info.type != TABLETYPE_PRUNING) {
    205 			LOG("[checkdata] Skipping '%s'\n", info.solver);
    206 			continue;
    207 		}
    208 
    209 		ed = expected_h48[info.h48h][info.bits].table;
    210 		em = expected_h48[info.h48h][info.bits].max;
    211 
    212 		LOG("[checkdata] Checking distribution for '%s' from "
    213 		    "table preamble\n", info.solver);
    214 		if (!distribution_equal(ed, info.distribution, em)) {
    215 			LOG("[checkdata] Distribution from the table preamble "
    216 			    "does not match the expected one\n");
    217 			return NISSY_ERROR_DATA;
    218 		}
    219 
    220 		LOG("[checkdata] Checking distribution for '%s' from "
    221 		    "actual table\n", info.solver);
    222 		getdistribution(table, actual_distribution, &info);
    223 		if (!distribution_equal(ed, actual_distribution, em)) {
    224 			LOG("[checkdata] Distribution from the actual table "
    225 			    "does not match the expected one\n");
    226 			return NISSY_ERROR_DATA;
    227 		}
    228 	} while (info.next != 0);
    229 
    230 	return NISSY_OK;
    231 }