0回答
Z3的运行时间分析
z3、smt、sat
我使用的是通过Z3实现的python解算器。我有源代码，我希望有一些，任何，进程正在运行的指示。是否可以使用一些详细的命令或任何东西来了解进程当前正在执行的操作？我知道它背后的算法，但我想要可视化，即使使用printf，在代码中发生了什么。
谢谢!
浏览 10提问于2016-07-18得票数 1
2回答
Z3的性能可见性
z3
有没有办法了解Z3在幕后做了什么？我希望能够看到它正在采取的步骤，他们花了多长时间，多少步骤，等等。我正在检查浮点加法/乘法硬件设计与Z3内置的浮点加法/乘法的等价性。它花费的时间比预期的要长，看看它在这个过程中到底在做什么将是有帮助的。
浏览 12提问于2020-06-24得票数 0
1回答
我刚刚下载了seq和regexp排序的基准测试(使用z3-4.3.2)。在运行"membership_1.smt2“之后，当结果未知时，会有什么问题呢？谢谢我进一步注意到，“重新开始”是不被认可的。这与z3的版本有关吗?还是您忘了一个命令行选项？
浏览 1提问于2014-07-01得票数 3
1回答
将z3符号表达式存储到字典键中的有效方法
z3、z3py
我正在使用Z3Py开发一些工具，在我的代码中，我维护多个dictionaries来跟踪一些信息。
将string表示形式存储为字典的键。然而，一些分析和观察表明，从z3表达式到string的转换需要相当长的<e
浏览 3提问于2016-09-17得票数 1
回答已采纳
2回答
使用Z3进行有界模型检查-构建表达式
z3、model-checking
我们使用Z3进行有界模型检查。为此，我们提供了一大堆如下形式的表达式：换句话说，我们通过为每个时间步长提供一个单独的表达式来编码时间流逝(步数)。显然，这导致了数千个表达式。虽然Z3解决这些问题所需的时间是可以接受的(考虑到状态机的复杂性)，
浏览 0提问于2016-07-05得票数 2
3回答
的wiki页面建议使用Z3 Axiom Profiler；然而，Z3 Axiom Profiler似乎只在Z3上可靠工作。
在没有Z3公理分析器的情况下，我怎么能很容易地得到激发最多的量词呢？
浏览 5提问于2019-01-21得票数 1
回答已采纳
1回答
是否有可能估计z3的运行时间，或者DPLL(T)算法的运行时间？即使是最坏的情况
algorithm、z3、smt
我正在致力于可视化微软z3的原型。我想知道是否有可能估计z3或算法的运行时间？如果我能得到最坏的运行时间，那就太好了。
另外，在z3中，有没有什么方法可以通过理论求解器获得每个检查进程的运行时间？谢谢你的回答。
浏览 6提问于2016-08-11得票数 0
回答已采纳
1回答
在写硕士论文的时候，我用微软的z3 smt证明器做了一些实验。在我的用例中，我需要检查包含量词的简单公式(具有相等的一阶逻辑)的可满足性(无模型)。z3在几毫秒内很好地解决了我的所有示例，除了这个示例：我使用z3 java绑定在rise4fun.com和我的电脑我意识到这样一个事实，这样的
浏览 14提问于2016-09-27得票数 1
1回答
指数型要素的Z3支持
z3、smt
我是Z3的新手，我试图了解它是如何工作的，以及它能做什么和不能做什么。我知道Z3至少支持幂(^)运算符的指数(参见、和)。我不清楚的是，这种支持有多广泛，以及z3可以对指数进行什么样的推断。下面是一个简单的例子，它涉及z3可以分析的指数要素。另一方面，下面是一个Z3无法分析的简单示例：
(define-fun exp ((x R
浏览 0提问于2018-03-22得票数 4
回答已采纳
1回答
当运行带有Z3命令选项的-st 3.1时，我会得到奇怪的统计结果。如果按Ctrl，Z3会报告total_time < time。否则，如果您等到Z3完成: total_time > time。测量“总时间”和“时间”是什么？是一个bug(虽然很小)(上面描述的差异)？
谢谢!
浏览 3提问于2011-09-07得票数 2
回答已采纳
1回答
从Z3调用外部SAT求解器
z3、smt、sat
在我工作的公司，我们可以访问多个SAT Solver。我们想要分析每个SAT求解器如何影响Z3 SMT求解器的性能。
是否可以从Z3调用外部SAT求解器？如果不是，应该在哪里修改Z3以调用外部求解器？
浏览 9提问于2016-07-18得票数 1
1回答
Z3的检查点机制
z3
我计划使用Microsoft的Z3 SMT解决程序做一些工作，它将在有执行时间限制的计算服务器上运行。我预计这项工作将超过这一限度。这样，任何进程的运行时间都不会超过执行时间限制，因此其他用户也有机会运行他们的作业，但是使用的总计算时间可以超过单个作业的超时时间。
Z3是否支持读写检查点？所谓“检查点”，我指的
浏览 5提问于2015-02-25得票数 0
回答已采纳
2回答
有一个用于调试跟踪的Z3工具，称为"Z3 Axiom“。我已经找到了，这似乎是公理分析器，并且已经有了三年的历史。从这些VCC源构建是获得分析器的正确方法，还是在某个地方有一个更新的版本？
浏览 0提问于2016-01-26得票数 2
回答已采纳
1回答
Z3时间限制优化
optimization、z3、smt
我已经看到Z3通过assert支持优化。据我所知，如果给出足够的时间，Z3将报告给定SMT公式的最优解。但是，我感兴趣的是是否有可能在有限的时间内运行Z3，并让它报告它能够找到的最佳解决方案(这并不一定意味着它是最佳解决方案)。如果我在SMT公式上运行Z3并限制时间(通过参数-T)，如果它没有最优地解决这个问题，它只会报告‘超时值’。我读到默认<
浏览 6提问于2015-11-23得票数 0
回答已采纳
1回答
我在z3中遇到了一些不寻常的运行时行为，我想问一下为什么会发生这种情况： 示例1： (set-info :smt-lib-version 2.6)
(forall ((x0 FPN)) (not (fp.geq (afun x0) x0)))(get-model)
(exit) 示例1的运行时间为~0.26s，示例2的运行时间</em
浏览 7提问于2020-12-09得票数 1
回答已采纳
2回答
我试图在SMT 2中建立一个小型编程语言的模型。我的目的是表达一些程序分析问题，并用Z3解决它们。不过，我想我误解了forall的说法。下面是我的代码片段。(= (group b1) (group b2))(check-sat)
当我运行z3 -smt2 barriers.smt2时，结果是unsat。我认为，我的<
浏览 3提问于2020-04-02得票数 0
回答已采纳
1回答
我在.Net中使用z3。我的系统上的空闲CPU使用率大约为1%到10%。当运行Z3时，我有大约30%到40%的CPU使用率(4核)。我以前用过Gurobi，大部分时间CPU使用率都是100%。有没有办法将z3配置为更多地使用cpu，从而更快地获得解决方案？
浏览 13提问于2017-07-03得票数 0
回答已采纳
这个在几乎没有时间使用Z3 4.3.2时生成了一个正确的模型，但是在Rise4fun上运行了几秒钟之后，Z3 4.4.2和超时差似乎永远运行。n=5脚本的一个版本(链接的脚本有n=4)也在4.3.2上运行了很长时间。我试着改变了sat.random_seed和smt.random_seed，但都没有效果。我还能做什么呢？
浏览 0提问于2016-03-28得票数 0
回答已采纳
1回答
从模型中获取具体的数组值
z3、z3py
我使用Z3检查数组属性片段中公式的可满足性。Z3返回的数组变量的模型通常使用其他if表达式、if-then-else案例分析等来表示。我想以某种方式解析Z3输出的模型并创建数组，它显式地满足输入的SMT-LIB公式。例如，我希望能够以某种方式始终将Z3输出的模型简化为以下形式： 1 -> 3 else -> 6是否有一些简单<em
浏览 1提问于2013-07-03得票数 1
1回答
Z3中的触发问题
z3
最近，我在Z3中观察到了一些与触发有关的行为，但我不明白。不幸的是，这些例子来自大型的Boogie文件，所以我想现在我应该抽象地描述它们，看看是否有明显的答案。Z3用作触发器。我检查了前一个程序的Z3翻译，t1上的(琐碎的)等式确实在Boogie翻译中幸存下来(也就是说，Boogie不是试图做一些聪明的事情)。
第二：二级模式似乎不适合我。在这两种情况下，运行Boogie的
浏览 4提问于2012-07-25得票数 6
回答已采纳
云服务器
ICP备案
对象存储
云点播
即时通信 IM
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号