Changeset 1237

Timestamp:

2015-06-11T14:50:23-07:00 (9 years ago)

Author:

Marek Rychlik

Message:

* empty log message *

File:

• branches/f4grobner/division.lisp (modified) (2 diffs)

branches/f4grobner/division.lisp

@@ -64 +64 @@
             (scalar-times-poly-1 ring c1 (monom-times-poly m g))))
 
+(defun check-loop-invariant (ring-and-order c f0 a fl r f
+                             &aux 
+                               (ring (ro-ring ring-and-order))
+                               (p-zero (make-poly-zero)))
+  "Loop invariant: c*f0=sum ai*fi+r+f, where f0 is the initial value of f"
+  (flet ((p-add (p q) (poly-add ring-and-order p q))
+         (p-sub (p q) (poly-sub ring-and-order p q))
+         (p-mul (p q) (poly-mul ring-and-order p q)))
+    (poly-zerop
+     (p-sub
+      (scalar-times-poly ring c f0)
+      (reduce #'p-add
+              (list (inner-product a fl p-add p-mul p-zero)
+                    r
+                    f))))))
+  
+
+
 (defun poly-pseudo-divide (ring-and-order f fl
                            &aux
@@ -76 +94 @@
 the quotients is initialized to default."
   (declare (type poly f) (list fl))
+  ;; Loop invariant: c*f0=sum ai*fi+r+f, where f0 is the initial value of f
   (do ((r (make-poly-zero))
        (c (funcall (ring-unit ring)))