z3py相关内容

无法为Z3中的GADT创建抽象加法运算

问题 我在Z3中使用以下Datatype定义。我的目标是从本质上“重载”加法操作符。我使用ForAll尝试了以下技巧,但Z3似乎认为它无效。 问题 这是怎么回事?为什么这不起作用? 代码 import pytest from z3 import Datatype, IntSort, Solver, Ints def test_stackoverflow(): ..
发布时间:2022-08-22 09:49:30 Python

Z3:无效的有界变量

我正在尝试查看Z3(Python)中的一句话的有效性,但收到以下消息:Invalid bounded variable(s) 我在这里复制我遵循的步骤: v, a, b, c, d, e = Ints('v a b c d e') lt_1 = (v == 4) lt_2 = (v == 2) lt_3 = (v == 3) lt_4 = (v == 5) lt_5 = (v == ..
发布时间:2022-08-22 09:16:00 Python

为什么Z3&Quot;舍入&Real小到1.0/0.0?

我正在使用Z3的pythonAPI进行一些线性实数运算。我遇到过一种情况,非常接近于零的雷亚尔以某种方式转换为1.0/0.0。这进而导致Z3的C++部分内部出现浮点异常。 例如,我有以下的Python程序: from z3 import * s = Solver() s.add(0.00001 * Real("a") + 0.00001 * Real("b") > 0.0) print ..
发布时间:2022-08-22 09:00:51 Python

Z3-Python中的SAT查询变慢了:增量式SAT怎么办?

在Z3(Python)中,循环内的SAT查询速度变慢,我可以使用增量SAT来解决此问题吗? 问题如下:我在循环中执行具体的SAT搜索。在每次迭代中,我都会得到一个模型(当然,我存储了该模型的否定,以便不会再次探索相同的模型)。此外,如果该模型满足某个属性,我还会添加它的子查询,并将其他限制添加到公式中。然后再次迭代,直到获得UNSAT(即不再有模型)。 我提供代码的定向快照: ..
发布时间:2022-08-22 00:00:00 其他开发

Z3py SMT编码跟随变量及公式

我对Z3和SMT解算器真的很陌生。 我有以下问题,我不知道如何在Z3py中编码。 在上图中,N是节点集,因此N={Node1,Node2,Node3,Node4,Node5,Node6,Node7} i是输入集合,i={i1,i2,i3,i4} O是输出集合,O={O1,O2,O3} G是这样一个组,其中对于任何连续的2个输出(O i、O j),如果Oi是第一个生成的输出,并且 ..
发布时间:2022-08-21 23:47:56 其他开发

表示Z3中的集合有哪些替代方案?

PERthis answerZ3集合排序是使用数组实现的,考虑到API中提供的SetAdd和SetDel方法,这是有意义的。还声称here如果从未使用数组修改函数,则使用数组而不是未解释的函数是浪费开销的。鉴于此,如果我对集合的唯一用途是使用IsMember应用约束(无论是在单个值上还是作为量化的一部分),那么使用从底层元素排序到布尔值的未解释函数映射是不是更好?所以: from z3 im ..
发布时间:2022-08-21 23:31:19 其他开发

使用Z3为特定CHC系统的猜测解决方案找到反例?

假设我有以下CHC系统(i(X)是一个未知谓词): (x = 0) -> I(x) (x = 5) -> x = 5 现在假设我猜测i(X)的解为x<;2(实际上是一个错误的猜测)。我可以为Z3Py编写代码来(I)检查它是否是有效的解,以及(Ii)如果不正确,找一个反例,即一个满足x ..
发布时间:2022-08-21 23:20:43 其他开发

巨蟒--优化的不等式组

我正在编写一个用Python语言编写的程序,其中的一小部分涉及优化方程/不等式系统。理想情况下,我会像在Modelica中所能做的那样,写出方程,让求解器来处理。 求解器和线性规划的操作有点超出了我的舒适区,但我还是决定尝试一下。问题是,程序的总体设计是面向对象的,并且有许多不同的组合来形成方程,以及一些非线性,所以我无法将其转化为线性规划问题(但我可能是错的)。 经过一些研究后,我发 ..
发布时间:2022-08-21 22:45:17 Python

采用数组数据类型的Z3建模图

我试图在Z3中为有向图建模,但我被卡住了。我在图中添加了一个公理,即边的存在意味着它所连接的节点的存在。但仅此一项就会导致未命中 GraphSort = Datatype('GraphSort') GraphSort.declare('Graph', ('V', ArraySort(IntSort(), BoolSort())), ('E', ArraySort(IntSor ..
发布时间:2022-08-21 22:38:52 Python

以SMT2格式保存Z3求解器的状态(&Q)

是否可以使用Z3 API(例如,Python API)将求解器的当前状态保存到SMT2格式的文件中,包括求解器已学习的内容(在SAT求解中,我们称其为“已学习的子句”)? 因为我希望能够将求解器的状态保存在临时文件中,以便以后继续求解,以便有一些时间了解我应该对其进行哪些进一步查询。 提前表示感谢... 推荐答案 SMT2没有规定保存给定的求解器状态,这无疑会因求解器的不同 ..
发布时间:2022-08-21 22:30:29 Python

尝试在Python中使用Z3找到布尔公式的所有解

我是Z3的新手,正在尝试创建一个求解器,它返回布尔公式的所有可满足解。我记下了其他帖子的笔记,我编写了我希望能起作用的代码,但事实并非如此。问题似乎是,通过添加前面的解决方案,我删除了一些变量,但它们在后来的解决方案中返回? 目前我只想解决a或b或c。 如果我解释得不好,请让我知道,我会尝试进一步解释。 提前感谢您的回复:) 我的代码: from z3 import ..
发布时间:2022-08-21 21:51:21 其他开发

如何在z3py中连接正则表达式?

我想构造一个正则表达式,比如a*b*c*,Z3中有一个函数re.++,它可以将3个正则表达式连接在一起,这样我就可以构造a*b*c*,如下 (assert (str.in.re "aabbc" (re.++ (re.* (str.to.re "a")) (re.* (str.to.re "b")) (re.* (str.to.re "c"))))) (check-sat) 但是,我在z3 ..
发布时间:2022-08-21 21:40:49 其他开发

如何使Z3';(Python)的SAT解算偏向某个标准,例如更倾向于有更多否定的文字

在Z3(Python)中,有没有办法将SAT搜索“偏向”“条件”? 一个案例:我希望Z3获得一个模型,但不是任何模型:如果可能,请给我一个有大量否定文字的模型。 例如,如果我们必须搜索A or B,可能的模型是[A = True, B = True],但我宁愿收到模型[A = True, B = False]或模型[A = False, B = True],因为它们有更多的False分 ..
发布时间:2022-08-21 21:35:15 其他开发

使用 SMTLib for z3 的 Datalog 中的循环关系

我想用 SMTLib 格式表达这个问题,并使用 Z3 进行评估. edge("som1","som3").边缘(“som2",“som4").边缘(“som4",“som1").边缘(“som3",“som4").路径(x,y): - 边缘(x,y).% x 和 y 是字符串路径(x,z):-边(x,y),路径(y,z).:- 路径(x,y), 路径(y,x).%循环路径. 我的问题是如何编写 ..
发布时间:2021-10-04 20:42:22 其他开发

简化模型中的函数解释

在 SMT:检查函数的唯一性和完整性中,我给出了函数公理化并要求 Z3 提供模型.但是,由于解决带有量词的问题通常是不可判定的,因此 Z3 超时. 这是一个修改版本,其中“int"大小写被建模为单个值: (declare-datatypes()((ABC int error none)))(declare-fun f (ABC ABC) ABC)(assert (forall ((x AB ..
发布时间:2021-10-04 20:42:17 其他开发

Z3 中的程序附件

我正在使用 z3py 我有一个关于需要使用自定义算法评估的两个整数的谓词.我一直在努力实现它,但没有取得多大成功.显然,我需要的是一个程序附件,现在已弃用.有人能告诉我如何在 z3py 中实现这个吗?我知道它涉及使用 Tactics,但恐怕我还没有弄清楚如何使用它们.我也不介意使用已弃用的方式,只要它有效. 解决方案 没有程序附件策略.所有战术都在Z3内部实施;你可以从外面制定战术.以前版 ..
发布时间:2021-10-04 20:41:51 其他开发

获取一个Z3模型名对应的python变量名

有没有办法得到一个z3模型名对应的python变量名? 假设我有以下代码: from z3 import *s = 求解器()a = [Real('a_%s' % k) for k in range(10)]对于范围内的我(10):s.add(a[i] > 10)s.check()m = s.model()对于 m 中的 d:打印(d,m[d]) 这里m中的d是a_0,a_1,a_2,. ..
发布时间:2021-10-04 20:41:30 Python