1回答
如何在Z3 Java API中定义排序？我需要做一件类似以下的事情： (define-sort Set (T) (Array T Bool))
浏览 9提问于2019-06-13得票数 0
2回答
Z3使用JNA引发无效的内存访问
、、、、
我在java中使用jna的Z3 C应用程序接口。我经常得到无效的内存访问，但仅限于windows (.dll)和mac os (.dylib)库。在线程中，用户遇到了类似的问题，事实证明这是由于一些编译配置造成的。jna4404318687023840668.tmp 0x000000010a00c884 ffi_call + 644
21 jna4404318687023840668.tmp 0x000000010a003ca5 Java_com_sun_jna_Native_ffi_1prep_1c
浏览 1提问于2012-09-03得票数 3
回答已采纳
1回答
去年)，我们曾经能够使用理论插件作为一种实现自定义简化器的方法。Z3文档甚至包含了。
我的问题很简单:有没有办法用Z3 4.x实现同样的目标？特别是，我感兴趣的是一种为Z3提供基本术语的外部计算评估的方法。
浏览 2提问于2012-12-10得票数 2
回答已采纳
在使用z3优化求解器时，需要模型的边界，特别是约束条件复杂。我可以在Z3 python api中找到函数upper和lower，但不能用于Java api。您能举一些例子来说明如何在Z3 java api中获取模型边界吗？
浏览 26提问于2020-08-16得票数 0
回答已采纳
1回答
我使用的是Z3的Java API，我需要定义自然的整数变量，即它们的值不能为负数。如何使用java API在z3中定义自然数据类型？
浏览 1提问于2015-06-17得票数 1
1回答
是否可以使用smt-lib或类似的C/C++ API来解析用户理论插件的输入？例如，在示例用户理论"test_user_theory.c“中，如何在输入文件中声明字符串变量和常量字符串(而不将其分解为位向量)？提前谢谢。
浏览 0提问于2012-09-28得票数 1
我正在使用Z3 java API。我需要定义一组配对元素e.x。{(e1，e2)...}我不知道如何使用Java API在z3中声明配对数据类型？
浏览 1提问于2015-02-10得票数 0
1回答
在Z3接口中，FuncDecl有一个DeclKind()来表示它是否是重写规则。但是如何在Z3 java API中创建重写规则呢？
浏览 4提问于2013-03-05得票数 1
回答已采纳
1回答
我希望在z3 api中使用api_parsers来解析smt2命令，然后我希望看到结果vectors的内容(如排序、变量、参数等)。#include<iostream>#include<z3_api.h>
expr e(ctx, a);
浏览 0提问于2016-04-10得票数 0
我对SMT Z3使用(如DbC)的代码和开源替代工具的实际示例很感兴趣，并寻找实例。因此，事实上，我对类似的Z3正式解决工具感兴趣，但是：
最后，关于将
浏览 3提问于2011-01-06得票数 5
回答已采纳
我是Z3的新手，所以请原谅这个问题听起来太简单了。我有两个问题，在Z3 Java中重新分级常量。
如何在内部创建常量？String, int)到public StringSymbol mkSymbol(String)，这最终调用了Native.mkStringSymbol(var1.nCtx(), var2)，后者在var3中生成了这一行中的变量另一件我感到困惑的事情是使用API定义常量的范围。在交互式Z3<em
浏览 2提问于2017-12-31得票数 1
我正在尝试通过Z3的Java API使用以下方法读取一个常见的SMTLib2文件：有没有什么办法能让我错过这个机会呢？感谢您的考虑。
浏览 0提问于2017-08-28得票数 3
1回答
我需要使用java API在z3中定义一个函数，该函数接受一个目录的输入，然后递归删除其中的所有内容。既然z3不支持递归函数，有没有办法表达这种功能呢？
浏览 3提问于2015-08-12得票数 0
我已经使用java API在Scala中定义了以下循环排序：(其中ctx是一个Z3上下文) val circleConstructor = ctx.mkConstructor(
"Circle
浏览 16提问于2020-08-25得票数 0
回答已采纳
我正在尝试对Java 32位整数算法进行建模。我正在尝试使用z3位向量来实现这一点。我使用的是来自不稳定分支的Z3 Java API。
但是，我不知道如何从z3获得正确的溢出行为。
浏览 1提问于2013-12-05得票数 0
1回答
有时(或多次)发生的情况是，问题太大，以至于Z3求解器有很多超时。在这种情况下，我认为将问题分成更小的子问题将是有益的。
我想特别问一下Z3中的Theory Plugins。
浏览 0提问于2013-02-20得票数 0
回答已采纳
,13BMW,z3,14BMW,z3,16Honda,Civic,13BMW,z3,16BMW,X3,15用这种方式编写一个可以比较两个文件的java程序，哪种方式是最好的方法？我知道最简单的方法是使用一些unix命令(使用排序获取所有制造商，使用grep获取每个制造商的行，使用排序获取所有模型和grep )，但我必
浏览 3提问于2015-11-06得票数 1
我一直在阅读尼古拉的文章《使用Z3的工程理论》，这篇文章讲述了如何将自定义决策过程与Z3连接起来。Z3 API在。有人能告诉我他们或他们的替代品在哪里吗? 2.在相关的注释中，我在界面中看到了几个新概念，如探针和战术。这些都有描述或解释吗？
浏览 0提问于2012-12-27得票数 1
1回答
我想知道排序序列的定义是什么。我在Z3 SMT2.0指南中找不到它的定义。我意识到Seq已经被定义了，因为我试图定义一个名为Seq的排序。是否有一些断言与Seq相关？最大值
浏览 0提问于2012-05-18得票数 1
我想问一下，如何下载使用Java的稳定版本的Z3？在codeplex的主分支中，源不包含目录src/api/java。
这是存在于一些分支，如cade24或rc和其他。我不知道该选哪一个。
浏览 1提问于2014-10-23得票数 1
回答已采纳
云服务器
对象存储
ICP备案
云点播
实时音视频
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号