如何将 Z3Py 代码转换为 C# 代码（Z3、SAT）答案

【问题标题】：How to convert Z3Py code to C# code (Z3, SAT)如何将 Z3Py 代码转换为 C# 代码（Z3、SAT）
【发布时间】：2020-07-15 20:27:10
【问题描述】：

过去我编写了一些 Z3Py 代码，现在我想将其转换为 C# .NetCore。我检查了很多例子，但我有一些问题:-)

我已经定义了名为 MyFun 的函数，它接受参数并根据值返回变量。简单例子：

H0 = BitVec('H0', 8)
H1 = BitVec('H1', 8)
H2 = BitVec('H2', 8)
H3 = BitVec('H3', 8)
I1 = BitVec('I1', 8)
T1 = BitVec('T1', 8)

def MyFun(N):
  return z3.If(N == 0x00, H0,
         z3.If(N == 0x01, H1,
         z3.If(N == 0x02, H2, H3)))

s.add(T1 == z3.If(MyFun(I1) == 0x33, 0x11, 0x12) )

“函数定义”有问题，“z3.If”也有问题。我认为 MkFuncDecl 是为了别的。也许解决方案是用经典的 C# If 创建普通的 C# Function 然后直接调用它？我认为它必须在 Z3 中以某种方式定义...（由于速度，Z3 C#）或者它在 Z3Py 中也以相同的方式工作（Python 函数 与，Python如果包装）？

【问题讨论】：

标签： z3 smt z3py

【解决方案1】：

这将是一个常规的 C# 函数，但调用 Z3 的 If，而不是 C# 的 If。本质上，您正在为表达式构建抽象语法树，它恰好在 C# 中而不是 Python 中。否则，它是一样的。

【讨论】：

嗯，但是 C# 中 Z3 的 If 的命令是什么 :-) 我搜索了所有 IF，但没有找到有用的（Context.MkIff， Context.When、Context.Then...)
这就是你要找的东西：z3prover.github.io/api/html/…
是的，这是正确的答案。 C# 中等效的 Z3Py z3.If 函数是 MkITE (BoolExpr t1, Expr t2, Expr t3)。非常感谢;-)