← Back to branch summary

~tapaal-red/verifypn/rule-l

« back to all changes in this revision

Viewing changes to src/LTL/SuccessorGeneration/HeuristicLexer.l

  • Committer: Nikolaj Jensen Ulrik
  • Date: 2021-06-22 10:54:32 UTC
  • mto: This revision was merged to the branch mainline in revision 246.
  • Revision ID: nikolaj@njulrik.dk-20210622105432-61m9h1a09wynwp46
More elaborate parsing scheme for LTL heuristics

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/LTL/SuccessorGeneration/HeuristicLexer.l
 
1
%{
 
2
#include <string>
 
3
#include <memory>
 
4
 
 
5
#include "LTL/SuccessorGeneration/Heuristics.h"
 
6
#include "LTL/Structures/BuchiAutomaton.h"
 
7
#include "HeuristicParser.parser.hpp"
 
8
 
 
9
#define SAVE_TOKEN heurlval.string = new std::string(heurtext, heurleng)
 
10
#define SAVE_QUOTED_TOKEN heurlval.string = new std::string(heurtext+1, heurleng-2)
 
11
#define TOKEN(t) (heurlval.token = t)
 
12
 
 
13
#ifdef __clang__
 
14
#pragma clang diagnostic push
 
15
#pragma clang diagnostic ignored "-Wkeyword-macro"
 
16
#pragma clang diagnostic ignored "-Wunneeded-internal-declaration"
 
17
#endif
 
18
 
 
19
#define register      // Deprecated in C++11.
 
20
extern "C" int heurwrap(){return 1;}
 
21
extern std::unique_ptr<LTL::Heuristic> heuristic;
 
22
extern int heurparse();
 
23
%}
 
24
%option prefix="heur"
 
25
%option nounput
 
26
 
 
27
digit         [0-9]
 
28
letter        [a-zA-Z_]
 
29
%%
 
30
 
 
31
[ \t\n\r]         ;
 
32
"aut" {return TOKEN(AUT);}
 
33
"automaton" {return TOKEN(AUT);}
 
34
"dist" {return TOKEN(DIST);}
 
35
"distance" { return TOKEN(DIST); }
 
36
"fc" { return TOKEN(FIRECOUNT); }
 
37
"firecount" { return TOKEN(FIRECOUNT); }
 
38
"fire-count" { return TOKEN(FIRECOUNT); }
 
39
"fire" { return TOKEN(FIRECOUNT); }
 
40
"sum" { return TOKEN(SUM);}
 
41
"("                                                     {return TOKEN(LPAREN);}
 
42
")"                                                     {return TOKEN(RPAREN);}
 
43
{letter}({letter}|{digit})* {SAVE_TOKEN; return TEXT;}
 
44
{digit}+          {SAVE_TOKEN; return INT;}
 
45
"," { return TOKEN(COMMA);}
 
46
%%
 
47
namespace LTL {
 
48
std::unique_ptr<LTL::Heuristic> ParseHeuristic(const PetriEngine::PetriNet *net,
 
49
                                               const Structures::BuchiAutomaton &aut,
 
50
                                               const PetriEngine::PQL::Condition_ptr &cond,
 
51
                                               const char* heurString) {
 
52
        //Load up input buffer in Flex
 
53
        YY_BUFFER_STATE buf = heur_scan_string(heurString);
 
54
 
 
55
        if(heurparse(net, aut, cond) != 0)
 
56
                return NULL;
 
57
 
 
58
        //Delete the buffer
 
59
        heur_delete_buffer(buf);
 
60
        return std::move(heuristic);
 
61
}
 
62
}
 
63
#ifdef __clang__
 
64
#pragma clang diagnostic pop
 
65
#endif