Changeset 1241

Timestamp:

2015-06-11T15:04:51-07:00 (10 years ago)

Author:

Marek Rychlik

Message:

* empty log message *

File:

• branches/f4grobner/division.lisp (modified) (4 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
+(defun check-loop-invariant (ring-and-order c f0 a fl r p
                              &aux 
                                (ring (ro-ring ring-and-order))
@@ -83 +83 @@
               (list (inner-product a fl p-add p-mul p-zero)
                     r
-                    f))))))
+                    p))))))
   
 
@@ -98 +98 @@
 the quotients is initialized to default."
   (declare (type poly f) (list fl))
-  ;; Loop invariant: c*f0=sum ai*fi+r+p, where f0 is the initial value of f
+  ;; Loop invariant: c*f=sum ai*fi+r+p, where p must eventually become 0
   (do ((r (make-poly-zero))
        (c (funcall (ring-unit ring)))
@@ -121 +121 @@
             (setf (poly-sugar r) (max (poly-sugar r) (term-sugar (poly-lt p))))
             (pop (poly-termlist p))     ;remove lt(p) from p
+            ;; Run the check here
+            (assert (check-loop-invariant ring-and-order c f a fl r p))
             t)
            ((monom-divides-p (poly-lm (car fl)) (poly-lm p)) ;division occurred