z3py 相关问题

Z3 Theorem Prover的Python接口

添加多个约束后 Z3 位向量无法满足

对于 CTF 挑战,我需要根据每个字节的几个约束重建一个字节数组。 然而,在 Z3 中尝试了一下位向量后,我注意到solver.check()返回...

回答 1 投票 0

与 Z3 Python API 进行异或 - 仅返回单个解决方案

我正在使用 Z3 的 Python API 测试单个 XOR 语句。 这是我得到的输出: [B_L = 真,A_L = 假,C_L = 假] 然而,我应该有 3 个解决方案,其中两个变量是......

回答 1 投票 0

Z3 求解器类型错误:“ArithRef”对象无法解释为整数

我正在尝试使用 Z3py 运行下面的代码,主要问题是我想使用求解器找到我的函数的参数。我想在我的

回答 1 投票 0

Z3-Solver 的“TransitiveClosure”功能是否有 bug?

这是使用 TransitiveClosure 的简单示例的代码。 从 z3 导入 * defcompute_transitive_closure(图): num_nodes = len(图) # 创建 Z3 上下文 ctx = 上下文() #

回答 1 投票 0

Z3优化模块出现意外行为?

我也有一个带有软约束的优化问题。所有软约束都具有相同的权重 1. 问题:如果软约束改变了优化,那么它们实际上是否应该被忽略......

回答 1 投票 0

z3 中最大满足子集查找器的文档示例中的错误

我正在尝试使用 z3 文档示例中的代码来查找 z3 中最令人满意的子集。这是我复制的代码: 从 z3 导入 * def main(): x, y = 实数('x y')

回答 1 投票 0

为什么 Z3 对于类似的约束返回 sat 和 unsat?

我是Z3的新手,并试图用它解决“发送+更多=金钱”的难题。我通过复制其他人的代码解决了一些错误,但我不太明白它为什么有效。 Q1: 为什么...

回答 1 投票 0

Z3 SMT Solver:有没有办法生成具有特定变量集的模型

我正在解决一个问题,我在 Z3 中定义了大量变量(大约 500 个)。我有兴趣找到满足我的要求的多个模型(致力于多个解决方案)...

回答 1 投票 0

如何将x-d列表转换为数组?

从其他问题中,我知道如何将一维列表转换为数组。里面的“Store”功能可以完成这个。然而,我想得到一个通用的方法来完成这项工作。 这是一个前任...

回答 1 投票 0

尝试用 Z3 证明二分查找终止,但 Z3 发现了无效的计数器示例

我正在尝试学习和实验 z3 试图证明二分搜索。第一步是询问函数是否终止。这应该可以通过证明尺寸函数 (r -...

回答 1 投票 0

在 Z3 求解器中使用封闭世界假设求解约束

我正在使用Python中的Z3求解器解决约束满足问题,我需要解决以下形式的约束: ForAll([x, y], 暗示(And(情况(x), 情况(y)), And(动作(...

回答 1 投票 0

Z3 来解决一个难题(8 块瓷砖)吗?

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

回答 1 投票 0

使用 z3 定理获得基于给定约束的唯一解决方案

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

回答 1 投票 0

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

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

回答 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...

回答 1 投票 0

Z3中高效的模运算

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

回答 1 投票 0

Z3-Solver(z3.z3types.Z3Exception:Z3 无效替换,需要表达式对。)

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

回答 1 投票 0

StringSort 类型的工作序列时未知

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

回答 1 投票 0

z3优化和软约束

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

回答 1 投票 0

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

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

回答 1 投票 0

© www.soinside.com 2019 - 2024. All rights reserved.