controlled-configuration

other

(in-package "ACL2")

controlled-configuration-fnfunction

(defun controlled-configuration-fn
  (induction-depth tau no-function hooks state)
  (declare (xargs :stobjs state))
  `(progn (local (include-book "kestrel/built-ins/disable" :dir :system))
    (local (disable-most-builtin-logic-defuns))
    (local (disable-builtin-rewrite-rules-for-defaults))
    (set-induction-depth-limit ,INDUCTION-DEPTH)
    ,@(AND (NOT TAU) '((LOCAL (IN-THEORY (DISABLE (:E TAU-SYSTEM))))))
    ,@(AND
   (NOT
    (EQ (GETPROPC 'STD::MAKE-DEFINE-CONFIG 'MACRO-ARGS :ABSENT (W STATE))
        :ABSENT))
   `((STD::MAKE-DEFINE-CONFIG :NO-FUNCTION ,NO-FUNCTION :HOOKS ,HOOKS)))))

controlled-configurationmacro

(defmacro controlled-configuration
  (&key (induction-depth '0)
    (tau 'nil)
    (no-function 't)
    (hooks '(:fix)))
  `(make-event (controlled-configuration-fn ,INDUCTION-DEPTH
      ,TAU
      ,NO-FUNCTION
      ',HOOKS
      state)))