問題タブ [quantifiers]

量指定子a?は一致するはずa single or no occurrence of aです。指定されたプログラムはjava.util.regexpackage を使用して正規表現を文字列と照合します。

私の質問は、プログラムの出力/パターン マッチングの結果についてです。

プログラムの出力:-

Enter your regex: a? Enter input string to search: a I found the text "a" starting at index 0 and ending at index 1. I found the text "" starting at index 1 and ending at index 1.

質問：-

a の 1 回または 0 回の出現に一致するはずです。したがって、 a zero-length ""(つまり、の不在/ゼロ回の出現a)に一致し、starting and ending at index 0次に and に一致a starting at index 0しending at index 0、次に aに一致するべきではありません"" starting and ending at index 1か? そうすべきだと思います。

このように、は文字列から 'smatcherを探し続けているように見えます。そして、 's'aがなくなったことが確認されるとa(つまりend、文字列の ? )、zero occurrence/ が存在しないa?を探します。それは退屈だと思いますし、そうではありません。しかし、開始と終了の?starting and ending at 0に一致する前に"" を見つける必要があります。index 0index 1

プログラム：-

セミコロンの前の数字を一致させようとしていますが、後読みで量指定子を使用できないため、これを機能させる方法がわかりません。

文字列 (はい、「item[##]」と「=」の間にタブスペースがあります)

13、13、7、2 を入手したい

これは私の現在の正規表現であり、明らかに機能しません:

3 つ以上出現する場合は、最後のスラッシュを置き換える必要があります。このようなパスがある場合"/foo/bar/"、それは になるはず"/foo/bar"です。ただし、次のようなパスに"/foo/"は触れないでください。

エスケープされたスラッシュ ( \/) と量指定子 ( {3,})で試してみました。

ただし、この正規表現は、スラッシュの直後にあるスラッシュのみに一致します。"/foo/bar///"

この問題を解決する方法はありますか? 多分正/負lookaheadで？

http://www.regexr.com/393pm

視覚化するには:

Fede、Avinash Raj、Amal Muraliに感謝します。パフォーマンスは重要なので、@Fede が勝者です: http://jsperf.com/match-last-slash-if-there-are-at-least-nth-occurrences

括弧内に 2 と 4 を入れたのに、この関数がハイフンの前に 3 桁、ハイフンの後に 5 桁を使用するのはなぜですか? 親切に助け..

Java チュートリアルには、正規表現量指定子の例と説明があります。

貪欲 - 文字列全体を食べてから、1 文字ずつ戻って再試行します

気が進まない - 最初から始めて、一度に 1 文字ずつ食べます

Possessive - マッチのために 1 回試して文字列全体を食べる

それらは問題なく理解できますが、正規表現が文字クラスに変更されるとどうなるか説明してもらえますか? 他にルールはありますか？

Python の抽象代数ライブラリに取り組んでいたとき、多くの汚れた作業が量指定子を使用した論理式に対応するループを構築しているだけであることに気付きました。その後、Python で論理量化の関数を実装するのは難しいかもしれませんが、Haskell や他の言語では簡単に実装できることに気付きました。

現在、プロパティが量化されている1つの変数のみを含む限り機能する量指定子があり、量化する関係に3つの変数がある場合にのみ、これらの障壁を乗り越えるのは難しい部分のようです.

たとえば、ステートメント∀x ∃y (x < y)は問題を引き起こしますが、問題ありません∀x (x = 2) ∃y (y < 3)。

このような値レベルの論理量指定子を実装する既存の Haskell ライブラリはありますか? 「論理量指定子Haskell」の行に沿って何かを検索するたびに、型量指定子について多くのことを取得するため、検索が困難です。これは私が望んでいるものではありません。

私が見つけた唯一のものはforAllTest.QuickCheckであり、これには「存在」はありません。

Z3 がタイムアウトする次の簡単な例があります。

ここで、アサーションを単純化して等価性を伝搬すると、z3 はすぐに UNSAT を返します (予想どおり)。

この例は、Z3 が量指定子の下で等式を伝搬しないことを示しているようです。たとえば、次のアサーションは機能します (UNSAT が生成されます)。

z3 に等式を伝播させる方法、または方程式を使用する別の検索戦略を選択する方法はありますか?

コンテキストに仮説H : forall ( x : X ), P xと変数x : Xがあるとします。普遍的なインスタンス化を実行して、新しい仮説を取得したいH' : P x。これを行うための最も痛みのない方法は何ですか? どうやらapply H in x機能しません。assert ( P x )do が続きますが、複雑apply Hな場合は非常に面倒になる可能性があります。P

多少関連していると思われる同様の質問があります。ただし、ここで適用できるかどうかはわかりません。