是否有一种Z3策略可以将目标(例如，一个带有量词和未解释函数的断言)重写为一组无连接的公式？例如，以下公式： (declare-fun P (Int) Bool)(declare-fun R (Int Int) Bool)
(assert
浏览 50提问于2020-06-23得票数 1
1回答
我正在试验枚举类型公式的量词消去策略。我想知道是否有任何方法通过调整求解器来提高性能。在简单地浏览了一下源代码之后，我得出结论，量化消除策略(例如qe_lite.cpp)似乎有不同的策略，但它们并不公开为qe策略的参数。在我的例子中，公式有一个简单的命题结构，有时量化的变量甚至不会出现在公式中
浏览 1提问于2013-04-18得票数 1
回答已采纳
1回答
我使用Java在UbuntuLinux14.04上与Z3通信。关于Z3，我使用github上找到的主分支的当前版本(今天编译)。组合(连词、断续、否定)
(or-else (try-for smt x) (then qe smt))
原因是有些公式简单，检验速度快，不需要消去量词，而普通的s
浏览 2提问于2015-08-06得票数 3
回答已采纳
1回答
从Ocaml调用Z3为黑匣子
、、、、
为了避免实现所需的所有有效性和量词消除方法，我希望能够在Ocaml中访问Z3的量词消去策略。有人能帮忙吗？我问这是为了找到更多的信息，类似的问题在未来。
浏览 3提问于2021-11-09得票数 2
回答已采纳
3回答
如何使用Z3的Python执行量词消除？虽然我检查了教程和API，但无法做到这一点。谢谢!
此外:在做了量词消除后，我将“添加”与另一个无量词公式。那么，如果我使
浏览 0提问于2013-07-28得票数 4
回答已采纳
1回答
我正在试验优化使用Z3来证明一阶理论的事实.目前，我在Python中指定了一阶理论，将量词放在那里，并将所有子句连同证明目标的否定一起发送给Z3。我有以下的想法，我希望能优化结果:我只想把理论中的公式发送给Z3，这些公式与证明目标相关。我不打算详细讨论这个概念，但我认为直觉很简单:我的理论是公式的结合，我只想发送可能影响证明目标的真值的连
浏览 4提问于2012-12-21得票数 1
回答已采纳
1回答
一个非常类似的问题已经被问到了，但是我找不到以下问题的答案。使用所有量词都可以很容易地表示线性最大化问题：像上面这样的查询可以提交给z3。因此，我想问一问，当z3看到一个LP问题时，它是否聪明到能够识别一个LP问题，它是否会应用一种单纯形方法来消除所有量词？我做了一些实验，这似乎是可行的，但我还没有在更复杂的例子上尝试过。
谢谢!
浏览 3提问于2014-06-12得票数 0
回答已采纳
1回答
我试图解决一个涉及命题可满足性(带有量词)和线性算法的问题。下面是一个高度简化的问题，它抓住了我想要解决的问题的本质。有人能给我建议吗？我试着读一些像纳尔逊·奥本方法之类的东西，但是有很多不熟悉的符号，学习起来需要很长时间。
另外，Z3允许用户调整这
浏览 2提问于2013-12-06得票数 2
回答已采纳
我想使用Z3的策略来预处理公式，并要求保持等价性。，莱昂纳多·德莫拉表示，几种战术只能产生均衡的结果。谢谢!
浏览 4提问于2013-12-19得票数 2
我要求Z3使用SMTLIB2接口在UFLIA理论中进行量词消除。所以我断言一个公式有21个存在量化的变量，其中7个是整数，14个是布尔型。然后我做(apply qe)，Z3返回一个目标，它仍然包含九个存在量化的变量，名为(x!1 Int)，(x!14 Int)和(x!14!1 Int)到(x!14!7 Int)。这是否意味着qe策略不会一次消除所有量词？
如果我执行两次(assert qe)，除了重命名的量化变量之外，目标保持不变。但
浏览 4提问于2013-08-27得票数 2
T7 T7) Bool) (= (set23 bv0 bv1) (= bv0 bv1))))请注意，Z3
浏览 3提问于2014-03-26得票数 1
回答已采纳
1回答
我目前正在使用Z3 C++ API来解决位向量上的查询。有些查询可能在顶层包含一个存在量词。
通常情况下，量词消除很简单，并且可以由Z3快速执行。但是，在量词消除返回到枚举数千个可行解决方案的情况下，我想放弃这一策略，并以其他方式处理查询。我试过用“尝试-为”策略包装‘qe’-策略，希望如果量词消除失败(比如100 if )，我会知道我最好以其他方式处理查询。不幸的是，“尝试-fo
浏览 5提问于2015-09-06得票数 4
回答已采纳
我试着用solve(g)找到满足公式g = And(ForAll([i, j, k], Implies(And(k <= 0, A * i + B * j + C * k + D <= 0), k +i - j <= 0)),Not(And(A==0,B==0,C==0)))的A，B，C，D的值。这有许多可能的解决方案，一种是A=1,B=-1,C=D=0，但Z3似乎无法做到这一点(solve(g)不会终止)。
Z3能做这种非线性(但简单)的公式
浏览 3提问于2013-02-19得票数 2
回答已采纳
1回答
我正在使用微软的Z3进行一些简单的动态观察分析。作为其中的一部分，如果我可以将一些公式从使用一组变量转换为另一组目标变量，这将是很有帮助的。我对Z3真的很陌生，但我知道它有一些内部简化规则和其他转换公式的方法……基本上，我想知道是否有可能进行一些转换，比如：(declare-constmidstep 1.0)))
(assert (= foo_ret local_1) :nam
浏览 1提问于2012-06-20得票数 1
2回答
Z3或Z3Py中的假设
、、、
有没有一种方法可以在Z3 (我使用的是Z3Py库)中表达假设，这样引擎就不会检查它们的有效性，而是像定理证明一样将它们作为基本理论？用Z3Py编码，如下所示：assumption1 = ForAll(t，f1(t) = f2(t))。当前代码的问题是我的断言集非常大，并且我使用量词(我试图证明实时系统的可满足性)。如果
浏览 27提问于2016-03-23得票数 2
1回答
在对线性算术公式h应用Z3中的量词消除后，我得到了一个大约30行的公式。事实证明，这个公式等同于h2=And(n>2, i>=0, i<=n-2)，我更喜欢将其作为输出。Not(i >= 1), Not(n + -1*i <= 1)), i >= 0)
现在，Not(n<=2)可以更简洁地表示为n>=3，Not(n + -1*i <= 1)表示为n-i>=2，并且在此公式<e
浏览 0提问于2014-02-12得票数 1
我希望将公式中的所有嵌套量词拉到最外层。我希望以下命令能在Z3中工作，但它们不能：(simplify (exists ((x Int)) (and (>=) :pull-nested-quantifiers的用途是什么如
浏览 6提问于2012-03-07得票数 1
回答已采纳
下面的“最小”程序是从一个大得多的程序中提取出来的，预计它会产生unsat (和to )。但是，去掉量词AX-1中的附加连词，结果将更改为unknown (在Windows10上的Z3 4.5.0 x64中)。false)))
(check-sat); (pop)
量词实例化统计数据显
浏览 4提问于2016-10-03得票数 0
回答已采纳
1回答
我正在通过Z3py使用Z3的量词剔除策略，并尝试了以下示例。from z3 import *t = Tactic('qe')
#returns: [[Or(10 <= x, And(y <= 10, y >= 0, And(x <= 7,
浏览 3提问于2018-11-11得票数 0
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
云直播
对象存储
实时音视频活动推荐
腾讯云开发者
