|
(defmethod pvs-sxhash* ((e1 rational-expr) bindings)
(declare (ignore bindings))
(with-slots ((n1 number)) e1
(sxhash n1)))
(defmethod translate-to-prove :around ((obj name-expr))
(if (and (free-variables obj)(or *bound-variables* *bindings*))
(call-next-method)
(let ((hashed-value (gethash obj *translate-to-prove-hash*)))
(or hashed-value
(let ((result (call-next-method)))
(setf (gethash obj *translate-to-prove-hash*)
result)
result)))))
(defmethod translate-to-prove :around ((obj binding-expr))
(if (and (free-variables obj)(or *bound-variables* *bindings*))
(call-next-method)
(let ((hashed-value
(gethash obj *translate-to-prove-hash*)))
(or hashed-value
(let ((result (call-next-method)))
(setf (gethash obj *translate-to-prove-hash*)
result)
result)))))
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
