summaryrefslogtreecommitdiff
path: root/proofs/lfsc_checker/trie.h
blob: 094a9060a6340ce22e0d61d6a3aa6bee9e016765 (plain)
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
127
128
129
#ifndef sc2__trie_h
#define sc2__trie_h

#include <vector>
#include <string.h>
#include <stdlib.h>

template<class Data>
class Trie {
protected:
  char *str;
  Data d;
  bool using_next;
  std::vector<Trie<Data> *> next;

  // s is assumed to be non-empty (and non-null)
  Data insert_next(const char *s, const Data &x) {
    unsigned c = s[0];
    if (c >= next.size()) {
      using_next = true;
      next.resize(c+1);
      next[c] = new Trie<Data>;
    }
    else if (!next[c]) 
      next[c] = new Trie<Data>;

    return next[c]->insert(&s[1], x);
  }

  // s is assumed to be non-empty (and non-null)
  Data get_next(const char *s) {
    unsigned c = s[0];
    if (c >= next.size())
      return Data();
    Trie<Data> *n = next[c];
    if (!n)
      return Data();
    return n->get(&s[1]);
  }

public:
  Trie() : str(), d(), using_next(false), next() { }

  ~Trie();

  class Cleaner {
  public:
    virtual ~Cleaner() {}
    virtual void clean(Data d) = 0;
  };

  static Cleaner *cleaner;

  bool eqstr(const char *s1, const char *s2) {
    while (*s1 && *s2) {
      if (*s1++ != *s2++)
	return false;
    }
    return (*s1 == *s2);
  }

  Data get(const char *s) {
    if (!s[0] && (!str || !str[0]))
      return d;
    if (str && eqstr(str,s))
      return d;
    if (using_next)
      return get_next(s);
    return Data();
  }

  Data insert(const char *s, const Data &x) {
    if (s[0] == 0) {
      // we need to insert x right here.
      if (str) {
	if (str[0] == 0) {
	  // we need to replace d with x
	  Data old = d;
	  d = x;
	  return old;
	}
	// we need to push str into next.
	(void)insert_next(str,d);
	free(str);
      }
      str = strdup(s);
      d = x;
      return Data();
    }
    
    if (str) {
      // cannot store x here 
      if (str[0] != 0) {
	insert_next(str,d);
	free(str);
	str = 0;
	d = Data();
      }
      return insert_next(s,x);
    }

    if (using_next)
      // also cannot store x here 
      return insert_next(s,x);

    // we can insert x here as an optimization
    str = strdup(s);
    d = x;
    return Data();
  }

};

template<class Data> 
Trie<Data>::~Trie() 
{
  cleaner->clean(d);
  for (int i = 0, iend = next.size(); i < iend; i++) {
    Trie *t = next[i];
    if (t)
      delete t;
  }
  if (str)
    free(str);
}

extern void unit_test_trie();

#endif
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback