My Project
Functions
kverify.cc File Reference
#include "kernel/mod2.h"
#include "misc/mylimits.h"
#include "misc/options.h"
#include "kernel/ideals.h"
#include "kernel/polys.h"
#include "polys/monomials/ring.h"
#include "kernel/GBEngine/kutil.h"
#include "kernel/GBEngine/kverify.h"
#include "Singular/feOpt.h"
#include <stdlib.h>
#include <string.h>
#include "kernel/oswrapper/vspace.h"
#include <sys/types.h>
#include <sys/wait.h>
#include <unistd.h>

Go to the source code of this file.

Functions

BOOLEAN kVerify1 (ideal F, ideal Q)
 
BOOLEAN kVerify2 (ideal F, ideal Q)
 

Function Documentation

◆ kVerify1()

BOOLEAN kVerify1 ( ideal  F,
ideal  Q 
)

Definition at line 21 of file kverify.cc.

23 {
25  kStrategy strat=new skStrategy;
26  strat->ak = id_RankFreeModule(F,currRing);
27  strat->kModW=kModW=NULL;
28  strat->kHomW=kHomW=NULL;
29  initBuchMoraCrit(strat); /*set Gebauer, honey, sugarCrit*/
30  initBuchMoraPos(strat);
31  initBba(strat);
32  initBuchMora(F, Q,strat);
33  /*initBuchMora:*/
34  strat->tail = pInit();
35  /*- set s -*/
36  strat->sl = -1;
37  /*- set L -*/
38  strat->Lmax = ((IDELEMS(F)+setmaxLinc-1)/setmaxLinc)*setmaxLinc;
39  strat->Ll = -1;
40  strat->L = initL(strat->Lmax);
41  /*- set B -*/
42  strat->Bmax = setmaxL;
43  strat->Bl = -1;
44  strat->B = initL();
45  /*- set T -*/
46  strat->tl = -1;
47  strat->tmax = setmaxT;
48  strat->T = initT();
49  strat->R = initR();
50  strat->sevT = initsevT();
51  /*- init local data struct.---------------------------------------- -*/
52  strat->P.ecart=0;
53  strat->P.length=0;
54  strat->P.pLength=0;
55  initS(F, Q,strat); /*sets also S, ecartS, fromQ */
56  strat->fromT = FALSE;
57  strat->noTailReduction = FALSE;
58  /*----------------------------------------------------------------------*/
59  /* build pairs */
60  if (strat->fromQ!=NULL)
61  {
62  for(int i=1; i<=strat->sl;i++)
63  {
64  initenterpairs(strat->S[i],i-1,0,strat->fromQ[i],strat);
65  }
66  }
67  else
68  {
69  for(int i=1; i<=strat->sl;i++)
70  {
71  initenterpairs(strat->S[i],i-1,0,FALSE,strat);
72  }
73  }
74  if (TEST_OPT_PROT) printf("%d pairs created\n",strat->Ll+1);
75  if (TEST_OPT_DEBUG) messageSets(strat);
76  /*---------------------------------------------------------------------*/
77  BOOLEAN all_okay=TRUE;
78  for(int i=strat->Ll;i>=0; i--)
79  {
80  /* spolys */
81  int red_result=1;
82  /* picks the last element from the lazyset L */
83  strat->P = strat->L[i];
84  if (pNext(strat->P.p) == strat->tail)
85  {
86  // deletes the short spoly
87  pLmFree(strat->P.p);
88  strat->P.p = NULL;
89  poly m1 = NULL, m2 = NULL;
90  kCheckSpolyCreation(&(strat->P), strat, m1, m2);
91  ksCreateSpoly(&(strat->P), NULL, strat->use_buckets,
92  strat->tailRing, m1, m2, strat->R);
93  }
94  if ((strat->P.p == NULL) && (strat->P.t_p == NULL))
95  {
96  red_result = 0;
97  }
98  else
99  {
101  && (currRing->pFDeg(strat->P.p,currRing)>Kstd1_deg))
102  {
103  /*
104  * omit pair
105  * if 24 IN test and the degree of P is bigger then
106  *a predefined number Kstd1_deg
107  */
108  strat->P.Delete();
109  red_result=0;
110  if (TEST_OPT_PROT) { printf("D"); mflush(); }
111  }
112  else
113  {
114  int sl=strat->sl;
115  strat->P.GetP();
116  poly p=redNF(strat->P.p,sl,TRUE,strat);
117  if (p==NULL) red_result=0;
118  #ifdef KDEBUG
119  else
120  {
121  if (TEST_OPT_DEBUG)
122  {
123  printf("p: ");p_wrp(p,currRing, currRing); printf("\n");
124  }
125  }
126  #endif
127  }
128  }
129  if (red_result!=0)
130  {
131  if (TEST_OPT_PROT) printf("fail: %d, result: %d\n",i,red_result);
132  all_okay=FALSE;
133  }
134  }
135  return all_okay;
136 }
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
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 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
#define assume(x)
Definition: mod2.h:387
#define pNext(p)
Definition: monomials.h:36
#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
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

