File: countbits.c

package info (click to toggle)
boolector 3.2.4-1
  • links: PTS, VCS
  • area: main
  • in suites: sid
  • size: 20,744 kB
  • sloc: ansic: 83,136; cpp: 18,159; sh: 3,668; python: 2,889; makefile: 210
file content (126 lines) | stat: -rw-r--r-- 2,323 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
/* Verifies correcntess of Peter Wegner's algorithm:
 *
 *   P. Wegner.
 *   A technique for counting ones in a binary computer.
 *   CACM 3(5), 1960.
 *
 *  The algorithm goes as follows:
 *
 *    for (y = x, c = 0; y; y &= y - 1)
 *      c++;
 *
 *  We unroll this bit witdh (n) times
 *
 *    for (c = i = 0; i < n; i++, y &= y - 1)
 *      if (y)
 *        c++;
 *
 *  and compare it against
 *
 *    for (s = i = 0; i < n; i++)
 *      if (x & (1 << i))
 *        s++;
 *
 *  then 's = c'.
 */
#include <stdarg.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

static void
die (const char* fmt, ...)
{
  va_list ap;
  fputs ("*** countbits: ", stderr);
  va_start (ap, fmt);
  vfprintf (stderr, fmt, ap);
  va_end (ap);
  fputc ('\n', stderr);
  exit (1);
}

int
main (int argc, char** argv)
{
  int i, j, n = -1, x, y, c, tmp, s;

  for (i = 1; i < argc; i++)
  {
    if (!strcmp (argv[i], "-h"))
    {
      fprintf (stderr, "usage: countbits -h | <bits>\n");
      exit (0);
    }
    else if (argv[i][0] == '-')
      die ("unsupported command line option '%s'", argv[i]);
    else if (n >= 0)
      die ("more than one argument");
    else if ((n = atoi (argv[i])) <= 1)
      die ("number bits has to be larger than one");
  }

  if (n < 0) die ("number of bits missing");

  tmp = 1;

  printf ("1 var %d\n", n);
  x = y = 1;

  printf ("2 const %d ", n);

  for (j = 1; j < n; j++) fputc ('0', stdout);

  fputs ("1\n", stdout);

  printf ("3 zero %d\n", n);
  c = s = 3;

  tmp = 4;

  for (i = 0; i < n; i++)
  {
    if (i < n - 1)
    {
      printf ("%d sub %d %d 2\n", tmp, n, y);
      tmp++;

      printf ("%d and %d %d %d\n", tmp, n, y, tmp - 1);
      tmp++;
    }

    if (i)
    {
      printf ("%d add %d %d 2\n", tmp, n, c);
      tmp++;
    }

    printf ("%d redor 1 %d\n", tmp, y);
    tmp++;

    y = i ? tmp - 3 : tmp - 2;

    printf ("%d cond %d %d %d %d\n", tmp, n, tmp - 1, i ? tmp - 2 : 2, c);
    c = tmp++;

    if (i)
    {
      printf ("%d add %d %d 2\n", tmp, n, s);
      tmp++;
    }

    printf ("%d slice 1 %d %d %d\n", tmp, x, i, i);
    tmp++;

    printf ("%d cond %d %d %d %d\n", tmp, n, tmp - 1, i ? tmp - 2 : 2, s);
    s = tmp++;
  }

  printf ("%d eq 1 %d %d\n", tmp, c, s);
  tmp++;

  printf ("%d root 1 %d\n", tmp, -(tmp - 1));
  tmp++;

  return 0;
}