z3の関数宣言

Question

z3では、別の関数を引数とする関数を宣言できますか？たとえば、この

(declare-fun foo (((Int) Bool)) Int) 

はあまり動作していないようです。ありがとう。

Answer 1

Leonardoが述べたように、SMT-Libはではなく、は高次関数を可能にします。これは単なる構文上の制限ではありません。高次関数による推論は（一般的に）SMTソルバが処理できるものを超えています。 （未解釈の機能はいくつかの特別な場合に使用することができますが。）

あなたは高階関数と理由する必要がある場合は、その後、対話型の定理証明は選択の主な武器です：いくつかのことIsabelle、HOL、Coq例。

ただし、高次関数ではなく、の方が、プログラミングタスクを単純化することができます。 SMT-Lib入力言語は、エンドユーザが実際には通常必要とする高水準プログラミングには適していません。それがあなたのユースケースであれば、SMT-Libを直接使用するのではなく、Z3（または他のSMTソルバー）にアクセスできるプログラミング言語を使って作業することをお勧めします。いくつかの選択肢がご利用の場合に最も適したものをホスト言語に応じて、あります

• あなたはPythonのユーザーであれば、単にZ3 4.0に同梱されてZ3Pyが移動するための方法である、
• あなたがいる場合Scalaユーザーの場合は、Scala^Z3を参照してください。
• もしHaskellがあなたの好みの言語なら、SBVを見てください。

各バインドには独自の機能セットがあり、Z3PyはおそらくZ3の人々によって直接サポートされているので最も汎用性が高いと思われます。 （それはまた、少なくとも当分の間、他の選択のためにアクセスできないZ3内部へのアクセスを提供する。

Answer 2

いいえ、これはできません。ただし、配列を引数として取る関数を定義することはできます。

（宣言 - 楽しいのfoo（（アレイのIntブール値））のInt）

あなたは、あなたの質問内の1つのような高次の機能をシミュレートするために、このトリックを使用することができます。ここで

は一例です：http://rise4fun.com/Z3/qsED

Z3 guideはZ3とSMTの詳細情報が含まれています。