		Search-engine friendly clone of the ACL2 documentation.

Svjumpstate

Make-svjumpstate

Basic constructor macro for svjumpstate structures.

Syntax

(make-svjumpstate [:constraints <constraints>] 
                  [:breakcond <breakcond>] 
                  [:breakst <breakst>] 
                  [:continuecond <continuecond>] 
                  [:continuest <continuest>] 
                  [:returncond <returncond>] 
                  [:returnst <returnst>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svjumpstate

(defmacro make-svjumpstate (&rest args)
  (std::make-aggregate 'svjumpstate
                       args
                       '((:constraints)
                         (:breakcond)
                         (:breakst)
                         (:continuecond)
                         (:continuest)
                         (:returncond)
                         (:returnst))
                       'make-svjumpstate
                       nil))

Function: svjumpstate

(defun svjumpstate (constraints breakcond breakst continuecond
                                continuest returncond returnst)
  (declare (xargs :guard (and (constraintlist-p constraints)
                              (svex-p breakcond)
                              (svstate-p breakst)
                              (svex-p continuecond)
                              (svstate-p continuest)
                              (svex-p returncond)
                              (svstate-p returnst))))
  (declare (xargs :guard t))
  (let ((__function__ 'svjumpstate))
    (declare (ignorable __function__))
    (b* ((constraints (mbe :logic (constraintlist-fix constraints)
                           :exec constraints))
         (breakcond (mbe :logic (svex-fix breakcond)
                         :exec breakcond))
         (breakst (mbe :logic (svstate-fix breakst)
                       :exec breakst))
         (continuecond (mbe :logic (svex-fix continuecond)
                            :exec continuecond))
         (continuest (mbe :logic (svstate-fix continuest)
                          :exec continuest))
         (returncond (mbe :logic (svex-fix returncond)
                          :exec returncond))
         (returnst (mbe :logic (svstate-fix returnst)
                        :exec returnst)))
      (list (cons 'constraints constraints)
            (cons 'breakcond breakcond)
            (cons 'breakst breakst)
            (cons 'continuecond continuecond)
            (cons 'continuest continuest)
            (cons 'returncond returncond)
            (cons 'returnst returnst)))))