share/contrib/bitwise/rtest_bitwise.mac

   1 (load(bitwise),0);
   2 0$
   3
   4 declare(di,integer);
   5 'done$
   6 declare(dj,integer);
   7 'done$
   8 declare(dk,integer);
   9 'done$
  10 assume(dk>=0);
  11 '[dk>=0]$
  12 declare(de,even);
  13 'done$
  14 declare(d_o,odd);
  15 'done$
  16
  17
  18 bit_not(8);
  19 -9$
  20 bit_not(x);
  21 'bit_not(x)$
  22 bit_not(bit_not(x));
  23 x$
  24 bit_not(di);
  25 -di-1$
  26
  27
  28 bit_and();
  29 -1$
  30 bit_and(42);
  31 42$
  32 bit_and(x);
  33 x$
  34 bit_and(0,x);
  35 0$
  36 bit_and(-1,x);
  37 x$
  38 bit_and(42,z,63,y,127,x);
  39 'bit_and(42,x,y,z)$
  40 bit_and(x,x,x,y);
  41 'bit_and(x,y)$
  42 bit_and(di,-di-1,y);
  43 0$
  44 bit_and(x,bit_not(x),y);
  45 0$
  46 bit_and(de,1);
  47 0$
  48 bit_and(d_o,1);
  49 1$
  50
  51
  52 bit_or();
  53 0$
  54 bit_or(x);
  55 x$
  56 bit_or(x,x,x,y);
  57 'bit_or(x,y)$
  58 bit_or(0,x,y);
  59 'bit_or(x,y)$
  60 bit_or(-1,x,y);
  61 -1$
  62 bit_or(di,-di-1,y);
  63 -1$
  64 bit_or(x,bit_not(x),y);
  65 -1$
  66 bit_or(1,de,y);
  67 'bit_or(de+1,y)$
  68 bit_or(1,de,-de-2);
  69 -1$
  70 bit_or(1,x,d_o);
  71 'bit_or(d_o,x)$
  72
  73
  74 bit_xor();
  75 0$
  76 bit_xor(7);
  77 7$
  78 bit_xor(x);
  79 x$
  80 bit_xor(x,x);
  81 0$
  82 bit_xor(0,x);
  83 x$
  84 bit_xor(-1,x);
  85 'bit_not(x)$
  86 bit_xor(-1,di);
  87 -di-1$
  88 bit_xor(5,7,15,x);
  89 'bit_xor(13,x)$
  90 bit_xor(x,bit_not(x));
  91 -1$
  92 bit_xor(x,bit_not(x),y,z);
  93 'bit_xor(bit_not(y),z)$
  94 bit_xor(x,bit_not(x),di);
  95 -di-1$
  96 bit_xor(2*x,-di-1,bit_not(2*x),di,y,z);
  97 'bit_xor(y,z)$
  98 bit_xor(1,de);
  99 de+1$
 100 bit_xor(1,d_o,x);
 101 'bit_xor(d_o-1,x)$
 102 bit_xor(1,d_o,-d_o);
 103 -1$
 104
 105
 106 bit_lsh(21,1);
 107 42$
 108 bit_lsh(21,-1);
 109 10$
 110 bit_lsh(x,-1);
 111 'bit_lsh(x,-1)$
 112 bit_lsh(x,3);
 113 8*x$
 114 bit_lsh(17,dk);
 115 17*2^dk$
 116 bit_lsh(17,-dk);
 117 'bit_lsh(17,-dk)$
 118 bit_lsh(x,dk);
 119 2^dk*x$
 120
 121
 122 bit_rsh(21,1);
 123 10$
 124 bit_rsh(21,-1);
 125 42$
 126 bit_rsh(x,-3);
 127 8*x$
 128 bit_rsh(x,1);
 129 'bit_lsh(x,-1)$
 130
 131
 132 bit_onep(8,3);
 133 true$
 134 bit_onep(8,2);
 135 false$
 136 bit_onep(de,0);
 137 false$
 138 bit_onep(d_o,0);
 139 true$
 140 assume(0<=xx,xx<2^7);
 141 '[xx>=0,xx<128]$
 142 bit_onep(xx,7);
 143 false$
 144 bit_onep(xx,6);
 145 'bit_onep(xx,6)$
 146 bit_onep(2^dk,dk);
 147 true$
 148 bit_onep(4^dk,2*dk);
 149 true$
 150 bit_onep(di^dj,dj*log(di)/log(2));
 151 true$
 152
 153
 154 bit_length(8);
 155 4$
 156 bit_length(2^dk);
 157 dk+1$
 158 bit_length(4^dk);
 159 2*dk+1$