gpt4 book ai didi

.net - Z3 中的 TryFor 在给定的时间限制后不会停止检查

转载 作者:行者123 更新时间:2023-12-04 20:16:17 25 4
gpt4 key购买 nike

我正在使用 Z3 的 .NET API。当我通过调用实例化求解器时:

Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit));

并为某些模型指定 60 秒(60000 毫秒)的 TimeLimit
s.Check()

60 秒后不返回。对于某些型号,它会在几秒钟后返回,在我的情况下这不是问题,但对于某些型号,它根本不会返回(我在 3 天后取消了该过程)。

如何在给定的时间限制后强制 Z3 停止检查?

最佳答案

TryFor组合器是使用“取消”标志实现的。新战术 react 灵敏,并在设置“取消”标志时很快终止。不幸的是,通用策略 smt是通用求解器的封装。这个通用求解器 react 不灵敏。它可能在几个关键位置“丢失”:量词实例化、Simplex 等。qflia策略建立在 smt 之上和许多其他策略。因为,您正在尝试解决无量词问题。我假设 smt策略在 Simplex 模块内部的循环中。 smt 中的 Simplex 模块策略是使用任意精度有理数实现的。因此,对于非平凡的线性实数/整数问题可能非常耗时。

要解决此问题,您无能为力。如果你真的需要强有力的运行时间保证,我看到的唯一解决方案是创建一个运行 Z3 的单独进程,并在需要更多 k 时将其终止。秒解决问题。

话虽如此,Z3 的 future 版本将拥有一个全新的算术模块。当取消标志设置时,这个新模块(如新策略)将快速终止。

关于.net - Z3 中的 TryFor 在给定的时间限制后不会停止检查,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/11923957/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com