1回答
Z3:在C++中优化超时
、、、
我正在尝试理解如何使用C++ API为Z3的optimize类设置超时。这是我的代码：optimize opt(c);par.set("timeout", 1000);但是我在opt.set(par)行上得到了“未知参数‘超时’”异常。是否可以设置优化类的超时时间(在超时后，我希望获得找到的最佳解决方案)
浏览 4提问于2016-07-30得票数 1
2回答
Z3优化的超时
、、、、
如何为z3优化器设置超时，以便在时间耗尽时为您提供最知名的解决方案？from z3 import *# Hard Problemprint(s.model())
后续问题，你能把z3设置为随机爬山，还是它总是执行一个完整的搜索
浏览 5提问于2020-03-25得票数 3
回答已采纳
是否可以使用C API在运行时更改求解器的超时值？为了设置超时，可以执行以下操作：Z3_set_param_value(cfg, "SOFT_TIMEOUT", "10000") //Z3_check_and_get_model(ctx);
但是，假设我们想要在保留上下文的同时更改下一次查询的超时，是否可以在两者之间更改超时值？
浏览 2提问于2012-05-31得票数 1
回答已采纳
我在z3 shell和java api中都尝试了相同的假设。declare-const x (_ BitVec 32))
(check-sat)在z3外壳中，解决方案是:x=9，但在z3应用程序接口中，解决方案是:x= 0x80000000在我的应用程序中，我更喜欢外壳结果。所以我想知道我是否错过了API使用
浏览 0提问于2016-11-08得票数 1
对于我的应用程序代码，我为我的求解器使用了以下z3参数设置 p.set(":relevancy", static_cast<unsigned>(1)); p.set(":timeout", timeout); 在更新到最新的Z#不稳定之后，我得到了C++异常，本质上说逻辑和超时不
浏览 2提问于2015-01-26得票数 0
回答已采纳
1回答
Z3时间限制优化
、、
我已经看到Z3通过assert支持优化。据我所知，如果给出足够的时间，Z3将报告给定SMT公式的最优解。但是，我感兴趣的是是否有可能在有限的时间内运行Z3，并让它报告它能够找到的最佳解决方案(这并不一定意味着它是最佳解决方案)。如果我在SMT公式上运行Z3并限制时间(通过参数-T)，如果它没有最优地解决这个问题，它只会报告‘超时值’。
浏览 6提问于2015-11-23得票数 0
回答已采纳
1回答
Z3优化超时
、、
我想在z3中设置一个超时，这样我就不会得到一个最优的解决方案，而是一个符合约束的解决方案。solver.Check();}因此，我现在的问题是，在超时后如何获得到目前为止的最佳解决方案，以及如何将其与MkOptimize一起使用
浏览 2提问于2017-06-27得票数 1
1回答
我在为求解器设置超时时遇到问题：encoding = parse_smt2_file("ex.smt2")
s.set("timeout",File "/Users/X/Documents/encode.py", line 108, in parse_polyedra s.set("timeout",1) File "/Users/X/z3
浏览 4提问于2015-02-05得票数 1
我试图最小化一个变量，但是z3需要很长时间才能给出一个解决方案。如果是的话，我该怎么做？
提前行动！
浏览 1提问于2019-03-26得票数 1
回答已采纳
我正在试验Z3 (使用python api)，其中我正在为类赋值构建一个调度模型，其中我必须经常使用模(因为它是周期性的)。模运算似乎已经使z3减慢了很多，但是如果我尝试在顶部做一些优化(最小化一个成本函数，这是一个和)，那么对于相当小的问题需要相当长的时间。在没有优化的情况下，它可以很好地工作(对于较小的问题，需要几秒钟)。话虽如此，我现在有两个问题：
1)如何使用模函数有什么窍门吗？我已经将模数值赋给了一个函数。此外，我认为如果我使用超时选项solver.set(&
浏览 1提问于2018-06-28得票数 2
在这个例子中，我试图让z3求解器在0.1s后超时(考虑两个素数的32位乘积)，使用C++接口。它在Windows (VC++，2013年)上工作，但在Linux (CentOS 6.5)上不起作用，解决程序在大约2.5s (调试构建)内完成。表示，2012年z3 v3.2只支持z3命令行超时，但这应该在下一个版本中得到解决--根据RELEASE_NOTES的说法，我们使用的是z3 v4.4。我是否对
浏览 5提问于2015-06-17得票数 0
回答已采纳
1回答
使用z3解决大型优化问题，这不太可能在合理的时间内达到最优。有什么办法可以得到中间解决方案吗？也许可以设置一个内部超时，这样它就可以提供到目前为止找到的最佳解决方案？谢谢，Ofer
浏览 0提问于2016-03-08得票数 2
1回答
我目前正在使用Z3 C++ API来解决位向量上的查询。有些查询可能在顶层包含一个存在量词。
通常情况下，量词消除很简单，并且可以由Z3快速执行。但是，在量词消除返回到枚举数千个可行解决方案的情况下，我想放弃这一策略，并以其他方式处理查询。在一个中，一个类似的问题被讨论，而'smt‘策略被指责没有反应。同样的理由也适用于“量化宽松”策略吗？但同一篇文章指出，“未来”版本应该更有响应性。是否有任何方法或启发式来确定量词消除是否需要长时间的(除了在单独的线程<em
浏览 5提问于2015-09-06得票数 4
回答已采纳
1回答
有没有一种方法可以像在Python中那样以人类可读的形式打印AST？我想要一些像这样的东西而不是
(and (= x 3) (> (f 3) 2)
浏览 2提问于2013-04-23得票数 1
回答已采纳
我看到了一个，它谈到了如何使用z3的python来获得最小化问题的次优解。我使用z3 -t:140000 smt2 <filename>将超时设置为140秒。但是z3求解器返回未知值(而不是sat和一个非零的目标值)。我也尝试了超时145秒，并看到了类似的结果。当我将超
浏览 2提问于2018-01-25得票数 3
回答已采纳
1回答
我对Z3给我一个模型感兴趣，同时如果它试图将一个目标函数考虑为启发式，我会很高兴，但我不想支付寻找实际(最大)imum的性能损失。
这在Z3中是可能的吗？
浏览 0提问于2018-03-02得票数 1
回答已采纳
1回答
我正在试验优化使用Z3来证明一阶理论的事实.目前，我在Python中指定了一阶理论，将量词放在那里，并将所有子句连同证明目标的否定一起发送给Z3。我有以下的想法，我希望能优化结果:我只想把理论中的公式发送给Z3，这些公式与证明目标相关。我不打算详细讨论这个概念，但我认为直觉很简单:我的理论是公式的结合，我只想发送可能影响证明目标的真值的连词。我的问题是:这能导致效率的提高吗，还是Z3已经使用了类似的方法？我想不会，因为我不认为Z3总是
浏览 4提问于2012-12-21得票数 1
回答已采纳
1回答
我想在C++中使用Z3，并且我遵循了安装指南-- 。
我成功构建了它，然后我还将构建路径添加到了系统路径中。然而，当我试图运行文件时，我仍然得到一个错误。谁能告诉我，在使用Visual Studio Command Prompt成功构建Z3之后，为了在c++中运行Z3，我还需要进行其他配置吗？
浏览 10提问于2018-08-24得票数 1
回答已采纳
1回答
我想学习用于c++的z3 API以及如何在c++程序中使用它们。我试着找一个教程，但是找不到。我可以从哪里学到呢？有什么教程什么的吗？谢谢。
浏览 1提问于2013-07-08得票数 1
1回答
z3最小化和超时
、、
我尝试使用z3求解器来解决最小化问题。我试图得到一个超时，并返回到目前为止最好的解决方案。我使用python，超时选项"smt.timeout“与这实际上是在大约1秒后超时。如果它试图连续地评估我的目标的较大值，那么当超时发生时，它不应该找到一个可满足的实例.
编辑：在opt.maxres日志中，上限永不缩小。为了记录在案，
浏览 1提问于2016-02-04得票数 4
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
腾讯会议
云直播活动推荐
腾讯云开发者
