我正在尝试使用Z3来解决一个随机的广义条带打包问题(LRA)，我在c程序中调用了Z3 api，下面是代码。0);我也尝试通过命令"z3smttest“来解决终端中的smttest问题。然而，在终端上，它的运行速度比在c
浏览 4提问于2016-09-22得票数 1
回答已采纳
1回答
我想使用Z3通过SBV使用多核。 --我应该能够通过将parallel.enable=true传递给命令行中的z3可执行文件来做到这一点。由于我使用的是SBV，所以我需要通过SBV与各种SMTLib解决程序的接口，下面是我所尝试的： ...(SBV.solver z3) cfg ++ ["parallel.enable=true"]
浏览 7提问于2020-07-30得票数 0
2回答
是否有z3支持的所有理论/逻辑的完整列表？我查阅了这个提供了许多逻辑的，但我不认为这个列表是详尽无遗的。z3文档本身似乎没有指定支持哪些逻辑。我之所以这样问是因为我有一个smt文件，它不能在中的任何逻辑下解决(当用‘set逻辑’指定时)，但是在没有指定逻辑的情况下可以解决。
浏览 6提问于2014-05-03得票数 6
回答已采纳
1回答
这个初始模型是解决类似查询的结果，很可能这个模型有一个正确的部分，甚至可能对当前查询是真的。目前，我正在使用增量求解和来模拟这一点; an initial model, which may be (partiallybe used as initial below
(check-sat) ; Z3will use trans_assumed
浏览 0提问于2012-03-27得票数 2
回答已采纳
我想运行Z3Py (使用Python的Z3应用程序接口)。我下载了Z3 v4.3.1，使用Macports-2.1.2安装了clangv2.9，最后，当我为Z3运行时>.*** [shell/datalog_frontend.o] Error 127我不
浏览 1提问于2012-12-05得票数 1
回答已采纳
考虑到与ES5相比，在某些操作上ES6代码的V8执行速度较慢。谁能指出一篇文章/论文/帖子，其中执行了测试，以找出这种性能差异是否会影响使用node.js开发的应用程序接口的正常操作？
浏览 1提问于2019-07-10得票数 0
2回答
z3比工具SAT慢得多。为什么？
、、、、
我正在为一个玩具尝试不同的解决方案，并惊讶地发现使用似乎比快得多。考虑到z3在发布的基准测试中表现得如此出色，我想知道我是否做错了什么。z3查找最大团大小：z3.set_option(verbose=1)for i in range(num_variables):结果表明，使用SAT的工具在默认情况下是多核的，使用</
浏览 21提问于2022-04-05得票数 0
回答已采纳
我已经使用C#的Z3应用程序接口开发了一个win-form应用程序。该应用程序可以在我用来开发的计算机上成功运行。打包的应用程序无法在开发计算机以外的计算机上成功运行。错误信息:运行时无法加载z3.dll。我应该怎么做才能解决这个问题？
浏览 0提问于2012-07-05得票数 1
我有一个很大的文件，我必须发送到一个网络应用程序接口client...The数据是多部分。问题是，如果文件是通过http web请求发送的，那么它会被快速上传到webapi上。如果相同的文件是通过Httpclient (.net 4.5)发送的，则与http web请求相比，上传速度较慢。我在Httpclient post async中使用了multipartformdatacontent。
那么，对于大文件，我们必须只使用web请求吗？
浏览 3提问于2014-03-06得票数 47
我正在使用z3py。我试图对不同大小的问题进行可满足性检验，并验证了该方法的可扩展性。然而，要做到这一点，我需要知道每个问题的解决者所消耗的内存。是否有一种方式访问内存或使z3py打印它在统计部分。Update-27/5/2015:
我试过使用paython内存分析器，但是生成的内存似乎非常大。我不确定，但报告的内存类似于python应用程序消耗的内存，而不仅仅是z3 (构造z3模型，检查sat，然后生成模型)。此外，多年来我一直使用正式的建模检查工
浏览 6提问于2015-05-25得票数 1
我使用hatt库来解析布尔表达式。
不幸的是，SBV似乎不适合于相当快的SAT求解，或者"allSat“函数找出所有的模型没有实现的速度。毕竟，SBV的目标是解决SMT问题。与picosat相比，我使用Z3和CVC4测试了haskell包的性能。我使用了一个包含36个变量和840个有效模型的命题公式。picosat的结果是它花了0.5秒，而Z3花了3分钟，CVC4花了6分钟。或者有一些关于SBV和"allSat“函
浏览 1提问于2014-04-26得票数 4
3回答
有没有办法从javascript中运行Z3求解器？或者有没有更好的SMT求解器，可以在JavaScript中使用？
浏览 1提问于2015-09-28得票数 7
我正在使用Z3源目录中的以下(标准)命令从源代码中使用OCaml编译Z3：然后从然后运行和出现以下错误：
Cannot load required shared library dllz3ml.对于识别问题，以及如何解决问题，有什么建议吗？
浏览 35提问于2019-07-17得票数 2
回答已采纳
1回答
我用SMT-LIB的Z3方言编写了一个大型的库。不幸的是，我使用(declare-datatypes)来创建元组意味着我不能按我希望的那样将逻辑设置为QF_AUFBV。这样做的副作用是，与以编程方式手动创建公式并使用QF_ABV求解时相比，这会使我的脚本速度变慢(有时超时)。因此，我想从我的脚本中删除(declare-datatypes)。有没有一种解决方案可以让我在仍然使用QF_AUFBV逻辑的情况下进行这样的排序？
浏览 2提问于2014-02-04得票数 1
4回答
我想知道SMT求解器是否可以帮助解决这个问题。我了解到Z3支持quantifiers，并且能够判断布尔表达式是否可满足。但问题是，Z3是否可以帮助找到函数area的最优解。
有谁知道吗？任何关于SMT求解器，Z3或其他算法的评论将不胜感激…
浏览 0提问于2011-12-14得票数 1
回答已采纳
1回答
我希望提高SMT解决方案的可伸缩性。我实际上已经实现了增量求解。但我想要提高更多。在不了解问题本身的情况下，有没有其他通用的方法来改进它？
浏览 2提问于2019-08-26得票数 3
我正在开发一个安卓应用程序，它依赖于动态数据的.NET网络服务。因此，为了与SOAP web方法通信，我使用了KSOAP2第三方API。它工作得很好。但我需要使用KSOAP2获取每次web服务调用的往返时间，因为与在iPhone中运行的相同应用程序相比，我的应用程序运行速度较慢。所以我需要知道RTT来提高我的Android应用程序的性能。
浏览 1提问于2011-07-28得票数 2
回答已采纳
我使用PhoneGap编程，并了解到跨平台应用程序与本机应用程序相比确实会产生速度较慢的应用程序。我从学到javascript模板将显著提高我的移动应用程序的速度。
我开发单页应用程序。特别是杂志应用程序。包含一个overflow:用于页面和页面过渡的隐藏容器(CSS3转换)。我只想问我如何实现javascript模板(Mustache)来解决我的杂志应用
浏览 0提问于2011-12-24得票数 0
回答已采纳
我正在处理本机应用程序，它在调试模式上运行得非常慢。它需要大量的时间来加载和挂起多次。我在以下设备上运行我的应用程序：
使用RN版本: 0.61.4
请建议我如何在调试模式下快速运行应用程序？我还能用什么其他设备来做这个呢？
浏览 3提问于2019-11-28得票数 0
回答已采纳
云服务器
ICP备案
云直播
对象存储
实时音视频
腾讯云开发者
