maude: witness-path search for puzzle solvers (8 tests, 221 total)

lib/maude/searchpath.sx — mau/search-path returns the shortest sequence of states from start to goal (the solution moves), mau/search-length its step count. BFS over all one-step successors, threading the path. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2026-06-07 15:36:46 +00:00
parent ed40af66f5
commit d09af71f6e
6 changed files with 173 additions and 4 deletions
--- a/lib/maude/searchpath.sx
+++ b/lib/maude/searchpath.sx
@@ -0,0 +1,96 @@
+;; lib/maude/searchpath.sx — reachability search returning the witness path.
+;;
+;; mau/search (rewrite.sx) answers yes/no. For puzzle solvers you want the
+;; actual sequence of states from start to goal. mau/search-path runs the same
+;; BFS but threads the path so far; it returns the list of canonical states
+;; start..goal (shortest by step count) or nil if unreachable within depth.
+
+(define mau/reverse2 (fn (xs) (mau/rev-acc xs (list))))
+
+(define
+  mau/rev-acc
+  (fn
+    (xs acc)
+    (if (empty? xs) acc (mau/rev-acc (rest xs) (cons (first xs) acc)))))
+
+;; find a frontier path whose current state (its head) matches the goal canon
+(define
+  mau/path-hit
+  (fn
+    (theory frontier goal)
+    (cond
+      ((empty? frontier) nil)
+      ((= (mau/canon theory (first (first frontier))) goal)
+        (first frontier))
+      (else (mau/path-hit theory (rest frontier) goal)))))
+
+(define
+  mau/bfs-path
+  (fn
+    (theory eqs rules frontier seen goal depth)
+    (let
+      ((hit (mau/path-hit theory frontier goal)))
+      (cond
+        ((not (= hit nil)) hit)
+        ((<= depth 0) nil)
+        ((empty? frontier) nil)
+        (else
+          (let
+            ((newf (list)) (newseen seen))
+            (for-each
+              (fn
+                (path)
+                (for-each
+                  (fn
+                    (succ)
+                    (let
+                      ((c (mau/canon theory succ)))
+                      (when
+                        (not (mau/member? c newseen))
+                        (do
+                          (set! newseen (cons c newseen))
+                          (append! newf (cons succ path))))))
+                  (mau/all-successors theory eqs rules (first path))))
+              frontier)
+            (mau/bfs-path
+              theory
+              eqs
+              rules
+              newf
+              newseen
+              goal
+              (- depth 1))))))))
+
+(define
+  mau/search-path
+  (fn
+    (m start-src goal-src max-depth)
+    (let
+      ((theory (mau/build-theory m))
+        (eqs (mau/module-eqs m))
+        (rules (mau/module-rules m)))
+      (let
+        ((start (mau/cnormalize theory eqs (mau/parse-term-in m start-src) mau/reduce-fuel))
+          (goal
+            (mau/canon
+              theory
+              (mau/cnormalize
+                theory
+                eqs
+                (mau/parse-term-in m goal-src)
+                mau/reduce-fuel))))
+        (let
+          ((res (mau/bfs-path theory eqs rules (list (list start)) (list (mau/canon theory start)) goal max-depth)))
+          (if
+            (= res nil)
+            nil
+            (map (fn (t) (mau/canon theory t)) (mau/reverse2 res))))))))
+
+;; number of steps in the shortest solution (nil if unreachable)
+(define
+  mau/search-length
+  (fn
+    (m start-src goal-src max-depth)
+    (let
+      ((p (mau/search-path m start-src goal-src max-depth)))
+      (if (= p nil) nil (- (len p) 1)))))