← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/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:
include/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
            size_t write_indir(std::vector<double>& dest, std::vector<int32_t>& indir) const
 
79
            {
 
80
                size_t l = 1;
 
81
                for(const std::pair<int,int>& el : _data)
 
82
                {
 
83
                    dest[l] = el.second;
 
84
                    if(dest[l] != 0)
 
85
                    {
 
86
                        indir[l] = el.first + 1;
 
87
                        ++l;
 
88
                    }
 
89
                }
 
90
                return l;
 
91
            }
 
92
            
 
93
            
 
94
        private:
 
95
            Vector(const std::vector<int>& data)
 
96
            {
 
97
                for(size_t i = 0; i < data.size(); ++i)
 
98
                {
 
99
                    if(data[i] != 0)
 
100
                    {
 
101
                        _data.emplace_back(i, data[i]);
 
102
                    }
 
103
                }                
 
104
            }
 
105
 
 
106
            std::vector<std::pair<int,int>> _data;
 
107
            LPCache* factory = NULL;
 
108
            size_t ref = 0;
 
109
        };
 
110
    }
 
111
}
 
112
 
 
113
namespace std
 
114
{
 
115
    using namespace PetriEngine::Simplification;
 
116
    
 
117
    template <>
 
118
    struct hash<Vector>
 
119
    {
 
120
        size_t operator()(const Vector& k) const
 
121
        {
 
122
            return MurmurHash64A(k.raw(), 
 
123
                    k.data_size(), 
 
124
                    1337);
 
125
        }
 
126
    };
 
127
}
 
128
 
 
129
#endif /* VECTOR_H */
 
130