◆ kVerify2()

BOOLEAN kVerify2 ( ideal  F,
ideal  Q 
)

Definition at line 138 of file kverify.cc.

140 {
141 #ifdef HAVE_VSPACE
143  kStrategy strat=new skStrategy;
144  strat->ak = id_RankFreeModule(F,currRing);
145  strat->kModW=kModW=NULL;
146  strat->kHomW=kHomW=NULL;
147  initBuchMoraCrit(strat); /*set Gebauer, honey, sugarCrit*/
148  initBuchMoraPos(strat);
149  initBba(strat);
150  initBuchMora(F, Q,strat);
151  /*initBuchMora:*/
152  strat->tail = pInit();
153  /*- set s -*/
154  strat->sl = -1;
155  /*- set L -*/
156  strat->Lmax = ((IDELEMS(F)+setmaxLinc-1)/setmaxLinc)*setmaxLinc;
157  strat->Ll = -1;
158  strat->L = initL(strat->Lmax);
159  /*- set B -*/
160  strat->Bmax = setmaxL;
161  strat->Bl = -1;
162  strat->B = initL();
163  /*- set T -*/
164  strat->tl = -1;
165  strat->tmax = setmaxT;
166  strat->T = initT();
167  strat->R = initR();
168  strat->sevT = initsevT();
169  /*- init local data struct.---------------------------------------- -*/
170  strat->P.ecart=0;
171  strat->P.length=0;
172  strat->P.pLength=0;
173  initS(F, Q,strat); /*sets also S, ecartS, fromQ */
174  strat->fromT = FALSE;
175  strat->noTailReduction = FALSE;
176  /*----------------------------------------------------------------------*/
177  /* build pairs */
178  if (strat->fromQ!=NULL)
179  {
180  for(int i=1; i<=strat->sl;i++)
181  {
182  initenterpairs(strat->S[i],i-1,0,strat->fromQ[i],strat);
183  }
184  }
185  else
186  {
187  for(int i=1; i<=strat->sl;i++)
188  {
189  initenterpairs(strat->S[i],i-1,0,FALSE,strat);
190  }
191  }
192  if (TEST_OPT_PROT) printf("%d pairs created\n",strat->Ll+1);
193  if (TEST_OPT_DEGBOUND)
194  {
195  for(int i=strat->Ll; i>=0; i--)
196  {
197  if (currRing->pFDeg(strat->L[i].p,currRing)>Kstd1_deg)
198  {
199  /*
200  * omit pairs if 24 IN test and the degree of L[i] is bigger then
201  *a predefined number Kstd1_deg
202  */
203  deleteInL(strat->L,&strat->Ll,i,strat);
204  if (TEST_OPT_PROT) { printf("D"); mflush(); }
205  }
206  }
207  }
208  if (TEST_OPT_DEBUG) messageSets(strat);
209  /*---------------------------------------------------------------------*/
210  BOOLEAN all_okay=TRUE;
211  int cpus=(int)(long)feOptValue(FE_OPT_CPUS);
214  /* start no more than MAX_PROCESS-1 children */
215  int parent_pid=getpid();
216  using namespace vspace;
217  vmem_init();
218  // Create a queue of int
219  VRef<Queue<int> > queue = vnew<Queue<int> >();
220  VRef<Queue<int> > rqueue = vnew<Queue<int> >();
221  for(int i=strat->Ll;i>=0; i--)
222  {
223  queue->enqueue(i); // the tasks: process pair L[i]
224  }
225  for(int i=cpus;i>=0;i--)
226  {
227  queue->enqueue(-1); // stop sign, one for each child
228  }
229  int pid;
230  for (int i=0;i<cpus;i++)
231  {
232  pid = fork_process();
233  if (pid==0) break; //child
234  }
235  if (parent_pid!=getpid()) // child ------------------------------------------
236  {
237  loop
238  {
239  int ind=queue->dequeue();
240  if (ind== -1)
241  {
242  if (TEST_OPT_PROT) printf("child: end of queue\n");
243  rqueue->enqueue(0);
244  exit(0);
245  }
246  int red_result=1;
247  /* picks the element from the lazyset L */
248  LObject P;
249  P = strat->L[ind];
250  if (TEST_OPT_PROT) { printf("."); mflush();}
251  if (pNext(P.p) == strat->tail)
252  {
253  // deletes the short spoly
254  pLmFree(P.p);
255  P.p = NULL;
256  poly m1 = NULL, m2 = NULL;
257  /* spoly */
258  kCheckSpolyCreation(&P, strat, m1, m2);
259  ksCreateSpoly(&P, NULL, strat->use_buckets,
260  strat->tailRing, m1, m2, strat->R);
261  }
262  if ((P.p == NULL) && (P.t_p == NULL))
263  {
264  red_result = 0;
265  }
266  else
267  {
268  /* reduction */
269  int sl=strat->sl;
270  P.GetP();
271  poly p=redNF(P.p,sl,TRUE,strat);
272  if (p==NULL) red_result=0;
273  #ifdef KDEBUG
274  else
275  {
276  if (TEST_OPT_DEBUG)
277  {
278  printf("p: ");p_wrp(p,currRing, currRing); printf("\n");
279  }
280  }
281  #endif
282  }
283  if (red_result!=0)
284  {
285  if (TEST_OPT_PROT) printf("fail: result: %d\n",red_result);
286  rqueue->enqueue(1);
287  exit(0); // found fail, no need to test further
288  }
289  }
290  exit(0); // all done, quit child
291  }
292  else // parent ---------------------------------------------------
293  {
294  if (TEST_OPT_PROT) printf("%d children created\n",cpus);
295  // wait for all process to stop:
296  // each process sends an 0 at end or a 1 for failure
297  int res;
298  int remaining_children=cpus;
299  while(remaining_children>0)
300  {
301  res=rqueue->dequeue();
302  if (res==0) // a child finished
303  {
304  if (TEST_OPT_PROT) { printf("c");mflush(); }
305  //waitpid(-1,NULL,0); // ? see sig_chld_hdl
306  remaining_children--;
307  }
308  else if (res==1) // not a GB - clean up and return 0
309  {
310  if (TEST_OPT_PROT) { printf("C"); mflush(); }
311  remaining_children--;
312  all_okay=FALSE;
313  // clean queue:
314  int dummy;
315  do
316  {
317  dummy=queue->dequeue(); // remove remaining tasks
318  } while (dummy==0);
319  }
320  }
321  // removes queues
322  queue.free();
323  rqueue.free();
324  vmem_deinit();
325  return all_okay;
326  }
327 #else
328  return kVerify1(F,Q);
329 #endif
330 }
CanonicalForm res
Definition: facAbsFact.cc:60
static void * feOptValue(feOptIndex opt)
Definition: feOpt.h:40
void deleteInL(LSet set, int *length, int j, kStrategy strat)
Definition: kutil.cc:1295
class sLObject LObject
Definition: kutil.h:58
BOOLEAN kVerify1(ideal F, ideal Q)
Definition: kverify.cc:21
static const int MAX_PROCESS
Definition: vspace.h:1419
pid_t fork_process()
Definition: vspace.cc:976
static void vmem_deinit()
Definition: vspace.h:1742
static Status vmem_init()
Definition: vspace.h:1738
#define loop
Definition: structs.h:75
void free()
Definition: vspace.h:1805