← Back to branch summary

~verifydtapn-contributers/verifydtapn/trunk

« back to all changes in this revision

Viewing changes to src/DiscreteVerification/DataStructures/ptrie.h

  • Committer: Jiri Srba
  • Date: 2015-08-31 12:39:10 UTC
  • mfrom: (324.3.24 PTrieWorkflow)
  • Revision ID: srba@cs.aau.dk-20150831123910-qwr9g6pq7zntajhe
merged in a big branch implementing PTrie for workflow analysis

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/DiscreteVerification/DataStructures/ptrie.h
1
1
/* 
2
 
 * File:   PTrie.h
 
2
 * File:   ptrie.h
3
3
 * Author: Peter G. Jensen
4
4
 *
5
5
 * Created on 10 June 2015, 18:44
9
9
#define PTRIE_H
10
10
 
11
11
#include "binarywrapper.h"
 
12
#include "visitor.h"
12
13
#include <assert.h>
13
14
#include <limits>
14
15
#include <vector>
15
16
#include <stdint.h>
 
17
#include <stack>
16
18
 
17
19
namespace ptrie
18
20
{
35
37
            void set_meta(T);
36
38
            uint write_partial_encoding(encoding_t&) const;
37
39
            encoding_t& remainder() const;
 
40
            
38
41
            ptriepointer_t() : container(NULL), index(0) {};
 
42
            
 
43
            ptriepointer_t<T>& operator=(const ptriepointer_t<T>&);
 
44
            ptriepointer_t<T>& operator++();
 
45
            ptriepointer_t<T>& operator--();
 
46
            bool operator==(const ptriepointer_t<T>& other);
 
47
            bool operator!=(const ptriepointer_t<T>& other);
 
48
            
39
49
    };
40
50
    
41
51
    template<typename T>
45
55
    }
46
56
    
47
57
    template<typename T>
 
58
 
 
59
    ptriepointer_t<T>& ptriepointer_t<T>::operator=
 
60
                                                (const ptriepointer_t<T>& other)
 
61
    {
 
62
        container = other.container;
 
63
        index = other.index;
 
64
        return *this;
 
65
    }
 
66
    
 
67
    template<typename T>
 
68
    ptriepointer_t<T>& ptriepointer_t<T>::operator++()
 
69
    {
 
70
        ++index;
 
71
        assert(index <= container->_next_free_entry);
 
72
        return *this;
 
73
    }
 
74
    
 
75
    template<typename T>
 
76
    ptriepointer_t<T>& ptriepointer_t<T>::operator--()
 
77
    {
 
78
        --index;
 
79
        return *this;
 
80
    }
 
81
    
 
82
    template<typename T>
 
83
    bool ptriepointer_t<T>::operator==(const ptriepointer_t<T>& other)
 
84
    {
 
85
        return other.container == container && other.index == index;
 
86
    }
 
87
    
 
88
    template<typename T>
 
89
    bool ptriepointer_t<T>::operator!=(const ptriepointer_t<T>& other)
 
90
    {
 
91
        return !(*this == other);
 
92
    }
 
93
    
 
94
    /*
 
95
    template<typename T>
 
96
    void swap(ptriepointer<T>& lhs, ptriepointer<T>& rhs)
 
97
    {
 
98
        ptrie<T>* container = lhs.container;
 
99
        uint index = lhs.index;
 
100
        lhs.container = rhs.container;
 
101
        lhs.index = rhs.index;
 
102
        rhs.index = index;
 
103
        rhs.container = container;
 
104
    }*/
 
105
    
 
106
    template<typename T>
48
107
    T ptriepointer_t<T>::get_meta() const
49
108
    {
50
109
        return container->get_entry(index)->_data.get_meta();
72
131
    class ptrie_t {
73
132
        typedef binarywrapper_t<T> encoding_t;  
74
133
        friend class ptriepointer_t<T>;
75
 
        public:
 
134
        private:
76
135
            
77
136
            // nodes in the tree
78
137
            struct node_t
123
182
            std::pair<bool, ptriepointer_t<T> > find(const encoding_t& encoding);
124
183
            bool consistent() const;
125
184
            uint size() const { return _next_free_entry; }
 
185
            ptriepointer_t<T> begin();
 
186
            ptriepointer_t<T> end();
 
187
            ptriepointer_t<T> last();
 
188
            ptriepointer_t<T> rend();
 
189
            
 
190
            void visit(visitor_t<T>&);
126
191
    };
127
192
    
128
193
    template<typename T>
173
238
    }
174
239
    
175
240
    template<typename T>
 
241
    ptriepointer_t<T> ptrie_t<T>::begin()
 
242
    {
 
243
        return ptriepointer_t<T>(this, 0);
 
244
    }
 
245
    
 
246
    template<typename T>
 
247
    ptriepointer_t<T> ptrie_t<T>::end()
 
248
    {
 
249
        return ptriepointer_t<T>(this, _next_free_entry);
 
250
    }
 
251
    
 
252
    template<typename T>
 
253
    ptriepointer_t<T> ptrie_t<T>::last()
 
254
    {
 
255
        return ptriepointer_t<T>(this, _next_free_entry-1);
 
256
    }
 
257
    
 
258
    template<typename T>
 
259
    ptriepointer_t<T> ptrie_t<T>::rend()
 
260
    {
 
261
        return ptriepointer_t<T>(this, std::numeric_limits<uint>::max());
 
262
    }
 
