		Search-engine friendly clone of the ACL2 documentation.

Ubdd/level

Make-ubdd/level

Basic constructor macro for ubdd/level structures.

Syntax

(make-ubdd/level [:ubdd <ubdd>] 
                 [:level <level>])

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

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

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-ubdd/level

(defmacro make-ubdd/level (&rest args)
  (std::make-aggregate 'ubdd/level
                       args '((:ubdd) (:level))
                       'make-ubdd/level
                       nil))

Function: ubdd/level

(defun ubdd/level (ubdd level)
  (declare (xargs :guard (and (acl2::ubddp ubdd) (natp level))))
  (declare (xargs :guard t))
  (let ((__function__ 'ubdd/level))
    (declare (ignorable __function__))
    (b* ((ubdd (mbe :logic (acl2::ubdd-fix ubdd)
                    :exec ubdd))
         (level (mbe :logic (nfix level) :exec level)))
      (hons ubdd level))))