My Project
Loading...
Searching...
No Matches
f5gb.cc
Go to the documentation of this file.
1/****************************************
2* Computer Algebra System SINGULAR *
3****************************************/
4/*
5* ABSTRACT: f5gb interface
6*/
7
8#include "kernel/mod2.h"
9#ifdef HAVE_F5
10#include <unistd.h>
11#include <omp.h>
12#include "kernel/structs.h"
14#include "kernel/polys.h"
17#include "kernel/ideals.h"
20#include "polys/kbuckets.h"
21#include "polys/weight.h"
22#include "misc/intvec.h"
23#include "kernel/polys.h"
28
29#define pDeg(A) p_Deg(A,currRing)
30
31VAR int notInG = 0;
35VAR int spolsTime = 0;
45/*
46====================================================================
47sorting ideals by decreasing total degree "left" and "right" are the
48pointer of the first and last polynomial in the considered ideal
49====================================================================
50*/
51void qsortDegree(poly* left, poly* right)
52{
53 poly* ptr1 = left;
54 poly* ptr2 = right;
55 poly p1,p2;
56 p2 = *(left + (right - left >> 1));
57 do
58 {
59 while(p_Totaldegree(*ptr1, currRing) < p_Totaldegree(p2, currRing))
60 {
61 ptr1++;
62 }
63 while(p_Totaldegree(*ptr2, currRing) > p_Totaldegree(p2,currRing))
64 {
65 ptr2--;
66 }
67 if(ptr1 > ptr2)
68 {
69 break;
70 }
71 p1 = *ptr1;
72 *ptr1 = *ptr2;
73 *ptr2 = p1;
74 } while(++ptr1 <= --ptr2);
75
76 if(left < ptr2)
77 {
78 qsortDegree(left,ptr2);
79 }
80 if(ptr1 < right)
81 {
82 qsortDegree(ptr1,right);
83 }
84}
85
86/*!
87 * ======================================================================
88 * builds the sum of the entries of the exponent vectors, i.e. the degree
89 * of the corresponding monomial
90 * ======================================================================
91*/
92long sumVector(int* v, int k) {
93 int i;
94 long sum = 0;
95 for(i=1; i<=k; i++) {
96 Print("%d\n",v[i]);
97 Print("%ld\n",sum);
98 sum = sum + v[i];
99 }
100 return sum;
101}
102
103/*!
104==========================================================================
105compares monomials, i.e. divisibility tests for criterion 1 and criterion 2
106==========================================================================
107*/
108bool compareMonomials(int* m1, int** m2, int numberOfRules, int k) {
109 int i,j;
110 long sumM1 = sumVector(m1,k);
111 //int k = sizeof(m1) / sizeof(int);
112 for(i=0; i<numberOfRules; i++) {
113 if(sumVector(m2[i],k) <= sumM1) {
114 for(j=1; j<=k; j++) {
115 if(m1[j]>m2[i][j]) {
116 return true;
117 }
118 }
119 }
120 }
121 return false;
122}
123
124/*
125==================================================
126computes incrementally gbs of subsets of the input
127gb{f_m} -> gb{f_m,f_(m-1)} -> gb{f_m,...,f_1}
128==================================================
129*/
130LList* F5inc(int i, poly f_i, LList* gPrev, LList* reducers, ideal gbPrev, poly ONE, LTagList* lTag, RList* rules, RTagList* rTag, int plus, int termination) {
131 //Print("in f5inc\n");
132 //pWrite(rules->getFirst()->getRuleTerm());
133 int iterationstep = i;
134 int j;
135 //Print("%p\n",gPrev->getFirst());
136 //pWrite(gPrev->getFirst()->getPoly());
137 poly tempNF = kNF(gbPrev,currRing->qideal,f_i);
138 f_i = tempNF;
139 //gPrev->insert(ONE,i,f_i);
140 gPrev->insert(ONE,gPrev->getLength()+1,f_i);
141 // tag the first element in gPrev of the current index for findReductor()
142 lTag->setFirstCurrentIdx(gPrev->getLast());
143 //Print("1st gPrev: ");
144 //pWrite(gPrev->getFirst()->getPoly());
145 //Print("2nd gPrev: ");
146 //pWrite(gPrev->getFirst()->getNext()->getPoly());
147 //pWrite(gPrev->getFirst()->getNext()->getPoly());
148 CListOld* critPairs = new CListOld();
149 CNode* critPairsMinDeg = new CNode();
150 PList* rejectedGBList = new PList();
151 // computation of critical pairs with checking of criterion 1 and criterion 2 and saving them
152 // in the list critPairs
153 criticalPair(gPrev, critPairs, lTag, rTag, rules, rejectedGBList, plus);
154 STATIC_VAR LList* sPolyList = new LList();
155 //sPolyList->print();
156 // labeled polynomials which have passed reduction() and have to be added to list gPrev
157 STATIC_VAR LList* completed = new LList();
158 // the reduced labeled polynomials which are returned from subalgorithm reduction()
159 STATIC_VAR LList* reducedLPolys = new LList();
160 // while there are critical pairs to be further checked and deleted/computed
161 while(NULL != critPairs->getFirst()) {
162 // critPairs->getMinDeg() deletes the first elements of minimal degree from
163 // critPairs, thus the while loop is not infinite.
164 // adds all to be reduced S-polynomials in the list sPolyList and adds
165 // the corresponding rules to the list rules
166 // NOTE: inside there is a second check of criterion 2 if new rules are
167 // added
168 //int timer4 = initTimer();
169 //startTimer();
170 //critPairs->print();
171
172 //definition of a local numberUsefulPairs variable for the next degree
173 //step:
174 //if in this degree all pairs are useless, skip this degree step
175 //completely!
176 //long arrideg = critPairs->getFirst()->getData()->getDeg();
177 //if(plus && highestDegreeGBCriticalPair < critPairs->getFirst()->getData()->getDeg()) {
178 // return gPrev;
179 //}
180 //else {
181 critPairsMinDeg = critPairs->getMinDeg();
182 //numberUsefulPairsMinDeg = computeUsefulMinDeg(critPairsMinDeg);
183 //if(numberUsefulPairs > 0) {
184 //if(numberUsefulPairsMinDeg > 0) {
185 //Print("number of useful pairs: %d\n",numberUsefulPairs);
186 //Print("number of useless pairs: %d\n\n",numberUselessPairs);
187 //Print("Degree of following reduction: %d\n",critPairsMinDeg->getData()->getDeg());
188 long degreecheck = critPairsMinDeg->getData()->getDeg();
189
190 computeSPols(critPairsMinDeg,rTag,rules,sPolyList, rejectedGBList);
191 //}
192 //}
193 //}
194 //else {
195 // return gPrev;
196 //}
197 //timer4 = getTimer();
198 //Print("SPOLS TIMER: %d\n",timer4);
199 //spolsTime = spolsTime + timer4;
200 // DEBUG STUFF FOR SPOLYLIST
201 LNode* temp = sPolyList->getFirst();
202 //while(NULL != temp && NULL != temp->getLPoly()) {
203 //Print("Spolylist element: ");
204 //pWrite(temp->getPoly());
205 //temp = temp->getNext();
206 //}
207 // reduction process of new S-polynomials and also adds new critical pairs to critPairs
208 //int timer3 = initTimer();
209 //startTimer();
210 //sPolyList->print();
211 //reduction(sPolyList, critPairs, gPrev, rules, lTag, rTag, gbPrev);
212 //Print("BEFORE REDUCTION: \n");
213 //Print("number of useful pairs: %d\n",numberUsefulPairs);
214 //Print("number of useless pairs: %d\n\n",numberUselessPairs);
215 newReduction(sPolyList, critPairs, gPrev, reducers, rules, lTag, rTag, gbPrev, termination, rejectedGBList, plus);
216 //Print("ITERATION: %d",iterationstep);
217 //Print("NAECHSTER GRAD: %ld",degreecheck);
218 //sleep(5);
219 //if(i == 5 && pDeg(gPrev->getLast()->getPoly()) == 8) {
220 // Print("RAUS BEI DEG 8 \n");
221 // return gPrev;
222 //}
223 //Print("ARRIS DEG: %ld\n",arrideg);
224 // Arris idea stated by John in an email
225 //if(arrisCheck(critPairs->getFirst(),gPrev->getFirst(),arrideg)) {
226 // Print("ARRIS DEGREE: %ld\n", arrideg);
227 // return gPrev;
228 //}
229
230
231 //bool aha = checkDGB(gPrev);
232
233
234 //timer3 = getTimer();
235 //reductionTime = reductionTime + timer3;
236 //Print("REDUCTION TIMER: %d\n",timer3);
237 // DEBUG STUFF FOR GPREV
238 //temp = gPrev->getFirst();
239 //int number = 1;
240 //Print("\n\n");
241 //while(NULL != temp) {
242 // Print("%d. ",number);
243 // pWrite(temp->getPoly());
244 // temp = temp->getNext();
245 // number++;
246 // Print("\n");
247 //}
248 //sleep(5);
249
250 }
251 //Print("REDUCTION DONE\n");
252 //Print("%p\n",rules->getFirst());
253 //Print("%p\n",rTag->getFirst());
254 //if(rules->getFirst() != rTag->getFirst()) {
255 //Print("+++++++++++++++++++++++++++++++++++++NEW RULES+++++++++++++++++++++++++++++++++++++\n");
256 //rTag->insert(rules->getFirst());
257 //}
258 //else {
259 //Print("+++++++++++++++++++++++++++++++++++NO NEW RULES++++++++++++++++++++++++++++++++++++\n");
260 //}
261 lTag->insert(lTag->getFirstCurrentIdx());
262 //Print("INDEX: %d\n",tempTag->getIndex());
263 //pWrite(tempTag->getPoly());
264 //Print("COMPLETED FIRST IN F5INC: \n");
265 //Print("1st gPrev: ");
266 //pWrite(gPrev->getFirst()->getPoly());
267 //Print("2nd gPrev: ");
268 //pWrite(gPrev->getFirst()->getNext()->getPoly());
269 //Print("3rd gPrev: ");
270 //pWrite(gPrev->getFirst()->getNext()->getNext()->getPoly());
271 //delete sPolyList;
272 //critPairs->print();
273 delete critPairs;
274 //Print("IN F5INC\n");
275 /*
276 PrintS("\n\n\nRULES: \n");
277 RNode* tempR = rules->getFirst();
278 Print("%p\n",tempR);
279 int t = 1;
280 while(NULL != tempR) {
281 Print("ADDRESS OF %d RNODE: %p\n",t,tempR);
282 Print("ADDRESS OF RULE: %p\n",tempR->getRule());
283 pWrite(tempR->getRuleTerm());
284 Print("ADDRESS OF TERM: %p\n",tempR->getRuleTerm());
285 Print("%d\n\n",tempR->getRuleIndex());
286 tempR = tempR->getNext();
287 t++;
288 }
289 */
290 //gPrev->print();
291 //Print("COMPLETE REDUCTION TIME UNTIL NOW: %d\n",reductionTime);
292 //Print("COMPLETE SPOLS TIME UNTIL NOW: %d\n",spolsTime);
293 degreeBound = 0;
294 return gPrev;
295}
296
297
298
299bool checkDGB(LList* gPrev) {
300 Print("D-GB CHECK at degree %ld\n",pDeg(gPrev->getLast()->getPoly()));
301 LNode* temp = gPrev->getFirst();
302 LNode* temp2;
303 bool isDGb = 0;
304 // construct the d-GB gb
305 ideal gb = idInit(gPrev->getLength(),1);
306 for(int j=0;j<=gPrev->getLength()-1;j++) {
307 gb->m[j] = temp->getPoly();
308 pWrite(gb->m[j]);
309 temp = temp->getNext();
310 }
311 /*
312 Kstd1_deg = pDeg(gPrev->getLast()->getPoly());
313 BITSET save = test;
314 test |= Sy_bit(OPT_DEGBOUND);
315 kStd();
316 test = save;
317 */
318 temp = gPrev->getFirst();
319 while(NULL != temp) {
320 temp2 = temp->getNext();
321 number nOne = nInit(1);
322 poly lcm = pOne();
323 poly sp = pOne();
324 while(NULL != temp2) {
325 pLcm(temp->getPoly(),temp2->getPoly(),lcm);
326 pSetCoeff(lcm,nOne);
327 pSetm(lcm);
328 PrintS("LCM: ");
329 pWrite(lcm);
330 if(pDeg(lcm) <= pDeg(gPrev->getLast()->getPoly())) {
331 poly u1 = pOne();
332 poly u2 = pOne();
333 u1 = pMDivide(lcm,temp->getPoly());
334 pSetCoeff(u1,nOne);
335 u2 = pMDivide(lcm,temp2->getPoly());
336 pSetCoeff(u2,nOne);
337 sp = ksOldSpolyRedNew(ppMult_qq(u1,temp->getPoly()),
338 ppMult_qq(u2,temp2->getPoly()));
339 pNorm(sp);
340
341 poly reducer = pOne();
342 //reducer = gb->m[0];
343 int i = 0;
344 pWrite(pHead(sp));
345
346 while(i<IDELEMS(gb)) {
347 reducer = gb->m[i];
348 if(pDivisibleBy(reducer,pHead(sp))) {
349 poly uReducer = pOne();
350 uReducer = pMDivide(lcm,reducer);
351 pSetCoeff(uReducer,nOne);
352 sp = ksOldSpolyRedNew(sp,ppMult_qq(uReducer,reducer));
353 //pNorm(tempSP);
354 //sp = tempSP;
355 pNorm(sp);
356 pWrite(sp);
357 i = 0;
358 }
359 else {
360 i++;
361 }
362 }
363
364 pWrite(pHead(sp));
365 }
366 temp2 = temp2->getNext();
367 }
368 temp = temp->getNext();
369 }
370 PrintS("------------------\n");
371 return isDGb;
372}
373
374/*
375 * Arris Check if we are finished after the current degree step:
376 * Checks all remaining critical pairs, i.e. those of higher degree,
377 * by the two Buchberger criteria.
378 * return value: 0, if all remaining critical pairs are deleted by
379 * Buchberger's criteria
380 * 1, otherwise
381 */
382bool arrisCheck(CNode* first, LNode* firstGCurr, long arrideg) {
383 CNode* temp = first;
384
385 //product criterion check
386 while(NULL != temp) {
387 if(!pLmEqual(pHead(temp->getLp2Poly()),temp->getT1())) {
388 return 0;
389 }
390 temp = temp->getNext();
391 }
392
393 // chain criterion
394 LNode* tempPoly = firstGCurr;
395 while(NULL != tempPoly) {
396 LNode* tempPoly2 = tempPoly->getNext();
397 while(NULL != tempPoly2) {
398 number nOne = nInit(1);
399 poly lcm = pOne();
400 pLcm(tempPoly->getPoly(),tempPoly2->getPoly(),lcm);
401 pSetCoeff(lcm,nOne);
402 pSetm(lcm);
403 if(pDeg(lcm) > arrideg) {
404 LNode* tempPoly3 = firstGCurr;
405 while(NULL != tempPoly3) {
406 if(tempPoly3 != tempPoly2 && tempPoly3 != tempPoly && pDivisibleBy(tempPoly3->getPoly(),lcm)) {
407 poly lcm1 = pOne();
408 poly lcm2 = pOne();
409 pLcm(tempPoly3->getPoly(),tempPoly->getPoly(),lcm1);
410 pSetCoeff(lcm1,nOne);
411 pSetm(lcm1);
412 pLcm(tempPoly3->getPoly(),tempPoly2->getPoly(),lcm2);
413 pSetCoeff(lcm2,nOne);
414 pSetm(lcm2);
415 if(pDeg(lcm1) < pDeg(lcm) && pDeg(lcm2) < pDeg(lcm)) {
416 return 0;
417 }
418 }
419 tempPoly3 = tempPoly3->getNext();
420 }
421 }
422 tempPoly2 = tempPoly2->getNext();
423 }
424 tempPoly = tempPoly->getNext();
425 }
426 return 1;
427}
428
429
430
431/*
432================================================================
433computes a list of critical pairs for the next reduction process
434the first element is always "useful" thus the critical pair
435computed is either "useful" or "useless" depending on the second
436element which generates the critical pair.
437first element in gPrev is always the newest element which must
438build critical pairs with all other elements in gPrev
439================================================================
440*/
441inline void criticalPair(LList* gPrev, CListOld* critPairs, LTagList* lTag, RTagList* rTag, RList* rules, PList* rejectedGBList, int plus) {
442 //Print("IN CRITPAIRS\n");
443 // initialization for usage in pLcm()
444 number nOne = nInit(1);
445 LNode* newElement = gPrev->getLast();
446 LNode* temp = gPrev->getFirst();
447 poly u1 = pOne();
448 poly u2 = pOne();
449 poly lcm = pOne();
450 poly t = pHead(newElement->getPoly());
451 RuleOld* testedRuleOld = NULL;
452 //Print("NEW: ");
453 //pWrite(newElement->getPoly());
454 //Print("ADDRESS: %p",newElement);
455 if(NULL != rules->getFirst()) {
456 testedRuleOld = rules->getFirst()->getRuleOld();
457 }
458 // computation of critical pairs
459 while( gPrev->getLast() != temp) {
460 //Print("TEMP: ");
461 //pWrite(pHead(temp->getPoly()));
462 //Print("ADDRESS: %p",temp);
463 pLcm(newElement->getPoly(), temp->getPoly(), lcm);
464 pSetCoeff(lcm,nOne);
465 // computing factors u2 for new labels
466 u1 = pMDivide(lcm,t);
467 if(NULL == u1) {
468 break;
469 }
470 pSetCoeff(u1,nOne);
471 u2 = pMDivide(lcm,temp->getPoly());
472 pSetCoeff(u2,nOne);
473 int degree = pDeg(ppMult_qq(u2,pHead(temp->getPoly())));
474 // testing both new labels by the F5 Criterion
475 if(!temp->getDel()) {
476 if(plus && highestDegreeGBCriticalPair < degree) {
478 }
479 if(!criterion2(gPrev->getFirst()->getIndex(), u2, temp, rules, rTag)
480 && !criterion2(gPrev->getFirst()->getIndex(), u1, newElement, rules, rTag)
481 && !criterion1(gPrev,u1,newElement,lTag) && !criterion1(gPrev,u2,temp,lTag)) {
482 // if they pass the test, add them to CListOld critPairs, having the LPolyOld with greater
483 // label as first element in the CPairOld
484 if(newElement->getIndex() == temp->getIndex() &&
485 -1 == pLmCmp(ppMult_qq(u1, newElement->getTerm()),ppMult_qq(u2, temp->getTerm()))) {
486 CPairOld* cp = new CPairOld(pDeg(ppMult_qq(u2,pHead(temp->getPoly()))), u2,
487 temp->getLPolyOld(), u1, newElement->getLPolyOld(), 0 , testedRuleOld);
488 critPairs->insert(cp);
489 // counting the number of useful pairs
491 }
492 else {
493 CPairOld* cp = new CPairOld(pDeg(ppMult_qq(u2,pHead(temp->getPoly()))), u1,
494 newElement->getLPolyOld(), u2, temp->getLPolyOld(), 0, testedRuleOld);
495 critPairs->insert(cp);
496 // counting the number of useful pairs
498 }
499 }
500 else {
501 // TODO: generate a list of lcms of rejected GB critical pairs and
502 // check F5 critical pairs with it at their creation
503 //Print("--------------------------------------------------------------------\n");
504 //Print("--------------------------------------------------------------------\n");
505 pSetm(lcm);
506 rejectedGBList->insert(lcm);
507 //Print("-----------------------REJECTED IN CRIT PAIR------------------------\n");
508 //pWrite(lcm);
509 //Print("--------------------------------------------------------------------\n");
510 //rejectedGBList->print();
511 }
512 }
513 else {
514 //Print("LABEL: ");
515 //pWrite(ppMult_qq(u1,newElement->getTerm()));
516 //if(rejectedGBList->check(lcm)) { // if there is equality of lcms then we need the F5 critical pair
517 if(!criterion2(gPrev->getFirst()->getIndex(), u2, temp, rules, rTag)
518 && !criterion2(gPrev->getFirst()->getIndex(), u1, newElement, rules, rTag)
519 && !criterion1(gPrev,u1,newElement,lTag) && !criterion1(gPrev,u2,temp,lTag)) {
520 // if they pass the test, add them to CListOld critPairs, having the LPolyOld with greater
521 // label as first element in the CPairOld
522 if(newElement->getIndex() == temp->getIndex() &&
523 -1 == pLmCmp(ppMult_qq(u1, newElement->getTerm()),ppMult_qq(u2, temp->getTerm()))) {
524 CPairOld* cp = new CPairOld(pDeg(ppMult_qq(u2,pHead(temp->getPoly()))), u2,
525 temp->getLPolyOld(), u1, newElement->getLPolyOld(), 1 , testedRuleOld);
526 critPairs->insert(cp);
528 }
529 else {
530 CPairOld* cp = new CPairOld(pDeg(ppMult_qq(u2,pHead(temp->getPoly()))), u1,
531 newElement->getLPolyOld(), u2, temp->getLPolyOld(), 1, testedRuleOld);
532 critPairs->insert(cp);
534 }
535 }
536 //}
537 }
538 temp = temp->getNext();
539 }
540}
541
542
543
544/*
545================================================================
546computes a list of critical pairs for the next reduction process
547the first element is always "useless" thus the critical pair
548computed is "useless".
549first element in gPrev is always the newest element which must
550build critical pairs with all other elements in gPrev
551================================================================
552*/
553inline void criticalPair2(LList* gPrev, CListOld* critPairs, LTagList* lTag, RTagList* rTag, RList* rules, PList* rejectedGBList) {
554 //Print("IN CRITPAIRS\n");
555 // initialization for usage in pLcm()
556 number nOne = nInit(1);
557 LNode* newElement = gPrev->getLast();
558 LNode* temp = gPrev->getFirst();
559 poly u1 = pOne();
560 poly u2 = pOne();
561 poly lcm = pOne();
562 poly t = pHead(newElement->getPoly());
563 RuleOld* testedRuleOld = NULL;
564 if(NULL != rules->getFirst()) {
565 testedRuleOld = rules->getFirst()->getRuleOld();
566 }
567 // computation of critical pairs
568 while( gPrev->getLast() != temp) {
569 pLcm(newElement->getPoly(), temp->getPoly(), lcm);
570 pSetCoeff(lcm,nOne);
571 // computing factors u2 for new labels
572 u1 = pMDivide(lcm,t);
573 if(NULL == u1) {
574 break;
575 }
576 pSetCoeff(u1,nOne);
577 u2 = pMDivide(lcm,temp->getPoly());
578 pSetCoeff(u2,nOne);
579 // testing both new labels by the F5 Criterion
580 //Print("LABEL: ");
581 //pWrite(ppMult_qq(u1,newElement->getTerm()));
582 //if(rejectedGBList->check(lcm)) { // if there is equality of lcms then we need the F5 critical pair
583 if(!criterion2(gPrev->getFirst()->getIndex(), u2, temp, rules, rTag)
584 && !criterion2(gPrev->getFirst()->getIndex(), u1, newElement, rules, rTag)
585 && !criterion1(gPrev,u1,newElement,lTag) && !criterion1(gPrev,u2,temp,lTag)) {
586 // if they pass the test, add them to CListOld critPairs, having the LPolyOld with greater
587 // label as first element in the CPairOld
588 if(newElement->getIndex() == temp->getIndex() &&
589 -1 == pLmCmp(ppMult_qq(u1, newElement->getTerm()),ppMult_qq(u2, temp->getTerm()))) {
590 CPairOld* cp = new CPairOld(pDeg(ppMult_qq(u2,pHead(temp->getPoly()))), u2,
591 temp->getLPolyOld(), u1, newElement->getLPolyOld(), 1 , testedRuleOld);
592 critPairs->insert(cp);
594 }
595 else {
596 CPairOld* cp = new CPairOld(pDeg(ppMult_qq(u2,pHead(temp->getPoly()))), u1,
597 newElement->getLPolyOld(), u2, temp->getLPolyOld(), 1, testedRuleOld);
598 critPairs->insert(cp);
600 }
601 }
602 //}
603 temp = temp->getNext();
604 }
605}
606
607
608
609/*
610========================================
611Criterion 1, i.e. Faugere's F5 Criterion
612========================================
613*/
614inline bool criterion1(LList* gPrev, poly t, LNode* l, LTagList* lTag) {
615 // starts at the first element in gPrev with index = (index of l)-1, these tags are saved in lTag
616 int idx = l->getIndex();
617 int i;
618 if(idx == 1) {
619 //Print("HIER\n");
620 return false;
621 }
622 else {
623 LNode* testNode = gPrev->getFirst();
624 // save the monom t1*label_term(l) as it is tested various times in the following
625 poly u1 = ppMult_qq(t,l->getTerm());
626 //Print("------------------------------IN CRITERION 1-----------------------------------------\n");
627 //Print("TESTED ELEMENT: ");
628 //pWrite(l->getPoly());
629 //pWrite(l->getTerm());
630 //pWrite(ppMult_qq(t,l->getTerm()));
631 //Print("%d\n\n",l->getIndex());
632 while(testNode->getIndex() < idx) { // && NULL != testNode->getLPoly()) {
633 //pWrite(testNode->getPoly());
634 //Print("%d\n",testNode->getIndex());
635 if(pLmDivisibleByNoComp(testNode->getPoly(),u1)) {
636 //Print("Criterion 1 NOT passed!\n");
637 if(idx != gPrev->getLast()->getIndex()) {
638 //Print("DOCH!\n");
639 }
640 return true;
641 }
642 //pWrite(testNode->getNext()->getPoly());
643 testNode = testNode->getNext();
644 }
645 /*
646 ideal testId = idInit(idx-1,1);
647 for(i=0;i<idx-1;i++) {
648 testId->m[i] = pHead(testNode->getPoly());
649 testNode = testNode->getNext();
650 }
651 poly temp = kNF(testId,currRing->qideal,u1);
652 //pWrite(temp);
653 for(i=0;i<IDELEMS(testId);i++) {
654 testId->m[i] = NULL;
655 }
656 idDelete(&testId);
657 if(NULL == temp) {
658 //if(l->getIndex() != gPrev->getFirst()->getIndex()) {
659 // Print("----------------------------Criterion1 not passed----------------------------------\n");
660 //}
661 return true;
662 }
663 */
664 return false;
665 }
666}
667
668
669
670/*
671=====================================
672Criterion 2, i.e. Rewritten Criterion
673=====================================
674*/
675inline bool criterion2(int idx, poly t, LNode* l, RList* rules, RTagList* rTag) {
676 //Print("------------------------------IN CRITERION 2/1-----------------------------------------\n");
677 /*
678 PrintS("RULES: \n");
679 RNode* tempR = rules->getFirst();
680 Print("%p\n",tempR);
681 int i = 1;
682 while(NULL != tempR) {
683 Print("ADDRESS OF %d RNODE: %p\n",i,tempR);
684 Print("ADDRESS OF RULE: %p\n",tempR->getRule());
685 pWrite(tempR->getRuleTerm());
686 Print("ADDRESS OF TERM: %p\n",tempR->getRuleTerm());
687 Print("%d\n\n",tempR->getRuleIndex());
688 tempR = tempR->getNext();
689 i++;
690 }
691 //Print("TESTED ELEMENT: ");
692 //pWrite(l->getPoly());
693 //pWrite(l->getTerm());
694 //pWrite(ppMult_qq(t,l->getTerm()));
695 //Print("%d\n\n",l->getIndex());
696 */
697// start at the previously added element to gPrev, as all other elements will have the same index for sure
698 if(idx > l->getIndex()) {
699 return false;
700 }
701
702 RNode* testNode; // = new RNode();
703 testNode = rules->getFirst();
704 /*
705 if(NULL == rTag->getFirst()) {
706 if(NULL != rules->getFirst()) {
707 testNode = rules->getFirst();
708 }
709 else {
710 return false;
711 }
712 }
713
714 else {
715
716 if(l->getIndex() > rTag->getFirst()->getRuleIndex()) {
717 testNode = rules->getFirst();
718 }
719 else {
720 //Print("HIER\n");
721 //Print("DEBUG\n");
722 //Print("L INDEX: %d\n",l->getIndex());
723 *-------------------------------------
724 * TODO: WHEN INTERREDUCING THE GB THE
725 * INDEX OF THE PREVIOUS ELEMENTS
726 * GETS HIGHER!
727 *-----------------------------------*
728 //testNode = rules->getFirst();
729 testNode = rTag->get(l->getIndex());
730 if(NULL == testNode) {
731 testNode = rules->getFirst();
732 }
733 //Print("TESTNODE ADDRESS: %p\n",testNode);
734 }
735 }
736 */
737 //testNode = rules->getFirst();
738 // save the monom t1*label_term(l) as it is tested various times in the following
739 poly u1 = ppMult_qq(t,l->getTerm());
740 // first element added to rTag was NULL, check for this
741 //Print("%p\n",testNode->getRule());
742 // NOTE: testNode is possibly NULL as rTag->get() returns NULL for elements of index <=1!
743 //Print("TESTNODE: %p\n",testNode);
744 //pWrite(testNode->getRuleTerm());
745 if(NULL != testNode ) {
746 //pWrite(testNode->getRuleTerm());
747 }
748 if(NULL != testNode) {
749 if(testNode->getRuleOld() == l->getRuleOld()) {
750 //Print("%p\n%p\n",testNode->getRule(),l->getRule());
751 //Print("EQUAL\n");
752 }
753 else {
754 //Print("NOT EQUAL\n");
755 }
756 }
757 while(NULL != testNode && testNode->getRuleOld() != l->getRuleOld()
758 && l->getIndex() == testNode->getRuleOldIndex()) {
759 //Print("%p\n",testNode);
760 //pWrite(testNode->getRuleTerm());
761 //pWrite(t);
762 //pWrite(l->getTerm());
763 //pWrite(u1);
764 //Print("%d\n",testNode->getRuleIndex());
765 if(pLmDivisibleByNoComp(testNode->getRuleOldTerm(),u1)) {
766 //Print("-----------------Criterion 2 NOT passed!-----------------------------------\n");
767 //Print("INDEX: %d\n",l->getIndex());
768 pDelete(&u1);
769 //Print("------------------------------IN CRITERION 2/1-----------------------------------------\n\n");
770 return true;
771 }
772 testNode = testNode->getNext();
773 }
774 //delete testNode;
775 pDelete(&u1);
776 //Print("------------------------------IN CRITERION 2/1-----------------------------------------\n\n");
777 return false;
778}
779
780
781
782/*
783=================================================================================================================
784Criterion 2, i.e. Rewritten Criterion, for its second call in computeSPols(), with added lastRuleTested parameter
785=================================================================================================================
786*/
787inline bool criterion2(poly t, LPolyOld* l, RList* rules, RuleOld* testedRuleOld) {
788 //Print("------------------------------IN CRITERION 2/2-----------------------------------------\n");
789 //Print("LAST RuleOld TESTED: %p",testedRuleOld);
790 /*
791 PrintS("RULES: \n");
792 RNode* tempR = rules->getFirst();
793 while(NULL != tempR) {
794 pWrite(tempR->getRuleTerm());
795 Print("%d\n\n",tempR->getRuleIndex());
796 tempR = tempR->getNext();
797 }
798 //Print("TESTED ELEMENT: ");
799 //pWrite(l->getPoly());
800 //pWrite(l->getTerm());
801 //pWrite(ppMult_qq(t,l->getTerm()));
802 //Print("%d\n\n",l->getIndex());
803 */
804// start at the previously added element to gPrev, as all other elements will have the same index for sure
805 RNode* testNode = rules->getFirst();
806 // save the monom t1*label_term(l) as it is tested various times in the following
807 poly u1 = ppMult_qq(t,l->getTerm());
808 // first element added to rTag was NULL, check for this
809 while(NULL != testNode && testNode->getRuleOld() != testedRuleOld) {
810 //pWrite(testNode->getRuleTerm());
811 if(pLmDivisibleByNoComp(testNode->getRuleOldTerm(),u1)) {
812 //Print("--------------------------Criterion 2 NOT passed!------------------------------\n");
813 //Print("INDEX: %d\n",l->getIndex());
814 pDelete(&u1);
815 //Print("------------------------------IN CRITERION 2/2-----------------------------------------\n\n");
816 return true;
817 }
818 testNode = testNode->getNext();
819 }
820 pDelete(&u1);
821 //Print("------------------------------IN CRITERION 2/2-----------------------------------------\n\n");
822 return false;
823}
824
825/*
826 * check for useful pairs in the given subset of critical pairs
827 */
829 CNode* temp = first;
831 while(NULL != temp) {
832 if(!temp->getDel()) {
834 }
835 temp = temp->getNext();
836 }
838}
839/*
840==================================
841Computation of S-Polynomials in F5
842==================================
843*/
844void computeSPols(CNode* first, RTagList* rTag, RList* rules, LList* sPolyList, PList* rejectedGBList) {
845 CNode* temp = first;
846 //Print("\nDegree: %d\n",temp->getData()->getDeg());
847 // only GB-critical pairs are computed
848 //while(NULL != temp && temp->getDel()) {
849 // temp = temp->getNext();
850 //}
851 //if(temp->getData()->getDeg() == 11) {
852 // Print("PAIRS OF DEG 11:\n");
853 //}
854 RList* f5rules = new RList();
855 CListOld* f5pairs = new CListOld();
856 poly sp = pInit();
857 number sign = nInit(-1);
858 //Print("###############################IN SPOLS##############################\n");
859 //first->print();
860/*
861 * first of all: do everything for GB critical pairs
862 */
863 while(NULL != temp) {
864 // if(temp->getData()->getDeg() == 11) {
865 //Print("--------------------------\n");
866 //Print("redundant? %d\n",temp->getDel());
867 //pWrite(pHead(temp->getLp1Poly()));
868 //Print("redundant: %d\n",temp->getAdLp1()->getDel());
869 //pWrite(pHead(temp->getLp2Poly()));
870 //Print("redundant: %d\n",temp->getAdLp2()->getDel());
871 //pWrite(pHead(ppMult_qq(temp->getT1(),temp->getLp1Poly())));
872 // sp = ksOldSpolyRedNew(ppMult_qq(temp->getT1(),temp->getLp1Poly()),
873 // ppMult_qq(temp->getT2(),temp->getLp2Poly()));
874 //Print("BEGIN SPOLY2\n====================\n");
875 // pNorm(sp);
876 // pWrite(pHead(sp));
877 //Print("--------------------------\n");
878 //}
879 if(!criterion2(temp->getT1(),temp->getAdLp1(),rules,temp->getTestedRuleOld())) {
880 //if(temp->getDel() == 0 && !criterion2(temp->getT1(),temp->getAdLp1(),rules,temp->getTestedRuleOld())) {
881 if(temp->getLp2Index() == temp->getLp1Index()) {
882 if(!criterion2(temp->getT2(),temp->getAdLp2(),rules,temp->getTestedRuleOld())) {
883 sp = ksOldSpolyRedNew(ppMult_qq(temp->getT1(),temp->getLp1Poly()),
884 ppMult_qq(temp->getT2(),temp->getLp2Poly()));
885 pNorm(sp);
886 if(NULL == sp) {
888 rules->insert(temp->getLp1Index(),ppMult_qq(temp->getT1(),temp->getLp1Term()));
890 pDelete(&sp);
891 }
892 else {
893 rules->insert(temp->getLp1Index(),ppMult_qq(temp->getT1(),temp->getLp1Term()));
895 sPolyList->insertByLabel(ppMult_qq(temp->getT1(),temp->getLp1Term()),temp->getLp1Index(),sp,rules->getFirst()->getRuleOld());
896 //Print("INSERTED\n");
898 }
899 }
900 else {
903 }
904 rejectedGBList->insert(pHead(ppMult_qq(temp->getT1(),temp->getLp1Poly())));
905 //Print("rejected!\n");
906
907 //Print("CRITERION 2 in SPOLS 2nd generator\n");
908 }
909 }
910 else {
911 sp = ksOldSpolyRedNew(ppMult_qq(temp->getT1(),temp->getLp1Poly()),
912 ppMult_qq(temp->getT2(),temp->getLp2Poly()));
913 //Print("BEGIN SPOLY2\n====================\n");
914 pNorm(sp);
915 //pWrite(sp);
916 //Print("END SPOLY2\n====================\n");
917 if(NULL == sp) {
919 rules->insert(temp->getLp1Index(),ppMult_qq(temp->getT1(),temp->getLp1Term()));
921 pDelete(&sp);
922 }
923 else {
924 rules->insert(temp->getLp1Index(),ppMult_qq(temp->getT1(),temp->getLp1Term()));
926 sPolyList->insertByLabel(ppMult_qq(temp->getT1(),temp->getLp1Term()),temp->getLp1Index(),sp,rules->getFirst()->getRuleOld());
927 //Print("INSERTED\n");
929 }
930 }
931 }
932 /*
933 if(temp->getDel() == 0 && criterion2(temp->getT1(),temp->getAdLp1(),rules,temp->getTestedRuleOld())) {
934 //Print("rejected!\n");
935 rejectedGBList->insert(pHead(ppMult_qq(temp->getT1(),temp->getLp1Poly())));
936 }
937
938
939 if(temp->getDel() == 1 && !criterion2(temp->getT1(),temp->getAdLp1(),rules,temp->getTestedRuleOld())) {
940 if(highestDegree < pDeg(ppMult_qq(temp->getT1(),temp->getLp1Poly()))) {
941 highestDegree = pDeg(ppMult_qq(temp->getT1(),temp->getLp1Poly()));
942 }
943 if(temp->getLp2Index() == temp->getLp1Index()) {
944 if(!criterion2(temp->getT2(),temp->getAdLp2(),rules,temp->getTestedRuleOld())) {
945 sp = ksOldSpolyRedNew(ppMult_qq(temp->getT1(),temp->getLp1Poly()),
946 ppMult_qq(temp->getT2(),temp->getLp2Poly()));
947 pNorm(sp);
948 if(NULL == sp) {
949 reductionsToZero++;
950 rules->insert(temp->getLp1Index(),ppMult_qq(temp->getT1(),temp->getLp1Term()));
951 numberOfRules++;
952 pDelete(&sp);
953 }
954 else {
955 rules->insert(temp->getLp1Index(),ppMult_qq(temp->getT1(),temp->getLp1Term()));
956 numberOfRules++;
957
958
959 // save the address of the rule again in a different
960 // list
961
962 f5rules->insert(rules->getFirst()->getRuleOld());
963 f5pairs->insertWithoutSort(temp->getData());
964 ///////////////////////////////////////
965
966 //sPolyList->insertByLabel(ppMult_qq(temp->getT1(),temp->getLp1Term()),temp->getLp1Index(),sp,rules->getFirst()->getRuleOld());
967 }
968 }
969 }
970 else {
971 sp = ksOldSpolyRedNew(ppMult_qq(temp->getT1(),temp->getLp1Poly()),
972 ppMult_qq(temp->getT2(),temp->getLp2Poly()));
973 //Print("BEGIN SPOLY2\n====================\n");
974 pNorm(sp);
975 //pWrite(sp);
976 //Print("END SPOLY2\n====================\n");
977 if(NULL == sp) {
978 reductionsToZero++;
979 //rules->insert(temp->getLp1Index(),ppMult_qq(temp->getT1(),temp->getLp1Term()));
980 numberOfRules++;
981 pDelete(&sp);
982 }
983 else {
984 rules->insert(temp->getLp1Index(),ppMult_qq(temp->getT1(),temp->getLp1Term()));
985 numberOfRules++;
986 // save the address of the rule again in a different
987 // list
988
989 f5rules->insert(rules->getFirst()->getRuleOld());
990 f5pairs->insertWithoutSort(temp->getData());
991 ///////////////////////////////////////
992 //sPolyList->insertByLabel(ppMult_qq(temp->getT1(),temp->getLp1Term()),temp->getLp1Index(),sp,rules->getFirst()->getRuleOld());
993 // numberOfSpolys++;
994 }
995 }
996 }
997 // the following else is not needed at all as we are checking
998 // F5-critical pairs in this step
999 /*
1000 else {
1001 if(!temp->getDel()) {
1002 rejectedGBList->insert(pHead(ppMult_qq(temp->getT1(),temp->getLp1Poly())));
1003 }
1004
1005 }
1006 */
1007
1008 temp = temp->getNext();
1009
1010 }
1011
1012 /*
1013 temp = f5pairs->getFirst();
1014 RNode* tempRule = f5rules->getFirst();
1015 int howmany = 1;
1016 while(NULL != temp) {
1017 //Print("RULE: ");
1018 //pWrite(ppMult_qq(temp->getT1(),temp->getLp1Term()));
1019 sp = ksOldSpolyRedNew(ppMult_qq(temp->getT1(),temp->getLp1Poly()),
1020 ppMult_qq(temp->getT2(),temp->getLp2Poly()));
1021 pNorm(sp);
1022 if(rejectedGBList->check(pHead(ppMult_qq(temp->getT1(),temp->getLp1Poly())))) { //|| (temp->getData()->getDeg() == 10 && howmany == 2)) {
1023 if((temp->getData()->getDeg() == 10) && (howmany == 2)) {
1024 //Print("HIER DRIN IM SAFTLADEN\n");
1025 }
1026 sPolyList->insertByLabel(ppMult_qq(temp->getT1(),temp->getLp1Term()),temp->getLp1Index(),sp,tempRule->getRuleOld());
1027 numberOfSpolys++;
1028 howmany++;
1029 }
1030 else {
1031 numberRejectedF5CriticalPairs++;
1032 howmany++;
1033 if(numberRejectedF5CriticalPairs < -1) { // ||
1034 }
1035 else {
1036 //numberRejectedF5CriticalPairs == 7) {
1037 /*
1038 PrintS("--------------------------------- rejected F5-critical pair-------------------------------------\n");
1039 pWrite(pHead(ppMult_qq(temp->getT1(),temp->getLp1Poly())));
1040 PrintS("Label: ");
1041 pWrite(ppMult_qq(temp->getT1(),temp->getLp1Term()));
1042 Print("%d\n",temp->getDel());
1043 PrintS("Comes from:\n ");
1044 pWrite(pHead(temp->getLp1Poly()));
1045 PrintS("Label: ");
1046 pWrite(temp->getLp1Term());
1047 Print("%d\n",temp->getLp1Index());
1048 pWrite(pHead(temp->getLp2Poly()));
1049 PrintS("Label: ");
1050 pWrite(temp->getLp2Term());
1051 Print("%d\n",temp->getLp2Index());
1052 //Print("--------------------------------------LIST OF GB PAIRS REJECTED-----------------------------------------\n");
1053 //rejectedGBList->print();
1054 PrintS("--------------------------------------------------------------------------------------------------------\n");
1055 //if(temp->getLp1Index() < 7) {
1056 sPolyList->insertByLabel(ppMult_qq(temp->getT1(),temp->getLp1Term()),temp->getLp1Index(),sp,tempRule->getRuleOld());
1057
1058 //}
1059 //numberOfSpolys++;
1060 }
1061 //pSetExp(tempRule->getRuleOld()->getTerm(),1,1000);
1062 }
1063 temp = temp->getNext();
1064 tempRule = tempRule->getNext();
1065
1066 }
1067 */
1068 // these critical pairs can be deleted now as they are either useless for further computations or
1069 // already saved as an S-polynomial to be reduced in the following
1070 delete first;
1071//Print("NUMBER SPOLYS: %d\n", numberOfSpolys);
1072//Print("SPOLY LIST: \n");
1073//LNode* tempSpoly = sPolyList->getFirst();
1074//if(NULL != tempSpoly) {
1075// pWrite(pHead(tempSpoly->getPoly()));
1076// tempSpoly = tempSpoly->getNext();
1077//}
1078//Print("-----SP------\n");
1079//else {
1080// Print("EMPTY SPOLYLIST!\n");
1081//}
1082}
1083
1084/*
1085========================================================================
1086reduction including subalgorithm topReduction() using Faugere's criteria
1087========================================================================
1088*/
1089void reduction(LList* sPolyList, CListOld* critPairs, LList* gPrev, RList* rules, LTagList* lTag, RTagList* rTag,
1090 ideal gbPrev, PList* rejectedGBList, int plus) {
1091 //Print("##########################################In REDUCTION!########################################\n");
1092 // check if sPolyList has any elements
1093 // NOTE: due to initialization sPolyList always has a default NULL element
1094 LNode* temp = sPolyList->getFirst();
1095 while(NULL != temp) {
1096 // temp is the first element in the sPolyList which should be reduced
1097 // due to earlier sorting this is the element of minimal degree AND
1098 // minimal label
1099 // delete the above first element from sPolyList, temp will be either reduced to
1100 // zero or added to gPrev, but never come back to sPolyList
1101 //pWrite(sPolyList->getFirst()->getPoly());
1102 //Print("LIST OF SPOLYNOMIALS!\n");
1103 //sPolyList->print();
1104 sPolyList->setFirst(temp->getNext());
1105 poly tempNF = kNF(gbPrev,currRing->qideal,temp->getPoly());
1106 if(NULL != tempNF) {
1107 pNorm(tempNF);
1108 temp->setPoly(tempNF);
1109 // try further reductions of temp with polynomials in gPrev
1110 // with label index = current label index: this is done such that there
1111 // is no label corruption during the reduction process
1112 //Print("lower label reduction: ");
1113 //pWrite(tempNF);
1114 topReduction(temp,sPolyList,gPrev,critPairs,rules,lTag,rTag,gbPrev, rejectedGBList,plus);
1115
1116 }
1117 else {
1119 delete temp;
1120 }
1121 //if(NULL != temp->getPoly()) {
1122 // criticalPair(gPrev,critPairs,lTag,rTag,rules);
1123 //}
1124 temp = sPolyList->getFirst();
1125 }
1126 //sPolyList->print();
1127 //delete sPolyList;
1128}
1129
1130/*
1131========================================================================
1132reduction including subalgorithm topReduction() using Faugere's criteria
1133========================================================================
1134*/
1135void newReduction(LList* sPolyList, CListOld* critPairs, LList* gPrev, LList* reducers, RList* rules, LTagList* lTag, RTagList* rTag,
1136 ideal gbPrev, int termination, PList* rejectedGBList, int plus) {
1137 //Print("##########################################In REDUCTION!########################################\n");
1138 // check if sPolyList has any elements
1139 // NOTE: due to initialization sPolyList always has a default NULL element
1140 //Print("--1--\n");
1141 LNode* temp = sPolyList->getFirst();
1142 //Print("START OF REDUCTION: ");
1143 while(NULL != temp) {
1145 // temp is the first element in the sPolyList which should be reduced
1146 // due to earlier sorting this is the element of minimal degree AND
1147 // minimal label
1148 // delete the above first element from sPolyList, temp will be either reduced to
1149 // zero or added to gPrev, but never come back to sPolyList
1150 //Print("LIST OF SPOLYNOMIALS!\n");
1151 //sPolyList->print();
1152 //pWrite(sPolyList->getFirst()->getPoly());
1153 sPolyList->setFirst(temp->getNext());
1154 //if(pDeg(temp->getPoly()) > 11) {
1155 // Print("YES!!!!!!!!!!!!!!!!\n");
1156 //}
1157 //pWrite(temp->getPoly());
1158 //poly tempNF = kNF(gbPrev,currRing->qideal,temp->getPoly());
1159 //Print("!!!\n");
1160 //if(NULL != tempNF) {
1161 //pNorm(tempNF);
1162 //temp->setPoly(tempNF);
1163 //Print("lower label reduction: ");
1164 //pWrite(tempNF);
1165 // try further reductions of temp with polynomials in gPrev
1166 // with label index = current label index: this is done such that there
1167 // is no label corruption during the reduction process
1168 findReducers(temp,sPolyList,gbPrev,gPrev,reducers,critPairs,rules,lTag,rTag, termination, rejectedGBList,plus);
1169 //}
1170 //else {
1171 // reductionsToZero++;
1172 // delete temp;
1173 //}
1174 //if(NULL != temp->getPoly()) {
1175 // criticalPair(gPrev,critPairs,lTag,rTag,rules);
1176 //}
1177 //Print("HIER AUCH ?\n");
1178 //Print("--2--\n");
1179 //sPolyList->print();
1180 //critPairs->print();
1181 temp = sPolyList->getFirst();
1182 //Print("%p\n",temp);
1183 }
1184 //sPolyList->print();
1185 //delete sPolyList;
1186 //Print("REDUCTION FERTIG\n");
1187}
1188
1189
1190/*!
1191 * ================================================================================
1192 * searches for reducers of temp similar to the symbolic preprocessing of F4 and
1193 * divides them into a "good" and "bad" part:
1194 *
1195 * the "good" ones are the reducers which do not corrupt the label of temp, with
1196 * these the normal form of temp is computed
1197 *
1198 * the "bad" ones are the reducers which corrupt the label of temp, they are tested
1199 * later on for possible new rules and S-polynomials to be added to the algorithm
1200 * ================================================================================
1201*/
1202void findReducers(LNode* l, LList* sPolyList, ideal gbPrev, LList* gPrev, LList* reducers, CListOld* critPairs, RList* rules, LTagList* lTag, RTagList* rTag, int termination, PList* rejectedGBList, int plus) {
1203 int canonicalize = 0;
1204 //int timerRed = 0;
1205 bool addToG = 1;
1206 number sign = nInit(-1);
1207 LList* good = new LList();
1208 LList* bad = new LList();
1209 LList* monomials = new LList(l->getLPolyOld());
1210 poly u = pOne();
1211 number nOne = nInit(1);
1212 LNode* tempRed = lTag->getFirstCurrentIdx();
1213 LNode* tempMon = monomials->getFirst();
1214 poly tempPoly = pInit();
1215 poly redPoly = NULL;
1216 int idx = l->getIndex();
1217 //Print("IN FIND REDUCERS: ");
1218 //pWrite(l->getPoly());
1219 tempPoly = pCopy(l->getPoly());
1220 //tempMon->setPoly(tempPoly);
1221 //while(NULL != tempMon) {
1222 // iteration over all monomials in tempMon
1223 kBucket* bucket = kBucketCreate(currRing);
1224 kBucketInit(bucket,tempPoly,0);
1225 tempPoly = kBucketGetLm(bucket);
1226 //Print("\n\n\nTO BE REDUCED: ");
1227 //pWrite(l->getPoly());
1228 //pWrite(l->getTerm());
1229 //pWrite(tempPoly);
1230 while(NULL != tempPoly) {
1231 // iteration of all elements in gPrev of the current index
1232 tempRed = gPrev->getFirst();
1233 while(NULL != tempRed) {
1234 //Print("TEMPREDPOLY: ");
1235 //pWrite(tempRed->getPoly());
1236 if(pLmDivisibleByNoComp(tempRed->getPoly(),tempPoly)) {
1237 u = pMDivideM(tempPoly,tempRed->getPoly());
1238 //Print("U: ");
1239 //pWrite(u);
1240 if(pLmCmp(u,pOne()) != 0) { // else u = 1 and no test need to be done!
1241 if(tempRed->getIndex() != idx) {
1242 // passing criterion1 ?
1243 if(!criterion1(gPrev,u,tempRed,lTag)) {
1244 poly tempRedPoly = tempRed->getPoly();
1245 //Print("REDUCER: ");
1246 //pWrite(tempRedPoly);
1247 pIter(tempRedPoly);
1248 int lTempRedPoly = pLength(tempRedPoly);
1249 kBucketExtractLm(bucket);
1250 kBucket_Minus_m_Mult_p(bucket,u,tempRedPoly,&lTempRedPoly);
1251 canonicalize++;
1252 //Print("Reduction\n");
1253 if(!(canonicalize % 50)) {
1254 kBucketCanonicalize(bucket);
1255 }
1256 tempPoly = kBucketGetLm(bucket);
1257 //Print("TEMPPOLY: ");
1258 //pWrite(tempPoly);
1259 if(NULL != tempPoly) {
1260 tempRed = gPrev->getFirst();
1261 continue;
1262 }
1263 else {
1264 break;
1265 }
1266 }
1267
1268 }
1269 else {
1270 if(pLmCmp(ppMult_qq(u,tempRed->getTerm()),l->getTerm()) == 0) {
1271 //Print("NOT ALLOWED REDUCER, EQUAL LABELS:\n");
1272 //pWrite(u);
1273 //pWrite(tempRed->getTerm());
1274 //pWrite(pHead(tempRed->getPoly()));
1275 addToG = 0;
1276 }
1277 if(pLmCmp(ppMult_qq(u,tempRed->getTerm()),l->getTerm()) != 0) {
1278 // passing criterion2 ?
1279 if(!criterion2(gPrev->getFirst()->getIndex(), u,tempRed,rules,rTag)) {
1280 // passing criterion1 ?
1281 if(!criterion1(gPrev,u,tempRed,lTag)) {
1282 if(pLmCmp(ppMult_qq(u,tempRed->getTerm()),l->getTerm()) == 1) {
1283 if(NULL == redPoly) {
1284 bad->insert(tempRed->getLPolyOld());
1285 addToG = 1;
1286 //poly tempRedPoly = tempRed->getPoly();
1287 //break;
1288 }
1289 }
1290 else {
1291 poly tempRedPoly = tempRed->getPoly();
1292 //Print("REDUCER: ");
1293 //pWrite(tempRedPoly);
1294 pIter(tempRedPoly);
1295 int lTempRedPoly = pLength(tempRedPoly);
1296 //Print("HEAD MONOMIAL KBUCKET: ");
1297 //pWrite(kBucketGetLm(bucket));
1298 kBucketExtractLm(bucket);
1299 kBucket_Minus_m_Mult_p(bucket,u,tempRedPoly,&lTempRedPoly);
1300 canonicalize++;
1301 //Print("REDUCTION\n");
1302 addToG = 1;
1303 if(!(canonicalize % 50)) {
1304 kBucketCanonicalize(bucket);
1305 }
1306 //Print("HEAD MONOMIAL KBUCKET: ");
1307 //pWrite(kBucketGetLm(bucket));
1308 tempPoly = kBucketGetLm(bucket);
1309 //Print("TEMPPOLY: ");
1310 //pWrite(tempPoly);
1311 if(NULL != tempPoly) {
1312 tempRed = gPrev->getFirst();
1313 continue;
1314 }
1315 else {
1316 break;
1317 }
1318 }
1319 }
1320 }
1321 else {
1322 //Print("CRIT 1 ");
1323
1324 if(pLmCmp(ppMult_qq(u,tempRed->getTerm()),l->getTerm()) == 1 ) {
1325 //Print("NOT ALLOWED REDUCER, CRIT 1:\n");
1326 //pWrite(u);
1327 //pWrite(tempRed->getTerm());
1328 //pWrite(tempRed->getPoly());
1329 if(pLmDivisibleByNoComp(tempRed->getTerm(),l->getTerm())) {
1330 //Print("REDUCER LABEL: ");
1331 //pWrite(tempRed->getTerm());
1332addToG = 0;
1333 }
1334 }
1335 }
1336 }
1337 else {
1338 //Print("CRIT 2 ");
1339 if(pLmCmp(ppMult_qq(u,tempRed->getTerm()),l->getTerm()) == 1) {
1340 //Print("NOT ALLOWED REDUCER, CRIT 2:\n");
1341 //pWrite(u);
1342 //pWrite(tempRed->getTerm());
1343 //pWrite(tempRed->getPoly());
1344 if(pLmDivisibleByNoComp(tempRed->getTerm(),l->getTerm())) {
1345 //Print("REDUCER LABEL: ");
1346 //pWrite(tempRed->getTerm());
1347addToG = 0;
1348 }
1349 }
1350 }
1351 }
1352 }
1353 else { // u = 1 => reduce without checking criteria
1354 poly tempRedPoly = tempRed->getPoly();
1355 //Print("REDUCER: ");
1356 //pWrite(tempRedPoly);
1357 pIter(tempRedPoly);
1358 int lTempRedPoly = pLength(tempRedPoly);
1359 kBucketExtractLm(bucket);
1360 kBucket_Minus_m_Mult_p(bucket,u,tempRedPoly,&lTempRedPoly);
1361 canonicalize++;
1362 //Print("Reduction\n");
1363 if(!(canonicalize % 50)) {
1364 kBucketCanonicalize(bucket);
1365 }
1366 tempPoly = kBucketGetLm(bucket);
1367 //Print("TEMPPOLY: ");
1368 //pWrite(tempPoly);
1369 if(NULL != tempPoly) {
1370 tempRed = gPrev->getFirst();
1371 continue;
1372 }
1373 else {
1374 break;
1375 }
1376
1377 }
1378 }
1379 tempRed = tempRed->getNext();
1380 }
1381 // reduction process with elements in LList* reducers
1382 if(NULL != tempPoly) {
1383 //Print("HERE\n");
1384 tempRed = reducers->getFirst();
1385 while(NULL != tempRed) {
1386 //Print("TEMPREDPOLY: ");
1387 //pWrite(tempRed->getPoly());
1388 //pWrite(tempPoly);
1389 if(pLmDivisibleByNoComp(tempRed->getPoly(),tempPoly)) {
1390 //Print("A\n");
1391 u = pMDivideM(tempPoly,tempRed->getPoly());
1392 //Print("U: ");
1393 //pWrite(u);
1394 if(tempRed->getIndex() != idx) {
1395 // passing criterion1 ?
1396 if(!criterion1(gPrev,u,tempRed,lTag)) {
1397 poly tempRedPoly = tempRed->getPoly();
1398 //Print("REDUCER: ");
1399 //pWrite(ppMult_qq(u,tempRedPoly));
1400 pIter(tempRedPoly);
1401 int lTempRedPoly = pLength(tempRedPoly);
1402 kBucketExtractLm(bucket);
1403 kBucket_Minus_m_Mult_p(bucket,u,tempRedPoly,&lTempRedPoly);
1404 canonicalize++;
1405 //Print("Reduction\n");
1406 if(!(canonicalize % 50)) {
1407 kBucketCanonicalize(bucket);
1408 }
1409 tempPoly = kBucketGetLm(bucket);
1410 //Print("TEMPPOLY: ");
1411 //pWrite(tempPoly);
1412 if(NULL != tempPoly) {
1413 tempRed = gPrev->getFirst();
1414 continue;
1415 }
1416 else {
1417 break;
1418 }
1419 }
1420
1421 }
1422 else {
1423 if(pLmCmp(ppMult_qq(u,tempRed->getTerm()),l->getTerm()) == 0) {
1424 //Print("NOT ALLOWED REDUCER, EQUAL LABELS:\n");
1425 //pWrite(u);
1426 //pWrite(tempRed->getTerm());
1427 //pWrite(pHead(tempRed->getPoly()));
1428 //addToG = 0;
1429 }
1430 if(pLmCmp(ppMult_qq(u,tempRed->getTerm()),l->getTerm()) != 0) {
1431 // passing criterion2 ?
1432 if(!criterion2(gPrev->getFirst()->getIndex(), u,tempRed,rules,rTag)) {
1433 // passing criterion1 ?
1434 if(!criterion1(gPrev,u,tempRed,lTag)) {
1435 if(pLmCmp(ppMult_qq(u,tempRed->getTerm()),l->getTerm()) == 1) {
1436 if(NULL == redPoly) {
1437 bad->insert(tempRed->getLPolyOld());
1438 addToG = 1;
1439 //poly tempRedPoly = tempRed->getPoly();
1440 //break;
1441 }
1442 }
1443 else {
1444 poly tempRedPoly = tempRed->getPoly();
1445 //Print("REDUCER: ");
1446 //pWrite(ppMult_qq(u,tempRedPoly));
1447 pIter(tempRedPoly);
1448 int lTempRedPoly = pLength(tempRedPoly);
1449 //Print("HEAD MONOMIAL KBUCKET: ");
1450 //pWrite(kBucketGetLm(bucket));
1451 kBucketExtractLm(bucket);
1452 kBucket_Minus_m_Mult_p(bucket,u,tempRedPoly,&lTempRedPoly);
1453 canonicalize++;
1454 //Print("REDUCTION\n");
1455 addToG = 1;
1456 if(!(canonicalize % 50)) {
1457 kBucketCanonicalize(bucket);
1458 }
1459 //Print("HEAD MONOMIAL KBUCKET: ");
1460 //pWrite(kBucketGetLm(bucket));
1461 tempPoly = kBucketGetLm(bucket);
1462 //Print("TEMPPOLY: ");
1463 //pWrite(tempPoly);
1464 if(NULL != tempPoly) {
1465 tempRed = gPrev->getFirst();
1466 continue;
1467 }
1468 else {
1469 break;
1470 }
1471 }
1472 }
1473 }
1474 else {
1475 //Print("CRIT 1 ");
1476
1477 if(pLmCmp(ppMult_qq(u,tempRed->getTerm()),l->getTerm()) == 1 ) {
1478 //Print("NOT ALLOWED REDUCER, CRIT 1:\n");
1479 //pWrite(u);
1480 //pWrite(tempRed->getTerm());
1481 //pWrite(tempRed->getPoly());
1482 if(pLmDivisibleByNoComp(tempRed->getTerm(),l->getTerm())) {
1483 //Print("REDUCER LABEL: ");
1484 //pWrite(tempRed->getTerm());
1485 addToG = 0;
1486 }
1487 }
1488 }
1489 }
1490 else {
1491 //Print("CRIT 2 ");
1492 if(pLmCmp(ppMult_qq(u,tempRed->getTerm()),l->getTerm()) == 1) {
1493 //Print("NOT ALLOWED REDUCER, CRIT 2:\n");
1494 //pWrite(u);
1495 //pWrite(tempRed->getTerm());
1496 //pWrite(tempRed->getPoly());
1497 if(pLmDivisibleByNoComp(tempRed->getTerm(),l->getTerm())) {
1498 //Print("REDUCER LABEL: ");
1499 //pWrite(tempRed->getTerm());
1500addToG = 0;
1501 }
1502 }
1503 }
1504 }
1505
1506 }
1507 tempRed = tempRed->getNext();
1508 }
1509 }
1510 if(NULL != tempPoly) {
1511 if(NULL == redPoly) {
1512 redPoly = kBucketExtractLm(bucket);
1513 }
1514 else {
1515 redPoly = p_Merge_q(redPoly,kBucketExtractLm(bucket),currRing);
1516 }
1517 // for top-reduction only
1518 redPoly = p_Merge_q(redPoly,kBucketClear(bucket),currRing);
1519 break;
1520 // end for top-reduction only
1521 tempPoly = kBucketGetLm(bucket);
1522
1523 }
1524 }
1525 if(NULL == redPoly) {
1527 //pDelete(&redPoly);
1528 }
1529 else
1530 {
1531 PrintS("\nELEMENT ADDED TO GPREV: ");
1532 pNorm(redPoly);
1533 if(highestDegree < pDeg(redPoly))
1534 {
1535 highestDegree = pDeg(redPoly);
1536 }
1537 pWrite(pHead(redPoly));
1538 //pWrite(l->getTerm());
1539 //Print("%d\n",canonicalize);
1540 l->setPoly(redPoly);
1541 // give "l" the label if it is "useful" (addToG = 0) or "useless"
1542 // (addToG = 1)
1543 l->setDel(!addToG);
1544 Print("redundant? %d\n\n",l->getDel());
1545 if(addToG == 0 && termination == 1) {
1546 reducers->insert(l->getLPolyOld());
1547 }
1548 else {
1549 gPrev->insert(l->getLPolyOld());
1550 }
1551 //Print("%d\n\n",termination);
1552 if(termination == 1) {
1553 if(addToG) {
1554 //Print("----------------HERE?-----------------\n");
1555 criticalPair(gPrev,critPairs,lTag,rTag,rules, rejectedGBList,plus);
1556 }
1557 else {
1558 notInG++;
1559 //Print("\nNONONO");
1560 //pWrite(pHead(l->getPoly()));
1561 //pWrite(l->getTerm());
1562 }
1563 }
1564 // case in which all new elements are added to gPrev!
1565 // using boolean "addToG" to know if the element is "useful" (0) or
1566 // "useless" (1)
1567 else {
1568 if(!l->getDel()) {
1569 criticalPair(gPrev,critPairs,lTag,rTag,rules,rejectedGBList,plus);
1570 }
1571 else {
1572 criticalPair2(gPrev,critPairs,lTag,rTag,rules, rejectedGBList);
1573 }
1574 }
1575 }
1576
1577 // if there are "bad" reducers than try to compute new S-polynomials and rules
1578
1579 if(NULL != bad->getFirst()) {
1580 //Print("BAD STUFF LIST:\n");
1581 //bad->print();
1582 LNode* tempBad = bad->getFirst();
1583 //pWrite(l->getPoly());
1584 while(NULL != tempBad) {
1585 if(pDivisibleBy(tempBad->getPoly(),l->getPoly())) {
1586 //Print("BAD STUFF\n");
1587 //pWrite(l->getPoly());
1588 //pWrite(tempBad->getPoly());
1589 u = pMDivide(l->getPoly(),tempBad->getPoly());
1590 //Print("MULTIPLIER: ");
1591 //pWrite(u);
1592 pSetCoeff(u,nOne);
1593 if(pLmCmp(ppMult_qq(u,tempBad->getTerm()),l->getTerm()) != 0) {
1594 // passing criterion2 ?
1595 if(!criterion2(gPrev->getFirst()->getIndex(), u,tempBad,rules,rTag)) {
1596 // passing criterion1 ?
1597 if(!criterion1(gPrev,u,tempBad,lTag)) {
1598 //Print("HIERHIERHIERHIERHIERHIER\n");
1599 rules->insert(tempBad->getIndex(),ppMult_qq(u,tempBad->getTerm()));
1600 numberOfRules++;
1601 //gPrev->print();
1602 //pWrite(l->getPoly());
1603 poly temp = ksOldSpolyRedNew(ppMult_qq(u,tempBad->getPoly()),l->getPoly());
1604 //pWrite(l->getPoly());
1605 //Print("%p\n",temp);
1606 //gPrev->print();
1607 if(NULL != temp) {
1608 pNorm(temp);
1609 LNode* tempBadNew = new LNode(ppMult_qq(u,tempBad->getTerm()),tempBad->getIndex(),temp,rules->getFirst()->getRuleOld());
1610 //pWrite(temp);
1611 //pWrite(tempBadNew->getPoly());
1612 //pWrite(tempBadNew->getTerm());
1613 //pWrite(pHead(tempBadNew->getPoly()));
1614 //Print("%p\n",tempBadNew->getPoly());
1615 //tempRed->getLPoly()->setRule(rules->getFirst()->getRule());
1616 tempBadNew->setDel(1);
1617
1618 sPolyList->insertByLabel(tempBadNew);
1619 //Print("BAD SPOLYLIST: \n");
1620 //sPolyList->print();
1621 }
1622 }
1623 }
1624 }
1625 }
1626 //Print("HIER\n");
1627 tempBad = tempBad->getNext();
1628 //Print("%p\n",tempBad);
1629 }
1630 // Print("-------------------BAD STUFF LIST-----------------------------\n");
1631 }
1632 //Print("HIER AUCH\n");
1633 //Print("SPOLYLIST IN BAD: \n");
1634 //sPolyList->print();
1635 //Print("END FIND REDUCERS\n");
1636}
1637
1638/*
1639=======================================================================================
1640merging 2 polynomials p & q without requiring that all monomials of p & q are different
1641if there are equal monomials in p & q only one of these monomials (always that of p!)
1642is taken into account
1643=======================================================================================
1644
1645poly p_MergeEq_q(poly p, poly q, const ring r) {
1646 assume(p != NULL && q != NULL);
1647 p_Test(p, r);
1648 p_Test(q, r);
1649#if PDEBUG > 0
1650 int l = pLength(p) + pLength(q);
1651#endif
1652
1653 spolyrec rp;
1654 poly a = &rp;
1655 DECLARE_LENGTH(const unsigned long length = r->CmpL_Size);
1656 DECLARE_ORDSGN(const long* ordsgn = r->ordsgn);
1657
1658 Top: // compare p and q w.r.t. monomial ordering
1659 p_MemCmp(p->exp, q->exp, length, ordsgn, goto Equal, goto Greater , goto Smaller);
1660
1661 Equal:
1662 a = pNext(a) = p;
1663 pIter(p);
1664 pIter(q);
1665 if(NULL == p) {
1666 if(NULL == q) {
1667 goto Finish;
1668 }
1669 else {
1670 pNext(a) = q;
1671 goto Finish;
1672 }
1673 }
1674 goto Top;
1675
1676 Greater:
1677 a = pNext(a) = p;
1678 pIter(p);
1679 if (p==NULL) { pNext(a) = q; goto Finish;}
1680 goto Top;
1681
1682 Smaller:
1683 a = pNext(a) = q;
1684 pIter(q);
1685 if (q==NULL) { pNext(a) = p; goto Finish;}
1686 goto Top;
1687
1688 Finish:
1689
1690 p_Test(pNext(&rp), r);
1691#if PDEBUG > 0
1692 pAssume1(l - pLength(pNext(&rp)) == 0);
1693#endif
1694 return pNext(&rp);
1695}
1696*/
1697
1698/*
1699=====================================================================================
1700top reduction in F5, i.e. reduction of a given S-polynomial by labeled polynomials of
1701the same index whereas the labels are taken into account
1702=====================================================================================
1703*/
1704void topReduction(LNode* l, LList* sPolyList, LList* gPrev, CListOld* critPairs, RList* rules, LTagList* lTag, RTagList* rTag, ideal gbPrev, PList* rejectedGBList, int plus) {
1705 //Print("##########################################In topREDUCTION!########################################\n");
1706 // try l as long as there are reductors found by findReductor()
1707 LNode* gPrevRedCheck = lTag->getFirstCurrentIdx();
1708 LNode* tempRed;
1709 poly pOne = pOne();
1710 do {
1711 //int timer5 = initTimer();
1712 //startTimer();
1713 //Print("TOP REDUCTION: ");
1714 //pWrite(l->getPoly());
1715 tempRed = findReductor(l,sPolyList,gPrevRedCheck,gPrev,rules,lTag,rTag);
1716 //timer5 = getTimer();
1717 //reductionTime = reductionTime + timer5;
1718 // if a reductor for l is found and saved in tempRed
1719 if(NULL != tempRed) {
1720 // if label of reductor is greater than the label of l we have to built a new element
1721 // and add it to sPolyList
1722
1723 if(pLmCmp(tempRed->getTerm(),l->getTerm()) == 1) {
1724 // needed sinc pSub destroys the arguments!
1725 //poly temp_poly_l = pInit();
1726 //temp_poly_l = pCopy(l->getPoly());
1727 //Print("VORHER: ");
1728 //pWrite(tempRed->getPoly());
1729 //poly temp = pMinus_mm_Mult_qq(tempRed->getPoly(),pOne,l->getPoly());
1730 poly temp = ksOldSpolyRedNew(l->getPoly(),tempRed->getPoly());
1731 rules->insert(tempRed->getIndex(),tempRed->getTerm());
1732 //Print("NACHHER: ");
1733 //pWrite(tempRed->getPoly());
1734 //Print("TEMP: ");
1735 //pWrite(temp);
1736 if(NULL != temp) {
1737 pNorm(temp);
1738 //tempRed->setPoly(temp);
1739 //tempRed->setDel(1);
1740 //rules->insert(tempRed->getIndex(),tempRed->getTerm());
1741 LNode* tempRedNew = new LNode(tempRed->getTerm(),tempRed->getIndex(),temp,rules->getFirst()->getRuleOld());
1742 //tempRed->getLPoly()->setRule(rules->getFirst()->getRule());
1743 tempRedNew->setDel(1);
1744 sPolyList->insertByLabel(tempRedNew);
1745 }
1746 else {
1747 pDelete(&temp);
1749 //delete tempRed;
1750 }
1751 }
1752
1753 // label of reductor is smaller than the label of l, subtract reductor from l and delete the
1754 // gPrevRedCheck pointer added to l during findReductor() as the head term of l changes
1755 // after subtraction
1756 else {
1757
1758 //poly temp_poly_l = pInit();
1759 //temp_poly_l = pCopy(l->getPoly());
1760 //poly temp = pMinus_mm_Mult_qq(tempRed->getPoly(),pOne,l->getPoly());
1761 //Print("REDUCER: ");
1762 //pWrite(tempRed->getPoly());
1763 //pWrite(tempRed->getTerm());
1764 poly temp = ksOldSpolyRedNew(l->getPoly(),tempRed->getPoly());
1765 //Print("REDUCED ELEMENT: ");
1766 if(NULL != temp) {
1767 pNorm(temp);
1768 //pWrite(temp);
1769 poly tempNF = kNF(gbPrev,currRing->qideal,temp);
1770 pNorm(tempNF);
1771 if(NULL == tempNF) {
1773 pDelete(&tempNF);
1774 l->setPoly(NULL);
1775 break;
1776 }
1777 l->setPoly(tempNF);
1778
1779 gPrevRedCheck = lTag->getFirstCurrentIdx();
1780 }
1781 else {
1783 pDelete(&temp);
1784 l->setPoly(NULL);
1785 break;
1786 }
1787 }
1788 }
1789 else {
1790 if(NULL != l->getPoly()) {
1791 pNorm(l->getPoly());
1792 //Print("ELEMENT ADDED TO GPREV: ");
1793 //pWrite(l->getPoly());
1794 gPrev->insert(l->getLPolyOld());
1795 //Print("TEMP RED == 0 ");
1796 //pWrite(l->getPoly());
1797 //pWrite(l->getTerm());
1798 //rules->print();
1799 criticalPair(gPrev,critPairs,lTag,rTag,rules, rejectedGBList,plus);
1800 //Print("LIST OF CRITICAL PAIRS: \n");
1801 //critPairs->print();
1802 }
1803 break;
1804 }
1805 } while(1);
1806}
1807
1808
1809/*
1810=====================================================================
1811subalgorithm to find a possible reductor for the labeled polynomial l
1812=====================================================================
1813*/
1814LNode* findReductor(LNode* l, LList* sPolyList, LNode* gPrevRedCheck, LList* gPrev, RList* rules, LTagList* lTag,RTagList* rTag, PList* rejectedGBList) {
1815 // allociation of memory for the possible reductor
1816 //Print("LPOLY: ");
1817 //pWrite(l->getPoly());
1818 poly u = pOne();
1819 poly red;
1820 number nOne = nInit(1);
1821 LNode* temp;
1822 // head term of actual element such that we do not have to call pHead at each new reductor test
1823 poly t = pHead(l->getPoly());
1824 // if l was already checked use the information in gPrevRedCheck such
1825 // that we can start searching for new reducers from this point and
1826 // not from the first element of gPrev with the current index
1827 temp = gPrevRedCheck;
1828 // search for reductors until we are at the end of gPrev resp. at the
1829 // end of the elements of the current index
1830 while(NULL != temp && temp->getIndex() == l->getIndex()) {
1831 // does the head of the element of gPrev divides the head of
1832 // the to be reduced element?
1833 if(pLmDivisibleByNoComp(pHead(temp->getPoly()),t)) {
1834 // get all the information needed for the following tests
1835 // of the criteria
1836 u = pMDivide(t,temp->getPoly());
1837 pSetCoeff(u,nOne);
1838 red = ppMult_qq(u,temp->getPoly());
1839 pNorm(red);
1840 // check if both have the same label
1841 if(pLmCmp(ppMult_qq(u,temp->getTerm()),l->getTerm()) != 0) {
1842 // passing criterion2 ?
1843 if(!criterion2(gPrev->getFirst()->getIndex(), u,temp,rules,rTag)) {
1844 // passing criterion1 ?
1845 if(!criterion1(gPrev,u,temp,lTag)) {
1846 gPrevRedCheck = temp->getNext();
1847 LNode* redNode = new LNode(ppMult_qq(u,temp->getTerm()),temp->getIndex(),red,NULL,NULL);
1848 return redNode;
1849 }
1850 }
1851 }
1852 if(pLmCmp(ppMult_qq(u,temp->getTerm()),l->getTerm()) == 1) {
1853 // passing criterion2 ?
1854 if(!criterion2(gPrev->getFirst()->getIndex(), u,temp,rules,rTag)) {
1855 // passing criterion1 ?
1856 if(!criterion1(gPrev,u,temp,lTag)) {
1857 poly tempSpoly = ksOldSpolyRedNew(red,l->getPoly());
1858 rules->insert(temp->getIndex(),ppMult_qq(u,temp->getTerm()));
1859 gPrevRedCheck = temp->getNext();
1860 if(NULL != tempSpoly) {
1861 pNorm(tempSpoly);
1862 sPolyList->insertByLabel(ppMult_qq(u,temp->getTerm()),temp->getIndex(),tempSpoly,rules->getFirst()->getRuleOld());
1863 //Print("NEW ONE: ");
1864 //pWrite(tempSpoly);
1865 //Print("HIER\n");
1866 //sPolyList->print();
1867 //sleep(5);
1868 }
1869 }
1870 }
1871 }
1872 }
1873 //Print("AUCH HIER\n");
1874 temp = temp->getNext();
1875 }
1876
1877// delete temp;
1878 return NULL;
1879}
1880
1881
1882
1883/*
1884==========================================================================
1885MAIN:computes a gb of the ideal i in the ring r with our F5 implementation
1886OPTIONS: INTEGER "opt" is to be set "0" for F5, "1" for F5R, "2" for F5C
1887==========================================================================
1888*/
1889ideal F5main(ideal id, ring r, int opt, int plus, int termination)
1890{
1891 switch(opt)
1892 {
1893 case 0:
1894 PrintS("\nComputations are done by the standard F5 Algorithm");
1895 break;
1896 case 1:
1897 PrintS("\nComputations are done by the variant F5R of the F5 Algorithm");
1898 break;
1899 case 2:
1900 PrintS("\nComputations are done by the variant F5C of the F5 Algorithm");
1901 break;
1902 default:
1903 WerrorS("\nThe option can only be set to \"0\", \"1\" or \"2\":\n\"0\": standard F5 Algorithm\n\"1\": variant F5R\n\"2\": variant F5C\nComputations are aborted!\n");
1904 return id;
1905 }
1906
1907 int timer = initTimer();
1908 startTimer();
1909 int i,j,k,l;
1910 int gbLength;
1911 // 1 polynomial for defining initial labels & further tests
1912 poly ONE = pOne();
1913 poly pOne = pOne();
1914 number nOne = nInit(1);
1915 // tag the first element of index i-1 for criterion 1
1916 //Print("LTAG BEGINNING: %p\n",lTag);
1917
1918 // DEBUGGING STUFF START
1919 //Print("NUMBER: %d\n",r->N);
1920 /*
1921 int* ev = new int[r->N +1];
1922 for(i=0;i<IDELEMS(id);i++) {
1923 p_GetExpV(id->m[i],ev,currRing);
1924 //ev2 = pGetExp(id->m[i],1);
1925 pWrite(id->m[i]);
1926 Print("EXP1: %d\n",ev[1]);
1927 Print("EXP2: %d\n",ev[2]);
1928 Print("EXP3: %d\n\n",ev[3]);
1929 Print("SUM: %ld\n\n\n",sumVector(ev,r->N));
1930 }
1931 delete ev;
1932 */
1933 /*DEBUGGING STUFF END */
1934
1935 // first element in rTag is first element of rules which is NULL RNode,
1936 // this must be done due to possible later improvements
1937 RList* rules = new RList();
1938 //Print("RULES FIRST: %p\n",rules->getFirst());
1939 //Print("RULES FIRST DATA: %p\n",rules->getFirst()->getRule());
1940 //RTagList* rTag = new RTagList(rules->getFirst());
1941 RTagList* rTag = NULL;
1942 i = 1;
1943 /*for(j=0; j<IDELEMS(id); j++) {
1944 if(NULL != id->m[j]) {
1945 if(pComparePolys(id->m[j],ONE)) {
1946 PrintS("One Polynomial in Input => Computations stopped\n");
1947 ideal idNew = idInit(1,1);
1948 idNew->m[0] = ONE;
1949 return(idNew);
1950 }
1951 }
1952 }*/
1953 ideal idNew = kInterRed(id);
1954 id = idNew;
1955 //qsortDegree(&id->m[0],&id->m[IDELEMS(id)-1]);
1956 //idShow(id);
1957 LList* gPrev = new LList(ONE, i, id->m[0]);
1958 LList* reducers = new LList();
1959 //idShow(id);
1960 //Print("%p\n",id->m[0]);
1961 //pWrite(id->m[0]);
1962 //Print("%p\n",gPrev->getFirst()->getPoly());
1963 //pWrite(gPrev->getFirst()->getPoly());
1964
1965 LTagList* lTag = new LTagList(gPrev->getFirst());
1966 //lTag->insert(gPrev->getFirst());
1967 lTag->setFirstCurrentIdx(gPrev->getFirst());
1968 // computing the groebner basis of the elements of index < actual index
1969 gbLength = gPrev->getLength();
1970 //Print("Laenge der bisherigen Groebner Basis: %d\n",gPrev->getLength());
1971 ideal gbPrev = idInit(gbLength,1);
1972 // initializing the groebner basis of elements of index < actual index
1973 gbPrev->m[0] = gPrev->getFirst()->getPoly();
1974 //idShow(gbPrev);
1975 //idShow(currRing->qideal);
1976 for(i=2; i<=IDELEMS(id); i++) {
1977 LNode* gPrevTag = gPrev->getLast();
1978 //Print("Last POlynomial in GPREV: ");
1979 //Print("%p\n",gPrevTag);
1980 //pWrite(gPrevTag->getPoly());
1981 Print("Iteration: %d\n\n",i);
1982 gPrev = F5inc(i, id->m[i-1], gPrev, reducers, gbPrev, ONE, lTag, rules, rTag, plus, termination);
1983 //Print("%d\n",gPrev->count(gPrevTag->getNext()));
1984 //Print("%d\n",gPrev->getLength());
1985 //Print("____________________________________ITERATION STEP DONE________________________________________\n");
1986
1987 // DEBUGGING STUFF
1988 LNode* temp = gPrev->getFirst();
1989
1990
1991 /////////////////////////////////////////////////////////////////////////////////
1992 // //
1993 // one needs to choose one of the following 3 implementations of the algorithm //
1994 // F5,F5R or F5C //
1995 // //
1996 /////////////////////////////////////////////////////////////////////////////////
1997
1998
1999 //
2000 // standard "F5"
2001 //
2002 if(0 == opt) {
2003 if(gPrev->getLength() > gbLength) {
2004 if(i < IDELEMS(id)) {
2005 ideal gbAdd = idInit(gPrev->getLength()-gbLength,1);
2006 LNode* temp = gPrevTag;
2007 int counter = 0;
2008 for(j=0;j<=gPrev->getLength()-gbLength-1;j++) {
2009 temp = temp->getNext();
2010 if(0 == temp->getDel()) {
2011 counter++;
2012 gbAdd->m[j] = temp->getPoly();
2013 }
2014 }
2015 gbPrev = idAdd(gbPrev,gbAdd);
2016 }
2017 else {
2018 ideal gbAdd = idInit(gPrev->getLength()-gbLength,1);
2019 LNode* temp = gPrevTag;
2020 for(j=0;j<=gPrev->getLength()-gbLength-1;j++) {
2021 temp = temp->getNext();
2022 gbAdd->m[j] = temp->getPoly();
2023 }
2024 gbPrev = idAdd(gbPrev,gbAdd);
2025 }
2026 //if(i == IDELEMS(id)) {
2027 // ideal tempId = kInterRed(gbPrev);
2028 // gbPrev = tempId;
2029 //}
2030 }
2031 gbLength = gPrev->getLength();
2032 }
2033
2034
2035 //
2036 // "F5R"
2037 //
2038 if(1 == opt) {
2039 if(gPrev->getLength() > gbLength) {
2040 if(i < IDELEMS(id)) {
2041 ideal gbAdd = idInit(gPrev->getLength()-gbLength,1);
2042 LNode* temp = gPrevTag;
2043 int counter = 0;
2044 for(j=0;j<=gPrev->getLength()-gbLength-1;j++) {
2045 temp = temp->getNext();
2046 if(0 == temp->getDel()) {
2047 counter++;
2048 gbAdd->m[j] = temp->getPoly();
2049 }
2050 }
2051 gbPrev = idAdd(gbPrev,gbAdd);
2052 }
2053 else {
2054 ideal gbAdd = idInit(gPrev->getLength()-gbLength,1);
2055 LNode* temp = gPrevTag;
2056 for(j=0;j<=gPrev->getLength()-gbLength-1;j++) {
2057 temp = temp->getNext();
2058 gbAdd->m[j] = temp->getPoly();
2059 }
2060 gbPrev = idAdd(gbPrev,gbAdd);
2061 }
2062 // interreduction stuff
2063 // comment this out if you want F5 instead of F5R
2064 if(i<IDELEMS(id)) {
2065 ideal tempId = kInterRed(gbPrev);
2066 gbPrev = tempId;
2067 }
2068 }
2069 gbLength = gPrev->getLength();
2070 }
2071
2072
2073 //
2074 // "F5C"
2075 //
2076 if(2 == opt) {
2077 if(gPrev->getLength() > gbLength) {
2078 if(i < IDELEMS(id)) {
2079 ideal gbAdd = idInit(gPrev->getLength()-gbLength,1);
2080 LNode* temp = gPrevTag;
2081 for(j=0;j<=gPrev->getLength()-gbLength-1;j++) {
2082 temp = temp->getNext();
2083 gbAdd->m[j] = temp->getPoly();
2084 }
2085 gbPrev = idAdd(gbPrev,gbAdd);
2086 }
2087 else {
2088 ideal gbAdd = idInit(gPrev->getLength()-gbLength,1);
2089 LNode* temp = gPrevTag;
2090 for(j=0;j<=gPrev->getLength()-gbLength-1;j++) {
2091 temp = temp->getNext();
2092 gbAdd->m[j] = temp->getPoly();
2093 }
2094 gbPrev = idAdd(gbPrev,gbAdd);
2095 }
2096 if(i<IDELEMS(id)) {
2097 ideal tempId = kInterRed(gbPrev);
2098 gbPrev = tempId;
2099 delete gPrev;
2100 delete rules;
2101 gPrev = new LList(pOne,1,gbPrev->m[0]);
2102 gPrev->insert(pOne,1,gbPrev->m[1]);
2103 rules = new RList();
2104 //rTag = new RTagList(rules->getFirst());
2105 for(k=2; k<IDELEMS(gbPrev); k++) {
2106 gPrev->insert(pOne,k+1,gbPrev->m[k]);
2107 /*
2108 for(l=0; l<k; l++) {
2109 }
2110 rTag->insert(rules->getFirst());
2111 */
2112 }
2113 }
2114 gbLength = gPrev->getLength();
2115 }
2116 }
2117
2118
2119 }
2120 timer = getTimer();
2121 //Print("\n\nADDING TIME IN REDUCTION: %d\n\n",reductionTime);
2122 Print("\n\nNumber of zero-reductions: %d\n",reductionsToZero);
2123 Print("Number of rules: %d\n",numberOfRules);
2124 Print("Number of rejected F5-critical pairs:%d\n",numberRejectedF5CriticalPairs);
2125 Print("Number of reductions: %d\n",numberOfReductions);
2126 Print("Elements not added to G: %d\n",notInG);
2127 Print("Highest Degree during computations: %d\n",highestDegree);
2128 Print("Degree d_0 in F5+: %d\n",highestDegreeGBCriticalPair);
2129 Print("Time for computations: %d/1000 seconds\n",timer);
2130 Print("Number of elements in gb: %d\n",IDELEMS(gbPrev));
2131 //LNode* temp = gPrev->getFirst();
2132 //while(NULL != temp) {
2133 // pWrite(temp->getPoly());
2134 // temp = temp->getNext();
2135 // }
2136 //gPrev->print();
2137 //delete lTag;
2138 delete rTag;
2139 delete gPrev;
2140 notInG = 0;
2141 numberOfRules = 0;
2142 reductionsToZero = 0;
2143 highestDegree = 0;
2145 reductionTime = 0;
2146 spolsTime = 0;
2151 numberOfSpolys = 0;
2152 return(gbPrev);
2153
2154
2155}
2156
2157#endif
int degree(const CanonicalForm &f)
int l
Definition: cfEzgcd.cc:100
int i
Definition: cfEzgcd.cc:132
int k
Definition: cfEzgcd.cc:99
CNode * getMinDeg()
Definition: f5lists.cc:952
void insert(CPairOld *c)
Definition: f5lists.cc:938
CNode * getFirst()
Definition: f5lists.cc:946
Definition: f5lists.h:232
LPolyOld * getAdLp2()
Definition: f5lists.cc:832
CPairOld * getData()
Definition: f5lists.cc:820
LPolyOld * getAdLp1()
Definition: f5lists.cc:828
poly getT1()
Definition: f5lists.cc:860
bool getDel()
Definition: f5lists.cc:876
poly getLp2Poly()
Definition: f5lists.cc:840
int getLp2Index()
Definition: f5lists.cc:856
RuleOld * getTestedRuleOld()
Definition: f5lists.cc:880
poly getLp1Term()
Definition: f5lists.cc:844
poly getT2()
Definition: f5lists.cc:868
CNode * getNext()
Definition: f5lists.cc:824
int getLp1Index()
Definition: f5lists.cc:852
poly getLp1Poly()
Definition: f5lists.cc:836
long getDeg()
Definition: f5data.h:162
Definition: f5lists.h:127
LNode * getFirst()
Definition: f5lists.cc:519
void insert(LPolyOld *lp)
Definition: f5lists.cc:457
int getLength()
Definition: f5lists.cc:527
void setFirst(LNode *l)
Definition: f5lists.cc:531
void insertByLabel(poly t, int i, poly p, RuleOld *r=NULL)
Definition: f5lists.cc:493
LNode * getLast()
Definition: f5lists.cc:523
Definition: f5lists.h:65
LNode * getNext()
Definition: f5lists.cc:321
int getIndex()
Definition: f5lists.cc:339
poly getPoly()
Definition: f5lists.cc:331
void setPoly(poly p)
Definition: f5lists.cc:356
void setDel(bool d)
Definition: f5lists.cc:372
bool getDel()
Definition: f5lists.cc:351
LPolyOld * getLPolyOld()
Definition: f5lists.cc:326
poly getTerm()
Definition: f5lists.cc:335
void setFirstCurrentIdx(LNode *l)
Definition: f5lists.cc:633
LNode * getFirstCurrentIdx()
Definition: f5lists.cc:645
void insert(LNode *l)
Definition: f5lists.cc:628
class PList of lists of PNodes
Definition: f5lists.h:50
void insert(poly p)
Definition: f5lists.cc:80
Definition: f5lists.h:313
RNode * getFirst()
Definition: f5lists.cc:1091
void insert(RuleOld *r)
Definition: f5lists.cc:1083
Definition: f5lists.h:290
poly getRuleOldTerm()
Definition: f5lists.cc:1035
RNode * getNext()
Definition: f5lists.cc:1023
int getRuleOldIndex()
Definition: f5lists.cc:1031
RuleOld * getRuleOld()
Definition: f5lists.cc:1027
#define Print
Definition: emacs.cc:80
VAR int numberOfSpolys
Definition: f5gb.cc:44
VAR int numberUsefulPairsMinDeg
Definition: f5gb.cc:40
bool compareMonomials(int *m1, int **m2, int numberOfRules, int k)
Definition: f5gb.cc:108
VAR int reductionTime
Definition: f5gb.cc:34
VAR int numberOfRules
Definition: f5gb.cc:32
VAR int notInG
Definition: f5gb.cc:31
VAR int numberOfReductions
Definition: f5gb.cc:43
VAR int numberUsefulPairs
Definition: f5gb.cc:38
void topReduction(LNode *l, LList *sPolyList, LList *gPrev, CListOld *critPairs, RList *rules, LTagList *lTag, RTagList *rTag, ideal gbPrev, PList *rejectedGBList, int plus)
Definition: f5gb.cc:1704
VAR int highestDegreeGBCriticalPair
Definition: f5gb.cc:41
VAR int reductionsToZero
Definition: f5gb.cc:33
LNode * findReductor(LNode *l, LList *sPolyList, LNode *gPrevRedCheck, LList *gPrev, RList *rules, LTagList *lTag, RTagList *rTag, PList *rejectedGBList)
Definition: f5gb.cc:1814
VAR int highestDegree
Definition: f5gb.cc:36
void criticalPair2(LList *gPrev, CListOld *critPairs, LTagList *lTag, RTagList *rTag, RList *rules, PList *rejectedGBList)
Definition: f5gb.cc:553
VAR int degreeBound
Definition: f5gb.cc:37
long sumVector(int *v, int k)
Definition: f5gb.cc:92
VAR int spolsTime
Definition: f5gb.cc:35
VAR int numberRejectedF5CriticalPairs
Definition: f5gb.cc:42
bool checkDGB(LList *gPrev)
Definition: f5gb.cc:299
void newReduction(LList *sPolyList, CListOld *critPairs, LList *gPrev, LList *reducers, RList *rules, LTagList *lTag, RTagList *rTag, ideal gbPrev, int termination, PList *rejectedGBList, int plus)
Definition: f5gb.cc:1135
void qsortDegree(poly *left, poly *right)
Definition: f5gb.cc:51
bool criterion2(int idx, poly t, LNode *l, RList *rules, RTagList *rTag)
Definition: f5gb.cc:675
void reduction(LList *sPolyList, CListOld *critPairs, LList *gPrev, RList *rules, LTagList *lTag, RTagList *rTag, ideal gbPrev, PList *rejectedGBList, int plus)
Definition: f5gb.cc:1089
void computeSPols(CNode *first, RTagList *rTag, RList *rules, LList *sPolyList, PList *rejectedGBList)
Definition: f5gb.cc:844
VAR int numberUselessPairs
Definition: f5gb.cc:39
bool criterion1(LList *gPrev, poly t, LNode *l, LTagList *lTag)
Definition: f5gb.cc:614
bool arrisCheck(CNode *first, LNode *firstGCurr, long arrideg)
Definition: f5gb.cc:382
LList * F5inc(int i, poly f_i, LList *gPrev, LList *reducers, ideal gbPrev, poly ONE, LTagList *lTag, RList *rules, RTagList *rTag, int plus, int termination)
Definition: f5gb.cc:130
void findReducers(LNode *l, LList *sPolyList, ideal gbPrev, LList *gPrev, LList *reducers, CListOld *critPairs, RList *rules, LTagList *lTag, RTagList *rTag, int termination, PList *rejectedGBList, int plus)
Definition: f5gb.cc:1202
#define pDeg(A)
Definition: f5gb.cc:29
int computeUsefulMinDeg(CNode *first)
Definition: f5gb.cc:828
void criticalPair(LList *gPrev, CListOld *critPairs, LTagList *lTag, RTagList *rTag, RList *rules, PList *rejectedGBList, int plus)
Definition: f5gb.cc:441
ideal F5main(ideal id, ring r, int opt, int plus, int termination)
Definition: f5gb.cc:1889
const Variable & v
< [in] a sqrfree bivariate poly
Definition: facBivar.h:39
bool bad
Definition: facFactorize.cc:64
int j
Definition: facHensel.cc:110
void WerrorS(const char *s)
Definition: feFopen.cc:24
#define STATIC_VAR
Definition: globaldefs.h:7
#define VAR
Definition: globaldefs.h:5
ideal idAdd(ideal h1, ideal h2)
h1 + h2
Definition: ideals.h:68
KINLINE poly ksOldSpolyRedNew(poly p1, poly p2, poly spNoether)
Definition: kInline.h:1186
void kBucketClear(kBucket_pt bucket, poly *p, int *length)
Definition: kbuckets.cc:521
void kBucket_Minus_m_Mult_p(kBucket_pt bucket, poly m, poly p, int *l, poly spNoether)
Bpoly == Bpoly - m*p; where m is a monom Does not destroy p and m assume (*l <= 0 || pLength(p) == *l...
Definition: kbuckets.cc:722
void kBucketInit(kBucket_pt bucket, poly lm, int length)
Definition: kbuckets.cc:493
poly kBucketExtractLm(kBucket_pt bucket)
Definition: kbuckets.cc:511
kBucket_pt kBucketCreate(const ring bucket_ring)
Creation/Destruction of buckets.
Definition: kbuckets.cc:209
const poly kBucketGetLm(kBucket_pt bucket)
Definition: kbuckets.cc:506
int kBucketCanonicalize(kBucket_pt bucket)
Canonicalizes Bpoly, i.e. converts polys of buckets into one poly in one bucket: Returns number of bu...
ideal kInterRed(ideal F, ideal Q)
Definition: kstd1.cc:3761
poly kNF(ideal F, ideal Q, poly p, int syzComp, int lazyReduce)
Definition: kstd1.cc:3182
int lcm(unsigned long *l, unsigned long *a, unsigned long *b, unsigned long p, int dega, int degb)
Definition: minpoly.cc:709
#define pIter(p)
Definition: monomials.h:37
#define nInit(i)
Definition: numbers.h:24
#define NULL
Definition: omList.c:12
static int pLength(poly a)
Definition: p_polys.h:188
static poly p_Merge_q(poly p, poly q, const ring r)
Definition: p_polys.h:1210
static long p_Totaldegree(poly p, const ring r)
Definition: p_polys.h:1505
VAR ring currRing
Widely used global variable which specifies the current polynomial ring for Singular interpreter and ...
Definition: polys.cc:13
Compatibility layer for legacy polynomial operations (over currRing)
#define pDelete(p_ptr)
Definition: polys.h:186
#define pHead(p)
returns newly allocated copy of Lm(p), coef is copied, next=NULL, p might be NULL
Definition: polys.h:67
#define pSetm(p)
Definition: polys.h:271
#define pLmEqual(p1, p2)
Definition: polys.h:111
#define pSetCoeff(p, n)
deletes old coeff before setting the new one
Definition: polys.h:31
void pNorm(poly p)
Definition: polys.h:362
#define ppMult_qq(p, q)
Definition: polys.h:208
void pWrite(poly p)
Definition: polys.h:308
#define pInit()
allocates a new monomial and initializes everything to 0
Definition: polys.h:61
#define pDivisibleBy(a, b)
returns TRUE, if leading monom of a divides leading monom of b i.e., if there exists a expvector c > ...
Definition: polys.h:138
#define pLmCmp(p, q)
returns 0|1|-1 if p=q|p>q|p<q w.r.t monomial ordering
Definition: polys.h:105
#define pMDivide(a, b)
Definition: polys.h:293
#define pCopy(p)
return a copy of the poly
Definition: polys.h:185
#define pOne()
Definition: polys.h:315
#define pLcm(a, b, m)
Definition: polys.h:295
#define pLmDivisibleByNoComp(a, b)
like pLmDivisibleBy, does not check components
Definition: polys.h:142
void PrintS(const char *s)
Definition: reporter.cc:284
static int sign(int x)
Definition: ring.cc:3427
ideal idInit(int idsize, int rank)
initialise an ideal / module
Definition: simpleideals.cc:35
#define IDELEMS(i)
Definition: simpleideals.h:23
int getTimer()
Definition: timer.cc:95
int initTimer()
Definition: timer.cc:67
void startTimer()
Definition: timer.cc:80