scala - Scala ^ Z3 DSLでは、未解釈の関数はどのように宣言されますか？

Question

Scala ^Z3DSL式を読みやすいようにラテックスに変換する小さなScalaプログラムがあります。しかし、DSLを使用して未解釈の関数を宣言する方法がわかりません。他の構造を使用して関数の動作をハッキングする方法はたくさんあります。ハッキングされた関数を印刷するのは簡単なので、ラテックスの通常の関数のように見えます。しかし、それが何らかの形で可能であれば、私はむしろ未解釈の関数を宣言したいと思います。

Answer 1

Val[_]解釈されない関数を解決する 1 つの方法は、型コンストラクターで Scala 関数型を使用することです。例えば：

import z3.scala._
import z3.scala.dsl._

choose(
  (x : Val[Int], f : Val[Int=>Int]) => x < f(x)
)

> res0: (Int, Int=>Int) = (0,<function1>)

次に、関数は実際の Scala 関数によってモデル化されます。

val f = res0._2
f(0)

> 1