(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)
))