Merge branch 'main' into kjcjohnson/json-problem

com.kjcjohnson.synthkit.asd

@@ -95,12 +95,15 @@
                "com.kjcjohnson.synthkit/smt")
   :serial t
   :components ((:file "package")
+               (:file "variables")
                (:file "counters")
                (:file "atom")
                (:file "node")
                (:file "hole")
+               (:file "traversal")
                (:file "ast")
                (:file "calling-card")
+               (:file "program-compiler")
                (:file "execution")))
 
 (asdf:defsystem "com.kjcjohnson.synthkit/specification"

src/ast/ast.lisp

@@ -3,6 +3,10 @@
 ;;;
 (in-package #:com.kjcjohnson.synthkit.ast)
 
+(deftype transformer ()
+  "A function that takes an input state and returns an output state and success Boolean"
+  '(function (smt:state) (values (or null smt:state) boolean)))
+
 (defgeneric semantics-descriptors-for-non-terminal (semantics non-terminal)
   (:documentation "Gets a list of semantics descriptors valid for NON-TERMINAL."))
 
@@ -23,17 +27,6 @@
   (:method (semantics output) output)
   (:method (semantics (output smt:state)) (smt:canonicalize-state output)))
 
-(defun compile-program (node semantics)
-  (with-slots (production) node
-    (when (null production) (error "Cannot compile a program node without a production."))
-    (let ((input-state-var (gensym "INPUT"))
-          (output-state-var (gensym "OUTPUT")))
-      `(lambda (,input-state-var) ; TODO: update for descriptors properly
-         ,(dolist (s (operational-semantics-for-production semantics nil production))
-            `(let ((,output-state-var (funcall ,s ,input-state-var)))
-               (unless (null ,output-state-var) (return ,output-state-var))))
-         (error "No applicable semantics for production: ~a" ,production)))))
-
 (defun subst-application (relation old-fn-name new-name-computer when arg-transformer)
   (when (typep relation 'smt:application)
     (when (and (string= (smt:name relation) old-fn-name)
@@ -58,7 +51,7 @@
     (setf child-names (nreverse child-names))
     ;; Grab our semantics TODO - handle multiple semantics per production
     (setf rel (first (relational-semantics-for-production semantics rel-name (production node))))
-        
+
     ;; Substitute relations
     (dolist (d (map 'list #'(lambda (c) (relational-semantics-for-non-terminal semantics (g:instance (production c)))) (children node)))
       (subst-application (smt:definition rel)
@@ -81,4 +74,3 @@
 
     ;; Return SMT forms
     (append smt (list (smt:to-smt rel)))))
-

src/ast/atom.lisp

@@ -3,7 +3,58 @@
 ;;;;
 (in-package #:com.kjcjohnson.synthkit.ast)
 
-(defclass program-atom () ())
+(defclass program-atom ()
+  ((compile-cache :accessor %compile-cache
+                  :initarg :compile-cache
+                  :documentation "A-list of descriptors to compiled functions")
+   (compilation-flag :accessor %compilation-flag
+                     :initarg :compilation-flag
+                     :documentation "T if currently compiling this node, else NIL"))
+  ;;(:default-initargs :compile-cache nil :compilation-flag nil)
+  (:documentation "The top-level AST node or hole class"))
+
+;;;
+;;; Cache handling
+;;;
+(defun check-compile-cache (atom descriptor)
+  "Checks the compile cache for ATOM with descriptor DESCRIPTOR. Returns NIL if nothing
+cached, or a transformer function taking and returning states"
+  (and (slot-boundp atom 'compile-cache)
+       (*:when-let (cell (assoc descriptor (%compile-cache atom)))
+         (cdr cell))))
+
+(defun compile-or-cache (atom descriptor comp-fn)
+  "Compiles ATOM if needed, else returns value from the cache"
+  (*:if-let (fn (and (slot-boundp atom 'compile-cache)
+                     (*:assocdr descriptor (%compile-cache atom))))
+    fn
+    (if (and (slot-boundp atom 'compilation-flag)
+             (%compilation-flag atom))
+        #'(lambda (is) ; Don't recursively compile nodes - return a cache lookup lambda
+            (declare (type smt:state is))
+            (declare (optimize (speed 3)))
+            (let ((fn (*:assocdr descriptor (%compile-cache atom) :test #'eql)))
+              (declare (type (function (smt:state) smt:state) fn))
+              (cond
+                ((> *self-recursion-counter* *self-recursion-limit*)
+                 (abort-program-execution)))
+                ;; TODO: can we safely detect when we're not making loop progress?
+              (incf *self-recursion-counter*)
+              (multiple-value-prog1
+                  (funcall fn is)
+                (decf *self-recursion-counter*))))
+        (progn
+          (setf (%compilation-flag atom) t)
+          (let ((fn (funcall comp-fn)))
+            (if (slot-boundp atom 'compile-cache)
+                (push (cons descriptor fn) (%compile-cache atom))
+                (setf (%compile-cache atom) (list (cons descriptor fn))))
+            (setf (%compilation-flag atom) nil)
+            fn)))))
+
+(defmacro do-compile-or-cache ((atom descriptor) &body body)
+  (*:with-thunk (body)
+    `(compile-or-cache ,atom ,descriptor ,body)))
 
 ;;;
 ;;; Program atom protocols
@@ -40,6 +91,12 @@
 (defgeneric non-terminal (program)
   (:documentation "Returns the root non-terminal of PROGRAM"))
 
+(defgeneric invalidate-cache (program)
+  (:documentation "Invalidates caches on PROGRAM")
+  (:method ((atom program-atom))
+            (setf (%compile-cache atom) nil)
+            (setf (%compilation-flag atom) nil)))
+
 (defmacro swap-nth-child (place n thing)
   "Swaps the Nth child of THING with PLACE."
   `(psetf ,place (nth-child ,n ,thing)

src/ast/execution.lisp

@@ -3,35 +3,6 @@
 ;;;;
 (in-package #:com.kjcjohnson.synthkit.ast)
 
-;;;
-;;; Allows exiting a program early
-;;;
-(defvar *program-execution-exit-hook*)
-(defun abort-program-execution ()
-  (funcall *program-execution-exit-hook*))
-
-;;;
-;;; Handles simple unbounded-recursion detection
-;;;
-(defvar *self-recursion-counter* 0
-  "Counts recursion depth to find probably-non-terminating programs.")
-(defparameter *self-recursion-limit* 200)
-
-;;;
-;;; Debugging controls
-;;;
-(defvar *exe-debug* nil "Set to T when execution debugging is triggered")
-(defvar *exe-level* 0 "Level of nested program execution")
-(defvar *exe-debug-match* nil "If non-nil, must be a string that, when contained in the
-serialization of a program node, triggers ``*EXE-DEBUG*`` to be set to T.")
-(declaim (type (or null string) *exe-debug-match*))
-
-;;;
-;;; Stores the root input state
-;;;
-(defvar *root-input-state* nil "The initial input state passed to EXECUTE-PROGRAM")
-(defvar *root-input-descriptor* nil "The initial descriptor passed to EXECUTE-PROGRAM")
-
 ;;;
 ;;; Public execution interface
 ;;;
@@ -48,7 +19,26 @@ serialization of a program node, triggers ``*EXE-DEBUG*`` to be set to T.")
                   (*self-recursion-counter* 0)
                   (*root-input-state* input-state)
                   (*root-input-descriptor* descriptor))
-              (setf result (%execute-program semantics descriptor node input-state)))
+              (if *use-program-compiler*
+                  (let ((comp-fn (compile-program semantics descriptor node)))
+                    (declare (type transformer comp-fn))
+                    (multiple-value-bind (res valid)
+                        (funcall comp-fn input-state)
+                      (if (or (not (null res)) valid)
+                          (setf result res)
+                          (go abort-execution))))
+                  (setf result
+                        (%execute-program semantics descriptor node input-state))))
+
+            ;; --- Validate program compiler ---
+            #+ks2-validate-program-compiler
+            (let* ((compiled-program (compile-program semantics descriptor node))
+                   (comp-ex-result (funcall compiled-program input-state)))
+              (unless (smt:state= result comp-ex-result)
+                (error "Mismatch in behavior: ~a vs. ~a on ~a"
+                       comp-ex-result result node)))
+            ;; ---------------------------------
+
             (go finish-execution)
           abort-execution
             (setf abort-exit t)

src/ast/node.lisp

@@ -41,6 +41,11 @@
   "Returns the non-terminal that this node is rooted at"
   (g:instance (production atom)))
 
+(defmethod invalidate-cache ((node program-node))
+  "Invalidates the cache of all the node's children"
+  (call-next-method) ; Invalidate base atom cache
+  (map nil #'invalidate-cache (children node)))
+
 ;;;
 ;;; Helpers
 ;;;

src/ast/package.lisp

@@ -5,7 +5,8 @@
   (:use #:cl)
   (:local-nicknames (#:g #:com.kjcjohnson.synthkit.grammar)
                     (#:smt #:com.kjcjohnson.synthkit.smt)
-                    (#:a #:alexandria))
+                    (#:a #:alexandria)
+                    (#:* #:serapeum/bundle))
   (:export #:program-atom
            #:program-node
            #:program-hole
@@ -58,4 +59,8 @@
            #:*concrete-candidates-by-size*
            #:*prune-candidate-counter*
            #:*prune-attempt-counter*
-           #:*prune-success-counter*))
+           #:*prune-success-counter*)
+  ;; Control variables
+  (:export #:*use-program-compiler*)
+  ;; Traversals
+  (:export #:traverse-program #:do-traverse-program))

src/ast/program-compiler.lisp

@@ -0,0 +1,45 @@
+;;;;
+;;;; Compiles programs into a single state transformer function
+;;;;
+(in-package #:com.kjcjohnson.synthkit.ast)
+
+(defun %compile-process-calling-card (semantics node cc)
+  "Processes a single calling card and returns a transformer function"
+  (let* ((children-sem-fns
+           (loop for req in (semantics-descriptor-requests cc)
+                 for desc = (semantics-descriptor-request-descriptor req)
+                 for id = (semantics-descriptor-request-node-id req)
+                 if (eql id :self) ; do-compile-and-cache handles the rec call machinery
+                   collect (compile-program semantics desc node)
+                 else
+                   collect (compile-program semantics desc (nth-child id node)))))
+    (funcall (semantic-builder-function cc)
+             children-sem-fns
+             node
+             (children node))))
+
+(defun %compile-combine-chc-transformers (chc-transformers)
+  "Combines multiple CHC transformer functions into a single transformer"
+  (if (> (length chc-transformers) 1)
+      (lambda (input-state)
+        (declare (type smt:state input-state))
+        (declare (optimize (speed 3)))
+        (loop for transformer in chc-transformers
+              do (multiple-value-bind (result valid)
+                     (funcall (the transformer transformer)
+                              input-state)
+                   (when (or (not (null result)) valid)
+                     (return (values result t)))))
+        (error "No applicable semantics"))
+      (first chc-transformers)))
+
+(defun compile-program (semantics descriptor node)
+  "Walks program rooted at NODE and returns a compiled function of one argument, the
+input state, that returns the output state computed using SEMANTICS from DESCRIPTOR"
+  (do-compile-or-cache (node descriptor)
+    (let ((ccs (operational-semantics-for-production semantics
+                                                     descriptor
+                                                     (production node))))
+      (%compile-combine-chc-transformers
+       (loop for cc in ccs
+             collecting (%compile-process-calling-card semantics node cc))))))

src/ast/traversal.lisp

@@ -0,0 +1,26 @@
+;;;;
+;;;; Program traversal
+;;;;
+(in-package #:com.kjcjohnson.synthkit.ast)
+
+(defun traverse-program (program function type)
+  "Traverses the atoms of PROGRAM, calling FUNCTION on each one (at time by TYPE)"
+  (declare (type program-atom program)
+           (type (function (program-atom)) function)
+           (type (member :pre-order :post-order) type))
+  (flet ((call-node ()
+           (funcall function program))
+         (iterate-children ()
+           (when (typep program 'program-node)
+             (loop for child in (children program)
+                   do (traverse-program child function type)))))
+    (case type
+      (:pre-order
+       (call-node)
+       (iterate-children))
+      (:post-order
+       (iterate-children)
+       (call-node)))))
+
+(*:define-do-macro do-traverse-program ((var program type &optional return) &body body)
+  `(traverse-program ,program #'(lambda (,var) ,@body) ,type))

src/ast/variables.lisp

@@ -0,0 +1,39 @@
+;;;;
+;;;; Variables for AST and execution control
+;;;;
+(in-package #:com.kjcjohnson.synthkit.ast)
+
+;;;
+;;; Allows exiting a program early
+;;;
+(defvar *program-execution-exit-hook*)
+(defun abort-program-execution ()
+  (funcall *program-execution-exit-hook*))
+
+;;;
+;;; Handles simple unbounded-recursion detection
+;;;
+(defvar *self-recursion-counter* 0
+  "Counts recursion depth to find probably-non-terminating programs.")
+(defparameter *self-recursion-limit* 200)
+(declaim (type fixnum *self-recursion-counter* *self-recursion-limit*))
+
+;;;
+;;; Debugging controls
+;;;
+(defvar *exe-debug* nil "Set to T when execution debugging is triggered")
+(defvar *exe-level* 0 "Level of nested program execution")
+(defvar *exe-debug-match* nil "If non-nil, must be a string that, when contained in the
+serialization of a program node, triggers ``*EXE-DEBUG*`` to be set to T.")
+(declaim (type (or null string) *exe-debug-match*))
+
+;;;
+;;; Stores the root input state
+;;;
+(defvar *root-input-state* nil "The initial input state passed to EXECUTE-PROGRAM")
+(defvar *root-input-descriptor* nil "The initial descriptor passed to EXECUTE-PROGRAM")
+
+;;;
+;;; Control variables
+;;;
+(defvar *use-program-compiler* nil "Whether or not to use the program compiler")

src/package.lisp

@@ -9,4 +9,13 @@
            #:ensure-vector
            #:ensure-list
            #:set-slot-if-unbound
-           #:stash))
+           #:stash)
+
+  ;; Timing utilities
+  (:export #:with-timing
+           #:declare-timed-section
+           #:with-timed-section
+           #:get-timed-section-real-time
+           #:get-timed-section-gc-time
+           #:get-timed-section-bytes-consed
+           #:reset-timed-section-time))

src/semgus/operationalizer/operationalizer.lisp

@@ -641,7 +641,7 @@
     (%apply-usage-table-rule-3 usage-table)
 
     (unless (%is-usage-table-complete? usage-table)
-      (pprint-usage-table *error-output* usage-table)
+      (pprint-usage-table *trace-output* usage-table)
       (error 'operationalization-error :message "Usage table incomplete."))
 
     (let* ((node-table (%build-semantic-node-table conjuncts

src/semgus/package.lisp

@@ -59,6 +59,7 @@
 
   ;; Reader things
   (:export #:*semgus-context*
+           #:*load-semgus-problem-time*
            #:auxiliary-functions
            #:constraints
            #:root-relations
@@ -75,7 +76,8 @@
   (:export #:verify-program
            #:verifier-for-specification
            #:check-program
-           #:unknown-verifier-result)
+           #:unknown-verifier-result
+           #:*check-program-time*)
 
   ;; CEGIS
   (:export #:cegis-supported-for-specification?
@@ -97,7 +99,8 @@
   (:export #:write-problem #:write-program)
 
   ;; Operationalizer protocol
-  (:export #:operationalize-chc)
+  (:export #:operationalize-chc
+           #:*debug-compile* #:when-debug-compile #:if-debug-compile)
 
   ;; CHC-related exports
   (:export #:arguments #:body #:head #:head-relations