# source:git/Singular/LIB/digimult.lib@c999545

spielwiese
Last change on this file since c999545 was c999545, checked in by Michael Brickenstein <bricken@…>, 17 years ago
• Property mode set to `100644`
File size: 3.5 KB
Line
1///////////////////////////////////////////////////////////////////////////////
2version="\$Id: digimult.lib,v 1.5 2006-05-19 11:42:31 bricken Exp \$";
3category="Logic";
4info="
5LIBRARY: digimult.lib   Satisfiability of prop. logical expressions
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  }
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){
55    if (c>0) {max=max+c;}else{min=min+c;}
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    summand=summand/subst(summand,var(1),l[i][1]);
80    summand=summand*l[i][2];
81    erg=erg+summand;
82  }
83  return(erg);
84}
85
86
87proc zero_one_comb(int n){
88  list l;
89  if (n==1){
90    list erg=list(0),list(1);
91    return(erg);
92  }
93  list rec= zero_one_comb(n-1);
94  int i=0;
95  list l0;
96  for(i=1;i<=size(rec);i++){
97    l0[i]=list(0)+rec[i];
98  }
99  list l1;
100  for(i=1;i<=size(rec);i++){
101    l1[i]=list(1)+rec[i];
102  }
103  return(l1+l0);
104}
105
106proc gen_min_term(list point)
107"RETURN: poly function, which is 1 on point, 0 else"
108{
109  int n=size(point);
110  def oldring=basering;
111  ring helperring=char(basering),x(1..n),dp;
112  list comb=zero_one_comb(n);
113  int i,j;
114  poly erg=0;
115  poly m;
116  for(i=1;i<=size(comb);i++){
117    m=1;
118    for(j=1;j<=n;j++){
119      m=m*(var(j))^comb[i][j];
120    }
121    erg=erg+m;
122  }
123  list erg_l=helperring,erg;
124  setring oldring;
125  //return(erg_l);
126}
127
128proc satisfiable(ideal i)
129"USAGE: use with x(x-1) polys"
130{
131   ideal bit_ideal=gen_var_ideal(1,nvars(basering));
132   int it;
133   list var_order;
134   for(it=1;it<=nvars(basering);it++){
135     var_order[it]=it;
136   }
137   int step=0;
138   return(simple_gps(i,var_order,0));
139}
140
141static proc simple_gps(ideal i, list var_order, int step){
142  if ((size(i)==0)){~;}
143  step=step+1;
144  degBound=step+1;
145  ideal j;
146  if (size(var_order)==0){
147    ~;
148    degBound=0;
149    j=std(i);
150    if (reduce(1,j)==0){
151      //whole ring
152      return(0);
153    }
154    else {
155      return(1);
156    }
157  }
158
159  j=std(i);
160  if (reduce(1,j)==0){
161    //whole ring
162    return(0);
163  }
164  j=simplify(j,2);
165  //j=simplify(j,8);
166
167  poly v=var(var_order[1]);
168  var_order=delete(var_order,1);
169  ideal j0=subst(j,v,0);
170  "setting", v, "to",0;
171  j0=simplify(j0,2);
172
173  j0=simplify(j0,8);
174  if (simple_gps(j0,var_order,step)==1){
175    return(1);
176  } else{
177    "setting", v, "to",1;
178    ideal j1=subst(j,v,1);
179    j1=simplify(j1,2);
180    //j0=simplify(j1,8);
181    return(simple_gps(j1,var_order, step));
182  }
183
184}
Note: See TracBrowser for help on using the repository browser.