wdRegExRules.key

Taclets

Enabled under choices: wdChecks:on

wd_RegEx

wd_RegEx  {
\find (                    wd   (                    regEx   (                    s ) ) )
  \replacewith (                     wd   (                    s ) ) 
\heuristics  (simplify )

};

defined in: wdRegExRules.key Line: 12 Offset :4

wd_RegEx_Opt

wd_RegEx_Opt  {
\find (                    wd   (                    opt   (                    a ) ) )
  \replacewith (                     wd   (                    a ) ) 
\heuristics  (simplify )

};

defined in: wdRegExRules.key Line: 23 Offset :4

wd_RegEx_Alt

wd_RegEx_Alt  {
\find (                    wd   (                    alt   (                    a ,                    b ) ) )
  \replacewith (                     wd   (                    a ) &             wd   (                    b ) ) 
\heuristics  (simplify )

};

defined in: wdRegExRules.key Line: 34 Offset :4

wd_RegEx_Concat

wd_RegEx_Concat  {
\find (                    wd   (                    regExConcat   (                    a ,                    b ) ) )
  \replacewith (                     wd   (                    a ) &             wd   (                    b ) ) 
\heuristics  (simplify )

};

defined in: wdRegExRules.key Line: 45 Offset :4

wd_RegEx_Repeat

wd_RegEx_Repeat  {
\find (                    wd   (                    repeat   (                    a ,                    n ) ) )
  \replacewith (                     wd   (                    a ) &             leq   (                    0 ,                    n ) ) 
\heuristics  (simplify )

};

defined in: wdRegExRules.key Line: 56 Offset :4

wd_RegEx_Star

wd_RegEx_Star  {
\find (                    wd   (                    repeatStar   (                    a ) ) )
  \replacewith (                     wd   (                    a ) ) 
\heuristics  (simplify )

};

defined in: wdRegExRules.key Line: 67 Offset :4

wd_RegEx_Plus

wd_RegEx_Plus  {
\find (                    wd   (                    repeatPlus   (                    a ) ) )
  \replacewith (                     wd   (                    a ) ) 
\heuristics  (simplify )

};

defined in: wdRegExRules.key Line: 78 Offset :4

wd_RegEx_Pred_Match

wd_RegEx_Pred_Match  {
\find (                    WD   (                    match   (                    a ,                    s ) ) )
  \replacewith (                     wd   (                    a ) &             wd   (                    s ) ) 
\heuristics  (simplify )

};

defined in: wdRegExRules.key Line: 89 Offset :4

KeY Logic Documentation

Defined symbols in the KeY System

Overview