version 1.20, 2020/02/03 05:51:52 |
version 1.22, 2020/02/11 01:43:57 |
|
|
* DEVELOPER SHALL HAVE NO LIABILITY IN CONNECTION WITH THE USE, |
* DEVELOPER SHALL HAVE NO LIABILITY IN CONNECTION WITH THE USE, |
* PERFORMANCE OR NON-PERFORMANCE OF THE SOFTWARE. |
* 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.21 2020/02/05 04:56:10 noro Exp $ |
*/ |
*/ |
#include "ca.h" |
#include "ca.h" |
|
|
Line 2755 DPM dpm_sp_nf_asir(VECT psv,int i,int j,DPM *nf); |
|
Line 2755 DPM dpm_sp_nf_asir(VECT psv,int i,int j,DPM *nf); |
|
void dpm_sort(DPM p,DPM *r); |
void dpm_sort(DPM p,DPM *r); |
|
|
extern int DP_Multiple; |
extern int DP_Multiple; |
|
extern int DP_Print; |
|
|
void dpm_nf_z(NODE b,DPM g,VECT psv,int full,int multiple,DPM *rp); |
void dpm_nf_z(NODE b,DPM g,VECT psv,int full,int multiple,DPM *rp); |
NODE dpm_sort_list(NODE l); |
NODE dpm_sort_list(NODE l); |
Line 3039 int compdp_lex(DP *a,DP *b) |
|
Line 3040 int compdp_lex(DP *a,DP *b) |
|
return -cmpdl_lex(compdp_nv,BDY(*a)->dl,BDY(*b)->dl); |
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; |
LIST l; |
NODE nd,in,b0,b,n1,n2,n3,t; |
NODE nd,in,b0,b,n1,n2,n3,t; |
Line 3087 DMMstack_array dpm_schreyer_frame(NODE g) |
|
Line 3088 DMMstack_array dpm_schreyer_frame(NODE g) |
|
} |
} |
s = s1; |
s = s1; |
level++; |
level++; |
|
if ( DP_Print ) printf("level=%d,len=%d\n",level,n); |
|
|
|
|
/* create new list */ |
/* create new list */ |
MKVECT(psv,n+1); |
MKVECT(psv,n+1); |
ps = (DPM *)BDY(psv); |
ps = (DPM *)BDY(psv); |
Line 3122 DMMstack_array dpm_schreyer_frame(NODE g) |
|
Line 3123 DMMstack_array dpm_schreyer_frame(NODE g) |
|
} |
} |
if ( h ) m[p2] = h; |
if ( h ) m[p2] = h; |
} |
} |
#if 0 |
if ( lex ) { |
// compress m to m2 |
// compress m to m2 |
for ( j = 0, n2 = NEXT(n1); n2; n2 = NEXT(n2) ) { |
for ( j = 0, n2 = NEXT(n1); n2; n2 = NEXT(n2) ) { |
p2 = (long)BDY(n2); |
p2 = (long)BDY(n2); |
if ( m[p2] ) m2[j++] = m[p2]; |
if ( m[p2] ) m2[j++] = m[p2]; |
} |
} |
qsort(m2,j,sizeof(DP),(int (*)(const void *,const void *))compdp_lex); |
qsort(m2,j,sizeof(DP),(int (*)(const void *,const void *))compdp_lex); |
for ( k = 0; k < j; k++ ) { |
for ( k = 0; k < j; k++ ) { |
NEWDMM(dmm); dmm->dl = BDY(m2[k])->dl; dmm->pos = p1; dmm->c = (Obj)ONE; |
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); |
MKDPM(nv,dmm,dpm); |
NEXTNODE(b0,b); BDY(b) = (pointer)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 ) { |
if ( !b0 ) { |
Line 3606 DPM dpm_compress(DPM p,int *tab) |
|
Line 3607 DPM dpm_compress(DPM p,int *tab) |
|
} |
} |
|
|
// input : s, s = syz(m) output simplified s, m |
// 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) |
void dpm_simplify_syz(LIST s,LIST m,LIST *s1,LIST *m1,LIST *w1) |
{ |
{ |
int lm,ls,i,j,k,pos,nv; |
int lm,ls,i,j,k,pos,nv; |
Line 3628 void dpm_simplify_syz(LIST s,LIST m,LIST *s1,LIST *m1, |
|
Line 3630 void dpm_simplify_syz(LIST s,LIST m,LIST *s1,LIST *m1, |
|
p = as[i]; |
p = as[i]; |
if ( p == 0 ) continue; |
if ( p == 0 ) continue; |
nv = NV(p); |
nv = NV(p); |
for ( d = BDY(p); d; d = NEXT(d) ) { |
for ( d = BDY(p); d; ) { |
dd = d->dl->d; |
dd = d->dl->d; |
for ( k = 0; k < nv; k++ ) if ( dd[k] ) break; |
for ( k = 0; k < nv; k++ ) if ( dd[k] ) break; |
if ( k == nv ) break; |
if ( k == nv ) break; |
|
pos = d->pos; |
|
while ( d && d->pos == pos ) d = NEXT(d); |
} |
} |
if ( d ) { |
if ( d ) { |
c = d->c; pos = d->pos; |
c = d->c; pos = d->pos; |