chiark / gitweb /
latin.c: call a user-provided validator function. [NFC]
authorSimon Tatham <anakin@pobox.com>
Sat, 23 May 2020 07:34:58 +0000 (08:34 +0100)
committerSimon Tatham <anakin@pobox.com>
Sat, 23 May 2020 08:08:08 +0000 (09:08 +0100)
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.

keen.c
latin.c
latin.h
towers.c
unequal.c
unfinished/group.c

diff --git a/keen.c b/keen.c
index baa1d81802f56329f92f2a0af49adc7eb3a43efb..4c6e330cb0d5b573e24cd430dd61514d460858e8 100644 (file)
--- a/keen.c
+++ b/keen.c
@@ -591,6 +591,11 @@ static int solver_hard(struct latin_solver *solver, void *vctx)
 #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 @@ static int solver(int w, int *dsf, long *clues, digit *soln, int maxdiff)
     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);
diff --git a/latin.c b/latin.c
index 9d06ccd9384dcfaed6670610b9813f790f14afc2..39930166e789d5119daf00e90a67f62b735a383a 100644 (file)
--- 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 @@ int latin_solver_diff_set(struct latin_solver *solver,
 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 @@ static int latin_solver_recurse
             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_recurse
 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 @@ static int latin_solver_top(struct latin_solver *solver, int maxdiff,
         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 @@ static int latin_solver_top(struct latin_solver *solver, int maxdiff,
     }
 #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 @@ static int latin_solver_top(struct latin_solver *solver, int maxdiff,
 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 @@ int latin_solver_main(struct latin_solver *solver, int maxdiff,
     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_main(struct latin_solver *solver, int maxdiff,
 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 @@ int latin_solver(digit *grid, int o, int maxdiff,
     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;
 }
diff --git a/latin.h b/latin.h
index ff6f07c922e8cd25c075d8b617852bb7eaec67a4..bb172ec3c781f581efd378c0e22adeb67770cfa2 100644 (file)
--- a/latin.h
+++ b/latin.h
@@ -85,6 +85,7 @@ int latin_solver_diff_set(struct latin_solver *solver,
                           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 @@ enum { diff_impossible = 10, diff_ambiguous, diff_unfinished };
 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);
 
index a72cae680d2dd07b171f92780f19e9f08eece45e..27d875150a28af87b58da8457b7e7ee010b7c3ba 100644 (file)
--- a/towers.c
+++ b/towers.c
@@ -574,6 +574,11 @@ static int solver_hard(struct latin_solver *solver, void *vctx)
 #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 @@ static int solver(int w, int *clues, digit *soln, int maxdiff)
     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);
index d5b2bb1aa8c3b7ba4e6ab2de6109d1219c979819..a1b01b80882a0861da3571351a8eb4d9ee104288 100644 (file)
--- a/unequal.c
+++ b/unequal.c
@@ -816,6 +816,11 @@ static int solver_set(struct latin_solver *solver, void *vctx)
 #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 @@ static int solver_state(game_state *state, int maxdiff)
     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 @@ static int solve(game_params *p, char *desc, int debug)
     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);
 
index 3c565cb976b953f4d5bd10e61545afcd8619ad69..3a44a678720e3e884412074bfa281d2a88dd3b73 100644 (file)
@@ -448,6 +448,11 @@ static int solver_normal(struct latin_solver *solver, void *vctx)
 #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 @@ static int solver(const game_params *params, digit *grid, int maxdiff)
     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);