		Search-engine friendly clone of the ACL2 documentation.

Observability-config

Make-observability-config

Basic constructor macro for observability-config structures.

Syntax

(make-observability-config [:hyp-max-size <hyp-max-size>] 
                           [:concl-min-size <concl-min-size>] 
                           [:min-ratio <min-ratio>] 
                           [:gatesimp <gatesimp>])

This is the usual way to construct observability-config structures. It simply conses together a structure with the specified fields.

This macro generates a new observability-config structure from scratch. See also change-observability-config, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-observability-config

(defmacro make-observability-config (&rest args)
  (std::make-aggregate 'observability-config
                       args
                       '((:hyp-max-size . 3000)
                         (:concl-min-size . 5000)
                         (:min-ratio . 10)
                         (:gatesimp default-gatesimp))
                       'make-observability-config
                       nil))

Function: observability-config

(defun observability-config
       (hyp-max-size concl-min-size min-ratio gatesimp)
 (declare (xargs :guard (and (acl2::maybe-natp hyp-max-size)
                             (acl2::maybe-natp concl-min-size)
                             (rationalp min-ratio)
                             (gatesimp-p gatesimp))))
 (declare (xargs :guard t))
 (let ((__function__ 'observability-config))
  (declare (ignorable __function__))
  (b* ((hyp-max-size (mbe :logic (acl2::maybe-natp-fix hyp-max-size)
                          :exec hyp-max-size))
       (concl-min-size
            (mbe :logic (acl2::maybe-natp-fix concl-min-size)
                 :exec concl-min-size))
       (min-ratio (mbe :logic (rfix min-ratio)
                       :exec min-ratio))
       (gatesimp (mbe :logic (gatesimp-fix gatesimp)
                      :exec gatesimp)))
    (cons :observability-config
          (list (cons 'hyp-max-size hyp-max-size)
                (cons 'concl-min-size concl-min-size)
                (cons 'min-ratio min-ratio)
                (cons 'gatesimp gatesimp))))))