| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/vectors/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle pvs-strategies Sprache: PVS |
|||||||||
|
(defparameter vect-distr-rewrite-rules '("vx_distr_add" "vy_distr_add" "vz_distr_add" "vx_distr_sub" "vy_distr_sub" "vz_distr_sub" "vx_scal" "vy_scal" "vz_scal" "sqv_scal" "norm_scal" "neg_distr_sub" "neg_distr_add" "dot_add_left" "dot_add_right " "dot_sub_left" "dot_sub_right" "scal_add_left" "scal_sub_left" "scal_add_right" "scal_sub_right" "vx_scal" "vy_scal")) (defstep vect-distr () (let ((rewrite-step `(auto-rewrite ,@vect-distr-rewrite-rules))) rewrite-step) "Turns on auto-rewrites for vectors that apply distributive properties." "~%Distributive properties for vectors added as auto-rewrites") (defstep vect-distr-off () (let ((rewrite-step `(stop-rewrite ,@vect-distr-rewrite-rules))) rewrite-step) "Turns off auto-rewrites for vectors that apply distributive properties." "~%Distributive propertieauto-rewrites for vectors turned off") ;;;;;; ;;; Load Manip extensions for vectors if available. (let* ((dir (loop for d in *pvs-library-path* for p = (make-pathname :directory (append (pathname-directory d) '("vectors"))) when (file-exists-p p) return p finally (return (make-pathname)))) (lib-file (make-pathname :directory (pathname-directory dir) :name "manip-vectors" :type "lisp"))) (when (and (file-exists-p lib-file) (boundp '*manip-strategies-version*) (>= (read-from-string *manip-strategies-version*) 1.3)) (load lib-file) )) ¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28