← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Simplification/Vector.h

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Simplification/Vector.h
1
 
/* 
2
 
 * File:   LPFactory.h
3
 
 * Author: Peter G. Jensen
4
 
 *
5
 
 * Created on 31 May 2017, 09:26
6
 
 */
7
 
 
8
 
 
9
 
#include <vector>
10
 
#include <cstdlib>
11
 
#include <iostream>
12
 
#include <vector>
13
 
#include <cstring>
14
 
#include <cassert>
15
 
#include "MurmurHash2.h"
16
 
 
17
 
#ifndef VECTOR_H
18
 
#define VECTOR_H
19
 
 
20
 
namespace PetriEngine {
21
 
    namespace Simplification {
22
 
        enum op_t 
23
 
        {
24
 
            OP_EQ,
25
 
            OP_LE,
26
 
            OP_GE,
27
 
            OP_LT,
28
 
            OP_GT,
29
 
            OP_NE
30
 
        };
31
 
        class LPCache;
32
 
        class Vector {
33
 
        public:
34
 
            friend LPCache;
35
 
                        
36
 
            void free();
37
 
            
38
 
            void inc();
39
 
            
40
 
            size_t data_size() const;
41
 
 
42
 
            bool operator ==(const Vector& other) const
43
 
            {
44
 
                return  _data == other._data;
45
 
            }
46
 
            
47
 
            
48
 
            
49
 
            const void* raw() const
50
 
            {
51
 
                return _data.data();
52
 
            }
53
 
            
54
 
            size_t refs() const { return ref; }
55
 
            
56
 
            std::ostream& print(std::ostream& ss) const
57
 
            {
58
 
                int index = 0;
59
 
                for(const std::pair<int,int>& el : _data)
60
 
                {
61
 
                    while(index < el.first) { ss << "0 "; ++index; }
62
 
                    ss << el.second << " ";
63
 
                    ++index;
64
 
                }
65
 
                return ss;
66
 
            }
67
 
            
68
 
            void write(std::vector<double>& dest) const
69
 
            {
70
 
                memset(dest.data(), 0, sizeof (double) * dest.size());
71
 
                
72
 
                for(const std::pair<int,int>& el : _data)
73
 
                {
74
 
                    dest[el.first + 1] = el.second;
75
 
                }
76
 
            }
77
 
            
78
 
            
79
 
        private:
80
 
            Vector(const std::vector<int>& data)
81
 
            {
82
 
                for(size_t i = 0; i < data.size(); ++i)
83
 
                {
84
 
                    if(data[i] != 0)
85
 
                    {
86
 
                        _data.emplace_back(i, data[i]);
87
 
                    }
88
 
                }                
89
 
            }
90
 
 
91
 
            std::vector<std::pair<int,int>> _data;
92
 
            LPCache* factory = NULL;
93
 
            size_t ref = 0;
94
 
        };
95
 
    }
96
 
}
97
 
 
98
 
namespace std
99
 
{
100
 
    using namespace PetriEngine::Simplification;
101
 
    
102
 
    template <>
103
 
    struct hash<Vector>
104
 
    {
105
 
        size_t operator()(const Vector& k) const
106
 
        {
107
 
            return MurmurHash64A(k.raw(), 
108
 
                    k.data_size(), 
109
 
                    1337);
110
 
        }
111
 
    };
112
 
}
113
 
 
114
 
#endif /* VECTOR_H */
115