|
|
|---|
|
|
|
|---|
Raw constructor for glmc-fsm-p structures.
Syntax:
(glmc-fsm nextst prop fsm-constr
bit-constr initst st-hyp hyp st-hyp-next
interp-clauses hyp-var-bound var-bound)This is the lowest-level constructor for glmc-fsm-p structures. It simply conses together a structure with the specified fields.
Note: It's generally better to use macros like make-glmc-fsm or change-glmc-fsm instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.
The glmc-fsm-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-glmc-fsm instead.
This is an ordinary constructor function introduced by std::defaggregate.
Function:
(defun 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)))) (cons (cons 'nextst nextst) (cons (cons 'prop prop) (cons (cons 'fsm-constr fsm-constr) (cons (cons 'bit-constr bit-constr) (cons (cons 'initst initst) (cons (cons 'st-hyp st-hyp) (cons (cons 'hyp hyp) (cons (cons 'st-hyp-next st-hyp-next) (cons (cons 'interp-clauses interp-clauses) (cons (cons 'hyp-var-bound hyp-var-bound) (cons (cons 'var-bound var-bound) nil))))))))))))