問題タブ [quantifiers]

数式内のネストされたすべての量指定子を最も外側のレベルに移動したいと考えています。次のコマンドが Z3 で機能することを期待していましたが、機能しません。

の目的は:pull-nested-quantifiers何ですか? SMT-LIB または Z3 API を使用してネストされた量指定子を取得するにはどうすればよいですか?

Z3 を使用して、セット内の要素の包含と除外をモデル化しようとしています。具体的には、個別の値を持つ要素を含め、ターゲット セットにまだ含まれていない要素を除外します。したがって、基本的には、セット U が必要であり、Z3 に、U の異なる値を持つ要素のみを含むセット U_d を見つけてもらいたいと考えています。

私の現在のアプローチでは量指定子を使用していますが、U に表示される場合は常に U_d に要素を含めたいと述べる方法を理解するのに苦労しています.

それが生成する割り当ては次のとおりです。

希望する課題は次のとおりです。

A と B の両方に false を割り当てることが論理的に正しいことは理解していますが、そのような場合を除外するような方法で物事を述べる方法がわかりません。

おそらく私は問題について正しく考えていません。

アドバイスをいただければ幸いです。:)

Haskell Wikiは実存型の使い方をうまく説明していますが、私はそれらの背後にある理論を完全には理解していません。

実存型のこの例を考えてみましょう。

に変換できるものの型ラッパーを定義しますString。ウィキは、私たちが本当に定義したいのは次のようなタイプであると述べています

つまり、真の「存在する」型-大まかに言うと、これは「データコンストラクターはインスタンスが存在するSすべての型を取り、それをラップする」と言っていると思います。実際、GADTは次のように書くことができます。Show

私はそれをコンパイルしようとはしていませんが、うまくいくはずです。私にとって、GADTは明らかに私たちが書きたいコード（2）と同等です。

しかし、なぜ（1）が（2）と同等であるのかは私にはまったくわかりません。データコンストラクターを外部に移動すると、がに変わるのはなぜforallですかexists？

私が考えることができる最も近いものは、論理のド・モルガンの法則です。ここでは、否定と数量詞の順序を入れ替えると、存在記号が全称記号に変わり、その逆も同様です。

しかし、データコンストラクターは、否定演算子とはまったく異なる獣のようです。

forall存在しないタイプの代わりに存在するタイプを定義する機能の背後にある理論は何existsですか？

Z3 .net APIを使用して、存在記号exprを取得しようとしています。以下は私のコードです：

'

プログラムの場合、次の結果が得られました。

私の質問は1です。！の意味は何ですか。結果に/2。satの結果が得られない理由は何ですか？3. Z3 WebサイトのAPIメニューに加えて、誰かがZ3.NETAPIに対応する武道を提供できますか。

どうもありがとう！

Z3以外に、線形整数演算の量化記号消去法を実行する、利用可能な（そしてまだサポートされている）SMTツールはありますか？

ありがとう。

表記法で反復最大値を使用する正式な証明を Z3 に検証させようとしています。たとえば、fa 関数 (↑i: 0 ≤ i < N: f(i)) は、0 と N の間の値に適用されたときの f の最大値を指定します。次のようにうまく公理化できます。

(↑i: p(i): f(i)) ≤  x <=> (∀i: p(i): f(i) ≤ x)

i の型に対する pa 述語を使用します。Z3 でそのような量指定子を定義する方法はありますか?

証明を定式化するのに非常に便利なので、できるだけこの定義に近づけたいと思います。

ありがとう！

重複の可能性：
Python正規表現-ワイルドカード式から複数のグループをキャプチャする方法は？
グループ一致のPython正規表現

私はこれを行うためのより良いまたはより簡単な方法があることを知っていますが、私がそれを自分で試したがうまくいかなかったので、なぜ私は興味があるので、ここに問題があります：

正規表現を使用してXml属性を取得したいとします。次のXMLノードを見てみましょう。

を解析するNodeにOtherNodeは、次の正規表現があります。

の出力pattern.findall(xml)は次のとおりです。

（'Node'、'key2 = "val2"'、'key2'、'val2'）（'OtherNode'、''、''、''）

およびの出力[m.groupdict() for m in pattern.finditer(xml)]：

最後のメタバーのみがグループとしてアクセスできるようです。

key1同様にどのように一致させるのkey2ですか？複数のグループを(...)*構成と一致させることはできませんか？言い換えると、正規表現がmeta存在する場合は、指定されたグループと複数回一致するようにします。

わかりました、与えられた関係があります: F(x) が真でない場合、G(x) と H(y,x) を満たすケースはありません。((∀x ¬F(x)) ⇒¬(∀y G(y) ˄ H(y,x)))

さて、これを次のように変換できますか: (∀y G(y) ˄ H(y,x))) ⇒ ((∀x F(x)) ????

そうでない場合、左辺は本質的に次のことを暗示する必要があります。F(x) が true でない場合.... For All または Existential 数量詞については何も言及していません。量指定子の外で否定を取ることはできますか、つまり (¬(∀x F(x)) のように置きますか?

C / C++APIを介して線形整数算術式の数量詞を削除するためにZ3を使用したいと思います。簡単な例を考えてみましょう：Exists（x）（x <= y＆y <= 2 * x）。同じモデルの数量詞なしの式はy>=0です。

私はそれをこのようにしようとしました：

私が得るものは

（exists（（x Int）（and（<= xy）（<= y（* 2 x））））

一方、私は次のようなものを取得したいのですが

（<= 0年）

Z3で入手できる可能性はありますか？よろしくお願いします。

たとえば、文字列が foo または bar で開始および/または終了し、正規表現グループの内部文字列を取得したい場合は、文字列をトリミングしたいと考えています。
例えば

「fooTestbar」は「Test」、
「Test2bar」は「Test2」
、「Test3」は「Test3」である必要があります。

私の現在の正規表現は次のとおりです。

しかし、これは機能しません。これは、Quantifier?を代替グループ ( (foo|bar)) に適用できないためです。

マイコード

どんな助けでも大歓迎です。