← Back to branch summary

~verifypn-maintainers/verifypn/new-trunk

« back to all changes in this revision

Viewing changes to PetriEngine/Simplification/LinearPrograms.h

  • Committer: Jiri Srba
  • Date: 2017-12-14 08:59:40 UTC
  • mfrom: (190.2.25 conjunction)
  • Revision ID: srba.jiri@gmail.com-20171214085940-7s5l2d3ow5jc7e7h
merged in branch lp:~verifypn-stub/verifypn/conjunction
- Compiles inequalities into a convex constraint-system when possible.
- Unfolds fire-ability propositions on-the-fly instead of up front.
- Removes occurrences of same variable of each side of an equality over commutative arithmetic operators (eg a+b+c<=a can be rewritten b+c<=0).
- Compiles id-expressions and constants directly into an array of a commutative arithmetic expression rather than as child-objects.
- Constructs lazy linear programs into a (balanced) tree instead of a linear walk through (fixes issue with stack-overflow).

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Simplification/LinearPrograms.h
14
14
                enum result_t { UNKNOWN, IMPOSSIBLE, POSSIBLE };
15
15
                result_t _result = result_t::UNKNOWN;
16
16
                
17
 
                virtual void satisfiableImpl(const PQL::SimplificationContext& context) = 0;
 
17
                virtual void satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime) = 0;
18
18
                bool has_empty = false;
19
19
            public:
20
20
                bool empty() { return has_empty; }
21
21
                
22
 
                virtual bool satisfiable(const PQL::SimplificationContext& context)
 
22
                virtual bool satisfiable(const PQL::SimplificationContext& context, uint32_t solvetime = std::numeric_limits<uint32_t>::max())
23
23
                {
24
24
                    reset();
25
 
                    if(context.timeout() || has_empty) return true;
 
25
                    if(context.timeout() || has_empty || solvetime == 0) return true;
26
26
                    if(_result != UNKNOWN)
27
27
                    {
28
28
                        if(_result == IMPOSSIBLE)
30
30
                            return _result == POSSIBLE;
31
31
                        }
32
32
                    }
33
 
                    satisfiableImpl(context);
 
33
                    satisfiableImpl(context, solvetime);
34
34
                    assert(_result != UNKNOWN);
35
35
                    return _result == POSSIBLE;
36
36
                }
54
54
            size_t current = 0;
55
55
            size_t _size = 0;
56
56
            
57
 
            virtual void satisfiableImpl(const PQL::SimplificationContext& context)
 
57
            virtual void satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime)
58
58
            {
59
59
                for(int i = lps.size() - 1; i >= 0; --i)
60
60
                {
61
 
                    if(lps[i]->satisfiable(context) || context.timeout())
 
61
                    if(lps[i]->satisfiable(context, solvetime) || context.timeout())
62
62
                    {
63
63
                        _result = POSSIBLE;
64
64
                        return;
141
141
            size_t curr = 0;
142
142
            size_t _size = 0;
143
143
 
144
 
            virtual void satisfiableImpl(const PQL::SimplificationContext& context)
 
144
            virtual void satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime)
145
145
            {
146
146
                // this is where the magic needs to happen
147
147
                bool hasmore = false;
158
158
                    else
159
159
                    {
160
160
                        if( context.timeout() ||
161
 
                            !prog.isImpossible(context))
 
161
                            !prog.isImpossible(context, solvetime))
162
162
                        {
163
163
                            _result = POSSIBLE;
164
164
                            break;
248
248
        private:
249
249
            LinearProgram program;
250
250
        protected:
251
 
            virtual void satisfiableImpl(const PQL::SimplificationContext& context)
 
251
            virtual void satisfiableImpl(const PQL::SimplificationContext& context, uint32_t solvetime)
252
252
            {
253
253
                // this is where the magic needs to happen
254
 
                if(!program.isImpossible(context ))
 
254
                if(!program.isImpossible(context, solvetime ))
255
255
                {
256
256
                    _result = POSSIBLE;
257
257
                }