Annotation of OpenXM/src/asir-contrib/packages/sample/verify-by-sm1, Revision 1.2
1.2 ! takayama 1: /* $OpenXM: OpenXM/src/asir-contrib/packages/sample/verify-by-sm1,v 1.1 2000/07/15 07:17:58 takayama Exp $ */
1.1 takayama 2: /*
3: How to use?
1.2 ! takayama 4: (1) Add the following lines to .asirc
1.1 takayama 5: load("/home/nobuki/OpenXM/src/asir-contrib/packages/sample/verify-by-sm1");
6: /home/nobuki/ may be changed to your directory where you put OpenXM
1.2 ! takayama 7: "check_trace" in gr is overriden by that in verify-by-sm1, so
! 8: verify-by-sm1 must be read after gr has been read.
! 9: (2)
1.1 takayama 10: Starting asir
11: Sid = ox_launch();
12: dp_gr_flags(["GenTrace",1,"OXCheck",Sid]);
13: ox_cmo_rpc(Sid,"dp_ord",Ord);
14: ox_execute_string(Sid,"sm1_init_verify(1);");
15: gr([x^2+y^2-1,x*y-1],[x,y],0);
16:
17: gr(katsura(5),[u0,u1,u2,u3,u4,u5],0);
18: RESTRICTIONS:
19: Only graded reverse lexicographic order can be used.
20: The number of variables must be even.
21: The number of variables 2*n should be specified by the command
22: ox_execute_string(Sid,"sm1_init_verify(n);");
23:
24: */
25:
1.2 ! takayama 26: extern NFArray;
! 27:
1.1 takayama 28: Sm1_proc = -1$
29:
30: #define SM1_FIND_PROC(P) P = getopt(proc);\
31: if (type(P) == -1) {\
32: P = sm1_find_proc();\
33: }
34:
35: def sm1_find_proc() {
36: extern Sm1_proc;
37: if (Sm1_proc == -1) {
38: A = ox_get_serverinfo();
39: /* Look for ox_sm1. Not yet written */
40: /* Start sm1 automatically if there is not ox_sm1 */
41: Sm1_proc = sm1_start();
42: sm1(Sm1_proc,"[(Strict) 0] system_variable ");
1.2 ! takayama 43: sm1(Sm1_proc,"[(cmoLispLike) 0] extension ");
1.1 takayama 44: }
45: return(Sm1_proc);
46: }
47:
48: def sm1_init_verify(N) {
49: SM1_FIND_PROC(P);
50: sm1(P,"[(Strict) 0] system_variable ");
51: ox_push_cmo(P,ntoint32(N));
52: sm1(P," /nn set ");
53: sm1(P,"[(defaultPolyRing) nn] extension ");
54: print("sm1_init_verify: the number of variables must be ",0);
55: print(N*2);
56: }
57:
58: /* Computation of G
59: G = (Coeff*G-Monomial*Reducer)/Divisor;
60: by sm1 */
61: /*
62: NOTE:
63: No rational coefficient is allowed.
64: Coeff, Monomial, Reducer must not be zero.
65: */
66: /*
67: Replace
68: G = (Coeff*G+Monomial*Reducer)/Denominator;
69: by
70: sm1_verify00(Coeff,G,Monomial,Reducer,Denominator);
71: in check_trace(NF,NFIndex,HL) in gr
72: */
73: def sm1_verify00(Coeff,G,Monomial,Reducer,Denominator) {
74: SM1_FIND_PROC(P);
75: ox_push_cmo(P,Coeff);
76: if (G != 0) {
77: ox_push_cmo(P,G);
78: }else{
79: sm1(P," (0). ");
80: }
81: sm1(P," mul ");
82: ox_push_cmo(P,Monomial);
83: ox_push_cmo(P,Reducer);
84: sm1(P," mul add /ff set ");
85: sm1(P," ff message ");
86: ox_push_cmo(P,Denominator);
87: sm1(P," /gg set ");
88: sm1(P,"[(divByN) ff gg] gbext 0 get");
89: G = ox_pop_cmo(P);
90: return(G);
91: }
92:
93: def check_example() {
94: Coeff = 123;
95: G = 10*<<0,0,0,0,0,0,0,0>> ;
96: Monomial = 6*<<1,2,3,4,0,1,1,1>>;
97: Reducer = 4*<<1,0,0,0,1,1,1,1>>+2*<<1,3,0,5,1,1,1,1>>;
98: Denominator = 2;
99:
100: G2 = (Coeff*G+Monomial*Reducer)/Denominator;
101: /* Computing G2 by sm1 */
102: G = sm1_verify00(Coeff,G,Monomial,Reducer,Denominator);
103:
104: return([G,G2]);
105: }
1.2 ! takayama 106:
! 107: /* This is a copy of check_trace of gr in the asir standard library */
! 108: def check_trace(NF,NFIndex,HL)
! 109: {
! 110: if ( !car(HL)[0] ) {
! 111: /* dehomogenization */
! 112: DH = dp_dehomo(NFArray[car(HL)[1]]);
! 113: if ( NF == DH ) {
! 114: realloc_NFArray(NFIndex);
! 115: NFArray[NFIndex] = NF;
! 116: return 0;
! 117: } else
! 118: error("check_trace(dehomo)");
! 119: }
! 120:
! 121: for ( G = 0, T = HL; T != []; T = cdr(T) ) {
! 122: H = car(T);
! 123:
! 124: Coeff = H[0];
! 125: Index = H[1];
! 126: Monomial = H[2];
! 127: Denominator = H[3];
! 128:
! 129: Reducer = NFArray[Index];
! 130: /* G = (Coeff*G+Monomial*Reducer)/Denominator; */
! 131: G = sm1_verify00(Coeff,G,Monomial,Reducer,Denominator);
! 132: }
! 133: if ( NF == G ) {
! 134: realloc_NFArray(NFIndex);
! 135: NFArray[NFIndex] = NF;
! 136: return 0;
! 137: } else
! 138: error("check_trace");
! 139: }
! 140:
1.1 takayama 141:
142: end$
FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>