← Back to branch summary

~verifypn-stub/verifypn/ctl-flow

« back to all changes in this revision

Viewing changes to PetriEngine/Simplification/LinearPrograms.h

  • Committer: Jiri Srba
  • Date: 2017-05-02 09:31:43 UTC
  • mfrom: (169.2.34 simplification_mem)
  • Revision ID: srba.jiri@gmail.com-20170502093143-o9mnpwobkzf7pe7p
Merged in branch lp:~verifypn-stub/verifypn/simplification_mem

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Simplification/LinearPrograms.h
7
7
    namespace Simplification {
8
8
 
9
9
        class LinearPrograms {
 
10
        private:
 
11
            std::vector<LinearProgram> lps;
 
12
            bool hasEmpty = false;
10
13
        public:
11
14
            LinearPrograms(){
12
15
            }
13
 
            LinearPrograms(const LinearProgram& lp){
14
 
                add(lp);
15
 
            }
 
16
                        
 
17
            LinearPrograms(LinearPrograms&& other) 
 
18
            : lps(std::move(other.lps)), hasEmpty(other.hasEmpty)
 
19
            {
 
20
                
 
21
            }
 
22
            
 
23
            LinearPrograms& operator = (LinearPrograms&& other)
 
24
            {
 
25
                lps = std::move(other.lps);
 
26
                hasEmpty = other.hasEmpty;
 
27
                return *this;
 
28
            }
 
29
            
16
30
            virtual ~LinearPrograms(){
17
31
            }
18
 
            std::vector<LinearProgram> lps;
19
32
            
20
 
            size_t sizeInBytes() {
21
 
                size_t content = 0;
22
 
                for (auto &lp : lps) {
23
 
                    content += lp.sizeInBytes();
24
 
                }
25
 
                return sizeof(std::vector<LinearProgram>) + content;
26
 
            }
27
 
 
28
33
            bool satisfiable(const PetriEngine::PetriNet* net, const PetriEngine::MarkVal* m0, uint32_t timeout) {
 
34
                if(hasEmpty) return true;
29
35
                for(uint32_t i = 0; i < lps.size(); i++){
30
36
                    if(!lps[i].isImpossible(net, m0, timeout)){
31
37
                        return true;
33
39
                }
34
40
                return false;
35
41
            }
36
 
 
37
 
            void add(const LinearProgram& lp){
38
 
                lps.push_back(lp);
39
 
            }
40
 
 
41
 
            static LinearPrograms lpsMerge(LinearPrograms& lps1, LinearPrograms& lps2){
42
 
                if (lps1.lps.size() == 0) {
43
 
                    return lps2;
 
42
            
 
43
            size_t size() const {
 
44
                return lps.size();
 
45
            }
 
46
 
 
47
            void add(const LinearProgram&& lp){
 
48
                if(lp.size() == 0)
 
49
                {
 
50
                    hasEmpty = true;
 
51
                }
 
52
                else
 
53
                {
 
54
                    lps.push_back(std::move(lp));
 
55
                }
 
56
            }
 
57
 
 
58
            void add(Equation&& eq){
 
59
                lps.emplace_back(std::move(eq));
 
60
            }
 
61
            
 
62
            /**
 
63
             * Merges two linear programs, this invalidates lps2 to restrict 
 
64
             * temporary memory-overhead. 
 
65
             * @param lps2
 
66
             */
 
67
            void merge(LinearPrograms& lps2){
 
68
                if (lps.size() == 0) {
 
69
                    lps.swap(lps2.lps);
 
70
                    return;
44
71
                }
45
72
                else if (lps2.lps.size() == 0) {
46
 
                    return lps1;
 
73
                    return;
47
74
                }
48
75
                
49
 
                LinearPrograms res;
50
 
                for(LinearProgram& lp1 : lps1.lps){        
 
76
                std::vector<LinearProgram> merged;
 
77
                merged.reserve(lps.size() * lps2.lps.size());
 
78
                for(LinearProgram& lp1 : lps){        
51
79
                    for(LinearProgram& lp2 : lps2.lps){
52
 
                        res.add(LinearProgram::lpUnion(lp1, lp2));
 
80
                        merged.push_back(LinearProgram::lpUnion(lp1, lp2));
53
81
                    }   
54
82
                }
55
 
                return res;
 
83
                if(lps2.hasEmpty)
 
84
                {
 
85
                    size_t osize = merged.size();
 
86
                    merged.resize(merged.size() + lps.size());
 
87
                    for(size_t i = 0; i < lps.size(); ++i) 
 
88
                        merged[osize + i].swap(lps[i]);
 
89
                }
 
90
                if(hasEmpty)
 
91
                {
 
92
                    size_t osize = merged.size();
 
93
                    merged.resize(merged.size() + lps2.size());
 
94
                    for(size_t i = 0; i < lps2.size(); ++i) 
 
95
                        merged[osize + i].swap(lps2.lps[i]);
 
96
                }
 
97
                lps.swap(merged);
 
98
                lps2.clear();
 
99
                hasEmpty = hasEmpty && lps2.hasEmpty;
56
100
            }
 
101
            
57
102
 
58
 
            static LinearPrograms lpsUnion(LinearPrograms& lps1, LinearPrograms& lps2){
59
 
                LinearPrograms res;
60
 
                for(LinearProgram& lp : lps1.lps){        
61
 
                    res.add(lp);
62
 
                }
63
 
                for(LinearProgram& lp : lps2.lps){        
64
 
                    res.add(lp);
65
 
                }
66
 
                return res;
 
103
            /**
 
104
             * Unions two linear programs, this invalidates lps2 to restrict 
 
105
             * temporary memory-overhead. 
 
106
             * @param lps2
 
107
             */
 
108
            void makeUnion(LinearPrograms& lps2)
 
109
            {
 
110
                // move data, dont copy!
 
111
                size_t osize = lps.size();
 
112
                lps.resize(lps.size() + lps2.lps.size());
 
113
                for(size_t i = 0; i < lps2.size(); ++i)
 
114
                {
 
115
                    lps[osize + i].swap(lps2.lps[i]);
 
116
                }
 
117
                lps2.clear();
 
118
                hasEmpty = hasEmpty || lps2.hasEmpty;
 
119
            }
 
120
            
 
121
            void clear()
 
122
            {
 
123
                lps.clear();
67
124
            }
68
125
        };
69
126
    }
70
127
}
71
128
 
72
 
#endif /* LINEARPROGRAMS_H */
 
 
b'\\ No newline at end of file'
 
129
#endif /* LINEARPROGRAMS_H */