1回答
当使用策略时，求解器返回空的unsat核心。)C = Bool('c')s.add(C == (x == -1))
s.check(B, C) 在这两种情况下，检查都会返回unsat值(这是理所应当的)，但在使用策略的第二种情况下，我会得到一个空的unsat核心。在使用</e
浏览 15提问于2020-01-20得票数 0
回答已采纳
我使用z3来提取不可满足的线性约束集的非卫星核心。我发现当将“自动配置”选项设置为false时，z3可能会为相同的问题提供不同的unsat核心。是否有其他选项可以使z3为同一问题提供不同的unsat核心？
以下是我之前的相关问题：
浏览 3提问于2013-08-18得票数 3
回答已采纳
Z3通过以下选项支持最小的unsat核心检测。记录在案的。
在API文档中，只提到了跟踪unsat核心的简单使用。是否有一种方法可以使用Python来实现最小的 unsat核心检测。
浏览 0提问于2019-05-07得票数 0
我的设想如下：
首先，我遵循乐观的假设，认为一切都很好；因此，我检查断言，而不要求一个unsat核心(仅仅使用断言)。然而，当我在一次测试中得到无法满足的状态时，我会改变策略，从一开始就使用AssertAndTrack来获得完整的unsat核心。对于4.3.2版本，这是完美的，但是在切换到4.4 (稳定的和最新的)之后，Z3通常返回未知的状态(即使是在不<em
浏览 2提问于2015-07-22得票数 1
回答已采纳
我正在使用SMTLIB2语言，通过SMTLIB求解器来解决我在逻辑QF_BV中表达的问题。我希望在非饱和核心生成时考虑的断言已经使用(assert (! (EXPR) :named NAME))构造指定了。不出所料，Z3给了我一个unsat。然而，Z3似乎总是丢弃由所
浏览 3提问于2012-02-28得票数 6
回答已采纳
1回答
迭代未满足的内核
、、
我在Z3中使用(get-unsat-core)来提取一组无法满足的约束的未满足核心。但是，某些约束可能具有多个未满足条件的核心。在这种情况下，有没有办法遍历unsat core？
浏览 9提问于2018-01-07得票数 0
回答已采纳
如何正确跟踪z3::optimize非卫星核心？ std::cout << "unsat problem!尽管如此，如果需要的话，我可以跟踪unsat的核心--例如添加opt.add(ctx.int_const("
浏览 0提问于2020-08-14得票数 2
回答已采纳
1回答
我需要在我的z3模型中命名一些断言，以便它能够生成unsat核心。(assert (!(assertion) :named x))有什么帮助吗？
浏览 0提问于2013-04-22得票数 2
回答已采纳
我正在使用Z3的Python，试图在我正在编写的一个研究工具中包含对它的支持。关于使用Python接口提取不可满足的核心，我有一个问题。(not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))(get-unsat-core)通过z3可执行文件(对于Z3 4.1)运行此查询，我将收到预期的结果：(__constr
浏览 8提问于2013-01-28得票数 3
回答已采纳
1回答
是否有可能在Z3 (4.8.9版)证明中获得断言名称？最起码的例子是：(assert (!false :named name))(get-proof)unsat然而，这是实际产出：unsat(let (($x27 (not name)))
(let ((@x30
浏览 5提问于2020-10-18得票数 0
我需要使用Z3_parse_smtlib2_string来使用C++ API将一些SMTLIB字符串解析成Z3，并使用Z3 C++ API来查找其中的unsat核心。我知道还有其他方法可以找到和所描述的unsat核心，这些方法更容易，也不那么麻烦，但我真的希望能够使用从字符串解析到Z3的数据结构来实现这一点。原因是我正在尝试使用Z3自动化一些东西。很明显，如果我把
浏览 4提问于2015-03-11得票数 0
回答已采纳
我试图使用Z3 4.3.0和.NET API启动unsat核心生成。调用context.UpdateParamValue("unsat_core", "true")会抛出一个异常，其消息是“错误设置'unsat_core'，原因:未知选项”。
浏览 4提问于2014-08-11得票数 2
回答已采纳
我的Python程序使用Z3 Python。它生成了许多假设，由Z3使用以下命令进行检查：然后，我使用命令获取unsat核心：有没有一种方法可以在我的python程序中使用命令假设数是在代码运行期间定义的，每次运行都会更改。
提前感谢！
浏览 6提问于2014-09-24得票数 2
回答已采纳
在前面的问题中，我问到当使用nlsat解算器处理非线性实算法上的多项式约束时，z3是否能给出一个完整的结果。正如泰勒所回答的，nksat的解算器是完整和健全的。当解决上帝军的约束时，Z3支持非卫星核心提取。我想知道是否有可能在使用nlsat解算器时提取出unsat核心？如果z3不支持，我能在z3之上实现它吗？另一个问题是它能处理多大的问题。
浏览 4提问于2014-04-13得票数 2
回答已采纳
1回答
在SMT求解器上进行新的研究多次受到这样一个事实的阻碍，即可用问题需要许多与决策过程没有直接关系的技巧和预处理技术。是否可以使用Z3作为预处理器，将问题以预处理的形式( z3本身用来解决问题的形式)转储出去？我没有看到任何命令行选项，但我猜可能会有一些方法来实现这一点，通过策略，通过python接口，甚至编写一些额外的代码。
浏览 0提问于2012-12-05得票数 5
回答已采纳
1回答
在过去的一年左右，我一直在使用Z3 4.0版本的Ocaml API，主要是位向量理论。现在，我需要在执行Z3.solver_check之后提取未饱和内核，但不幸的是，版本4没有此功能。我可以进行重写，使用假设来代表公式中的每个位向量方程，然后获得unsat核心，但这是代码的关键部分，它可能会影响整体性能。
有没有一种方法可以在不经过版本4的假设的情况下获得unsat内核？例如，有没有办法从unsat的证明(由Z3.s
浏览 5提问于2016-08-09得票数 1
1回答
抱歉，，我想再问一下这个问题-multiple (最小或其他) UNSAT核心和-multiple SAT分配
我已经在论坛上查看了关于这个主题的早期讨论，例如，在逻辑z3上使用QF_LRA时，如何获得不同的unsat核心。这些参考了z3 Python教程，例如，目前看来离线的。我尝试过其他的建议，如github等，以找到
浏览 1提问于2015-12-01得票数 0
如果使用了一种不适合特定问题的策略，Z3的一般行为是什么？我对此感到惊讶，因为问题不在QFLIA中。我本以为会出现错误或unknown。
即使你不知道你正在应用的策略是否真的适用于特定的问题实例，应用策略是否安全？
浏览 0提问于2016-05-25得票数 1
我使用的是z3 python api。我希望一方面使用Z3的非side核心功能，另一方面能够针对某些标准进行优化。
self._solver.unsat_core()) > 0这很好用。但除此之外，我还可以使用z3.Optimize()中的maximize()和minimize()函数。可以一起
浏览 0提问于2018-06-20得票数 1
我试图在smt api中使用Z3 (版本Z3 4.1.0.0)，也就是说，我试图解析来自smt的实例--竞赛unsat核心轨道。to_expr(c, f);s.add(r);但我得到了以下错误：(错误“第220行第15栏:未启用unsat
浏览 3提问于2012-10-16得票数 3
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
云直播
对象存储
腾讯会议活动推荐
腾讯云开发者
