Z3会支持AUFBV吗？
对于以下脚本:
(set-logic AUFBV)
(declare-fun x () (_ BitVec 16))
(declare-const t (Array (_ BitVec 16) (_ BitVec 16)))
(assert (= (select t #x0000) #x0000))
在线Z3演示似乎是高兴的set-logic呼叫,但随后抱怨的种类BitVec和Array.(顺便提一下,set-logic无论逻辑名称如何,在线演示似乎都对通话感到满意,即使是伪造的名字,例如(set-logic blarg).)
SMT-Lib网站既没有提及UFBV也没有提到AUFBV,但鉴于他们的无量词对应物(QF_UFBV和QF_AUFBV),我希望Z3也能支持AUFBV.
不用说,阵列在实践中起着非常重要的作用.我认为,鉴于有限性论证,AUFBV逻辑应保持可判定性.看到Z3支持它真的很高兴.
谢谢!
我有一些简单的约束,涉及生成的z3中的实数乘法unknown.问题似乎是它们被包装在数据类型中,因为展开的版本会产生sat.
这是一个简化的案例:
(declare-datatypes () ((T (NUM (n Real)))))
(declare-const a T)
(declare-const b T)
(declare-const c T)
(assert (is-NUM a))
(assert (is-NUM b))
(assert (is-NUM c))
(assert (= c (NUM (* (n a) (n b)))))
(check-sat)
;unknown
没有数据类型:
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (= c (* a b)))
(check-sat)
;sat
我正在使用z3 3.2,但这也可以在网络界面中重现.
我在Linux上使用Z3 4.1 C-API。我想为求解器指定一个超时。
我正在使用以下命令，但是在命令Z3_solver_set_params（）中出现分段错误。
Z3_context ctx = mk_context();
Z3_solver s = Z3_mk_solver(ctx);
Z3_params params = Z3_mk_params(ctx);
Z3_symbol r = Z3_mk_string_symbol(ctx, ":timeout");
Z3_params_set_uint(ctx, params, r, static_cast<unsigned>(10));
Z3_solver_set_params(ctx, s, params);
看来我没有正确使用API。
我在包含示例的test_capi.c文件中找不到用于C-API设置求解器超时的任何示例。有人可以帮忙吗？
我在以下链接http://research.microsoft.com/en-us/um/redmond/projects/z3/group_ maxsat _ex.html中找到了"MaxSAT/MaxSMT示例", 但它只提供C代码.
我对如何使用Z3直接编码感兴趣？有人可以给我一个例子吗？谢谢!
我在Z3中使用muZ,它有这个新的广义PDR.我想知道如何获得有关PDR算法的一些数据.PDR算法的不变量如下:
I => F_0
F_i => F_{i+1} for 0 <= i < k
F_i => P for 0 <= i <= k
F_i /\ T => F'_{i + 1}
我真的对终止时k的价值感兴趣.这个统计数据是否以某种方式提供？如果我在查询中启用:print-statistics true,我看不到它:
(query (p x) :print-statistics true)
我在 Z3 python 中有这个代码：
x = Bool('x')
y = Bool('y')
z = Bool('z')
z == (x xor y)
s = Solver()
s.add(z == True)
print s.check()
但是此代码在运行时报告以下错误：
c.py(4): error: invalid syntax
如果我替换xor为and，则没有问题。所以这意味着不支持异或？
我是使用 Z3 的新人。
想知道如何计算一组和两个不同组的最大值。
例如：
[1, 6, 5]- 较大的是 6
[1, 6, 5]e [10, 7, 2]- 较大的是 6
我使用以下代码进行设置：
(declare-sort Set 0)
(declare-fun contains (Set Int) bool)
( declare-const set Set )
( declare-const distinct_set Set )
( declare-const A Int )
( declare-const B Int )
( declare-const C Int )
( assert ( = A 0 ) )
( assert ( = B 1 ) )
( assert ( = C 2 ) )
( …我想使用 z3 求解器使用 C API 定义一个二维数组如下
a[3][3] = { {0,0,0},{0,0,0},{0,0,0}}
如何使用 Z3 求解器 C API 定义它，其中我需要添加约束，例如每行的总和等于 1，并且每个颜色的总和应该 <= 100。
多年来,我一直在追踪解决技术的问题 - 我还有一篇关于将它们应用于特定难题的博客文章 - "穿越梯子".
为了达到目的,我偶然发现了z3,并尝试将其用于特定问题.我使用了Python绑定,并写了这个:
$ cat laddersZ3.py
#!/usr/bin/env python
from z3 import *
a = Int('a')
b = Int('b')
c = Int('c')
d = Int('d')
e = Int('e')
f = Int('f')
solve(
a>0, a<200,
b>0, b<200,
c>0, c<200,
d>0, d<200,
e>0, e<200,
f>0, f<200,
(e+f)**2 + d**2 == 119**2,
(e+f)**2 + c**2 == 70**2,
e**2 + 30**2 == a**2,
f**2 + 30**2 == b**2,
a*d == 119*30,
b*c == 70*30,
a*f - 119*e + a*e == …p = Int('p')
q = Int('q')
s = Solver()
s.add(1<=p<=9, 1<=q<=19, 5<(3*p-4*q)<10)
s.check()
print s.model()
返回sat,并给出解决方案
[p = 0, q = 0]
这不符合约束.如果我删除最后的约束,它将返回一个满足前两个(平凡)约束的合理对.这是怎么回事？
永久链接在线试用:http://rise4fun.com/Z3Py/fk4
编辑:我是z3的新手,所以有可能我做了一些可怕的错误,让我知道.