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
             )
       )
  ）

所以我想知道如何使用 C# api 定义 fun，因为 Context.MkFuncDecl 仅用于生成未解释的函数。

Answer 1

define-fun 只是 SMT 2.0 中定义宏的一种机制。它不会为 SMT 求解器增加任何功能。我们确实在 API 中支持它，因为用户可以创建一个函数，以其喜欢的语言实现宏。也就是说，我们可以创建一个名为 test 的 C# 函数，给定 a 和 b 返回问题中的 ite 表达式。以下是有关如何在 Python 中执行此操作的示例:

http://rise4fun.com/Z3Py/to1

这是另一个定义 min 函数的例子，它接收任意数量的参数:

http://rise4fun.com/Z3Py/Vvp