z3 相关问题

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

我试图从以下描述中解决问题，这是我的代码：我的想法如下。空白空间表示为 1524。在每一步 s 中，一个方块都会移动到那个空的空间中......

smtp z3 smt z3py

回答 1 投票 0

我有一系列限制：车道（l0）==真，车道（l1）==真， OnComingLane(l1) == True, 车道标记(m1) == True, 车道标记(m0) == True, SolidWhiteLine(m1) == True, SolidWhiteLine(m0) == True,

python z3 solver z3py reasoning

回答 1 投票 0

Z3-Python 中的泰勒展开式三角函数

我需要在 Z3 中设计一个余弦（和正弦）函数，但这通常很困难且无法确定（例如，请参阅如何在 Z3 Python 中使用内置三角函数？）。不过，我还好

z3 smt z3py

回答 1 投票 0

如何在 Z3 Python 中使用内置三角函数？

我想做一些类似的事情：Exists y。 0<=cos(y)<=1., which could return a model e.g., y:=50. Is this possible in Z3? I know SMT solvers overall are problematic for non-linear/trascende...

z3 smt z3py

回答 1 投票 0

在 OCaml 中使用 Z3 获得无界变量的解释

问题我尝试使用 Z3 优化功能在检查可满足性时考虑一些目标。当我要求 Z3 最小化 x + y（其中 x > 0 且 y > 0）时，得到

ocaml z3

回答 1 投票 0

Z3中高效的模运算

我想在 BitVec 中的加法下使用整数模 3，所以基本上是 (a+b)%3。注意 BitVec 比整数快得多，因此我想确保所有操作都在 BitVec 内部。我需要

python z3 z3py

回答 1 投票 0

Z3-Solver（z3.z3types.Z3Exception：Z3 无效替换，需要表达式对。）

我有一个相对复杂的 Z3 布尔公式，当尝试设置特定变量的值时，出现以下错误：引发 Z3Exception(消息) z3.z3types.Z3Exception：Z3 无效

z3 z3py

回答 1 投票 0

StringSort 类型的工作序列时未知

我正在尝试使用序列（对 SQL 条件进行建模，并需要它与 ImportCountries 中“US”形式的 IN 子句一起使用，以查看两个条件是否可以同时为 True）...

z3 z3py

回答 1 投票 0

通过 C-API 检索正确找到的目标值

我试图找到公式中变量的边界值。为此，我将公式输入 Z3（版本 4.8.9 - Ubuntu 22.04 上的 64 位），然后使用客观标准来最小...

回答 1 投票 0

rust z3 版本 >= v 0.10.0 ast.Bool:: 和函数

铁锈z3 当z3的版本为“v.0.4.0”时，我们可以使用Bool::and函数来表示两个bool变量AND的结果。但在版本 >=“v.0.10.0”中，它......

rust boolean z3 smt

回答 1 投票 0

不要为符号指定具体值

我使用Z3来解决一些约束。我发明了一个表达式“x^m@mx where x noteq T”。有人提供“S^a”。我们知道“x^m@mx where x noteq T”可以以“S^a...

回答 1 投票 0

z3: sudo make install 无法在 MacOS Sonoma (M1 pro) 上设置动态库

我尝试在配备 M1 pro 处理器和 MacOS Sonoma 的 MacBook 上安装 z3，并从该存储库编译它（sudo make install）。使示例有效。我在另一个可怕的地方成功编译了一个文件...

g++ z3 dylib

回答 1 投票 0

如何使用pysmt同时计算同时包含整数和实数的公式

来自 pysmt.shortcuts 导入 * 从 pysmt.typing 导入 * hello = [“hello”中 s 的符号(s, INT)] pysmt = [“pysmt”中 s 的符号（s，实数）] 域_1 = And([And(GE(l, Int(1))...

z3 pysmt

回答 1 投票 0

solver_get_unsat_core() 返回空核心

我正在尝试使用 OCaml API 编写一个简单的 Z3 问题来提取未饱和的核心。问题是返回的 unsat 核心不应该是空的。你有什么想法或者你可以...

ocaml z3

回答 2 投票 0

达夫尼“真实”真的是“真实”吗

我想证明有关导数和极限的陈述，但未能取得进展，所以我想知道Dafny的实型是否真的与实数相符。达夫尼的文档状态...

z3 dafny boogie

回答 1 投票 0

是否可以使用 NuGet 在 Visual Studio 中安装 Z3 并与 C++ 一起使用？

标题应该很清楚，但只是为了记录，我尝试用NuGet安装Z3，但包没有包含目录或lib文件，当然它不允许C++或C

c++ visual-studio visual-c++ z3

回答 1 投票 0

Z3-solver安装在Python 3（Spyder编辑器）中，但无法到处导入

我尝试安装Z3定理求解器（https://github.com/Z3Prover/z3）。我可以运行发布版本 z3-4.12.4 中的示例文件。该文件位于“..\z3-4.12.4-x64-w...

python-3.x z3 windows-11

回答 1 投票 0

z3优化和软约束

以下代码在 only_2 为 True 时将 a 设置为 True，否则将 a 设置为 False。我不明白，因为如果我们最小化软约束，我们应该总是选择具有最高

z3 z3py

回答 1 投票 0

GNU/ANSI-C 中 Z3 的方程解示例

我正在努力寻找一个在普通 C 中使用 Z3 绑定（z3.h）的简单（真的像你好世界一样）的例子。我主要关心的是求解方程（或更确切地说是其系统），所以我需要看到什么是

z3 ansi-c

回答 1 投票 0

如何在Python中根据另一个变量来增加Z3变量？

我正在编写一个 Z3 Python 脚本，我试图根据涉及另一个变量 x 的条件来更改变量 y 。这是问题的简化版本：从 z3 导入 * x = BitVec...

python z3 z3py

回答 1 投票 0

z3 相关问题

最新问题