Z3固定小数点エンジンを使った∃-クエリと∀-クエリ

Question

Z3固定小数点エンジンの2つの異なる入力フォーマットがどのように関連しているのか混乱して苦労します。短い例：負の数の存在を証明したいとします。私は非負の数値に対して1、負に0を返し、関数が0を返す引数があれば失敗するように求める関数を宣言します。しかし、1つの制約があります：少なくとも1つが存在するときにソルバーがsatすべての数値が負でない場合はunsatとなります。

はdeclare-relとqueryフォーマットを使用して自明である。

(declare-rel f (Int Int)) 
(declare-rel fail()) 
(declare-var n Int) 
(declare-var m Int) 

(rule (=> (< n 0) (f n 0))) 
(rule (=> (>= n 0) (f n 1))) 

(rule (=> (and (f n m) (= m 0)) fail)) 
(query fail) 

しかし（forall有する）の純粋なSMT-LIB2フォーマットを使用しながら、それがトリッキーになります。たとえば、簡単な

(set-logic HORN) 
(declare-fun f (Int Int) Bool) 
(declare-fun fail() Bool) 

(assert (forall ((n Int)) 
    (=> (< n 0) (f n 0)))) 
(assert (forall ((n Int)) 
    (=> (>= n 0) (f n 1)))) 

(assert (forall ((n Int) (m Int)) 
    (=> (and (f n m) (= m 0)) fail))) 
(assert (not fail)) 

(check-sat) 

はunsatを返します。当然、(= m 0)を(= m 1)に変更すると同じ結果になります。 satは、failを暗示するだけです。(= m 2)です。問題は私が理解できないことです。このフォーマットを使用して解決方法を求める方法。答えsatすなわち、我々は唯一∀・解決策を見つけるために頼むことができるforall - 体を使用している間、私は、現時点ではそれを理解していますどのように

は、ソルバが解釈（または不変）すべてために、すべてのアサーションをsatisfiyingを見つけることができたことを意味しますの値であり、unsatはそのような機能がないことを意味します。つまり、をと証明し、モデルに「証明」（不変式）を入れようとします（明らかに、satの場合）。 declare-rel形式ソルバーでソリューションをINGの一方

、 queryは制約が∃-数量詞の下にあるいくつかの変数、同じよう のためのソリューションを検索します。換言すれば、のカウンタの例はです。 unsatの場合にのみ不変量を印刷できます。

私が質問のカップルしている：私はそれが正しい

1. を理解するだろうか？私はいくつかの重要なアイデアを逃すような気がする。たとえば、(assert (forall ...))の形で(query ...)をどのように表現するかという一般的な考え方は本当に役に立ちます（質問2を自動的に回答します）。
2. 純粋なSMT-LIB2形式でこのような∃-制約を解決する方法（反例が見つかるとsat）がありますか？はいの場合はどうですか？

Answer 1

まず、「declare-rel」、「declare-var」、「rule」および「query」を使用する形式は、SMT-LIB2のカスタム拡張です。 "declare-var"機能は、複数のルールからバウンド変数を省略するのに便利です。また、層別否定を使用してDatalogルールを定式化することもできます。これの意味は、層別否定から期待するべきものです。規約では、クエリに派生があることを示すために「sat」を使用し、クエリに対して派生が存在しないことを「unsat」としています。

標準SMT-LIB2はあなたが欲しいものをほとんど表現できることが判明しました ホーン条項は否定できない。ルールは意味を持ち、クエリーはフォームの意味（=>クエリーのfalse）、またはあなたが書いた（クエリーではない）意味です。 カスタムフォーマットの派生は、空の句の証明に対応する（例えば、「偽」を証明する「照会」の証明）。したがって、導出の存在は、SMT-LIB2アサーションが「不満」であることを意味する。逆に、ホーン句の解釈（モデル）がある場合、そのようなモデルは派生がないことを確立する。句は「座っている」。言い換えれば

：

"sat" for datalog extension <=> "unsat" for SMT-LIB2 formulation 
"unsat" for datalog extension <=> "sat" for SMT-LIB2 formulation 

それが適用されたときに、純粋なSMT-LIB2の形式を使用する利点は、特別な構文拡張が存在しない ということです。これらは普通のSMT公式であり、 このクラスの公式を解きたい人は特別な の拡張子を書く必要はありません。 に調整されたソルバーが適切な数式を認識できるようにするだけです。 （HORNフラグメントのZ3の実装 は、ホーン節を書き留める際にいくらかの柔軟性を許します。 体内での分離があり、あなたはカリー化の意味を持つことができます）。

ルールベースのフォーマットが役立つSMT-LIB2フォーマットを使用すると、1つの欠点があります。クエリの派生がある場合、ルールベースのフォーマットはタプルの要素を印刷するためのプラグマを持っています。一般的に、クエリの関係は引数を取ることができます。この機能は、有限ドメイン関係に役立ちます。 上記の例では整数が使用されているため、リレーションは有限ドメインではありませんが、オンラインチュートリアルの例には有限ドメインインスタンスが含まれています。 クエリの導出は、解決証明にも対応します。あなたはSMT-LIB2のケースから解決の証拠を抽出することができますが、それはむしろ であり、効果的に使用する方法が見つけられていないと言わなければなりません。ホーン句の「二元性」エンジンは、 よりもアクセス可能なフォーマットで派生を生成し、デフォルトの校正フォーマットZ3を生成します。いずれにしても、ほとんど使用されていないために証明証明書を使用しようとすると、ユーザーが障害に陥る可能性があります。ルールベースのフォーマットには、派生トレールに対応するインスタンスを持つ述語のセットをアセンブルする別の機能があります。この出力を視覚化する方が簡単です。