3

z3 では、別の関数を引数として取る関数を宣言することは可能ですか? たとえば、これ

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

うまくいかないようです。ありがとう。

4

2 に答える 2

8

Leonardoが述べたように、SMT-Libは高階関数を許可しません。これは単なる構文上の制限ではありません。高階関数を使用した推論は、（一般に）SMTソルバーが処理できる範囲を超えています。（ただし、一部の特殊なケースでは、解釈されない関数を使用できます。）

高階関数で推論する必要がある場合は、対話型定理証明器が主な選択の武器です。Isabelle 、 HOL 、 Coqがその例の一部です。

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

  • Pythonユーザーの場合は、Z34.0に同梱されたばかりのZ3Pyが最適です。
  • Scalaユーザーの場合は、Scala^Z3を調べてください。
  • Haskellがあなたの好みの言語であるなら、SBVを見てください。

各バインディングには独自の機能セットがあります。Z3PyはZ3の人々によって直接サポートされているため、おそらく最も用途が広いでしょう。（また、少なくとも当面の間、他の選択肢にはアクセスできないままのZ3内部へのアクセスを提供します。）

于 2012-05-13T20:06:21.120 に答える
6

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

（declare-fun foo（（Array Int Bool））Int）

このトリックを使用して、質問のような高階関数をシミュレートできます。

次に例を示します：http：//rise4fun.com/Z3/qsED

Z3ガイドには、Z3およびSMTに関する詳細情報が含まれています。

于 2012-05-12T23:02:59.937 に答える