时间戳

首页 > 解决方案 > 如何将 Z3Py 代码转换为 C# 代码（Z3、SAT）

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

问题描述

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

我已经定义了名为 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# 函数，然后直接调用它？我认为它必须以某种方式在 Z3 中定义......（由于速度，Z3 <-> C#）或者它在 Z3Py 中也以相同的方式工作（Python 函数，Python If包装器）？

标签： z3smtz3py

解决方案

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

推荐阅读