My Project
Loading...
Searching...
No Matches
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 "reporter/si_signals.h"
#include "kernel/oswrapper/vspace.h"
#include "Singular/cntrlc.h"
#include <sys/types.h>
#include <sys/wait.h>
#include <unistd.h>
#include "Singular/links/ssiLink.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 24 of file kverify.cc.

26{
28 kStrategy strat=new skStrategy;
29 strat->ak = id_RankFreeModule(F,currRing);
30 strat->kModW=kModW=NULL;
31 strat->kHomW=kHomW=NULL;
32 initBuchMoraCrit(strat); /*set Gebauer, honey, sugarCrit*/
33 initBuchMoraPos(strat);
34 initBba(strat);
35 initBuchMora(F, Q,strat);
36 /*initBuchMora:*/
37 strat->tail = pInit();
38 /*- set s -*/
39 strat->sl = -1;
40 /*- set L -*/
42 strat->Ll = -1;
43 strat->L = initL(strat->Lmax);
44 /*- set B -*/
45 strat->Bmax = setmaxL;
46 strat->Bl = -1;
47 strat->B = initL();
48 /*- set T -*/
49 strat->tl = -1;
50 strat->tmax = setmaxT;
51 strat->T = initT();
52 strat->R = initR();
53 strat->sevT = initsevT();
54 /*- init local data struct.---------------------------------------- -*/
55 strat->P.ecart=0;
56 strat->P.length=0;
57 strat->P.pLength=0;
58 initS(F, Q,strat); /*sets also S, ecartS, fromQ */
59 strat->fromT = FALSE;
60 strat->noTailReduction = FALSE;
61 /*----------------------------------------------------------------------*/
62 /* build pairs */
63 if (strat->fromQ!=NULL)
64 {
65 for(int i=1; i<=strat->sl;i++)
66 {
67 initenterpairs(strat->S[i],i-1,0,strat->fromQ[i],strat);
68 }
69 }
70 else
71 {
72 for(int i=1; i<=strat->sl;i++)
73 {
74 initenterpairs(strat->S[i],i-1,0,FALSE,strat);
75 }
76 }
77 if (TEST_OPT_PROT) printf("%d pairs created\n",strat->Ll+1);
78 if (TEST_OPT_DEBUG) messageSets(strat);
79 /*---------------------------------------------------------------------*/
80 BOOLEAN all_okay=TRUE;
81 for(int i=strat->Ll;i>=0; i--)
82 {
83 /* spolys */
84 int red_result=1;
85 /* picks the last element from the lazyset L */
86 strat->P = strat->L[i];
87 if (pNext(strat->P.p) == strat->tail)
88 {
89 // deletes the short spoly
90 pLmFree(strat->P.p);
91 strat->P.p = NULL;
92 poly m1 = NULL, m2 = NULL;
93 kCheckSpolyCreation(&(strat->P), strat, m1, m2);
94 ksCreateSpoly(&(strat->P), NULL, strat->use_buckets,
95 strat->tailRing, m1, m2, strat->R);
96 }
97 if ((strat->P.p == NULL) && (strat->P.t_p == NULL))
98 {
99 red_result = 0;
100 }
101 else
102 {
104 && (currRing->pFDeg(strat->P.p,currRing)>Kstd1_deg))
105 {
106 /*
107 * omit pair
108 * if 24 IN test and the degree of P is bigger then
109 *a predefined number Kstd1_deg
110 */
111 strat->P.Delete();
112 red_result=0;
113 if (TEST_OPT_PROT) { printf("D"); mflush(); }
114 }
115 else
116 {
117 int sl=strat->sl;
118 strat->P.GetP();
119 poly p=redNF(strat->P.p,sl,TRUE,strat);
120 if (p==NULL) red_result=0;
121 #ifdef KDEBUG
122 else
123 {
124 if (TEST_OPT_DEBUG)
125 {
126 printf("p: ");p_wrp(p,currRing, currRing); printf("\n");
127 }
128 }
129 #endif
130 }
131 }
132 if (red_result!=0)
133 {
134 if (TEST_OPT_PROT) printf("fail: %d, result: %d\n",i,red_result);
135 all_okay=FALSE;
136 }
137 }
138 return all_okay;
139}
int BOOLEAN
Definition auxiliary.h:88
#define TRUE
Definition auxiliary.h:101
#define FALSE
Definition auxiliary.h:97
int i
Definition cfEzgcd.cc:132
int p
Definition cfModGcd.cc:4086
intvec * kModW
Definition kutil.h:336
ring tailRing
Definition kutil.h:344
char noTailReduction
Definition kutil.h:377
int Ll
Definition kutil.h:352
TSet T
Definition kutil.h:327
int Bl
Definition kutil.h:353
polyset S
Definition kutil.h:307
LSet B
Definition kutil.h:329
int ak
Definition kutil.h:354
TObject ** R
Definition kutil.h:341
int tl
Definition kutil.h:351
unsigned long * sevT
Definition kutil.h:326
intvec * kHomW
Definition kutil.h:337
poly tail
Definition kutil.h:335
int tmax
Definition kutil.h:351
intset fromQ
Definition kutil.h:322
char use_buckets
Definition kutil.h:382
char fromT
Definition kutil.h:378
LObject P
Definition kutil.h:303
int Lmax
Definition kutil.h:352
LSet L
Definition kutil.h:328
int sl
Definition kutil.h:349
int Bmax
Definition kutil.h:353
KINLINE TSet initT()
Definition kInline.h:84
KINLINE TObject ** initR()
Definition kInline.h:95
KINLINE unsigned long * initsevT()
Definition kInline.h:100
void ksCreateSpoly(LObject *Pair, poly spNoether, int use_buckets, ring tailRing, poly m1, poly m2, TObject **R)
Definition kspoly.cc:1203
void initBba(kStrategy strat)
Definition kstd1.cc:1681
VAR intvec * kHomW
Definition kstd1.cc:2405
VAR intvec * kModW
Definition kstd1.cc:2405
EXTERN_VAR int Kstd1_deg
Definition kstd1.h:70
poly redNF(poly h, int &max_ind, int nonorm, kStrategy strat)
Definition kstd2.cc:2315
void initBuchMora(ideal F, ideal Q, kStrategy strat)
Definition kutil.cc:9751
void initBuchMoraPos(kStrategy strat)
Definition kutil.cc:9580
void initenterpairs(poly h, int k, int ecart, int isFromQ, kStrategy strat, int atR)
Definition kutil.cc:3816
void initS(ideal F, ideal Q, kStrategy strat)
Definition kutil.cc:7590
BOOLEAN kCheckSpolyCreation(LObject *L, kStrategy strat, poly &m1, poly &m2)
Definition kutil.cc:10481
void initBuchMoraCrit(kStrategy strat)
Definition kutil.cc:9435
void messageSets(kStrategy strat)
Definition kutil.cc:7540
#define setmaxL
Definition kutil.h:31
static LSet initL(int nr=setmaxL)
Definition kutil.h:419
#define setmaxT
Definition kutil.h:34
#define setmaxLinc
Definition kutil.h:32
#define assume(x)
Definition mod2.h:389
#define pNext(p)
Definition monomials.h:36
#define NULL
Definition omList.c:12
#define TEST_OPT_DEGBOUND
Definition options.h:115
#define TEST_OPT_PROT
Definition options.h:105
#define TEST_OPT_DEBUG
Definition options.h:110
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:71
#define pInit()
allocates a new monomial and initializes everything to 0
Definition polys.h:62
#define mflush()
Definition reporter.h:58
static BOOLEAN rIsNCRing(const ring r)
Definition ring.h:427
long id_RankFreeModule(ideal s, ring lmRing, ring tailRing)
return the maximal component number found in any polynomial in s
#define IDELEMS(i)
#define Q
Definition sirandom.c:26
skStrategy * kStrategy
Definition structs.h:54

