diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-12 18:24:54 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-16 22:28:26 -0500 |
commit | 5186ca79710fe935d1f7ed27c4a34e913ab547e8 (patch) | |
tree | 4f5ce4957063085f607492a6474b0d244e4b2da4 /proofs/lfsc_checker/trie.h | |
parent | 4d9caf9782c59823fb95519b9b518b7d7f89738a (diff) |
First attempt at incorporating LFSC proof checker into CVC4.
Diffstat (limited to 'proofs/lfsc_checker/trie.h')
-rw-r--r-- | proofs/lfsc_checker/trie.h | 129 |
1 files changed, 129 insertions, 0 deletions
diff --git a/proofs/lfsc_checker/trie.h b/proofs/lfsc_checker/trie.h new file mode 100644 index 000000000..094a9060a --- /dev/null +++ b/proofs/lfsc_checker/trie.h @@ -0,0 +1,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 |