Return to verify-by-sm1 CVS log

Up to [local] / OpenXM / src / asir-contrib / packages / sample

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$