ref: f21d3e4c74b23380f397a7ee0416928ee971a15d
parent: 8629ef8974aa379e578531c4b75ebe8c045286c8
author: Simon Tatham <anakin@pobox.com>
date: Sat May 23 04:34:58 EDT 2020
latin.c: call a user-provided validator function. [NFC] I've only just realised that there's a false-positive bug in the latin.c solver framework. It's designed to solve puzzles in which the solution is a latin square but with some additional constraints provided by the individual puzzle, and so during solving, it runs a mixture of its own standard deduction functions that apply to any latin-square puzzle and extra functions provided by the client puzzle to do deductions based on the extra clues or constraints. But what happens if the _last_ move in the solving process is performed by one of the latin.c built-in methods, and it causes a violation of the client puzzle's extra constraints? Nothing will ever notice, and so the solver will report that the puzzle has a solution when it actually has none. An example is the Group game id 12i:m12b9a1zd9i6d10c3y2l11q4r . This was reported by 'groupsolver -g' as being ambiguous. But if you look at the two 'solutions' reported in the verbose diagnostics, one of them is arrant nonsense: it has no identity element at all, and therefore, it fails associativity all over the place. Actually that puzzle _does_ have a unique solution. This bug has been around for ages, and nobody has reported a problem. For recursive solving, that's not much of a surprise, because it would cause a spurious accusation of ambiguity, so that at generation time some valid puzzles would be wrongly discarded, and you'd never see them. But at non-recursive levels, I can't see a reason why this bug _couldn't_ have led one of the games to present an actually impossible puzzle believing it to be soluble. Possibly this never came up because the other clients of latin.c are more forgiving of this error in some way. For example, they might all be very likely to use their extra clues early in the solving process, so that the requirements are already baked in by the time the final grid square is filled. I don't know! Anyway. The fix is to introduce last-minute client-side validation: whenever the centralised latin_solver thinks it's come up with a filled grid, it should present it to a puzzle-specific validator function and check that it's _really_ a legal solution. This commit does the plumbing for all of that: it introduces the new validator function as one of the many parameters to latin_solver, and arranges to call it in an appropriate way during the solving process. But all the per-puzzle validation functions are empty, for the moment.
--- a/keen.c
+++ b/keen.c
@@ -591,6 +591,11 @@
#define SOLVER(upper,title,func,lower) func,
static usersolver_t const keen_solvers[] = { DIFFLIST(SOLVER) };
+static bool keen_valid(struct latin_solver *solver, void *ctx)
+{
+ return true; /* FIXME */
+}
+
static int solver(int w, int *dsf, long *clues, digit *soln, int maxdiff)
{
int a = w*w;
@@ -638,7 +643,7 @@
ret = latin_solver(soln, w, maxdiff,
DIFF_EASY, DIFF_HARD, DIFF_EXTREME,
DIFF_EXTREME, DIFF_UNREASONABLE,
- keen_solvers, &ctx, NULL, NULL);
+ keen_solvers, keen_valid, &ctx, NULL, NULL);
sfree(ctx.dscratch);
sfree(ctx.iscratch);
--- a/latin.c
+++ b/latin.c
@@ -19,8 +19,8 @@
static int latin_solver_top(struct latin_solver *solver, int maxdiff,
int diff_simple, int diff_set_0, int diff_set_1,
int diff_forcing, int diff_recursive,
- usersolver_t const *usersolvers, void *ctx,
- ctxnew_t ctxnew, ctxfree_t ctxfree);
+ usersolver_t const *usersolvers, validator_t valid,
+ void *ctx, ctxnew_t ctxnew, ctxfree_t ctxfree);
#ifdef STANDALONE_SOLVER
int solver_show_working, solver_recurse_depth;
@@ -711,7 +711,7 @@
static int latin_solver_recurse
(struct latin_solver *solver, int diff_simple, int diff_set_0,
int diff_set_1, int diff_forcing, int diff_recursive,
- usersolver_t const *usersolvers, void *ctx,
+ usersolver_t const *usersolvers, validator_t valid, void *ctx,
ctxnew_t ctxnew, ctxfree_t ctxfree)
{
int best, bestcount;
@@ -817,7 +817,8 @@
ret = latin_solver_top(&subsolver, diff_recursive,
diff_simple, diff_set_0, diff_set_1,
diff_forcing, diff_recursive,
- usersolvers, newctx, ctxnew, ctxfree);
+ usersolvers, valid, newctx,
+ ctxnew, ctxfree);
latin_solver_free(&subsolver);
if (ctxnew)
ctxfree(newctx);
@@ -879,8 +880,8 @@
static int latin_solver_top(struct latin_solver *solver, int maxdiff,
int diff_simple, int diff_set_0, int diff_set_1,
int diff_forcing, int diff_recursive,
- usersolver_t const *usersolvers, void *ctx,
- ctxnew_t ctxnew, ctxfree_t ctxfree)
+ usersolver_t const *usersolvers, validator_t valid,
+ void *ctx, ctxnew_t ctxnew, ctxfree_t ctxfree)
{
struct latin_solver_scratch *scratch = latin_solver_new_scratch(solver);
int ret, diff = diff_simple;
@@ -941,7 +942,8 @@
int nsol = latin_solver_recurse(solver,
diff_simple, diff_set_0, diff_set_1,
diff_forcing, diff_recursive,
- usersolvers, ctx, ctxnew, ctxfree);
+ usersolvers, valid, ctx,
+ ctxnew, ctxfree);
if (nsol < 0) diff = diff_impossible;
else if (nsol == 1) diff = diff_recursive;
else if (nsol > 1) diff = diff_ambiguous;
@@ -990,6 +992,17 @@
}
#endif
+ if (diff != diff_impossible && diff != diff_unfinished &&
+ diff != diff_ambiguous && valid && !valid(solver, ctx)) {
+#ifdef STANDALONE_SOLVER
+ if (solver_show_working) {
+ printf("%*ssolution failed final validation!\n",
+ solver_recurse_depth*4, "");
+ }
+#endif
+ diff = diff_impossible;
+ }
+
latin_solver_free_scratch(scratch);
return diff;
@@ -998,8 +1011,8 @@
int latin_solver_main(struct latin_solver *solver, int maxdiff,
int diff_simple, int diff_set_0, int diff_set_1,
int diff_forcing, int diff_recursive,
- usersolver_t const *usersolvers, void *ctx,
- ctxnew_t ctxnew, ctxfree_t ctxfree)
+ usersolver_t const *usersolvers, validator_t valid,
+ void *ctx, ctxnew_t ctxnew, ctxfree_t ctxfree)
{
int diff;
#ifdef STANDALONE_SOLVER
@@ -1027,7 +1040,7 @@
diff = latin_solver_top(solver, maxdiff,
diff_simple, diff_set_0, diff_set_1,
diff_forcing, diff_recursive,
- usersolvers, ctx, ctxnew, ctxfree);
+ usersolvers, valid, ctx, ctxnew, ctxfree);
#ifdef STANDALONE_SOLVER
sfree(names);
@@ -1040,8 +1053,8 @@
int latin_solver(digit *grid, int o, int maxdiff,
int diff_simple, int diff_set_0, int diff_set_1,
int diff_forcing, int diff_recursive,
- usersolver_t const *usersolvers, void *ctx,
- ctxnew_t ctxnew, ctxfree_t ctxfree)
+ usersolver_t const *usersolvers, validator_t valid,
+ void *ctx, ctxnew_t ctxnew, ctxfree_t ctxfree)
{
struct latin_solver solver;
int diff;
@@ -1050,7 +1063,7 @@
diff = latin_solver_main(&solver, maxdiff,
diff_simple, diff_set_0, diff_set_1,
diff_forcing, diff_recursive,
- usersolvers, ctx, ctxnew, ctxfree);
+ usersolvers, valid, ctx, ctxnew, ctxfree);
latin_solver_free(&solver);
return diff;
}
--- a/latin.h
+++ b/latin.h
@@ -85,6 +85,7 @@
bool extreme);
typedef int (*usersolver_t)(struct latin_solver *solver, void *ctx);
+typedef bool (*validator_t)(struct latin_solver *solver, void *ctx);
typedef void *(*ctxnew_t)(void *ctx);
typedef void (*ctxfree_t)(void *ctx);
@@ -96,15 +97,15 @@
int latin_solver(digit *grid, int o, int maxdiff,
int diff_simple, int diff_set_0, int diff_set_1,
int diff_forcing, int diff_recursive,
- usersolver_t const *usersolvers, void *ctx,
- ctxnew_t ctxnew, ctxfree_t ctxfree);
+ usersolver_t const *usersolvers, validator_t valid,
+ void *ctx, ctxnew_t ctxnew, ctxfree_t ctxfree);
/* Version you can call if you want to alloc and free latin_solver yourself */
int latin_solver_main(struct latin_solver *solver, int maxdiff,
int diff_simple, int diff_set_0, int diff_set_1,
int diff_forcing, int diff_recursive,
- usersolver_t const *usersolvers, void *ctx,
- ctxnew_t ctxnew, ctxfree_t ctxfree);
+ usersolver_t const *usersolvers, validator_t valid,
+ void *ctx, ctxnew_t ctxnew, ctxfree_t ctxfree);
void latin_solver_debug(unsigned char *cube, int o);
--- a/towers.c
+++ b/towers.c
@@ -574,6 +574,11 @@
#define SOLVER(upper,title,func,lower) func,
static usersolver_t const towers_solvers[] = { DIFFLIST(SOLVER) };
+static bool towers_valid(struct latin_solver *solver, void *ctx)
+{
+ return true; /* FIXME */
+}
+
static int solver(int w, int *clues, digit *soln, int maxdiff)
{
int ret;
@@ -589,7 +594,7 @@
ret = latin_solver(soln, w, maxdiff,
DIFF_EASY, DIFF_HARD, DIFF_EXTREME,
DIFF_EXTREME, DIFF_UNREASONABLE,
- towers_solvers, &ctx, NULL, NULL);
+ towers_solvers, towers_valid, &ctx, NULL, NULL);
sfree(ctx.iscratch);
sfree(ctx.dscratch);
--- a/unequal.c
+++ b/unequal.c
@@ -816,6 +816,11 @@
#define SOLVER(upper,title,func,lower) func,
static usersolver_t const unequal_solvers[] = { DIFFLIST(SOLVER) };
+static bool unequal_valid(struct latin_solver *solver, void *ctx)
+{
+ return true; /* FIXME */
+}
+
static int solver_state(game_state *state, int maxdiff)
{
struct solver_ctx *ctx = new_ctx(state);
@@ -827,7 +832,8 @@
diff = latin_solver_main(&solver, maxdiff,
DIFF_LATIN, DIFF_SET, DIFF_EXTREME,
DIFF_EXTREME, DIFF_RECURSIVE,
- unequal_solvers, ctx, clone_ctx, free_ctx);
+ unequal_solvers, unequal_valid, ctx,
+ clone_ctx, free_ctx);
memcpy(state->hints, solver.cube, state->order*state->order*state->order);
@@ -2155,7 +2161,8 @@
diff = latin_solver_main(&solver, DIFF_RECURSIVE,
DIFF_LATIN, DIFF_SET, DIFF_EXTREME,
DIFF_EXTREME, DIFF_RECURSIVE,
- unequal_solvers, ctx, clone_ctx, free_ctx);
+ unequal_solvers, unequal_valid, ctx,
+ clone_ctx, free_ctx);
free_ctx(ctx);
--- a/unfinished/group.c
+++ b/unfinished/group.c
@@ -448,6 +448,11 @@
#define SOLVER(upper,title,func,lower) func,
static usersolver_t const group_solvers[] = { DIFFLIST(SOLVER) };
+static bool group_valid(struct latin_solver *solver, void *ctx)
+{
+ return true; /* FIXME */
+}
+
static int solver(const game_params *params, digit *grid, int maxdiff)
{
int w = params->w;
@@ -471,7 +476,7 @@
ret = latin_solver_main(&solver, maxdiff,
DIFF_TRIVIAL, DIFF_HARD, DIFF_EXTREME,
DIFF_EXTREME, DIFF_UNREASONABLE,
- group_solvers, NULL, NULL, NULL);
+ group_solvers, group_valid, NULL, NULL, NULL);
latin_solver_free(&solver);