My Project
kverify.cc
Go to the documentation of this file.
1 #include "kernel/mod2.h"
2 
3 #include "misc/mylimits.h"
4 #include "misc/options.h"
5 #include "kernel/ideals.h"
6 #include "kernel/polys.h"
7 #include "polys/monomials/ring.h"
10 #include "Singular/feOpt.h"
11 #include <stdlib.h>
12 #include <string.h>
13 
14 #ifdef HAVE_VSPACE
16 #include <sys/types.h>
17 #include <sys/wait.h>
18 #include <unistd.h>
19 #endif
20 
21 BOOLEAN kVerify1(ideal F, ideal Q)
22 {
24  kStrategy strat=new skStrategy;
25  strat->ak = id_RankFreeModule(F,currRing);
26  strat->kModW=kModW=NULL;
27  strat->kHomW=kHomW=NULL;
28  initBuchMoraCrit(strat); /*set Gebauer, honey, sugarCrit*/
29  initBuchMoraPos(strat);
30  initBba(strat);
31  initBuchMora(F, Q,strat);
32  /*initBuchMora:*/
33  strat->tail = pInit();
34  /*- set s -*/
35  strat->sl = -1;
36  /*- set L -*/
37  strat->Lmax = ((IDELEMS(F)+setmaxLinc-1)/setmaxLinc)*setmaxLinc;
38  strat->Ll = -1;
39  strat->L = initL(strat->Lmax);
40  /*- set B -*/
41  strat->Bmax = setmaxL;
42  strat->Bl = -1;
43  strat->B = initL();
44  /*- set T -*/
45  strat->tl = -1;
46  strat->tmax = setmaxT;
47  strat->T = initT();
48  strat->R = initR();
49  strat->sevT = initsevT();
50  /*- init local data struct.---------------------------------------- -*/
51  strat->P.ecart=0;
52  strat->P.length=0;
53  strat->P.pLength=0;
54  initS(F, Q,strat); /*sets also S, ecartS, fromQ */
55  strat->fromT = FALSE;
56  strat->noTailReduction = FALSE;
57  /*----------------------------------------------------------------------*/
58  /* build pairs */
59  if (strat->fromQ!=NULL)
60  {
61  for(int i=1; i<=strat->sl;i++)
62  {
63  initenterpairs(strat->S[i],i-1,0,strat->fromQ[i],strat);
64  }
65  }
66  else
67  {
68  for(int i=1; i<=strat->sl;i++)
69  {
70  initenterpairs(strat->S[i],i-1,0,FALSE,strat);
71  }
72  }
73  if (TEST_OPT_PROT) printf("%d pairs created\n",strat->Ll+1);
74  if (TEST_OPT_DEBUG) messageSets(strat);
75  /*---------------------------------------------------------------------*/
76  BOOLEAN all_okay=TRUE;
77  for(int i=strat->Ll;i>=0; i--)
78  {
79  /* spolys */
80  int red_result=1;
81  /* picks the last element from the lazyset L */
82  strat->P = strat->L[i];
83  if (pNext(strat->P.p) == strat->tail)
84  {
85  // deletes the short spoly
86  pLmFree(strat->P.p);
87  strat->P.p = NULL;
88  poly m1 = NULL, m2 = NULL;
89  kCheckSpolyCreation(&(strat->P), strat, m1, m2);
90  ksCreateSpoly(&(strat->P), NULL, strat->use_buckets,
91  strat->tailRing, m1, m2, strat->R);
92  }
93  if ((strat->P.p == NULL) && (strat->P.t_p == NULL))
94  {
95  red_result = 0;
96  }
97  else
98  {
100  && (currRing->pFDeg(strat->P.p,currRing)>Kstd1_deg))
101  {
102  /*
103  * omit pair
104  * if 24 IN test and the degree of P is bigger then
105  *a predefined number Kstd1_deg
106  */
107  strat->P.Delete();
108  red_result=0;
109  if (TEST_OPT_PROT) { printf("D"); mflush(); }
110  }
111  else
112  {
113  int sl=strat->sl;
114  strat->P.GetP();
115  poly p=redNF(strat->P.p,sl,TRUE,strat);
116  if (p==NULL) red_result=0;
117  #ifdef KDEBUG
118  else
119  {
120  if (TEST_OPT_DEBUG)
121  {
122  printf("p: ");p_wrp(p,currRing, currRing); printf("\n");
123  }
124  }
125  #endif
126  }
127  }
128  if (red_result!=0)
129  {
130  if (TEST_OPT_PROT) printf("fail: %d, result: %d\n",i,red_result);
131  all_okay=FALSE;
132  }
133  }
134  return all_okay;
135 }
136 
137 BOOLEAN kVerify2(ideal F, ideal Q)
138 {
139 #ifdef HAVE_VSPACE
141  kStrategy strat=new skStrategy;
142  strat->ak = id_RankFreeModule(F,currRing);
143  strat->kModW=kModW=NULL;
144  strat->kHomW=kHomW=NULL;
145  initBuchMoraCrit(strat); /*set Gebauer, honey, sugarCrit*/
146  initBuchMoraPos(strat);
147  initBba(strat);
148  initBuchMora(F, Q,strat);
149  /*initBuchMora:*/
150  strat->tail = pInit();
151  /*- set s -*/
152  strat->sl = -1;
153  /*- set L -*/
154  strat->Lmax = ((IDELEMS(F)+setmaxLinc-1)/setmaxLinc)*setmaxLinc;
155  strat->Ll = -1;
156  strat->L = initL(strat->Lmax);
157  /*- set B -*/
158  strat->Bmax = setmaxL;
159  strat->Bl = -1;
160  strat->B = initL();
161  /*- set T -*/
162  strat->tl = -1;
163  strat->tmax = setmaxT;
164  strat->T = initT();
165  strat->R = initR();
166  strat->sevT = initsevT();
167  /*- init local data struct.---------------------------------------- -*/
168  strat->P.ecart=0;
169  strat->P.length=0;
170  strat->P.pLength=0;
171  initS(F, Q,strat); /*sets also S, ecartS, fromQ */
172  strat->fromT = FALSE;
173  strat->noTailReduction = FALSE;
174  /*----------------------------------------------------------------------*/
175  /* build pairs */
176  if (strat->fromQ!=NULL)
177  {
178  for(int i=1; i<=strat->sl;i++)
179  {
180  initenterpairs(strat->S[i],i-1,0,strat->fromQ[i],strat);
181  }
182  }
183  else
184  {
185  for(int i=1; i<=strat->sl;i++)
186  {
187  initenterpairs(strat->S[i],i-1,0,FALSE,strat);
188  }
189  }
190  if (TEST_OPT_PROT) printf("%d pairs created\n",strat->Ll+1);
191  if (TEST_OPT_DEGBOUND)
192  {
193  for(int i=strat->Ll; i>=0; i--)
194  {
195  if (currRing->pFDeg(strat->L[i].p,currRing)>Kstd1_deg)
196  {
197  /*
198  * omit pairs if 24 IN test and the degree of L[i] is bigger then
199  *a predefined number Kstd1_deg
200  */
201  deleteInL(strat->L,&strat->Ll,i,strat);
202  if (TEST_OPT_PROT) { printf("D"); mflush(); }
203  }
204  }
205  }
206  if (TEST_OPT_DEBUG) messageSets(strat);
207  /*---------------------------------------------------------------------*/
208  BOOLEAN all_okay=TRUE;
209  int cpus=(int)(long)feOptValue(FE_OPT_CPUS);
210  int parent_pid=getpid();
211  using namespace vspace;
212  vmem_init();
213  // Create a queue of int
214  VRef<Queue<int> > queue = vnew<Queue<int> >();
215  VRef<Queue<int> > rqueue = vnew<Queue<int> >();
216  for(int i=strat->Ll;i>=0; i--)
217  {
218  queue->enqueue(i); // the tasks: process pair L[i]
219  }
220  for(int i=cpus;i>=0;i--)
221  {
222  queue->enqueue(-1); // stop sign, one for each child
223  }
224  int pid;
225  for (int i=0;i<cpus;i++)
226  {
227  pid = fork_process();
228  if (pid==0) break; //child
229  }
230  if (parent_pid!=getpid()) // child ------------------------------------------
231  {
232  loop
233  {
234  int ind=queue->dequeue();
235  if (ind== -1)
236  {
237  if (TEST_OPT_PROT) printf("child: end of queue\n");
238  rqueue->enqueue(0);
239  exit(0);
240  }
241  int red_result=1;
242  /* picks the element from the lazyset L */
243  LObject P;
244  P = strat->L[ind];
245  if (TEST_OPT_PROT) { printf("."); mflush();}
246  if (pNext(P.p) == strat->tail)
247  {
248  // deletes the short spoly
249  pLmFree(P.p);
250  P.p = NULL;
251  poly m1 = NULL, m2 = NULL;
252  /* spoly */
253  kCheckSpolyCreation(&P, strat, m1, m2);
254  ksCreateSpoly(&P, NULL, strat->use_buckets,
255  strat->tailRing, m1, m2, strat->R);
256  }
257  if ((P.p == NULL) && (P.t_p == NULL))
258  {
259  red_result = 0;
260  }
261  else
262  {
263  /* reduction */
264  int sl=strat->sl;
265  P.GetP();
266  poly p=redNF(P.p,sl,TRUE,strat);
267  if (p==NULL) red_result=0;
268  #ifdef KDEBUG
269  else
270  {
271  if (TEST_OPT_DEBUG)
272  {
273  printf("p: ");p_wrp(p,currRing, currRing); printf("\n");
274  }
275  }
276  #endif
277  }
278  if (red_result!=0)
279  {
280  if (TEST_OPT_PROT) printf("fail: result: %d\n",red_result);
281  rqueue->enqueue(1);
282  exit(0); // found fail, no neeed to test further
283  }
284  }
285  exit(0); // all done, quit child
286  }
287  else // parent ---------------------------------------------------
288  {
289  if (TEST_OPT_PROT) printf("%d children created\n",cpus);
290  // wait for all process to stop:
291  // each process sends an 0 at end or a 1 for failure
292  int res;
293  int remaining_children=cpus;
294  while(remaining_children>0)
295  {
296  res=rqueue->dequeue();
297  if (res==0) // a child finished
298  {
299  if (TEST_OPT_PROT) { printf("c");mflush(); }
300  //waitpid(-1,NULL,0); // ? see sig_chld_hdl
301  remaining_children--;
302  }
303  else if (res==1) // not a GB - clean up and return 0
304  {
305  if (TEST_OPT_PROT) { printf("C"); mflush(); }
306  remaining_children--;
307  all_okay=FALSE;
308  // clean queue:
309  int dummy;
310  do
311  {
312  dummy=queue->dequeue();
313  } while (dummy==0);
314  }
315  }
316  // removes queues
317  queue.free();
318  rqueue.free();
319  vmem_deinit();
320  return all_okay;
321  }
322 #else
323  return kVerify1(F,Q);
324 #endif
325 }
int BOOLEAN
Definition: auxiliary.h:87
#define TRUE
Definition: auxiliary.h:100
#define FALSE
Definition: auxiliary.h:96
int i
Definition: cfEzgcd.cc:132
int p
Definition: cfModGcd.cc:4078
intvec * kModW
Definition: kutil.h:335
ring tailRing
Definition: kutil.h:343
char noTailReduction
Definition: kutil.h:378
int Ll
Definition: kutil.h:351
TSet T
Definition: kutil.h:326
int Bl
Definition: kutil.h:352
polyset S
Definition: kutil.h:306
LSet B
Definition: kutil.h:328
int ak
Definition: kutil.h:353
TObject ** R
Definition: kutil.h:340
int tl
Definition: kutil.h:350
unsigned long * sevT
Definition: kutil.h:325
intvec * kHomW
Definition: kutil.h:336
poly tail
Definition: kutil.h:334
int tmax
Definition: kutil.h:350
intset fromQ
Definition: kutil.h:321
char use_buckets
Definition: kutil.h:383
char fromT
Definition: kutil.h:379
LObject P
Definition: kutil.h:302
int Lmax
Definition: kutil.h:351
LSet L
Definition: kutil.h:327
int sl
Definition: kutil.h:348
int Bmax
Definition: kutil.h:352
CanonicalForm res
Definition: facAbsFact.cc:60
static void * feOptValue(feOptIndex opt)
Definition: feOpt.h:40
STATIC_VAR jList * Q
Definition: janet.cc:30
KINLINE unsigned long * initsevT()
Definition: kInline.h:100
KINLINE TSet initT()
Definition: kInline.h:84
KINLINE TObject ** initR()
Definition: kInline.h:95
void ksCreateSpoly(LObject *Pair, poly spNoether, int use_buckets, ring tailRing, poly m1, poly m2, TObject **R)
Definition: kspoly.cc:1185
void initBba(kStrategy strat)
Definition: kstd1.cc:1676
VAR intvec * kHomW
Definition: kstd1.cc:2408
VAR intvec * kModW
Definition: kstd1.cc:2408
EXTERN_VAR int Kstd1_deg
Definition: kstd1.h:49
poly redNF(poly h, int &max_ind, int nonorm, kStrategy strat)
Definition: kstd2.cc:2135
void initBuchMora(ideal F, ideal Q, kStrategy strat)
Definition: kutil.cc:10057
void initBuchMoraPos(kStrategy strat)
Definition: kutil.cc:9884
void initenterpairs(poly h, int k, int ecart, int isFromQ, kStrategy strat, int atR)
Definition: kutil.cc:3902
void initS(ideal F, ideal Q, kStrategy strat)
Definition: kutil.cc:7891
BOOLEAN kCheckSpolyCreation(LObject *L, kStrategy strat, poly &m1, poly &m2)
Definition: kutil.cc:10791
void deleteInL(LSet set, int *length, int j, kStrategy strat)
Definition: kutil.cc:1295
void initBuchMoraCrit(kStrategy strat)
Definition: kutil.cc:9732
void messageSets(kStrategy strat)
Definition: kutil.cc:7841
#define setmaxL
Definition: kutil.h:30
static LSet initL(int nr=setmaxL)
Definition: kutil.h:421
#define setmaxT
Definition: kutil.h:33
#define setmaxLinc
Definition: kutil.h:31
class sLObject LObject
Definition: kutil.h:58
BOOLEAN kVerify2(ideal F, ideal Q)
Definition: kverify.cc:137
BOOLEAN kVerify1(ideal F, ideal Q)
Definition: kverify.cc:21
#define assume(x)
Definition: mod2.h:387
#define pNext(p)
Definition: monomials.h:36
pid_t fork_process()
Definition: vspace.cc:977
static void vmem_deinit()
Definition: vspace.h:1742
static Status vmem_init()
Definition: vspace.h:1738
#define NULL
Definition: omList.c:12
#define TEST_OPT_DEGBOUND
Definition: options.h:113
#define TEST_OPT_PROT
Definition: options.h:103
#define TEST_OPT_DEBUG
Definition: options.h:108
void p_wrp(poly p, ring lmRing, ring tailRing)
Definition: polys0.cc:373
VAR ring currRing
Widely used global variable which specifies the current polynomial ring for Singular interpreter and ...
Definition: polys.cc:13
Compatiblity layer for legacy polynomial operations (over currRing)
static void pLmFree(poly p)
frees the space of the monomial m, assumes m != NULL coef is not freed, m is not advanced
Definition: polys.h:70
#define pInit()
allocates a new monomial and initializes everything to 0
Definition: polys.h:61
#define mflush()
Definition: reporter.h:58
static BOOLEAN rIsNCRing(const ring r)
Definition: ring.h:421
long id_RankFreeModule(ideal s, ring lmRing, ring tailRing)
return the maximal component number found in any polynomial in s
#define IDELEMS(i)
Definition: simpleideals.h:23
#define loop
Definition: structs.h:75
void free()
Definition: vspace.h:1805