		Search-engine friendly clone of the ACL2 documentation.

Glmc-fsm-p

Honsed-glmc-fsm

Raw constructor for honsed glmc-fsm-p structures.

Syntax:

(honsed-glmc-fsm nextst prop fsm-constr 
                 bit-constr initst st-hyp hyp st-hyp-next 
                 interp-clauses hyp-var-bound var-bound)

This is identical to glmc-fsm, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by std::defaggregate.

Function: honsed-glmc-fsm

(defun honsed-glmc-fsm
       (nextst prop fsm-constr
               bit-constr initst st-hyp hyp st-hyp-next
               interp-clauses hyp-var-bound var-bound)
 (declare (xargs :guard (and (bfr-updates-p nextst)
                             (pseudo-term-list-listp interp-clauses)
                             (natp hyp-var-bound)
                             (natp var-bound))))
 (mbe
  :logic (glmc-fsm nextst prop fsm-constr
                   bit-constr initst st-hyp hyp st-hyp-next
                   interp-clauses hyp-var-bound var-bound)
  :exec
  (hons
   (hons 'nextst nextst)
   (hons
    (hons 'prop prop)
    (hons
     (hons 'fsm-constr fsm-constr)
     (hons
      (hons 'bit-constr bit-constr)
      (hons
       (hons 'initst initst)
       (hons
         (hons 'st-hyp st-hyp)
         (hons (hons 'hyp hyp)
               (hons (hons 'st-hyp-next st-hyp-next)
                     (hons (hons 'interp-clauses interp-clauses)
                           (hons (hons 'hyp-var-bound hyp-var-bound)
                                 (hons (hons 'var-bound var-bound)
                                       nil)))))))))))))