share/contrib/bitwise/bitwise_specification.txt

   1
   2 ;; Maxima bit functions
   3
   4 ;; bit_not      bitwise NOT
   5 ;; bit_and      bitwise AND
   6 ;; bit_xor      bitwise XOR
   7 ;; bit_or       bitwise OR
   8 ;; bit_lsh      bitwise LEFT SHIFT
   9 ;; bit_rsh      bitwise RIGHT SHIFT
  10
  11 ;; bit_length   number of necessary bits to represent a positive integer
  12 ;; bit_onep     test for bit 1
  13
  14
  15 ;; all functions except bit_onep have the property 'integer-valued
  16 ;; I'm not sure, if this is correct
  17 ;; if we allow bit_not(bit_not(x)) --> x, bit_and(x) --> x, etc. for any expression x
  18
  19
  20 ;; abbreviations:
  21 ;; i,j,k : literal integers
  22 ;; x,y,z : any expression
  23 ;; di,dj,dk : declared integer
  24 ;; de, do : declared even resp. odd
  25
  26
  27 ;; ERROR if at least one arg to bit_function is a non-integer constant, string or Maxima list
  28
  29
  30 ;; bitwise NOT:
  31 ;; bit_not(i) --> bitwise NOT i
  32 ;; bit_not(bit_not(x)) --> x  ;; di instead of x ?
  33 ;; bit_not(di) -->  - di - 1
  34
  35
  36 ;; bitwise AND:
  37 ;; bit_and() --> -1
  38 ;; bit_and(x,x,y) --> bit_and(x,y)
  39 ;; bit_and(i,j) --> bitwise i AND j
  40 ;; bit_and(0,x) --> 0
  41 ;; bit_and(-1,x) --> bit_and(x)
  42 ;; bit_and(i,j,x) --> bit_and(bit_and(i,j),x)
  43 ;; bit_and(x,bit_not(x),y) --> 0
  44 ;; bit_and(1,de,y) --> 0
  45 ;; bit_and(1,do) --> 1
  46 ;; bit_and(x) --> x  ;; di instead of x ?
  47
  48
  49
  50 ;; bitwise EXCLUSIVE OR:
  51 ;; bit_xor() --> 0
  52 ;; bit_xor(x,x,y,z) --> bit_xor(y,z)
  53 ;; bit_xor(i,j) --> bitwise i XOR j
  54 ;; bit_xor(i,j,x) --> bit_xor(bit_xor(i,j),x)
  55 ;; bit_xor(x,bit_not(x),y,z) --> bit_xor(-1,y,z)
  56 ;; bit_xor(0,x) --> bit_xor(x)
  57 ;; bit_xor(1,de,y) --> bit_xor(de+1,y)
  58 ;; bit_xor(1,do,y) --> bit_xor(do-1,y)
  59 ;; bit_xor(-1,x,y) --> bit_xor(bit_not(x),y)
  60 ;; bit_xor(x) --> x  ;; di instead of x ?
  61
  62
  63
  64 ;; bitwise OR:
  65 ;; bit_or() --> 0
  66 ;; bit_or(x,x,y) --> bit_or(x,y)
  67 ;; bit_or(i,j) --> bitwise i OR j
  68 ;; bit_or(-1,x) --> -1
  69 ;; bit_or(0,x) --> bit_or(x)
  70 ;; bit_or(i,j,x) --> bit_or(bit_or(i,j),x)
  71 ;; bit_or(x,bit_not(x),y) --> -1
  72 ;; bit_or(1,de,y) --> bit_or(de+1,y)
  73 ;; bit_or(1,do,y) --> bit_or(do,y)
  74 ;; bit_or(x) --> x  ;; di instead of x ?
  75
  76
  77 ;; bitwise LEFT SHIFT:
  78 ;; bit_lsh(i,k) --> bitwise LEFT SHIFT i,k
  79 ;; bit_lsh(x,dk) --> 2^dk*x, where dk>=0  ;; di instead of x ?
  80
  81
  82
  83 ;; bitwise RIGHT SHIFT:
  84 ;; bit_rsh(x,y) --> bit_lsh(x,-y)
  85
  86
  87
  88 ;; ONE-BIT TEST:
  89 ;; bit_onep(i,k) --> ONE-BIT TEST i,k, k>=0
  90 ;; bit_onep(de,0) --> false
  91 ;; bit_onep(do,0) --> true
  92 ;; bit_onep(x,dk) where 0<=x<2^dk, dk>=0 --> false
  93 ;; bit_onep(di^dj,y) where di^dj = 2^y --> true
  94
  95
  96
  97 ;; BIT LENGTH:
  98 ;; bit_length(i) --> BIT LENGTH i, i>=0
  99 ;; bit_length(2^dk) --> dk+1, bit_length(4^dk) --> 2*dk+1, etc., where dk>=0