		Search-engine friendly clone of the ACL2 documentation.

Ringosc3

Make-ringosc3

Basic constructor macro for ringosc3 structures.

Syntax

(make-ringosc3 [:n1 <n1>] 
               [:n2 <n2>] 
               [:n3 <n3>] 
               [:inv1 <inv1>] 
               [:inv2 <inv2>] 
               [:inv3 <inv3>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-ringosc3

(defmacro make-ringosc3 (&rest args)
  (std::make-aggregate 'ringosc3
                       args
                       '((:n1)
                         (:n2)
                         (:n3)
                         (:inv1)
                         (:inv2)
                         (:inv3))
                       'make-ringosc3
                       nil))

Function: ringosc3

(defun ringosc3 (n1 n2 n3 inv1 inv2 inv3)
  (declare (xargs :guard (and (sig-path-p n1)
                              (sig-path-p n2)
                              (sig-path-p n3)
                              (inverter-p inv1)
                              (inverter-p inv2)
                              (inverter-p inv3))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'ringosc3))
    (declare (ignorable acl2::__function__))
    (b* ((n1 (mbe :logic (sig-path-fix n1) :exec n1))
         (n2 (mbe :logic (sig-path-fix n2) :exec n2))
         (n3 (mbe :logic (sig-path-fix n3) :exec n3))
         (inv1 (mbe :logic (inverter-fix inv1)
                    :exec inv1))
         (inv2 (mbe :logic (inverter-fix inv2)
                    :exec inv2))
         (inv3 (mbe :logic (inverter-fix inv3)
                    :exec inv3)))
      (list (cons 'n1 n1)
            (cons 'n2 n2)
            (cons 'n3 n3)
            (cons 'inv1 inv1)
            (cons 'inv2 inv2)
            (cons 'inv3 inv3)))))