我使用 Z3 来解决符号执行器产生的路径条件,该执行器以深度优先顺序探索状态空间,与 CUTE、DART 或(可能)SAGE 非常相似。我们正在尝试使用 Z3 的不同方式。在一种极端情况下,我们将每个查询发送到 Z3 并在之后立即(重置)它。另一方面,我们(推送)每个附加分支约束,并在回溯时(弹出)正确削弱路径条件所需的最小值。问题是,似乎没有一种策略在所有情况下都比其他策略更有效。推送似乎提供了最好的优势,但我们遇到了一些情况,在每次查询后重置 Z3 比推送/弹出快一个数量级以上。请注意,通信开销可以忽略不计:几乎所有时间都花在 check-sat 内。
有没有人有任何经验可以分享,或者关于 Z3 内部保存的状态的一些指示(引理等),这可以帮助澄清其行为?其他 SMT 求解器的行为又如何呢?
下一个版本(v4.3.2)将公开一个可能对您有用的功能。在 Z3 中,默认求解器结合了非增量求解器和增量求解器。什么时候push
/pop
被使用(或多个check
使用 s 而不调用reset
),Z3将使用增量求解器。在下一个版本中,我们可以为增量求解器提供超时。如果增量求解器在给定的超时时间内无法解决问题,Z3 将自动切换到非增量求解器。也许,如果您使用此功能,您将能够获得“两全其美”的好处。要获取下一个候选版本的源代码,您应该使用
git clone https://git01.codeplex.com/z3 -b rc
为了编译它,我们使用
cd z3
python scripts/mk_make.py
cd build
make
要设置增量求解器的超时,我们必须提供以下命令行选项:
combined_solver.solver2_timeout=<time in milliseconds>
如果您使用的是编程 API,则可以使用新 API:
Z3_global_param_set(Z3_string param_id, Z3_string param_value)
请注意,下一个版本将有一个新的参数设置框架。它允许用户设置内部 Z3 模块的参数。
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)