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 (3907B)

      1 STATIC long long checkdata_h48(
      2     const char *, unsigned long long, const unsigned char *);
      3 
      4 /*
      5 Currently unused.
      6 TODO: re-introduce check on cocsep table
      7 */
      8 uint64_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 
     21 struct {
     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 
    177 STATIC long long
    178 checkdata_h48(
    179 	const char *solver,
    180 	unsigned long long data_size,
    181 	const unsigned char *data
    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 }