source: git/Singular/LIB/digimult.lib @ 28543b

spielwiese
Last change on this file since 28543b was 28543b, checked in by Michael Brickenstein <bricken@…>, 19 years ago
*bricken:initial version, only a playground git-svn-id: file:///usr/local/Singular/svn/trunk@8046 2c84dea3-7e68-4137-9b89-c4e89433aadc
  • Property mode set to 100644
File size: 3.4 KB
Line 
1///////////////////////////////////////////////////////////////////////////////
2version="$Id: digimult.lib,v 1.1 2005-05-04 15:41:12 bricken Exp $";
3category="Logic";
4info="
5LIBRARY: primdec.lib   Primary Decomposition and Radical of Ideals
6AUTHORS: Michael Brickenstein, bricken@mathematik.uni-kl.de
7
8OVERVIEW:
9        Various algorithms for verifiying digital circuits, including SAT-Solvers
10
11PROCEDURES:
12         satisfiable(I);   returns 1, if system is satisfiable
13";
14proc gen_integer_poly(ideal var_i){
15  poly erg=0;
16  number two=2;
17  int i;
18  for(i=1;i<=ncols(var_i);i++){
19
20    erg=erg+two^(i-1)*var_i[i];
21  }
22  return(erg);
23}
24
25proc gen_var_ideal(int start, int last){
26  ideal erg;
27  int i;
28  for(i=0;i<=last-start;i++){
29    erg[i+1]=var(i+start);
30  }
31  return(erg);
32}
33
34proc poly_cancel_mod_number(poly f, number n){
35  if (f==0){
36    return(0);
37  }
38  poly l=lead(f);
39  if ((leadcoef(l) mod n)==0){
40    return(poly_cancel_mod_number(f-l,n));
41  }
42 
43  return(l+poly_cancel_mod_number(f-l,n));
44}
45
46proc gen_poly_mod2(poly f){
47  number max=0;
48  number min=0;
49  //matrix M=coeffs(M);
50  int i=0;
51  poly terms=f;
52  number c;
53  while(terms!=0){
54    c=leadcoef(terms);
55    if (c>0) {max=max+c;}else{min=min+c;}
56    terms=terms-lead(terms);
57  }
58  number n=min;
59  list constr;
60  int z=0;
61  for(n=min;n<=max;n=n+1){
62    z++;
63    constr[z]=list(n,n % 2);
64  }
65  poly u=uni_poly_on_values(constr);
66  return(system("bit_subst",u,f)); //subst(u,var(1),f));
67  }
68proc uni_poly_on_values(list l){
69  poly summand;
70  poly erg=0;
71  int i,j;
72  for(i=1;i<=size(l);i++){
73    summand=1;
74    for(j=1;j<=size(l);j++){
75      if(i!=j){
76        summand=summand*(var(1)-l[j][1]);
77       
78      }
79    }
80    summand=summand/subst(summand,var(1),l[i][1]);
81    summand=summand*l[i][2];
82    erg=erg+summand;
83  }
84  return(erg);
85}
86
87
88proc zero_one_comb(int n){
89  list l;
90  if (n==1){
91    list erg=list(0),list(1);
92    return(erg);
93  }
94  list rec= zero_one_comb(n-1);
95  int i=0;
96  list l0;
97  for(i=1;i<=size(rec);i++){
98    l0[i]=list(0)+rec[i];
99  }
100  list l1;
101  for(i=1;i<=size(rec);i++){
102    l1[i]=list(1)+rec[i];
103  }
104  return(l1+l0);
105}
106
107proc gen_min_term(list point)
108"RETURN: poly function, which is 1 on point, 0 else"
109{
110  int n=size(point);
111  def oldring=basering;
112  ring helperring=char(basering),x(1..n),dp;
113  list comb=zero_one_comb(n);
114  int i,j;
115  poly erg=0;
116  poly m;
117  for(i=1;i<=size(comb);i++){
118    m=1;
119    for(j=1;j<=n;j++){
120      m=m*(var(j))^comb[i][j];
121    }
122    erg=erg+m;
123  }
124  list erg_l=helperring,erg;
125  setring oldring;
126  //return(erg_l);
127}
128
129proc satisfiable(ideal i)
130"USAGE: use with x(x-1) polys"
131{
132   ideal bit_ideal=gen_var_ideal(1,nvars(basering));
133   int it;
134   list var_order;
135   for(it=1;it<=nvars(basering);it++){
136     var_order[it]=it;
137   }
138   int step=0;
139   return(simple_gps(i,var_order,0));
140}
141
142static proc simple_gps(ideal i, list var_order, int step){
143  step=step+1;
144  degBound=step+1;
145  ideal j;
146  if (size(var_order)==0){
147    degBound=0;
148    j=std(i);
149    if (reduce(1,j)==0){
150      //whole ring
151      return(0);
152    }
153    else {
154      return(1);
155    }
156  }
157
158  j=std(i);
159  if (reduce(1,j)==0){
160    //whole ring
161    return(0);
162  }
163  j=simplify(j,2);
164  j=simplify(j,8);
165 
166  poly v=var(var_order[1]);
167  var_order=delete(var_order,1);
168  ideal j0=subst(j,v,0);
169  j0=simplify(j0,2);
170  j0=simplify(j0,8);
171  if (simple_gps(j0,var_order,step)==1){
172    return(1);
173  } else{
174    j0=subst(j,v,0);
175    j0=simplify(j0,2);
176    j0=simplify(j0,8);
177    return(simple_gps(j0,var_order, step));
178  }
179 
180}
Note: See TracBrowser for help on using the repository browser.