version 1.19, 2019/12/27 08:13:59 |
version 1.23, 2020/06/19 10:18:13 |
|
|
* 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.18 2019/12/12 04:44:59 noro Exp $ |
* $OpenXM: OpenXM_contrib2/asir2018/engine/dist.c,v 1.22 2020/02/11 01:43:57 noro Exp $ |
*/ |
*/ |
#include "ca.h" |
#include "ca.h" |
|
|
Line 591 void _addtodl(int n,DL d1,DL d2) |
|
Line 591 void _addtodl(int n,DL d1,DL d2) |
|
d2->d[i] += d1->d[i]; |
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) |
void _copydl(int n,DL d1,DL d2) |
{ |
{ |
int i; |
int i; |
Line 2755 DPM dpm_sp_nf_asir(VECT psv,int i,int j,DPM *nf); |
|
Line 2764 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 3049 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 3097 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 3132 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 3212 int compdmm_schreyer(int n,DMM m1,DMM m2) |
|
Line 3222 int compdmm_schreyer(int n,DMM m1,DMM m2) |
|
} |
} |
} |
} |
|
|
|
int compdmm_schreyer_old(int n,DMM m1,DMM m2) |
|
{ |
|
int pos1,pos2,t,npos1,npos2; |
|
DMM *in,*sum; |
|
DMMstack s; |
|
static DL d1=0,d2=0; |
|
static int dlen=0; |
|
|
|
sch_count++; |
|
pos1 = m1->pos; pos2 = m2->pos; |
|
if ( pos1 == pos2 ) return (*cmpdl)(n,m1->dl,m2->dl); |
|
if ( n > dlen ) { |
|
NEWDL(d1,n); NEWDL(d2,n); dlen = n; |
|
} |
|
sum = dmm_stack->sum; |
|
_copydl(n,m1->dl,d1); |
|
_copydl(n,m2->dl,d2); |
|
for ( s = dmm_stack; s; s = NEXT(s) ) { |
|
in = s->in; |
|
_addtodl(n,in[pos1]->dl,d1); |
|
_addtodl(n,in[pos2]->dl,d2); |
|
if ( in[pos1]->pos == in[pos2]->pos && _eqdl(n,d1,d2)) { |
|
if ( pos1 < pos2 ) return 1; |
|
else if ( pos1 > pos2 ) return -1; |
|
else return 0; |
|
} |
|
pos1 = in[pos1]->pos; |
|
pos2 = in[pos2]->pos; |
|
if ( pos1 == pos2 ) return (*cmpdl)(n,d1,d2); |
|
} |
|
if ( dpm_base_ordtype == 1 ) { |
|
if ( pos1 < pos2 ) return 1; |
|
else if ( pos1 > pos2 ) return -1; |
|
else return (*cmpdl)(n,d1,d2); |
|
} else { |
|
t = (*cmpdl)(n,d1,d2); |
|
if ( t ) return t; |
|
else if ( pos1 < pos2 ) return 1; |
|
else if ( pos1 > pos2 ) return -1; |
|
else return 0; |
|
} |
|
} |
|
|
|
extern int NaiveSchreyer; |
|
|
int compdmm(int n,DMM m1,DMM m2) |
int compdmm(int n,DMM m1,DMM m2) |
{ |
{ |
int t; |
int t,t1; |
int *base_ord; |
int *base_ord; |
|
|
switch ( dpm_ordtype ) { |
switch ( dpm_ordtype ) { |
Line 3235 int compdmm(int n,DMM m1,DMM m2) |
|
Line 3290 int compdmm(int n,DMM m1,DMM m2) |
|
else if ( m1->pos > m2->pos ) return -1; |
else if ( m1->pos > m2->pos ) return -1; |
else return (*cmpdl)(n,m1->dl,m2->dl); |
else return (*cmpdl)(n,m1->dl,m2->dl); |
case 3: /* Schreyer */ |
case 3: /* Schreyer */ |
return compdmm_schreyer(n,m1,m2); |
if ( NaiveSchreyer ) |
|
t = compdmm_schreyer_old(n,m1,m2); |
|
else |
|
t = compdmm_schreyer(n,m1,m2); |
|
return t; |
case 4: /* POT with base_ord */ |
case 4: /* POT with base_ord */ |
base_ord = dp_current_spec->module_base_ord; |
base_ord = dp_current_spec->module_base_ord; |
if ( base_ord[m1->pos] < base_ord[m2->pos] ) return 1; |
if ( base_ord[m1->pos] < base_ord[m2->pos] ) return 1; |
Line 3557 DPM dpm_compress(DPM p,int *tab) |
|
Line 3616 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 3579 void dpm_simplify_syz(LIST s,LIST m,LIST *s1,LIST *m1, |
|
Line 3639 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; |