1回答
我有一个Python程序，我在其中生成不同的z3公式，然后对其中一些公式进行存在量化。我的程序曾经运行得很好，但是突然之间，它在尝试对一些表达式进行量词消除时就死了。代码不会返回并挂起这些示例。我尝试打印expr，但从来没有打印出来。在有问题的情况下，该进程也不能轻易终止。我必须通过关闭终端(ubuntu)来强制它。这是我用来应用量词消除的代码：
z3_expr = And(*conjuncts)/
浏览 10提问于2020-02-07得票数 0
1回答
然而，对于真实的案例，它可以消除。(当i和k都是实数时)对于整数来说，消除量词是不是更难？我知道在量词消除后，这些约束被简化为线性约束。
我认为z3在检查可满足性之前会自动进行量词<
浏览 1提问于2012-05-04得票数 5
回答已采纳
我尝试在Python中应用以下量词消除。在第三次迭代中，z3没有返回并被卡住。我使用的是Python 2.7.17和Ubuntu 18.04.4。
浏览 9提问于2020-02-10得票数 0
回答已采纳
我要求Z3使用SMTLIB2接口在UFLIA理论中进行量词消除。所以我断言一个公式有21个存在量化的变量，其中7个是整数，14个是布尔型。这是否意味着qe策略不会一次消除所有量词？
如果我执行两次(assert qe)，除了重命名的量化变量之外，目标保持不变。我尝试了(repeat qe)，但它返回unsupported，而且将:eliminate-variables-as-block参数设置为true也不会改变任何事情。但是，如果我从目标中提取量化公式，自己断言它，并
浏览 4提问于2013-08-27得票数 2
1回答
有些查询可能在顶层包含一个存在量词。
通常情况下，量词消除很简单，并且可以由Z3快速执行。但是，在量词消除返回到枚举数千个可行解决方案的情况下，我想放弃这一策略，并以其他方式处理查询。我试过用“尝试-为”策略包装‘qe’-策略，希望如果量词消除失败(比如100 if )，我会知道我最好以其他方式处理查询。不幸的是，“尝试-for”策略无法取消量词消除(对于任何时间限制)。在
浏览 5提问于2015-09-06得票数 4
回答已采纳
我正在尝试实现本文中的一些代码：来证明关于一台简单机器的事实。我想我可能没有实现论文中描述的所有内容:我不明白“最后，在FORALL子句中强调实例化模式( PAT：{check tr (lst)} )的目的是很重要的。这个公理陈述了关于所有列表的一些内容。
浏览 8提问于2020-03-10得票数 1
1回答
所以我把它翻译成Z3py：x_1 = Int('x_1')w = Goal()
phi = Exists(x_1, ForAll这可能与result_ttt的类型<class 'z3.z3.ApplyResult'>有关(在执行type(result_ttt之后)。在这种情况下，结果是[[]] (因为量词消除是令人满意的)。在做assert [[]] ==
浏览 1提问于2021-11-11得票数 0
回答已采纳
我试图使用Z3Py从一个布尔公式开始，然后抽象它，以便布尔函数是未知的，然后将它转换为smt-约束，以便这些约束的每个模型对应一个与我原来的类似的公式。我想列举所有的模型。
浏览 1提问于2021-07-15得票数 0
回答已采纳
我已经在线性实数运算下的量词消除上尝试过Z3。这个公式不是很大，但是当要消除的变量数量超过5个时，它需要很长时间(或者永远不会终止)。有没有其他的求解器可以做得更好？或者有什么技巧可以帮助Z3？
浏览 0提问于2013-10-23得票数 1
我正在尝试学习如何使用Z3未解释的函数来显示n=2k+1 => log(m) + k*log(m*m) == n*log(m)。
浏览 2提问于2013-03-01得票数 0
下面的代码介绍了使用Z3和SMT的热带算法的基本特性： b(define-fun tropmul ((a Real)(b Real)) Real (+ a b))
(declare-fun x ()
浏览 0提问于2013-06-05得票数 1
回答已采纳
我正在阅读PCRE文档，它引用了拥有式量词，但没有明确或具体地定义它们。我知道什么是贪婪的量化词，我也知道什么是懒惰的量化者。但占有欲呢？
?
浏览 2提问于2009-07-13得票数 16
回答已采纳
1回答
使用所有量词都可以很容易地表示线性最大化问题：像上面这样的查询可以提交给z3。因此，我想问一问，当z3看到一个LP问题时，它是否聪明到能够识别一个LP问题，它是否会应用一种单纯形方法来消除所有量词？谢谢!
浏览 3提问于2014-06-12得票数 0
回答已采纳
2回答
Z3或Z3Py中的假设
、、、
有没有一种方法可以在Z3 (我使用的是Z3Py库)中表达假设，这样引擎就不会检查它们的有效性，而是像定理证明一样将它们作为基本理论？T=实数(“t”)
assumption1 = ForAll(t，f1(t) = f2(t))。当前代码的问题是我的断言集非常大，并且我使用量词(我试图证明实时系统的可满足性)。如果我将上述断言添加到其他断言的集合中，则检查过程不会终止。
浏览 27提问于2016-03-23得票数 2
1回答
我正在通过Z3py使用Z3的量词剔除策略，并尝试了以下示例。))我认为生成的公式是无限定符的DNF(这是我需要的)，但我在API有人知道qe在DNF中总是返回公式吗？编辑:所有公式都限制为线性整数运算。
浏览 3提问于2018-11-11得票数 0
1回答
在中，我给出了一个函数公理化，并要求Z3提供一个模型。但是，因为解决带有量词的问题在一般情况下是无法确定的，所以Z3会超时。是否可以通过自动消除这两个函数来简化模型？(define-fun f ((x!0 ABC) (x!1 error)) error我使用的是Z3Py，但一般Z3特定的答案和Z3Py特定的答案都是受欢迎的。
浏览 1提问于2016-05-29得票数 0
但是，去掉量词AX-1中的附加连词，结果将更改为unknown (在Windows10上的Z3 4.5.0 x64中)。false)))
(check-sat); (pop)
量词实例化统计数据显示，AX-2在这两种情况下都是实例化的，但是只有当附加的连接符不包括时，AX-1才被实例化。我的假设是，在后一种情况下，Z3消除了量词，因为量化的变量不在身体中。
浏览 4提问于2016-10-03得票数 0
回答已采纳
我可以得到for each循环的解释吗，因为它对我来说没有多大意义。特别地，STANDARDIZE second ()和倒数第二行做了什么？
浏览 3提问于2012-10-12得票数 4
回答已采纳
1回答
我一直在努力达到和这篇文章完全一样的目标。
但是，答案是在smt中，如何在python中使用check-sat-using中的z3py？有人能帮我把这段代码翻译成python代码吗？
浏览 1提问于2020-02-03得票数 1
回答已采纳
云服务器
ICP备案
对象存储
即时通信 IM
云直播
腾讯云开发者