◆ kVerify2()

BOOLEAN kVerify2 ( ideal F,
ideal Q )

Definition at line 141 of file kverify.cc.

143{
144#ifdef HAVE_VSPACE
146 kStrategy strat=new skStrategy;
147 strat->ak = id_RankFreeModule(F,currRing);
148 strat->kModW=kModW=NULL;
149 strat->kHomW=kHomW=NULL;
150 initBuchMoraCrit(strat); /*set Gebauer, honey, sugarCrit*/
151 initBuchMoraPos(strat);
152 initBba(strat);
153 initBuchMora(F, Q,strat);
154 /*initBuchMora:*/
155 strat->tail = pInit();
156 /*- set s -*/
157 strat->sl = -1;
158 /*- set L -*/
159 strat->Lmax = ((IDELEMS(F)+setmaxLinc-1)/setmaxLinc)*setmaxLinc;
160 strat->Ll = -1;
161 strat->L = initL(strat->Lmax);
162 /*- set B -*/
163 strat->Bmax = setmaxL;
164 strat->Bl = -1;
165 strat->B = initL();
166 /*- set T -*/
167 strat->tl = -1;
168 strat->tmax = setmaxT;
169 strat->T = initT();
170 strat->R = initR();
171 strat->sevT = initsevT();
172 /*- init local data struct.---------------------------------------- -*/
173 strat->P.ecart=0;
174 strat->P.length=0;
175 strat->P.pLength=0;
176 initS(F, Q,strat); /*sets also S, ecartS, fromQ */
177 strat->fromT = FALSE;
178 strat->noTailReduction = FALSE;
179 /*----------------------------------------------------------------------*/
180 /* build pairs */
181 if (strat->fromQ!=NULL)
182 {
183 for(int i=1; i<=strat->sl;i++)
184 {
185 initenterpairs(strat->S[i],i-1,0,strat->fromQ[i],strat);
186 }
187 }
188 else
189 {
190 for(int i=1; i<=strat->sl;i++)
191 {
192 initenterpairs(strat->S[i],i-1,0,FALSE,strat);
193 }
194 }
195 if (TEST_OPT_PROT) printf("%d pairs created\n",strat->Ll+1);
197 {
198 for(int i=strat->Ll; i>=0; i--)
199 {
200 if (currRing->pFDeg(strat->L[i].p,currRing)>Kstd1_deg)
201 {
202 /*
203 * omit pairs if 24 IN test and the degree of L[i] is bigger then
204 *a predefined number Kstd1_deg
205 */
206 deleteInL(strat->L,&strat->Ll,i,strat);
207 if (TEST_OPT_PROT) { printf("D"); mflush(); }
208 }
209 }
210 }
211 if (TEST_OPT_DEBUG) messageSets(strat);
212 /*---------------------------------------------------------------------*/
213 BOOLEAN all_okay=TRUE;
214 int cpus=(int)(long)feOptValue(FE_OPT_CPUS);
217 /* start no more than MAX_PROCESS-1 children */
218 if (cpus>strat->Ll) cpus=strat->Ll;
219 /* start no more children than elements in L */
220 int parent_pid=getpid();
221 using namespace vspace;
222 vmem_init();
223 // Create a queue of int
224 VRef<Queue<int> > queue = vnew<Queue<int> >();
225 VRef<Queue<int> > rqueue = vnew<Queue<int> >();
226 for(int i=strat->Ll;i>=0; i--)
227 {
228 queue->enqueue(i); // the tasks: process pair L[i]
229 }
230 for(int i=cpus*2;i>=0;i--)
231 {
232 queue->enqueue(-1); // stop sign, one for each child
233 }
234 int pid;
235 for (int i=0;i<cpus;i++)
236 {
237 pid = fork_process();
238 if (pid==0) break; //child
239 }
240 // input queue: queue: <index of L> -1 ...-1
241 // output queue: rqueue: pid .. pid 0 pid... pid for failure
242 // pid ... pid for success
243 if (parent_pid!=getpid()) // child ------------------------------------------
244 {
247 feSetOptValue(FE_OPT_CPUS,0);
248 loop
249 {
250 int ind=queue->dequeue();
251 if (ind== -1) // negative number as stop sign
252 {
253 if (TEST_OPT_PROT) printf("child: end of queue\n");
254 rqueue->enqueue(getpid()); // report pid of ending child
255 _exit(0);
256 }
257 int red_result=1;
258 /* picks the element from the lazyset L */
259 LObject P;
260 P = strat->L[ind];
261 if (TEST_OPT_PROT) { printf("."); mflush();}
262 if (pNext(P.p) == strat->tail)
263 {
264 // deletes the short spoly
265 pLmFree(P.p);
266 P.p = NULL;
267 poly m1 = NULL, m2 = NULL;
268 /* spoly */
269 kCheckSpolyCreation(&P, strat, m1, m2);
270 ksCreateSpoly(&P, NULL, strat->use_buckets,
271 strat->tailRing, m1, m2, strat->R);
272 }
273 if ((P.p == NULL) && (P.t_p == NULL))
274 {
275 red_result = 0;
276 }
277 else
278 {
279 /* reduction */
280 int sl=strat->sl;
281 P.GetP();
282 poly p=redNF(P.p,sl,TRUE,strat);
283 if (p==NULL) red_result=0;
284 #ifdef KDEBUG
285 else
286 {
287 if (TEST_OPT_DEBUG)
288 {
289 printf("p: ");p_wrp(p,currRing, currRing); printf("\n");
290 }
291 }
292 #endif
293 }
294 if (red_result!=0)
295 {
296 if (TEST_OPT_PROT) printf("fail: result: %d\n",red_result);
297 rqueue->enqueue(0);
298 rqueue->enqueue(getpid()); // pid of ending child
299 _exit(0); // found fail, no need to test further
300 }
301 }
302 // should never be reached:
303 rqueue->enqueue(getpid()); // stop sign
304 _exit(0); // all done, quit child
305 }
306 else // parent ---------------------------------------------------
307 {
308 if (TEST_OPT_PROT) printf("%d children created\n",cpus);
309 // wait for all process to stop:
310 // each process sends 0 for failure and its pid at end
311 // for success only the pid is send the end
312 int res;
313 int remaining_children=cpus;
314 while(remaining_children>0)
315 {
316 res=rqueue->dequeue();
317 if (res>0) // a child finished
318 {
319 if (TEST_OPT_PROT) { printf("c");mflush(); }
320 if (si_waitpid(res,NULL,WNOHANG)==0) // child not finished
321 {
322 if (kill(res,0)==0) // child is still running
323 {
324 struct timespec t;
325 struct timespec rem;
326 // wait till signal or 10s:
327 t.tv_sec=10;
328 t.tv_nsec=0;
329 nanosleep(&t, &rem); // should be interrupted by signal: SIG_CHLD
330 // child finished ?
331 if (si_waitpid(res,NULL,WNOHANG) ==0) //child not finished
332 {
333 kill(res,SIGTERM);
334 t.tv_sec=10;
335 t.tv_nsec=0;
336 nanosleep(&t, &rem); // should be interrupted by signal: SIG_CHLD
337 si_waitpid(res,NULL,WNOHANG);
338 }
339 }
340 }
341 remaining_children--;
342 }
343 else if (res==0) // not a GB - clean up and return 0
344 {
345 if (TEST_OPT_PROT) { printf("C"); mflush(); }
346 all_okay=FALSE;
347 // clean queue:
348 int dummy;
349 do
350 {
351 dummy=queue->dequeue(); // remove remaining tasks
352 } while (dummy>=0);
353 }
354 }
355 // removes queues
356 queue.free();
357 rqueue.free();
358 vmem_deinit();
359 return all_okay;
360 }
361#else
362 return kVerify1(F,Q);
363#endif
364}
si_hdl_typ si_set_signal(int sig, si_hdl_typ signal_handler)
meta function for binding a signal to an handler
Definition cntrlc.cc:121
void sig_term_hdl_child(int)
Definition cntrlc.cc:86
CanonicalForm res
Definition facAbsFact.cc:60
const char * feSetOptValue(feOptIndex opt, char *optarg)
Definition feOpt.cc:154
static void * feOptValue(feOptIndex opt)
Definition feOpt.h:40
void deleteInL(LSet set, int *length, int j, kStrategy strat)
Definition kutil.cc:1215
class sLObject LObject
Definition kutil.h:59
BOOLEAN kVerify1(ideal F, ideal Q)
Definition kverify.cc:24
void rem(unsigned long *a, unsigned long *q, unsigned long p, int &dega, int degq)
Definition minpoly.cc:572
static const int MAX_PROCESS
Definition vspace.h:1419
VRef< T > vnew()
Definition vspace.h:1872
pid_t fork_process()
Definition vspace.cc:1081
static void vmem_deinit()
Definition vspace.h:1742
static Status vmem_init()
Definition vspace.h:1738
#define loop
Definition structs.h:71
void free()
Definition vspace.h:1805