标签: z3py

假设这a是一个8位值的整数254.如果a是有符号整数,则实际考虑它-2.相反,如果a是未签名的,它仍然存在254.

我试图用Z3的BitVector理论模拟这个有符号/无符号整数问题,但似乎BitVector不允许这样做.这是真的？那么关于如何在Z3py中对此进行建模的任何想法？

非常感谢.

由于某些安全问题,rise4fun z3py在几周内无法使用.我试图找出一些学习z3py的资源,但结果徒劳无功.请提供一些资源来学习z3py

我试图在矩阵上执行一些符号计算(用符号作为矩阵的条目),之后我会有一些可能的解决方案.我的目标是根据约束选择解决方案/解决方案.

例如,M是一个矩阵,其中一个元素作为symbol.该矩阵将具有2个特征值,一个是正的,一个是负的.使用z3我试图找出唯一的负值,但我无法这样做,因为a被定义为一个符号,除非我将其转换为实际值,否则我不能将其写为约束.

我该怎么办？是否有任何方法可以将(符号)转换为实数或整数,以便我可以将其用作约束s.add(a>0)

from sympy import* 
from z3 import* 
from math import*

a=Symbol('a')

M=Matrix([[a,2],[3,4]]) m=M.eigenvals();

s=Solver()

s.add(m<0)
print(s.check())
model = s.model() print(model)

假设我有一个z3求解器，其中包含一定数量的可满足的已声明约束。假设S为一组约束，我想为S中的每个约束验证将约束添加到求解器时公式是否仍可满足要求。可以通过以下方式轻松地按顺序完成此操作：

results = []

for constraint in S:
  solver.push()
  solver.add(constraint)
  results.append(solver.check() == z3.sat)
  solver.pop()

print all(results)

现在，我想并行化它来加快处理速度，但是我不确定如何使用z3正确地执行此操作。

这是一个尝试。考虑下面的简单示例。所有变量都是非负整数，并且必须求和为1。现在，我想验证每个变量x是否可以独立地设为> 0。令x = 1并将0赋给其他变量。这是一个可能的并行实现：

from multiprocessing import Pool
from functools import partial
import z3

def parallel_function(f):
    def easy_parallize(f, sequence):
        pool   = Pool(processes=4)
        result = pool.map(f, sequence)

        pool.close()
        pool.join()

        return result

    return partial(easy_parallize, f)

def check(v):
    global solver
    global variables

    solver.push()
    solver.add(variables[v] > 0)
    result = solver.check() == z3.sat
    solver.pop()

    return result

RANGE = range(1000)
solver = z3.Solver()
variables = [z3.Int('x_{}'.format(i)) for i in …

我正在修改一个使用Z3(特别是Python API)来解决bitvector约束的工具.我需要使用一个特定的外部SAT求解器而不是内部的Z3求解器,所以我首先使用这个策略进行爆破

Then('simplify', 'bit-blast', 'tseitin-cnf')

之后我可以相对容易地将子句转储到DIMACS文件中.问题是将得到的命题模型映射回原始约束的模型:据我所知,Python API没有提供访问对应于策略的模型转换器的方法.这是真的？如果是这样,是否可以使用不同的API完成,或者是否有更简单的方法？基本上我只需要知道最终CNF子句中的命题变量如何与原始的bitvector变量相对应.

我正在研究Python中的一个程序,其中一小部分涉及优化方程/不等式系统.理想情况下,我本来想做的就像在Modelica中一样,写出方程并让解算器处理它.

解算器和线性编程的操作有点超出我的舒适范围,但我决定尝试.问题是程序的一般设计是面向对象的,组合方程有许多不同的可能性,以及一些非线性,所以我无法将其转化为线性规划问题(但我可能错了).

经过一些研究,我发现Z3求解器似乎做了我想要的.我想出了这个(这看起来像我想要优化的典型情况):

from z3 import *

a = Real('a')
b = Real('b')
c = Real('c')
d = Real('d')
e = Real('e')
g = Real('g')
f = Real('f')
cost = Real('cost')

opt = Optimize()
opt.add(a + b - 350 == 0)
opt.add(a - g == 0)
opt.add(c - 400 == 0)
opt.add(b - d * 0.45 == 0)
opt.add(c - f - e - d == 0)
opt.add(d <= 250)
opt.add(e <= 250)

opt.add(cost == If(f > 0, …

我无法让任何 z3py 示例正常工作。我能够使用 github 上的自述文件中的说明成功安装它。我成功更新了 python 路径以指向适当的目录。此外，我能够成功导入 z3，但每次声明变量时都会出现错误。编译器无法识别 Int、Ints、Real 和 RealVal。

我举了一个例子来说明。

代码：

from z3 import *
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

错误：回溯（最近一次调用）：文件“test.py”，第 3 行，在 x = Int('x') 中 NameError: 名称 'Int' 未定义

我真的很感激任何帮助。太感谢了。

在Z3中,它支持String和Sequence.但Z3py是否也支持它们,或者我们必须使用Python中的字符串或列表？从最新版本开始,似乎新版本确实支持String和Sequence的理论,但我不知道如何使用它.有人会给我一个关于序列的例子吗？

我正在 python 中试验 z3。我有以下模型：

(set-option :produce-models true)
(set-logic QF_AUFBV )
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun another () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (and  (=  false (=  (_ bv77 32) (concat  (select  a (_ bv3 32) ) (concat  (select  a (_ bv2 32) ) (concat  (select  a (_ bv1 32) ) (select  a (_ bv0 32) ) ) ) ) ) ) (=  false (=  (_ bv12 32) …

如何为 z3 优化器设置超时，以便在超时时为您提供最知名的解决方案？

from z3 import *
s = Optimize()
# Hard Problem
print(s.check())
print(s.model())

后续问题，你可以将z3设置为随机爬山还是始终执行完整搜索？