=================================================================== RCS file: /home/cvs/OpenXM_contrib2/asir2018/engine/dist.c,v retrieving revision 1.20 retrieving revision 1.25 diff -u -p -r1.20 -r1.25 --- OpenXM_contrib2/asir2018/engine/dist.c 2020/02/03 05:51:52 1.20 +++ OpenXM_contrib2/asir2018/engine/dist.c 2021/01/11 08:37:44 1.25 @@ -45,7 +45,7 @@ * DEVELOPER SHALL HAVE NO LIABILITY IN CONNECTION WITH THE USE, * PERFORMANCE OR NON-PERFORMANCE OF THE SOFTWARE. * - * $OpenXM: OpenXM_contrib2/asir2018/engine/dist.c,v 1.19 2019/12/27 08:13:59 noro Exp $ + * $OpenXM: OpenXM_contrib2/asir2018/engine/dist.c,v 1.24 2020/10/06 06:31:19 noro Exp $ */ #include "ca.h" @@ -582,6 +582,16 @@ void _adddl(int n,DL d1,DL d2,DL d3) d3->d[i] = d1->d[i]+d2->d[i]; } +void _subdl(int n,DL d1,DL d2,DL d3) +{ + int i; + + d3->td = d1->td-d2->td; + for ( i = 0; i < n; i++ ) + d3->d[i] = d1->d[i]-d2->d[i]; +} + + void _addtodl(int n,DL d1,DL d2) { int i; @@ -591,6 +601,15 @@ void _addtodl(int n,DL d1,DL d2) d2->d[i] += d1->d[i]; } +void _subfromdl(int n,DL d1,DL d2) +{ + int i; + + d2->td -= d1->td; + for ( i = 0; i < n; i++ ) + d2->d[i] -= d1->d[i]; +} + void _copydl(int n,DL d1,DL d2) { int i; @@ -2755,6 +2774,7 @@ DPM dpm_sp_nf_asir(VECT psv,int i,int j,DPM *nf); void dpm_sort(DPM p,DPM *r); extern int DP_Multiple; +extern int DP_Print; void dpm_nf_z(NODE b,DPM g,VECT psv,int full,int multiple,DPM *rp); NODE dpm_sort_list(NODE l); @@ -3039,7 +3059,7 @@ int compdp_lex(DP *a,DP *b) return -cmpdl_lex(compdp_nv,BDY(*a)->dl,BDY(*b)->dl); } -DMMstack_array dpm_schreyer_frame(NODE g) +DMMstack_array dpm_schreyer_frame(NODE g,int lex) { LIST l; NODE nd,in,b0,b,n1,n2,n3,t; @@ -3087,8 +3107,8 @@ DMMstack_array dpm_schreyer_frame(NODE g) } s = s1; level++; + if ( DP_Print ) printf("level=%d,len=%d\n",level,n); - /* create new list */ MKVECT(psv,n+1); ps = (DPM *)BDY(psv); @@ -3122,28 +3142,28 @@ DMMstack_array dpm_schreyer_frame(NODE g) } if ( h ) m[p2] = h; } -#if 0 - // compress m to m2 - for ( j = 0, n2 = NEXT(n1); n2; n2 = NEXT(n2) ) { - p2 = (long)BDY(n2); - if ( m[p2] ) m2[j++] = m[p2]; - } - qsort(m2,j,sizeof(DP),(int (*)(const void *,const void *))compdp_lex); - for ( k = 0; k < j; k++ ) { - NEWDMM(dmm); dmm->dl = BDY(m2[k])->dl; dmm->pos = p1; dmm->c = (Obj)ONE; - MKDPM(nv,dmm,dpm); - NEXTNODE(b0,b); BDY(b) = (pointer)dpm; - } -#else - for ( n2 = NEXT(n1); n2; n2 = NEXT(n2) ) { - p2 = (long)BDY(n2); - if ( m[p2] ) { - NEWDMM(dmm); dmm->dl = BDY(m[p2])->dl; dmm->pos = p1; dmm->c = (Obj)ONE; + if ( lex ) { + // compress m to m2 + for ( j = 0, n2 = NEXT(n1); n2; n2 = NEXT(n2) ) { + p2 = (long)BDY(n2); + if ( m[p2] ) m2[j++] = m[p2]; + } + qsort(m2,j,sizeof(DP),(int (*)(const void *,const void *))compdp_lex); + for ( k = 0; k < j; k++ ) { + NEWDMM(dmm); dmm->dl = BDY(m2[k])->dl; dmm->pos = p1; dmm->c = (Obj)ONE; MKDPM(nv,dmm,dpm); NEXTNODE(b0,b); BDY(b) = (pointer)dpm; } + } else { + for ( n2 = NEXT(n1); n2; n2 = NEXT(n2) ) { + p2 = (long)BDY(n2); + if ( m[p2] ) { + NEWDMM(dmm); dmm->dl = BDY(m[p2])->dl; dmm->pos = p1; dmm->c = (Obj)ONE; + MKDPM(nv,dmm,dpm); + NEXTNODE(b0,b); BDY(b) = (pointer)dpm; + } + } } -#endif } } if ( !b0 ) { @@ -3210,6 +3230,8 @@ int compdmm_schreyer(int n,DMM m1,DMM m2) else return 0; } } + /* XXX */ + return 0; } int compdmm_schreyer_old(int n,DMM m1,DMM m2) @@ -3292,6 +3314,7 @@ int compdmm(int n,DMM m1,DMM m2) else return (*cmpdl)(n,m1->dl,m2->dl); default: error("compdmm : invalid dpm_ordtype"); + return 0; } } @@ -3606,6 +3629,7 @@ DPM dpm_compress(DPM p,int *tab) } // input : s, s = syz(m) output simplified s, m +// assuming the term order is POT void dpm_simplify_syz(LIST s,LIST m,LIST *s1,LIST *m1,LIST *w1) { int lm,ls,i,j,k,pos,nv; @@ -3628,10 +3652,12 @@ void dpm_simplify_syz(LIST s,LIST m,LIST *s1,LIST *m1, p = as[i]; if ( p == 0 ) continue; nv = NV(p); - for ( d = BDY(p); d; d = NEXT(d) ) { + for ( d = BDY(p); d; ) { dd = d->dl->d; for ( k = 0; k < nv; k++ ) if ( dd[k] ) break; if ( k == nv ) break; + pos = d->pos; + while ( d && d->pos == pos ) d = NEXT(d); } if ( d ) { c = d->c; pos = d->pos;