在使用z3优化求解器时，需要模型的边界，特别是约束条件复杂。我可以在Z3 python api中找到函数upper和lower，但不能用于Java api。您能举一些例子来说明如何在Z3 java api中获取模型边界吗？
浏览 26提问于2020-08-16得票数 0
回答已采纳
2回答
Z3使用JNA引发无效的内存访问
、、、、
我在java中使用jna的Z3 C应用程序接口。我经常得到无效的内存访问，但仅限于windows (.dll)和mac os (.dylib)库。在线程中，用户遇到了类似的问题，事实证明这是由于一些编译配置造成的。这是我得到的异常(在Mac OS X 10.6.8上)Exception Codes: KERN_INVALID_ADDRESSjna4404318687023840668.tmp
浏览 1提问于2012-09-03得票数 3
回答已采纳
我对SMT Z3使用(如DbC)的代码和开源替代工具的实际示例很感兴趣，并寻找实例。因此，事实上，我对类似的Z3正式解决工具感兴趣，但是：
具有稳定(实用)的工具，如按合同设计(DbC)、静态类型验证等。请给出任何在实践中使用它们的反馈(代码示例是最好的
浏览 3提问于2011-01-06得票数 5
回答已采纳
1回答
在Z3接口中，FuncDecl有一个DeclKind()来表示它是否是重写规则。但是如何在Z3 java API中创建重写规则呢？
浏览 4提问于2013-03-05得票数 1
回答已采纳
我正在尝试对Java 32位整数算法进行建模。我正在尝试使用z3位向量来实现这一点。我使用的是来自不稳定分支的Z3 Java API。我可以用值0b10000000000000000000000000000000创建一个位向量，但是当我使用BitVecNum.getInt()时，我得到了一个异常BitVecNum)
ctx.mkBVAdd(ctx.mkBV(Integ
浏览 1提问于2013-12-05得票数 0
1回答
我们有一个使用.NET API v4.0的Z3项目。我们希望能够在Mono上编译和运行该项目。这听起来很奇怪，但我们的情况如下。我们有一个使用Z3的课程，所有的实验室计算机都安装了Windows和.NET框架。标记下添加以下信息：
<dllmap dll="z3.dll" target="libz3.dylib" os="o
浏览 3提问于2013-01-13得票数 10
回答已采纳
1回答
如何在Z3 Java API中定义排序？我需要做一件类似以下的事情： (define-sort Set (T) (Array T Bool))
浏览 9提问于2019-06-13得票数 0
到目前为止，我可以在Window上运行Z3来获得cmd中的方程的解：而是如何在Java中使用SMT-Lib标准输入运行Z3。提前感谢。
浏览 0提问于2015-06-01得票数 1
我是z3求解器的初学者。我想实现通用量词，我在https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html中发现context.mkForAll例如，我应该如何实现以下语句的检查:对于{2，4，6，8}中的任意y，存在整数x，其中x> y？ 这是我第一次在这里提问，所以请让我知道如何改进我的问题。
浏览 30提问于2020-07-08得票数 0
回答已采纳
我想问一下，如何下载使用Java的稳定版本的Z3？在codeplex的主分支中，源不包含目录src/api/java。
这是存在于一些分支，如cade24或rc和其他。我不知道该选哪一个。
浏览 1提问于2014-10-23得票数 1
回答已采纳
我是Z3的新手，所以请原谅这个问题听起来太简单了。我有两个问题，在Z3 Java中重新分级常量。
如何在内部创建常量？String, int)到public StringSymbol mkSymbol(String)，这最终调用了Native.mkStringSymbol(var1.nCtx(), var2)，后者在var3中生成了这一行中的变量另一件我感到困惑的事情是使用API定义常量的范围。在交互式Z3中，它
浏览 2提问于2017-12-31得票数 1
1回答
我正在尝试使用Python语言中的z3来实现一个问题(需要字符串操作)的求解器。我试过阅读documentation，但是没有足够的信息。
浏览 13提问于2019-09-01得票数 2
我有一个已有的smt2文件，并用z3 java api解析了这个，解决了这个问题。但我有一个关于如何将FuncDecl转换为Expr的问题，因为我想使用z3 java apis构建一些简单的公式。因为我的原始公式完全是用smt2文本文件编写的，所有内容都被解析到一个BoolExpr中。现在，我成功地提取了const，并且需要用新的公式来处理它们。我该怎么做呢？基本上，我正在寻找的是如何从FuncDecl构建Expr，或者是否有一种方法可以将其转换为Expr？有什么官方的
浏览 0提问于2013-12-13得票数 1
当涉及到z3和java时，我是一个初学者，并且已经尝试安装了很长一段时间。JavaExample“(在Linux和FreeBSD上)命令。
然后，我得到一个错误，在线程"main“java.lang.UnsatisfiedLinkError：.，/usr/lib/jni，/lib，/usr/lib/linux-gnu中没有异常。另外，在输入“env \ grep '^LD_LIBRARY_PATH‘
浏览 1提问于2018-06-14得票数 1
回答已采纳
当我尝试运行bin文件夹中的z3.exe文件时。提示符出现后立即消失。我需要知道如何通过z3.exe文件运行用z3编写的文件。
我该怎么做呢？或者，通过Java运行z3的最佳选择是什么？
浏览 6提问于2013-03-17得票数 3
回答已采纳
1回答
因此，我在SMT求解器中尝试了一个经典的逻辑编程示例。 例如appendo关系，我们可以向后执行它。即给定一个输出列表，返回所有可能的两个输入，当连接这两个输入列表时，返回输出列表。下面是我在z3/smt2 solver中实现的appendo关系 (define-fun-rec appendo ((l (List Int)) (s (List Int))) (List Int)中自动获得所有满意的模型。我们必须使用一些API绑定。 我尝试了几个小时的z3 python
浏览 36提问于2021-07-20得票数 1
回答已采纳
TL;DR:我最近升级到了Z3 Java的更新版本，现在我无法加载libz3java.dylib，因为忽略了libz3.dylib依赖项。Exception in thread "main" java.lang.UnsatisfiedLinkError在com.microsoft.z3.jar (自动生成的Native.
浏览 17提问于2015-11-05得票数 2
我正在尝试创建一些使用Z3的Java插值API的简单示例。我的意图是复制以下SMT-LIB：(compute-interpolant (> x 5) (< x 5)) System.out.print("Z3 Major Version: ");
System.
浏览 2提问于2015-04-12得票数 0
云服务器
ICP备案
对象存储
云点播
智聆口语评测
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号