在使用.NET 3.1版本时，使用Z3接口函数.parseSmtlib2String(String)时，如何使用设置逻辑？
我总是以Z3Error-Exception结束。在这种情况下不是必须的吗？
浏览 4提问于2011-09-08得票数 1
回答已采纳
1回答
我需要在我的z3模型中命名一些断言，以便它能够生成unsat核心。(assert (!(assertion) :named x))有什么帮助吗？
浏览 0提问于2013-04-22得票数 2
回答已采纳
2回答
我在变量上有一堆约束，我正在寻找一种方法来有效地在这个受约束的空间中采样。我尝试过Z3，它似乎能够告诉我空间是否是非平凡的(即约束是否可满足)，但我看不到从空间中获取示例的方法，除非我正在最小化或最大化某些东西。
我是不是错过了什么，或者这不是Z3的用途？
浏览 2提问于2016-08-30得票数 4
回答已采纳
我正在尝试使用Z3来解决一个随机的广义条带打包问题(LRA)，我在c程序中调用了Z3 api，下面是代码。0);我也尝试通过命令"z3smttest“来解决终端中的smttest问题。然而，在终端上，它的运行速度比在c程序中调用api要快。我想知道我需要设置什么配置才能让它在api模式下运
浏览 4提问于2016-09-22得票数 1
回答已采纳
2回答
在ASP.NET核心中使用Z3
、、、、
微软Z3 .NET应用编程接口可以处理.NET核心吗？我们在一个学校项目的调度算法中使用了它，我们相信当项目升级到.net核心时，z3停止了工作。我们找不到任何关于与.net核心一起使用的z3的信息。
浏览 0提问于2016-11-02得票数 1
1回答
rise4fun的教程提到了一个用于访问MuZ的.Net应用程序接口。然而，点击上面提到的任何一种方法，例如To add a rule, call: Z3_datalog_add_rule，都会导致一个死链接。这些方法在哪里被描述，它们目前是否被支持？此外，与这个问题没有直接关系，但我注意到可能使用SMT-LIB API的示例使用了define-fun命令。在.Net应用编程接口中有可用的等效函数吗
浏览 3提问于2013-04-04得票数 0
也许我遗漏了一些东西，但是使用z3 C++ API构造if-then-else表达式的方法是什么呢？向你致敬，朱利安
浏览 1提问于2013-01-04得票数 5
回答已采纳
2回答
Z3使用JNA引发无效的内存访问
、、、、
我在java中使用jna的Z3 C应用程序接口。我经常得到无效的内存访问，但仅限于windows (.dll)和mac os (.dylib)库。当然，这种解决方案是不可持续的。在线程中，用户遇到了类似的问题，事实证明这是由于一些编译配置造成的。这是我得到的异常(在Mac OS X 10.6.8上)
Exception Type: EXC_BAD_ACCESS (SI
浏览 1提问于2012-09-03得票数 3
回答已采纳
在z3 tutorial中，分别提到了str.indexof和seq.indexof。然而，在Z3 C应用编程接口中，只有一个相关的函数，即Z3_mk_seq_index。也就是说，如果我的序列都是字符串，Z3_mk_seq_index还会使用z3str3代码库吗？或者它会退回到Z3的序列求解器？
浏览 18提问于2019-12-20得票数 0
回答已采纳
我对MAX-SAT很感兴趣，并希望Z3能将其作为内置功能。在不久的将来有没有这样做的计划？最后，maxsat示例中的注释没有明确指定如何将约束标记为硬约束或
浏览 5提问于2012-05-22得票数 3
你好，我从下载了Z3，然后在Visual Studio2012中打开了Z3解决方案。(虽然我对VS并不是完全陌生，但我已经10多年没有用过它了)。我可以猜到其中的一些，但其他的不是很清楚。例如：Microsoft.Z3和Microsoft.Z3V3有什么区别？谁能简单地解释一下不同的项目是什么，以及要构建哪些项目？C:\Projects\z3-src-4.1.2\z3\ dll \dll.rc 10 1 dll错误3错误链接:无法打开
浏览 3提问于2012-10-20得票数 3
回答已采纳
1回答
回到过去的日子(即。去年)，我们曾经能够使用理论插件作为一种实现自定义简化器的方法。Z3文档甚至包含了。
我的问题很简单:有没有办法用Z3 4.x实现同样的目标？特别是，我感兴趣的是一种为Z3提供基本术语的外部计算评估的方法。
浏览 2提问于2012-12-10得票数 2
回答已采纳
我正在寻找一种方法，使用.NET应用编程接口向Z3求解器添加最小化/最大化目标。有什么办法吗？
谢谢你的帮助，祝你圣诞快乐:-)
浏览 2提问于2016-12-24得票数 2
1回答
我想知道是否有人能告诉我Z3和coq之间的区别？在我看来，coq是一个证明助手，因为它要求用户填写证明步骤，而Z3没有这一要求。但似乎coq也有类似于Z3的自动策略？或者可能coq中的证明搜索能力没有Z3那么强大？
浏览 1提问于2012-07-18得票数 44
回答已采纳
1回答
Z3有一个prove()方法，可以证明两个公式的等价性。需要提醒的是，“部分等价”保证了两个公式是等价的，如果给定相同的输入，则它们产生相同的输出。
浏览 2提问于2012-12-26得票数 3
回答已采纳
除了更改location_next的真值之外，我还想用另一个值重新初始化x_next。我该怎么做呢？
浏览 0提问于2012-08-08得票数 0
回答已采纳
根据我的经验，在较大模型的情况下，我发现与sat情况相比，Z3需要更长的时间来给出未饱和的结果。甚至有时Z3会运行无限的时间而不给出任何答案。在下面的例子中，我举了一个这样的例子。虽然我使用SMT进行形式化，但我在这里编写了等效的.NET -LIB2代码。在这里，在非sat结果的情况下，求解器花费的时间几乎是sat结果的40倍。当我们增加大小，例如，6辆车和8个插
浏览 5提问于2012-09-30得票数 0
回答已采纳
对于我的应用程序代码，我为我的求解器使用了以下z3参数设置 p.set(":relevancy", static_cast<unsigned>(C++异常，本质上说逻辑和超时不是有效的参数。我没有找到任何等价的选择逻辑，所以我假设这是自动推导。但是，对于超时，有两个选项soft_timout和solver2_timeout。我知
浏览 2提问于2015-01-26得票数 0
回答已采纳
云服务器
ICP备案
对象存储
云直播
腾讯会议
腾讯云开发者
