		Search-engine friendly clone of the ACL2 documentation.

Cgraph-formula

Make-cgraph-formula

Basic constructor macro for cgraph-formula structures.

Syntax

(make-cgraph-formula [:deps <deps>] 
                     [:name <name>] 
                     [:dep-success-vars <dep-success-vars>] 
                     [:success <success>] 
                     [:priority <priority>] 
                     [:value <value>] 
                     [:order <order>] 
                     [:ruletype <ruletype>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-cgraph-formula

(defmacro make-cgraph-formula (&rest args)
  (std::make-aggregate 'cgraph-formula
                       args
                       '((:deps)
                         (:name)
                         (:dep-success-vars)
                         (:success)
                         (:priority)
                         (:value)
                         (:order)
                         (:ruletype))
                       'make-cgraph-formula
                       nil))

Function: cgraph-formula

(defun cgraph-formula (deps name dep-success-vars
                            success priority value order ruletype)
  (declare (xargs :guard (and (fgl-object-bindings-p deps)
                              (symbolp name)
                              (pseudo-term-subst-p dep-success-vars)
                              (pseudo-termp success)
                              (pseudo-termp priority)
                              (pseudo-termp value)
                              (natp order)
                              (ctrex-ruletype-p ruletype))))
  (declare (xargs :guard t))
  (let ((__function__ 'cgraph-formula))
    (declare (ignorable __function__))
    (b* ((deps (mbe :logic (fgl-object-bindings-fix deps)
                    :exec deps))
         (name (mbe :logic (acl2::symbol-fix name)
                    :exec name))
         (dep-success-vars
              (mbe :logic (pseudo-term-subst-fix dep-success-vars)
                   :exec dep-success-vars))
         (success (mbe :logic (pseudo-term-fix success)
                       :exec success))
         (priority (mbe :logic (pseudo-term-fix priority)
                        :exec priority))
         (value (mbe :logic (pseudo-term-fix value)
                     :exec value))
         (order (mbe :logic (nfix order) :exec order))
         (ruletype (mbe :logic (ctrex-ruletype-fix ruletype)
                        :exec ruletype)))
      (list (cons 'deps deps)
            (cons 'name name)
            (cons 'dep-success-vars
                  dep-success-vars)
            (cons 'success success)
            (cons 'priority priority)
            (cons 'value value)
            (cons 'order order)
            (cons 'ruletype ruletype)))))