以下脚本http://rise4fun.com/Z3Py/Cbl有什么问题？添加最后两行给出了以下错误'instancemethod' object is not #subscriptable
x,t,t1,t2,x_next=Reals ('x t t1 t2 x_next')
location,location_next=Bools('location location_next')
x=0
location=BoolVal(False)
k=20
for i in range(k):
s=Solver()
s.add(Or(And(x_next-x>=2*t,x_next-x<=3*t,x_next<=12,t>0,Not(location)),
And(x_next-x>=-2*t,x_next-x<=-t,x_next>=0,t>0,location)),location_next==If(And(Not(location),x_next>=12),True,If(And(location,x_next<=0),False,location)))
print s.check()
print s.model()
m=s.model
#x=m[x_next]
#location=m[location_next]
我正在使用Z3的Python API,试图在我正在编写的研究工具中包含对它的支持.我有一个关于使用Python接口提取不可满足核心的问题.
我有以下简单查询:
(set-option :produce-unsat-cores true)
(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(check-sat)
(get-unsat-core)
(exit)
通过z3可执行文件(对于Z3 4.1)运行此查询,我收到了预期的结果:
unsat
(__constraint0)
对于Z3 4.3,我获得了一个分段错误:
unsat
Segmentation fault
这不是主要问题,尽管这是一个有趣的观察.然后我将查询(在文件中)修改为
(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(exit)
使用文件处理程序,我将此文件的内容(在变量`queryStr'中)传递给以下Python代码:
import z3
...
solver = z3.Solver()
solver.reset()
solver.add(z3.parse_smt2_string(queryStr))
querySatResult = solver.check()
if querySatResult == z3.sat:
...
elif querySatResult == z3.unsat:
print solver.unsat_core()
我从`unsat_core'函数接收空列表:[].我是否正确使用此功能？该函数的文档字符串表明我应该做类似的事情
solver.add(z3.Implies(p1, z3.Not(0 == 0)))
但是,我想知道是否仍然可以按原样使用查询,因为它符合SMT-LIB v2.0标准(我相信),以及我是否遗漏了一些明显的东西.
我一直在努力解决一个包含某些术语绝对值的小问题.在z3中,不支持abs()函数.在python中有,但我最终必须将它传递给z3py.有什么方法可以通过它将绝对运算符的术语从python传递给z3,还是有其他方法吗？以下是一个小例子的代码.
`
x = Int('x')
y = Int('y')
x= abs(2-y)
s=Solver()
s.add(x>0)
s.add(y>0)
s.check()
m=s.model()
print m`
答案应该是y = 1,这是删除abs()时的情况.有没有办法用绝对值函数来解决这个问题？ABS().或者有什么方法可以在python中解决它,然后我可以将它传递给z3.我也尝试过同情,但它不起作用.
In following Python code:
from itertools import product
from z3 import *
def get_sp(v0, v1):
res = sum([v0[i] * v1[i] for i in range(len(v0))])
return res
def get_is_mod_partition(numbers):
n = len(numbers)
mod_power = 2**n
for signs in product((1, -1), repeat = len(numbers)):
if get_sp(numbers, signs) % mod_power == 0:
return 1
return 0
def check_sat(numbers):
n = len(numbers)
s = Solver()
signs = [Int("s" + str(i)) for i in range(n)]
for i in range(n):
s.add(Or(signs[i] == -1, signs[i] == 1)) …我想使用 Int 向量作为数组索引。
Python。
array = [12,45,66,34]
s= Solver()
x = Int('x')
s.add(array[x] == 66)
所以 x 应该是 2..
我该怎么做？
这是一个由三部分组成的问题，涉及 Z3 (Z3Py) 的 Python API 的使用。
我以为我知道常量和变量之间的区别，但显然不知道。我想我可以声明一种排序并实例化该排序的变量，如下所示：
Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
n1 = Node('n1') # c.f. x = Int('x')
但是 python 抛出一个异常，说你不能“调用 Node”。似乎唯一有效的是声明n1一个常量
Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
n1 = Const('n1',Node)
但我对此感到困惑，因为我认为 a1,a2,a3 是常数。也许 n1 是一个符号常量，但我如何声明一个实际变量？
如何创建常量集？我尝试从一个空集开始并添加到其中，但这不起作用
Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
n1 = Const('n1',Node)
nodes = EmptySet(Node)
SetAdd(nodes, a1) #<-- want to create a set {a1}
solve([IsMember(n1,nodes)])
但这不起作用 Z3 没有返回任何解决方案。另一方面，将第三行替换为
nodes = Const('nodes',SetSort(Node))
现在过于宽松，允许 Z3 将节点解释为满足公式所需的任何节点集。如何只创建集合 {a1}？
除了看起来有点麻烦的数据类型声明之外，是否有一种简单的方法来创建对？例如
Edge = Datatype('Edge')
Edge.declare('pr', ('fst', Node), ('snd',Node)) …我想提高 SMT 求解的可扩展性。我实际上已经实现了增量求解。但我想提高更多。在不了解问题本身的情况下，还有其他一般方法可以改进它吗？
我是 Z3 的新手，正在尝试制作一个求解器，将每个可满足的解决方案返回到布尔公式。从其他 SO 帖子中记下笔记，我已经编写了我希望能起作用的代码，但事实并非如此。问题似乎是，通过添加以前的解决方案，我删除了一些变量，但它们又在后面的解决方案中返回了？
目前我只是想解决a或b或c。
如果我解释得不好，请告诉我，我会尽力进一步解释。
预先感谢您的回复:)
我的代码：
from z3 import *
a, b, c = Bools('a b c')
s = Solver()
s.add(Or([a, b, c]))
while (s.check() == sat):
print(s.check())
print(s)
print(s.model())
print(s.model().decls())
print("\n")
s.add(Or([ f() != s.model()[f] for f in s.model().decls() if f.arity() == 0]))
我的输出：
sat
[Or(a, b, c)]
[c = False, b = False, a = True]
[c, b, a]
sat
[Or(a, b, c), Or(c != False, b != False, a != True)]
[b = True, …from z3 import *
p = Int('p')
q = Int('q')
solve(Or(p==1,p==2,p==3), Or(q==1,q==2), Not(p==q), q==1)
给我[p = 2, q = 1]，但 p 可能是 2 或 3。所以答案应该是 {2,3}。我如何告诉 z3 通知我多个答案？
我对 SAT 和 Z3 很陌生（甚至还没有开始使用 SMT）。我一直在玩gophersat（一个很好的 Go 实现，可以解决一系列很好的 SAT 问题），我在那里发现了 DIMACS 格式。尽管我同意这不是使用变量的最佳方式，但对于一些简单的测试，我发现它非常方便。我尝试检查是否有直接方法从 Z3 中的 DIMACS 文件读取、解析和构造 SAT 公式。我没有找到任何（如上所述，我很新，所以我可能不知道它的存在）。所以我最终编写了以下代码。我想知道人们对此有何看法以及是否有更好的方法来实现同样的目标。
\n（注意：我没有对公式的子句数量和/或变量数量进行任何检查）
\nfrom z3 import *\n\n\ndef read_dimacs_and_make_SAT_formula(file_name: str):\n vars = dict()\n base_name = "x"\n with open(file_name, "r") as f:\n for idx, line in enumerate(f):\n if line.strip() != "\\n" and line.strip() != "" and line.strip() != "\\r" and line.strip() != None and idx > 0:\n splitted_vals = line.split()\n for element in splitted_vals:\n if int(element) != 0:\n if int(element) > 0 …