コンテキスト内にネストされた実存ステートメントH : exists ( a : A ) ( b : B ) ( c : C ) ... ( z : Z ), P a b c ... zがあるとします。H新しい仮説をインスタンス化して取得する最良の方法は何H' : P a b c ... zですか? これを繰り返すinversionと時間がかかり、 のような不要な中間ステップがすべて残りますH0 : exists ( b : B ) ( c : C ) ... ( z : Z ), P a b c ... z。

私の以前の質問は、これと非常によく似ています。たぶん、これを使用するpose proofかgeneralize、これを機能させる方法もあります。

以下のフォーマットをサポートする必要があります

3 桁の数字の後にオプションのスペースが続き、その後に次の文字セット ACERV 内で指定された 3 つの非反復文字が続きます (スペースは 2 つの文字の間でのみ有効です)。

有効な形式:

無効な形式:

これまでのところ、必ずしも必要ではない先読みでこれを複雑にしすぎている可能性があります。

先読み (?!\4) が追加されると、有効な形式との一致に失敗します 123 A - (?!\4) の数量詞を (?!\4)* または (?!\4)? に変更します。123 A を一致させることができますが、1 番目または 2 番目の文字を繰り返すことができます。

私は mod_rewrite regex で match quantifier {} を使用しています。rewrite ルールは、quantifier が 1 回または 2 回一致した場合に機能し、3 回以上一致した場合は機能しません。なんで？

.htaccess ファイルの例:

この作品（私は mydomain.com/download.ex が必要です）：

しかし、これは機能しません、500エラー、2から3の最大量指定子のみが変更されました（ mydomain.com/download.exe が必要です）：

それは素晴らしいですが、これは本物です。なぜそうなのですか？

バージョン:

放物線 y=(x+2)**2-3 の最小値を見つけようとしています。明らかに、x ==-2 の場合、答えは y==-3 になるはずです。しかし、z3 は答え [x = 0, y = 1] を返します。これは、ForAll アサーションを満たしていません。

私は何かを間違って仮定していますか？

Pythonコードは次のとおりです。

そして結果：

結果は、'qe' タクティックがその ForAll アサーションを True に削除したことを示していますが、常に true であるとは限りません。それがソルバーが間違った答えを出す理由ですか? このような式の最小 (または最大) 値を見つけるには、何をコーディングすればよいですか?

ところで、Z3 のバージョンは Mac では 4.3.2 です。

私が試したこと

JSFiddleを作成しました。

私が期待すること

変数matchesは次の配列になります。

私が得るもの

変数matchesは実際には次の配列です。

私の考え

私の推測では、キャプチャ グループや$ロジックに欠けているものがあると思います。どんな助けでも大歓迎です。（複数の正規表現でこれを行う方法を理解できることは知っていますが、ここで何が起こっているのかを理解したいです。）