equalRegEx {
\schemaVar \term RegEx rexp1 , rexp2 ;
\schemaVar \variables Seq string ;
\find ( rexp1 = rexp2 )
\varcond \replacewith ( \forall string ; ( match ( rexp1 , string )<-> match ( rexp2 , string )))
};defined in: regExAxioms.key Line: 7 Offset :4repeatAxiom {
\schemaVar \term RegEx rexp ;
\schemaVar \term Seq string ;
\schemaVar \term int nTimes ;
\schemaVar \variables int endIdx ;
\find ( match ( repeat ( rexp , nTimes ), string ))
\varcond \replacewith ( \if ( nTimes < 0 )\then ( false )\else ( \if ( nTimes = 0 )\then ( string = empty )\else ( \exists endIdx ; ( endIdx >= 0 & endIdx <= seqLen ( string )& match ( rexp , seqSub ( string , 0 , endIdx ))& match ( repeat ( rexp , nTimes - 1 ), seqSub ( string , endIdx , seqLen ( string )))))))
};defined in: regExAxioms.key Line: 17 Offset :4optAxiom {
\schemaVar \term RegEx rexp ;
\schemaVar \term Seq string ;
\find ( match ( opt ( rexp ), string ))
\replacewith ( match ( repeat ( rexp , 0 ), string )| match ( rexp , string ))
\heuristics (simplify )
};defined in: regExAxioms.key Line: 46 Offset :4altAxiom {
\schemaVar \term RegEx rexp1 , rexp2 ;
\schemaVar \term Seq string ;
\find ( match ( alt ( rexp1 , rexp2 ), string ))
\replacewith ( match ( rexp1 , string )| match ( rexp2 , string ))
\heuristics (simplify )
};defined in: regExAxioms.key Line: 56 Offset :4regExConcatAxiom {
\schemaVar \term RegEx rexp1 , rexp2 ;
\schemaVar \term Seq string ;
\schemaVar \variables int endIdx ;
\find ( match ( regExConcat ( rexp1 , rexp2 ), string ))
\varcond \replacewith ( \exists endIdx ; ( endIdx >= 0 & endIdx <= seqLen ( string )& match ( rexp1 , seqSub ( string , 0 , endIdx ))& match ( rexp2 , seqSub ( string , endIdx , seqLen ( string )))))
\heuristics (simplify )
};defined in: regExAxioms.key Line: 66 Offset :4regExAxiom {
\schemaVar \term Seq stringAsPattern , string ;
\find ( match ( regEx ( stringAsPattern ), string ))
\replacewith ( string = stringAsPattern )
\heuristics (concrete )
};defined in: regExAxioms.key Line: 85 Offset :4repeatStarAxiom {
\schemaVar \term RegEx rexp ;
\schemaVar \term Seq string ;
\schemaVar \variables int nTimes ;
\find ( match ( repeatStar ( rexp ), string ))
\varcond \replacewith ( \exists nTimes ; ( nTimes >= 0 & match ( repeat ( rexp , nTimes ), string )))
\heuristics (simplify )
};defined in: regExAxioms.key Line: 95 Offset :4repeatPlusAxiom {
\schemaVar \term RegEx rexp ;
\schemaVar \term Seq string ;
\schemaVar \variables int nTimes ;
\find ( match ( repeatPlus ( rexp ), string ))
\varcond \replacewith ( \exists nTimes ; ( nTimes >= 1 & match ( repeat ( rexp , nTimes ), string )))
\heuristics (simplify )
};defined in: regExAxioms.key Line: 107 Offset :4