		Search-engine friendly clone of the ACL2 documentation.

Flatten-res

Make-flatten-res

Basic constructor macro for flatten-res structures.

Syntax

(make-flatten-res [:assigns <assigns>] 
                  [:fixups <fixups>] 
                  [:constraints <constraints>] 
                  [:var-decl-map <var-decl-map>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-flatten-res

(defmacro make-flatten-res (&rest args)
  (std::make-aggregate 'flatten-res
                       args
                       '((:assigns)
                         (:fixups)
                         (:constraints)
                         (:var-decl-map))
                       'make-flatten-res
                       nil))

Function: flatten-res

(defun flatten-res (assigns fixups constraints var-decl-map)
  (declare (xargs :guard (and (assigns-p assigns)
                              (assigns-p fixups)
                              (constraintlist-p constraints)
                              (var-decl-map-p var-decl-map))))
  (declare (xargs :guard t))
  (let ((__function__ 'flatten-res))
    (declare (ignorable __function__))
    (b* ((assigns (mbe :logic (assigns-fix assigns)
                       :exec assigns))
         (fixups (mbe :logic (assigns-fix fixups)
                      :exec fixups))
         (constraints (mbe :logic (constraintlist-fix constraints)
                           :exec constraints))
         (var-decl-map (mbe :logic (var-decl-map-fix var-decl-map)
                            :exec var-decl-map)))
      (list (cons 'assigns assigns)
            (cons 'fixups fixups)
            (cons 'constraints constraints)
            (cons 'var-decl-map var-decl-map)))))