問題タブ [quantifiers]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
javascript - Javascript の正規表現でグループを定量化するにはどうすればよいですか?
文字列「QQxaxbxcQQ」があり、x の後に任意の文字が続くすべてのグループをキャプチャしたいとします。また、QQ 間のみを検索したい (文字列には他のものが含まれる場合があります)。私はこれがうまくいくと思いました：
ただし、これは最後の一致 (xc) のみを返すようです。正しい方向に私を向けることができますか？
編集:私の質問の最初のバージョンは単純化されすぎていました。元のレスポンダーに謝罪します。実際の問題に近づけるために編集しました。
php - Php Preg_Replace が一致しない文字数
preg_replaceing で文字列をフィルタリングしようとしています。数字とドット以外、およびドットの前に 5 個までの数字。wamp(UptoDate)の下のPHP 5.4.3。
グッドマッチ:
- 0.01
- 0.1
- 12345.11
- 12345.1
- 1
- 12345
悪い一致:
- 0,10
- 0,1
- 12345,11
- 12345,1
- 123456
私が抱えている最初の問題は、(,) カンマを削除できないことです。(.) ドットをセパレーターとして保持したいだけです。これは価格文字列用であることに注意してください。Phpは(,)カンマで計算しないみたいなので、入力はカンマのみにしたいです。コンマではありません。だから私は（^）を使用し、文字クラスを否定し、次に0-9. . 次に、一致する文字数を追加します。私は 1 から 5 の間でした (1 または 2 または 3 または... 5
私は何を間違っていますか。
ここに私が助けに使ってきた情報があります: http://www.regular-expressions.info/reference.html http://www.expreg.com/options.php
theorem-proving - 有限有界量指定子の消去規則
次の目標があります。
P 0この目標を、P 1、P 2、 、P 3の6 つのサブ目標に分割したいと思いP 4ますP 5。これは、 によって簡単に実行できapply autoます。しかし、これを行うために使用している関連するルールは何autoですか? 私の実際の目標は次のように見えるので、私は尋ねます：
apply autoその目標を同じように分解することはありません（それは私に与えます
代わりは）。
coq - Coqにおける普遍的数量化仮説
仮説Hを以下のフォームから変更したい
に
どちらも同じ目標を解決できると思いますが、後者の形式の仮説が必要です。または、より具体的には、以下のように、さらに k をその要素に分離します。仮説Hをこれら2つの形式に変更するにはどうすればよいですか?
java - Java の正規表現、\\s と \\s+
次の 2 つの式の違いは何ですか?
java - Z3: モデルが一意かどうかを確認する
Z3 で、特定のモデルが一意であり、他のソリューションが存在しないことを証明/表示する方法はありますか?
実証する小さな例
次のモデルがユニークであることは知っていますが、Z3 オプションを使用するか、アサーションを追加することでこれを保証できますか?
明確にするために、JAVA APIを介してZ3を使用しています
z3 - Z3 v4.3+ は、非線形演算の量指定子の削除をサポートしていますか?
Z3 が完全にサポートしている量指定子の削除の種類を見つけることができませんでした。私が持っているのは、一般的には非線形項に対する普遍的に定量化された式です。同等の量指定子のない式を取得したいと思います。Z3でそれは可能ですか？
ありがとう、フリードリヒ