		Search-engine friendly clone of the ACL2 documentation.

Sd-problem

Make-sd-problem

Basic constructor macro for sd-problem structures.

Syntax

(make-sd-problem [:type <type>] 
                 [:priority <priority>] 
                 [:groupsize <groupsize>] 
                 [:key <key>] 
                 [:ctx <ctx>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-sd-problem

(defmacro make-sd-problem (&rest args)
  (std::make-aggregate 'sd-problem
                       args
                       '((:type)
                         (:priority)
                         (:groupsize)
                         (:key)
                         (:ctx))
                       'make-sd-problem
                       nil))

Function: sd-problem

(defun sd-problem (type priority groupsize key ctx)
  (declare (xargs :guard (and (symbolp type)
                              (natp priority)
                              (natp groupsize)
                              (sd-key-p key)
                              (vl-context1-p ctx))))
  (declare (xargs :guard t))
  (let ((__function__ 'sd-problem))
    (declare (ignorable __function__))
    (b* ((type (mbe :logic (acl2::symbol-fix type)
                    :exec type))
         (priority (mbe :logic (nfix priority)
                        :exec priority))
         (groupsize (mbe :logic (nfix groupsize)
                         :exec groupsize))
         (key (mbe :logic (sd-key-fix key) :exec key))
         (ctx (mbe :logic (vl-context1-fix ctx)
                   :exec ctx)))
      (cons :sd-problem (cons (cons type priority)
                              (cons groupsize (cons key ctx)))))))