腾讯云
开发者社区
文档
建议反馈
控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
搜索
搜索
关闭
发布
登录/注册
精选内容/技术社群/优惠产品,
尽在小程序
立即前往
文章
问答
(9999+)
视频
沙龙
1
回答
如何在
Java
中使用多核运行
Z3
?
java
、
parallel-processing
、
z3
、
solver
、
smt
我正在尝试改善我
的
Z3
代码
的
时间。我
的
环境
的
Z3
使用
Java
,
Z3
的
版本是4.8.10。要在C ++中启用
并行
模式
,您应该
设置
set_param ("parallel.enable",true);。在
Java
的
情况下,如何将其
设置
为
并行
模式
?如果你愿意,我想要示例代码。 谢
浏览 71
提问于2021-07-28
得票数 0
回答已采纳
1
回答
如
何用
Java
设置
Z3
的
并行
模式
java
、
api
、
parallel-processing
、
z3
、
solver
我正在尝试改善我
的
Z3
代码
的
时间。我
的
环境
的
Z3
使用
Java
,
Z3
的
版本是4.8.10。为了
设置
并行
模式
,我使用了Global类并将其
设置
如下。如何使用
Java
API编写代码来
设置
并行
模式
? 还有,有没有样品?
浏览 6
提问于2021-08-04
得票数 0
回答已采纳
2
回答
Z3
中
的
并行
求解
c++
、
z3
Z3
4.8.1中
的
一个新特性是
并行
解决: 有人能提供一些示例代码来了解如何实现这个新特性吗? 谢谢
浏览 0
提问于2018-11-11
得票数 6
回答已采纳
1
回答
使用
Z3
与SBV
并行
化
haskell
、
z3
、
sbv
我想使用
Z3
通过SBV使用多核。 --我应该能够通过将parallel.enable=true传递给命令行中
的
z3
可执行文件来做到这一点。由于我使用
的
是SBV,所以我需要通过SBV与各种SMTLib解决程序
的
接口,下面是我所尝试
的
: ...(SBV.solver
z3
) cfg ++ ["parallel.enable=true"] } 但
浏览 7
提问于2020-07-30
得票数 0
1
回答
有没有办法让
Z3
使用多核(多线程)来解决大问题?
optimization
、
z3
、
smt
我正在尝试从商业求解器转移到
Z3
来解决大整数可满足性问题。我所说
的
“大”是指我试图求解
的
模型有大约300,000个整数和300,000个(assert (=...语句,每个语句可能有8-16个变量
的
组合。 我们
的
商业求解器花了1353秒来解决这个大问题。然而,这是一个简单
的
应用程序测试问题,所以我希望将其转移到
Z3
上,并抛弃商业优化器。正如我所指出
的
,商业优化器花了1353秒,但它也被允许使用32个核心,而且有迹象表明我使用了很多核心(我没有跟踪它最终
浏览 20
提问于2019-11-30
得票数 1
回答已采纳
2
回答
Z3
使用JNA引发无效
的
内存访问
java
、
c
、
java-native-interface
、
jna
、
z3
我在
java
中使用jna
的
Z3
C应用程序接口。我经常得到无效
的
内存访问,但仅限于windows (.dll)和mac os (.dylib)库。当然,这种解决方案是不可持续
的
。在线程中,用户遇到了类似的问题,事实证明这是由于一些编译配置造成
的
。at 0x000000000000000c Crashed Thread: 0 Dispatch queue: com.apple.main
浏览 1
提问于2012-09-03
得票数 3
回答已采纳
1
回答
在
Z3
API中支持C++浮点理论吗?
c++
、
api
、
floating-point
、
z3
从RELEASE_NOTES
的
最新版本
的
Z3
,Z3-4.4.1,它支持浮点理论。我已经用离线
的
方式成功地测试了这一点。然而,在我目前
的
项目中,
Z3
需要在C++ API中使用,在阅读了相关文档和源代码之后,我还没有找到任
何用
于浮点理论
的
API函数。
Z3
的
浮点理论在C++ API中支持吗?不过,也许我可以将约束
设置
为smt格式文件,然后使用
Z3
API解析该文件。但是,这是我最后一次尝
浏览 1
提问于2015-10-23
得票数 2
回答已采纳
1
回答
为字符串约束
设置
求解器
python
、
z3
、
z3py
我正在尝试使用Python语言中
的
z3
来实现一个问题(需要字符串操作)
的
求解器。我试过阅读documentation,但是没有足够
的
信息。我也尝试过阅读z3str documentation,但我找不到一种方法来使我
的
示例工作。我想要
设置
: len(string) = 8string_possible_characters = '3456789a' string.count("6") = 2
浏览 13
提问于2019-09-01
得票数 2
1
回答
手动
设置
互斥对象会提高性能吗?
python
、
python-3.x
、
python-multithreading
、
z3py
、
gil
我
的
python程序绝对是cpu绑定
的
,但是所花费
的
时间
的
40%到55%是在
z3
求解器中用C代码执行
的
(它对gil不了解任何情况),在这里,对C函数(z3_optimize_check)
的
每次调用几乎需要一分钟才能完成(到目前为止,parallel_enable参数仍然导致这个函数在单线程
模式
下工作并阻塞主线程)。我不能使用多处理,因为z3_objects不是可序列化
的
友好
的
(除非这里有人可以证明不是这样)。由于它们
浏览 5
提问于2019-11-04
得票数 1
1
回答
用
z3
表示推理规则
java
、
z3
我一直在阅读和研究几篇文档,我仍然不清楚如
何用
z3
表示我
的
推理规则。 我
的
z3
规则是否如此简单:b.(a ^ b) => c从那里开始,
java
实现在阅读文档时显得相当直接。这仅仅是从一个类型系统
的
推理规则到命题逻辑
的
初始转换,这让我感到很困扰。 我认为我
的
推理规则(
浏览 2
提问于2017-07-10
得票数 0
回答已采纳
1
回答
如何在Python中用
Z3
求拉格朗日插值多项式?
python
、
z3
、
polynomial-math
我正在用
Z3
库和Python语言学习数学,我不知道如何才能找到基于拉格朗日插值多项式
的
多项式?例如,f(0) = y0f(2) = y2我使用Scipy工作得很好,但当我切换到
Z3
库时,它没有更多
的
文档可以找到:(
浏览 1
提问于2014-04-29
得票数 0
1
回答
Z3
的
java
绑定
的
JavaExample.
java
测试编译错误
java
、
z3
我正在尝试使用
Z3
的
java
绑定,特别是尝试运行在
Z3
的
4.4.2版本中分发
的
Java
示例JavaExample.
java
。当我使用4.4.2 com.microsoft.z3.jar文件时,JavaExample.
java
编译得很好。但是,它不会运行,因为默认
的
libz3
java
.dll是32位,我
的
环境是64位。我尝试为它
的
Makefile制造商
Z3<
浏览 0
提问于2016-02-09
得票数 0
回答已采纳
1
回答
z3
:在
z3
位向量加法中模拟
Java
2
的
补码溢出和下溢
java
、
z3
我正在尝试对
Java
32位整数算法进行建模。我正在尝试使用
z3
位向量来实现这一点。我使用
的
是来自不稳定分支
的
Z3
Java
API。 .simplify()).getLong()); 我得到了我想要
的
结果
浏览 1
提问于2013-12-05
得票数 0
1
回答
线程"main“
java
.lang.UnsatisfiedLinkError中
的
异常:
java
.library.path中没有libz3
java
java
、
z3
当涉及到
z3
和
java
时,我是一个初学者,并且已经尝试安装了很长一段时间。为了解决这个问题,我搜索并发现您需要
设置
LD_LIBRARY_PATH,我遵循了在各个页面上给出
的
建议,但没有成功。另外,在输入“env \ grep '^LD_LIBRARY_PATH‘”时,我得到- LD_LIBRARY_PATH=/home/chaitanya/
z3
/build,这是我
的
libz3
java
.so上一次,我更改了整个“usr”文
浏览 1
提问于2018-06-14
得票数 1
回答已采纳
1
回答
多线程
Z3
?
z3
、
z3py
我正在从事一个Python项目,目前我正试图以一些可怕
的
方式加快速度:我
设置
了我
的
Z3
解决程序,然后分叉进程,让
Z3
在子进程中执行解决方案,并将模型
的
可泡沫化表示传递给父进程。这很好,代表了我所要做
的
第一步:父进程现在不再受CPU约束。下一步是多线程父进程,这样我们就可以
并行
地求解多个
Z3
求解器。我确信在
设置
阶段我已经互斥了对
Z3
的
任何并发访问,而且在任何时候只有一个线程应该接触到
浏览 3
提问于2014-08-28
得票数 9
回答已采纳
1
回答
z3
:枚举类型、ADT和递归函数
z3
、
smt
我正在尝试使用
z3
来解决一些约束系统。问题
的
直观或一般编码是通过三种枚举类型Variable、Field和Class以及ADT Path来完成
的
,该枚举类型由Variable或用Path扩展
的
Field组成。(语法上是x或p.f)。我们知道,如果路径是类Zero
的
实例,那么路径也是类Nat
的
实例;如果路径是类Succ
的
实例,并且路径具有类Nat
的
字段p,那么路径也是类Nat
的
实例。我们向求解器提出
的
问题是:是否可能a
浏览 8
提问于2021-07-14
得票数 0
2
回答
寻找SMT
Z3
使用程序(
如
DbC)和开源替代
Z3
的
实用示例?
.net
、
constraint-programming
、
sat-solvers
、
z3
我对SMT
Z3
使用(
如
DbC)
的
代码和开源替代工具
的
实际示例很感兴趣,并寻找实例。因此,事实上,我对类似的
Z3
正式解决工具感兴趣,但是: 具有稳定(实用)
的
工具,如按合同设计(DbC)、静态类型验证等。、Spear、
浏览 3
提问于2011-01-06
得票数 5
回答已采纳
1
回答
忽略JAX-RS服务中用于数据解析
的
@JsonFormat
java
、
rest
、
date
、
jersey
、
jax-rs
检查其他问题,
如
: at
java
.text.DateFormat.parse(DateFormat.
java
:366)该注释似乎被忽略了。调试
浏览 1
提问于2015-09-30
得票数 7
回答已采纳
1
回答
C语言中
的
Z3
数组而非python
c
、
multidimensional-array
、
z3
如果你不知道
Z3
求解器,请不要回答。我之前发布了这个问题,一些答案,比如如
何用
C实现up.There中
的
数组,是一些在这个forum.Its中开发
Z3
求解器的人,目的是为了them.If你不知道
Z3
求解器,请避免回答这个问题。我早些时候发布了这个问题,并得到了解决方案,因为在Python.we中已经实现了以下问题已经在python.we中尝试移植
Z3
求解器来集成
Z3
求解器到内部工具作为我
的
thesis.Could
的
一部分,您帮我显示了
浏览 0
提问于2013-04-22
得票数 1
回答已采纳
2
回答
如何为
Z3
设置
Java
开发环境
java
、
ubuntu
、
installation
、
z3
如何为
Z3
SMT解决程序
设置
Java
开发环境? 注:作者所写和回答
的
,见。
浏览 6
提问于2020-02-25
得票数 4
回答已采纳
点击加载更多
扫码
添加站长 进交流群
领取专属
10元无门槛券
手把手带您无忧上云
相关
资讯
顶翔电子固定翼专用飞控——Z3油动和电动版
顶翔Z3飞控,让航模瞬间成无人机
你的游戏手机该扔了,vivo Z3超越游戏手机的表现令人惊讶
解锁多核处理器的力量:探索数据并行化在 Java 8 Stream 中的应用
vivo Z3呈现光与影的艺术变现,全面实力派只为品质生活
热门
标签
更多标签
云服务器
ICP备案
实时音视频
对象存储
即时通信 IM
活动推荐
运营活动
广告
关闭
领券