263
    
 
264
    template<typename T>
176
265
    typename ptrie_t<T>::node_t*
177
266
    ptrie_t<T>::get_node(uint index) const
178
267
    {
218
307
    bool ptrie_t<T>::consistent() const
219
308
    {
220
309
        return true;
 
310
        assert(_next_free_node >= _nodevector.size());
 
311
        assert(_next_free_entry >= _entryvector.size());
221
312
        for(size_t i = 0; i < _next_free_node; ++i)
222
313
        {
223
314
            node_t* node = get_node(i);
269
360
    }
270
361
    
271
362
    template<typename T>
 
363
    void ptrie_t<T>::visit(visitor_t<T>& visitor)
 
364
    {
 
365
        std::stack<std::pair<uint, uint> > waiting;
 
366
        waiting.push(std::pair<int, uint>(-1, 0));
 
367
 
 
368
        bool stop = false;
 
369
        do{
 
370
            int distance = waiting.top().first;
 
371
            uint n_index = waiting.top().second;
 
372
            waiting.pop();
 
373
            
 
374
            if(distance > -1)
 
375
            {
 
376
                visitor.back(distance);
 
377
                visitor.set(distance, true);    // only high on stack
 
378
            }
 
379
            
 
380
            node_t* node = get_node(n_index);
 
381
            bool skip = false;
 
382
            do
 
383
            {
 
384
 
 
385
                if(node->_highpos != 0)
 
386
                {
 
387
                    waiting.push(std::pair<uint, uint>(distance + 1, node->_highpos));
 
388
                }                 
 
389
                
 
390
                if(node->_lowpos == 0) break;
 
391
                else
 
392
                {
 
393
                    ++distance;
 
394
                    node = get_node(node->_lowpos);
 
395
                    skip = visitor.set(distance, false);
 
396
                }
 
397
                
 
398
            } while(!skip);
 
399
            
 
400
            distance += 1;
 
401
            
 
402
            uint bucketsize = 0;
 
403
            if(!skip)
 
404
            {
 
405
                if(node->_highcount > 0) bucketsize += node->_highcount;
 
406
                if(node->_lowcount > 0) bucketsize += node->_lowcount;
 
407
                
 
408
                for(uint i = 0; i < bucketsize && !stop; ++i)
 
409
                {
 
410
                    stop = visitor.set_remainder(distance,
 
411
                                    ptriepointer_t<T>(this, node->_entries[i]));
 
412
                }
 
413
            }            
 
414
        } while(!waiting.empty() && !stop);
 
415
    }
 
416
    
 
417
    template<typename T>
272
418
    bool ptrie_t<T>::best_match(const encoding_t& encoding, uint& tree_pos, 
273
419
                uint& e_index, uint& enc_pos, uint& b_index, uint& bucketsize)
274
420
    {
316
462
        // start by creating an encoding that "points" to the "unmatched"
317
463
        // part of the encoding. Notice, this is a shallow copy, no actual
318
464
        // heap-allocation happens!
319
 
        encoding_t s_enc = encoding_t(  encoding.raw(), 
 
465
        encoding_t s_enc = encoding_t(  encoding.const_raw(), 
320
466
                                        (encsize - enc_pos), 
321
467
                                        enc_pos, 
322
468
                                        encsize);
341
487
                    e_index = node->_entries[b_index];
342
488
                    break;
343
489
                }
344
 
                else if(cmp == 1)
 
490
                else if(cmp > 0)
345
491
                {
346
492
                    low = b_index + 1;
347
493
                }
348
 
                else //if cmp == -1
 
494
                else //if cmp < 0
349
495
                {
350
496
                    high = b_index - 1;
351
497
                }
352
498
                
353
499
                if(low > high)
354
500
                {
355
 
                    if(cmp == 1)
 
501
                    if(cmp > 0)
356
502
                        b_index += 1;
357
503
                    break;
358
504
                }
367
513
        /*int tmp;// refference debug code!
368
514
        for(tmp = 0; tmp < bucketsize; ++tmp)
369
515
        {
370
 
            entry_t* ent = getEntry(node->entries[tmp]);
371
 
            if(ent->data < s_enc)
 
516
            entry_t* ent = get_entry(node->_entries[tmp]);
 
517
            if(ent->_data.cmp(s_enc) < 0)
372
518
            {
373
519
                continue;
374
520
            }
375
521
            else
376
 
            if(ent->data == s_enc)
 
522
            if(ent->_data == s_enc)
377
523
            {
378
524
                assert(found);
379
525
                break;
491
637
        uint enc_pos;
492
638
        uint bucketsize;
493
639
        uint e_index;
494
 
        
495
 
        if(best_match(encoding, tree_pos, e_index, enc_pos, bucketsize))
 
640
        uint b_index;
 
641
        if(best_match(encoding, tree_pos, e_index, enc_pos, b_index,  bucketsize))
496
642
        {
497
643
            return std::pair<bool, ptriepointer_t<T> >(true, 
498
644
                                                ptriepointer_t<T>(this, e_index));
534
680
                                    remainder_size, 
535
681
                                    enc_pos, 
536
682
                                    encsize);
537
 
        assert(n_entry->_data.raw() != encoding.raw());
 
683
        //assert(n_entry->_data.const_raw() != encoding.const_raw());
538
684
                
539
685
        n_entry->_nodeindex = tree_pos;
540
686