1回答
在Z3Py中，证明不返回反例。
、、、、
Z3如何返回有效的反例？以下代码set_param(proof=True)f = ForAll(x, x * x > 0)输出counterexample我不需要使用prove，但是我想在示例中找到一个与f类似的公式的有效反例。我该怎么做呢？
浏览 2提问于2018-06-11得票数 0
回答已采纳
1回答
当Z3中的一个公式未满足并指定了(get-proof)时，会有一个输出，我找不到任何关于它是什么的信息。我在哪里可以找到关于这方面的任何文档？
在我看来很难读，有没有什么工具可以把这个作为输入呢？
浏览 5提问于2012-02-02得票数 6
回答已采纳
1回答
在使用z3时生成更多反例
、、、
是否有可能让Z3Py在合理的时间内生成更多的反例？我可以使用z3.prove生成一个反例如下：goal = x < 0它提供了以下输出，[x = 1]
但如果我想要产生更多的反例呢？通过在反例的基础上递
浏览 0提问于2016-04-08得票数 1
回答已采纳
1回答
这是问题的扩展：from z3 import *
cex_List.append( cex[x] )
其思想是使用Z3来学习用于
浏览 4提问于2022-01-26得票数 0
回答已采纳
1回答
我使用Z3的PDR引擎来证明转换系统中的不变量。当转换系统包含计数器循环时，必须传递该计数器循环才能达到特定的状态，因此性能会很慢。在下面的源代码中，您可以看到一个包含3个状态和3个转换的转换系统的示例，该转换系统是使用上的转换系统Python类实现的。在最后一行中，有一个从状态L0开始到达状态L2的查询。TransitionSystem( And(state == L0, i == 0, y==10),[t1, t2, t3],[s
浏览 2提问于2013-04-11得票数 1
1回答
我正在尝试使用z3来解决一些约束系统。问题的直观或一般编码是通过三种枚举类型Variable、Field和Class以及ADT Path来完成的，该枚举类型由Variable或用Path扩展的Field组成。(语法上是x或p.f)。我们知道，如果路径是类Zero的实例，那么路径也是类Nat的实例；如果路径是类Succ的实例，并且路径具有类Nat的字段p，那么路径也是类Nat的实例。我们向求解器提出的问题是:是否可能a
浏览 8提问于2021-07-14得票数 0
我有兴趣阅读Z3背后的内部理论。具体来说，我想读一读Z3 SMT求解器是如何工作的，以及它如何能够为一个不正确的模型找到反例。我希望能够为一些非常简单的例子手工计算出一个跟踪。然而，所有的Z3引用似乎都是如何在其中编码；或者是对其算法的非常高层次的描述。我无法找到所用算法的描述。这些信息不是微软公开的吗？
有人能引用任何参考文献(论文/书籍)来全面洞察Z3</em
浏览 6提问于2022-01-21得票数 2
回答已采纳
1回答
z3工具的aaary元素的反例输出 我尝试了下面的python代码，并得到了一个反例 from z3 import Solver, parse_smt2_string#str11，(1，2) -> 4，(0，0) -> 3，else -> 7719)这样的代码行让我感到困惑吗？它们似乎重复行(s2，[(1，2) -> 4，(0，0) -> 3，else -> 7719.我可以添加一个不显示
浏览 23提问于2019-09-07得票数 0
2回答
我试图使用Z3Py证明函数，但它似乎返回了一个不正确的反例。有什么问题吗？?(Z3-4.7.1-x86-win，Python-2.7.15)>>> A = z3.BitVec('A', 8)>>
浏览 0提问于2018-10-11得票数 2
回答已采纳
我想找出一个最大的区间，在这个区间内，表达式e对于所有的x都为真。编写这样一个公式的方法应该是：Exists d : ForAll x in (-d,d) . e and ForAll x not in (-d,d) . !e。要获得这样的d，Z3中的公式f (查看上面的公式)可能如下所示：delta = Real('d')
e =另外:通过指定delta
浏览 1提问于2018-06-20得票数 2
当x是double时，(x - x)是否保证是+0.0，或者有时可能是-0.0 (取决于x的符号)？
浏览 2提问于2014-07-25得票数 69
回答已采纳
1回答
我正在尝试理解如何使用Z3有效地证明一个稍微简单的函数f : u32 -> u32是双射的： for i in range(10):N = BitVec('N', 32)solve(N !这是否真的更快，或者是否有一种方法可以有效
浏览 22提问于2020-05-28得票数 2
回答已采纳
使用Z3的角子句求解器：
如果答案是SAT，则可以得到对未知谓词的满意分配(在大多数应用中，这些谓词对应于某种转换系统或过程调用系统的归纳不变量)。如果答案是unsat，那么这就意味着存在着霍恩条款的展开和对霍恩条款中普遍量化的变量的赋值，这样至少违反了一个安全条件(带有false头的条款)。这是该系统没有解决办法的具体证据。我怀疑如果Z3能够得出unsat的结论，那么它在内部就有某种形式的
浏览 6提问于2015-06-10得票数 2
回答已采纳
这两个公式共享大多数变量，除了一些具有不同名称的“临时”(或者我称之为“自由”)变量，这些变量出于某些原因而存在。
现在我想证明F1 == F2，但是Z3的prove()方法总是考虑所有的变量。如何告诉prove()忽略这些“自由”变量，而只关注我真正关心的变量列表？我的意思是，对于我的变量列表中所有相同的输入，如果在输出时，F1和F2具有所有这些变量的相同值(不管'free‘变量的值是多少)，那么我认为它
浏览 1提问于2012-12-28得票数 2
回答已采纳
我目前正在Z3之上为我的编程语言编写一个自动验证器，作为一个有趣的项目，我试图使用它来证明使用循环的fibonacci实现等同于递归实现。如果输入程序是正确的，它似乎是有效的，即它为Z3生成了合理的输入，Z3说它是不可满足的，这意味着在我的上下文中，程序是正确的。但是，当我更改一个变量初始化，从而使程序不正确时，我的验证器提出了下面的Z3公式，对
浏览 8提问于2015-11-15得票数 2
回答已采纳
假设我们有两个未解释的函数func1和func2：stuct_sort func2(struct_sort ,int).他们有这样的关系：func2(p,n)=func1(func2(p,n-1)) if n>1((foralli:[1,m].func2(p,i)==Z)&&(q==func1(p))) implies (forall i:[1,m-1].fun
浏览 2提问于2013-01-06得票数 1
z3 -smt2 <filename>只输出'sat‘或'unsat’。如果满足约束，我希望Z3输出模型，如果不满足，则输出unsat核心。我应该使用哪些Z3选项？
浏览 8提问于2015-12-18得票数 0
回答已采纳
我正在使用CNF4.0中的以下代码片段将公式转换为z3。，也就是说，所有这些表达式都应该连接在一起，以产生实际的公式。显然，原始公式和编码后的公式不等价，因为编码后的公式包含执行Tseitin编码的新变量k!0, k!1, ...。然而，我期望它们是可均衡化的，或者实际上它们是由相同的模型满足的(当忽略k!也就是说，我认为(encoded formula) AND (NOT original formula)是无法满足的</e
浏览 2提问于2012-06-19得票数 4
回答已采纳
当我使用Z3 C++ API构建一组特定的约束时，我会得到“未知”作为响应。但是，如果我使用z3::solver ()序列化operator<<对象并将输出传递给z3二进制文件，它将产生"unsat“。有趣的是，如果我使用z3::solver::to_smt2()而不是operator<<()，那么Z3二进制文件就会输出“Uniting”。
为什么会发生这种事？如何让Z3使用C++
浏览 1提问于2017-01-26得票数 0
1回答
我用Python语言从输入文件中读取z3表达式。然后，在稍后的代码中，我对它们调用__deepcopy__()。问题是，有时输入的z3表达式是True或False，然后Python会感到困惑，认为它们是bool，并拒绝调用__deepcopy__()。错误消息是 AttributeError: 'bool' object has no attribute '__deepcopy__' 在这种情况下，我如何区分bool和z3表达式？
浏览 69提问于2020-01-23得票数 2
回答已采纳
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
腾讯会议
对象存储
云直播活动推荐
腾讯云开发者
