我最近观察到Z3中有关触发的几种行为,我不明白.不幸的是,这些例子来自大型Boogie文件,所以我想我现在抽象地描述它们,只是为了看看是否有明显的答案.但是,如果具体文件会更好,我可以附加它们.
基本上有三个问题,尽管第三个可能是第二个问题的特例.据我所知,没有任何行为是预期的,但也许我错过了一些东西.任何帮助将不胜感激!
首先:就触发而言,我的程序中的琐碎平等似乎被忽略了.例如,if t1是一个应该与量化公理的模式匹配的术语,如果我在表单的Boogie程序中添加一行
assert t1 == t1;
然后t1似乎没有被用作量化公理的触发器.我明确地添加了这一行,以便为t1证明者提供触发器,我经常在Boogie程序中做/做.
相反,如果我引入了额外的功能,比方说
function f(x : same_type_as_t1) : bool
{ true }
现在改为添加一行
assert f(t1);
我的节目,然后t1 就似乎被用来作为Z3的触发器.我检查了前程序的Z3翻译,并且(平凡的)平等t1确实在Boogie翻译中存活下来(即,不是Boogie尝试做一些聪明的事情).
其次:次要模式似乎对我不起作用.例如,我有一个程序,其中一个公理有形式
axiom (forall ... :: {t1,t2} {t3,t4,t5} ..... );
和一种情况,t3, t4并t5都发生了.程序无法验证,显然是因为公理没有实例化.但是,如果我重写公理为
axiom (forall ... :: {t3,t4,t5} {t1,t2} ..... );
然后程序验证.在这两种情况下,运行Boogie的时间大约为3秒,并且模式可以存活到Z3输出.
第三:这很可能是第二个问题的症状,但我对以下行为感到惊讶:
我写了这个形式的公理
axiom (forall .. :: {t1,t2} .... );
axiom (forall ... :: {t2,t4} {t2,t3} ...some expression involving …有等式Pell x*x - 193 * y*y = 1
在z3py:
x = BitVec('x',64)
y = BitVec('y',64)
solve(x*x - 193 * y*y == 1, x > 0, y > 0)
结果: [y = 2744248620923429728, x = 8169167793018974721]
为什么？
PS有效答案:[y = 448036604040,x = 6224323426849]
在使用z3处理我的硕士论文时,我发现了一些我无法理解的奇怪的东西.我希望你能帮助我.:)
我写的smt文件看起来像这样:
(set-logic QF_UF)
(set-info :smt-lib-version 2.0)
;Declare sort Node and its objects.
(declare-sort Node 0)
(declare-fun n0 () Node)
(declare-fun n1 () Node)
;Predicate
(declare-fun dead_0 (Node) Bool)
;Abbreviation
(declare-fun I () Bool)
;initial configuration
(assert(= I (and
(not(= n0 n1))
(not(dead_0 n0))
(dead_0 n1))))
;Predicate
(declare-fun dead_1 (Node) Bool)
;variable
(declare-fun m0_1 () Node)
;Abbreviation for Transformation
(declare-fun TL1_1 () Bool)
;Transformation1neuerKnoten1
(assert(or (= m0_1 n0)(= m0_1 n1)))
;Is the whole formula satisfiable?
(assert(= (and I TL1_1) true)) …我需要一个简单线性算术问题的定理证明器.但是,即使是简单的问题,我也无法让Z3工作.我知道它不完整,但它应该能够处理这个简单的例子:
(assert (forall ((t Int)) (= t 5)))
(check-sat)
我不确定我是否会忽略某些东西,但这应该是无足轻重的.我甚至试过这个更简单的例子:
(assert (forall ((t Bool)) (= t true)))
(check-sat)
这应该通过详尽的搜索来解决,因为启动只包含两个值.
在这两种情况下,z3以未知方式回答.我想知道我在这里做错了什么,或者如果你能为这些类型的公式推荐一个定理证明器.
.net API具有以下Context的构造函数:
Context (Dictionary< string, string > settings)
如何获取所有可能设置的列表？
具体来说,我感兴趣的是如何让Z3生产不饱和核心,即相当于SMT lib产生的不饱和核心.
我从Z3的运行中获得了几个统计数据.我需要了解这些意味着什么.对于sat和SMT解决方案的最新发展,我相当生疏,并且没有及时更新,因此我试图自己找到解释并且我可能会出错.所以我的问题主要是:
1)这些措施的名称是什么意思？
2)如果错了,你能指点我更好地理解他们所指的内容吗？
其他观察结果如下,概念上属于上述两个问题.提前致谢!
我的解释如下.
DPLL.下面的所有指标都参考了DPLL算法的行话,这是大多数求解器的基础.
决议.粗略地说,操作使解释条款成为集合; 从分辨率中获取的技术是解决SAT的另一种范例.
其他技术
其他方面
假设我在公式中有2个数组,我想用z3检查它的可满足性.如果z3返回sat,我想读入z3模型中的第一个数组,并将其打印为键,值对和默认值.后来我想将它转换为地图并对其进行进一步分析.这是我运行的示例:
void find_model_example_arr() {
std::cout << "find_model_example_involving_array\n";
context c;
sort arr_sort = c.array_sort(c.int_sort(), c.int_sort());
expr some_array_1 = c.constant("some_array_1", arr_sort);
expr some_array_2 = c.constant("some_array_2", arr_sort);
solver s(c);
s.add(select(some_array_1, 0) > 0);
s.add(select(some_array_2, 5) < -4);
std::cout << s.check() << "\n";
model m = s.get_model();
std::cout << m << "\n";
expr some_array_1_eval = m.eval(some_array_1);
std::cout << "\nsome_array_1_eval = " << some_array_1_eval << "\n";
func_decl some_array_1_eval_func_decl = some_array_1_eval.decl();
std::cout << "\nThe Z3 expr(fun_decl) for some_array_1_eval is : " << some_array_1_eval_func_decl << "\n";
// …我正在使用Z3解决八皇后难题。我知道在这个问题上每个女王可以用一个整数表示。但是，当我用两个整数表示皇后时，如下所示：
from z3 import *
X = [[Int("x_%s_%s" % (i+1, j+1)) for j in range(8)] for i in range(8) ]
cells_c = [Or(X[i][j] == 0, X[i][j] == 1) for i in range(8) for j in range(8) ]
rows_c = [Sum(X[i]) == 1 for i in range(8)]
cols_c = [Sum([X[i][j] for i in range(8)]) == 1 for j in range(8) ]
diagonals_c = [Implies(And(X[i][j] == 1, X[k][h] == 1), abs(k - i) != abs(j - h))
for i in range(8) for …当Z3中的公式不饱和并且(防止出现)时,有一个输出,我找不到任何关于它是什么的信息.我在哪里可以找到有关它的任何文件？
在我看来相当难以理解,是否有可能将此作为输入的工具？
干杯,马特
只是想知道z3py,我如何检查给定的常量表达式是变量还是值？例如
x = Int('x')
x_ = IntVal(7)
ColorVal, (White,Black) = EnumSort("ColorVal",["While","Black"])
mycolor = Const("mycolor",ColorVal)
所以x,mycolor都是变量而x_,True,False,White,Black都是值而不是变量.
z3py有is_var谓词,但出于不同的目的.如果我想将公式中的所有变量重命名为其他变量,这将非常有用.