問題タブ [quantifiers]

列挙型の式の量指定子除去戦術を試しています。何らかの方法でソルバーを調整してパフォーマンスを向上させる方法があるかどうかを知りたいです。ソースコードをざっと見た後、量指定子を削除するためのさまざまな戦略 (qe_lite.cpp など) があるように思われるが、それらは qe タクティックのパラメーターとして公開されていないという結論に達しました。私の場合、数式は単純な命題構造を持ち、量化された変数が数式に含まれていないこともありますが、手続きは数千回呼び出すことができます。だから私は推測します、私の質問は次のとおりです：

1. Z3 には量指定子の除去 (アプリケーション モード?) のためのある種のキャッシュがあり、類似または同一の数式をより高速に処理できますか?
2. Z3 に、有限領域の式で量指定子を削除するためのさまざまなアプローチを使用するように指示できますか?
3. Z3 で一般的に使用されている方法を知ることは興味深いでしょう。代入＋簡略化だけなのか、それとももっと凝ったテクニックを使っているのか。

ありがとうございました。

GLib リファレンス マニュアルの「正規表現の構文」セクション、サブセクション「原子グループ化と所有量指定子」から:

\d+foo文字列に適用されるパターンを考えてみましょう123456bar: 6 桁すべてに一致し、"foo" との一致に失敗した後、マッチャーの通常のアクションは、\d+ 項目に一致する 5 桁のみで再試行し、次に 4 で再試行することです。最終的に失敗する前に。

前の例で (アトミック グループ化(?>\d+)fooと呼ばれる)を使用すると、マッチャーは最初に "foo" の一致に失敗するとすぐにあきらめます。

上記の例のように、アトミック グループのサブパターンが 1 つの繰り返し項目である場合、「所有量指定子」と呼ばれるより単純な表記法を使用できます。\d++foo

*私の質問は次のとおりです。スター ( ) 繰り返し演算子に相当するものがない理由はありますか?

Java での例:

例外スタック トレースは次のとおりです。

K.Sierra を読んでいて、次の文章を見つけました。

貪欲な量指定子は、実際にはソース データ全体を読み取り、右端の一致が見つかるまで (右から) 逆方向に動作します。その時点で、ソース データの前の方から右端の一致の一部であるデータまでのすべてが含まれます。

ここで、次のようなソースがあるとします。

そしてパターン：proj1([^,])*

なぜそれはテキスト全体と一致しないのですか? 貪欲であるため、右端の「proj1.java」と一致する必要があり、返された一致は、右端の一致の前のソース全体である必要がありますか? 代わりに次を返します。

この正規表現を考えると：

および照合用のこの入力文字列:

xbbbx結果は、インデックス 0 から始まりインデックス 5 で終わる一致したテキストです。

しかし、正規表現と文字列の両方で最後の文字xをZに変更するだけで、次の正規表現が得られます。

そしてこの入力文字列：

結果は: no match foundです。

1 文字の変更で、このような動作の変更が生じるのはなぜですか?

私は最近正規表現を調べていて、?演算子が*、+、または?怠惰になると考えました。私の質問は、どのようにそれを行うのですか? *?たとえば、特別な演算子ですか、それとも?に影響があり*ますか? つまり、正規表現*?はそれ自体を 1 つの演算子として認識しますか、それとも正規表現*?は 2 つの別個の演算子*と? として認識し?ますか? 2 つの別個のオペレーターとして認識されている場合、それを遅延させるに*?はどのような?影響がありますか。*if?は*がオプションであることを意味しますが、これは*がまったく存在する必要がないことを意味するべきではありません。だったら声明で.*?正規表現は、短い文字列ではなく、個別の文字と文字列全体に一致しませんか? 説明してください、私は理解しようと必死です.どうもありがとう.

http://regexcrossword.com/で面白い正規表現クロスワードを実行したところ、(.)+ や (.)* など、グループの数量化の意味がわからないことがわかりました。

http://ole.michelsen.dk/tools/regex.htmlで試してみましょう。JavaScriptと PHP 正規表現エンジンが提供されています。

合わせる文字列は「トロロロ！」(引用符なし)。(「グローバルマッチ」をオンにして何かが変更された場合、PHP モードでは何も変更されていないため、プライミングされたバージョン、つまり JS として追加されます。)

これのセマンティクスとは何か、規範的な答えはありますか?