z3 相关问题

Z3是Microsoft Research开发的高性能定理证明器。

如何使用 z3 库将经过优化的 SMT 模型转换为由 cvc4 等不同求解器识别的 .smt2 文件？

我想使用文件.smt2中的z3库转换用python编写的SMT模型，以获得可以从不同求解器（例如cvc4-solver）运行的文件。问题是我的模型...

optimization z3 smt cvc4 smt-lib

回答 2 投票 0

如何使用Z3 C++ api读取smtlib2字符串？

我想从给定的 SMTLIB2 文件创建一个 expr 对象。我可以在 C 示例中看到 Z3_parse_smtlib_string 函数。 expr 类中有一个包装器吗？

回答 2 投票 0

Z3 使用 Visual Studio 构建错误：致命错误 LNK1112：模块机器类型“x86”与目标机器类型“x64”冲突

我尝试使用 Visual Studio 2019 在 Win10 64 Professional 上构建 Z3。我按照 README 说明进行操作，并在“build”目录中点击 nmake。之后，我得到以下信息： CL /...

回答 1 投票 0

有从Python-Z3到Z3/smt2的解析器吗？

我正在使用Z3的Python API，因为方便，但有时我需要将Python结果转换为Z3/smt2的可读输入。例如，每当我执行量词消除时...

z3 smt z3py quantifiers

回答 1 投票 0

如何编译Z3（Skolem）函数

我正在使用一个返回（Skolem）函数的工具，例如： (define-fun y ((x1 Int)(x2 Int)) Int （ite（<= (+ x1 (- x2)) 0) x2 x1)) Now, I would like to use such functions in some part of a p...

回答 1 投票 0

通过 Cygwin64 安装适用于 Ocaml 的 z3 库（Windows 11）

我正在尝试在 Cygwin64 终端（Windows 11）中为 Ocaml 安装 z3 库。我收到以下错误，即使已经安装了库，也找不到 -lstdc++ 。 # cc1：警告：c...

cygwin ocaml z3 opam

回答 1 投票 0

PyExZ3 未找到程序的所有可行路径

我提出的 PyExZ3 使用的一个小例子没有按预期工作。这是示例：定义 d1(x,y): 如果 y < x - 2 : return 7 else : return 2 def d2(x,y): if y > 3 ：

python z3 z3py pyexz3

回答 1 投票 0

z3py 示例不适用于 macOS

我无法让任何 z3py 示例正常工作。我能够使用 github 上的自述文件中的说明成功安装它。我成功更新了我的 python 路径以指向适当的

python z3 z3py

回答 2 投票 0

是否可以缩小Z3中FP数的有效数字范围？

我正在尝试在具有大量浮点运算的测试用例上运行Z3（C ++），并且需要很长时间才能完成或挂起。为了减少验证时间，是否可以强制...

floating-point z3

回答 1 投票 0

如何将 z3::expr(bv_val) 转换为数字的位表示形式？

我正在尝试将 Z3::expr 翻译成数字的位表示，以便找出数字包含多少位“1”，如果“1”的位数是偶数，那么我......

c++ z3 symbolic-execution

回答 1 投票 0

如何为 `int list` z3 adt dotnet api 定义 adt 构造函数

如何为 int 列表定义 adt 构造函数 Context.MkConstructor(name: string, recognizer: string, ?fieldNames: string array, ?sorts: Sort array, ?sortRefs: uint32 array) : 构造函数文件...

z3 adt

回答 0 投票 0

减少最大位向量大小的等价公式

是否有可能将 .smt2 公式转换为等效公式，以这样的方式重写它，即每个 (declare-const a (_ BitVec 256)) 将转换为一组 (declare-const a0 (_ BitVec .. .

z3 smt

回答 1 投票 0

Z3 Python Mod Int 问题

我想使用 Z3 打印小于 20 的素数。以下程序打印 2、3、5 和 7，但不打印 11、13、17 或 19。尽管 isPrime(11)、isPrime(13)、isPrime(17) 或 isPrime(...

python z3 smt sat

回答 1 投票 0

如何在 Z3 Java API 中声明带有类型参数的数据类型？

使用 Z3 可以声明采用类型参数的自定义数据类型（即记录）。例如，第一个和第二个元素分别采用 T1 和 T2 类型的 Pair 是 de...