c# - C# API を使用して楽しみを定義する方法

Question

Z3 をテキスト形式で使用すると、define-fun を使用して、後で再利用する関数を定義できます。例えば：

 （define-fun test((a Int) (b Int)) Int
      （ite  (and (> a 2) (<= b 3))
             1
             (ite （and (<= a 2)(> b 10))
                  2
                  a
             )
       )
  ）

Context.MkFuncDecl は未解釈の関数のみを生成するために使用されるため、C# api を使用して fun を定義する方法を知りたいです。

Answer 1

define-funSMT 2.0 でマクロを定義するための単なるメカニズムです。SMT ソルバーに力を加えるものではありません。ユーザーは好みの言語でマクロを実装する関数を作成できるため、API でサポートしています。つまり、test指定されたという C# 関数を作成し、質問の ite 式aを返すことができます。bこれを Python で行う方法の例を次に示します。

http://rise4fun.com/Z3Py/to1

min以下は、任意の数の引数を受け取る関数を定義する別の例です。

http://rise4fun.com/Z3Py/Vvp