java - 如何通过Java设置Z3的并行模式
问题描述
我正在尝试改进 Z3 代码的时间。我的环境Z3使用的是Java,Z3的版本是4.8.10。为了设置并行模式,我使用了 Global 类并设置如下。
Global.setParameter("parallel.enable", "true");
但是,出现了以下警告。
WARNING: invalid parameter, unknown module 'parallel'
接下来,我尝试了以下方法。
Global.setParameter("parallel", "true");
现在,我收到以下警告
WARNING: unknown parameter 'parallel'
Legal parameters are:
auto_config (bool) (default: true)
debug_ref_count (bool) (default: false)
dump_models (bool) (default: false)
memory_high_watermark (unsigned int) (default: 0)
memory_max_alloc_count (unsigned int) (default: 0)
memory_max_size (unsigned int) (default: 0)
model (bool) (default: true)
model_validate (bool) (default: false)
proof (bool) (default: false)
rlimit (unsigned int) (default: 0)
smtlib2_compliant (bool) (default: false)
timeout (unsigned int) (default: 4294967295)
trace (bool) (default: false)
trace_file_name (string) (default: z3.log)
type_check (bool) (default: true)
unsat_core (bool) (default: false)
verbose (unsigned int) (default: 0)
warning (bool) (default: true)
well_sorted_check (bool) (default: false)
似乎“平行”项目本身并不存在。
如何编写代码以使用 Java API 设置并行模式?
另外,有样品吗?
解决方案
根据https://github.com/Z3Prover/z3/blob/939860148fdfe914b3832127fc190bc2a008e69f/RELEASE_NOTES#L126-L128,并行模式从 z3 4.8.0 开始可用。
您可能需要仔细检查您是否确实拥有足够新的 z3 版本。例如,以下代码适用于 4.8.11:
import com.microsoft.z3.*;
class JavaZ3Example {
public static void main(String [] args) {
Context ctx = new Context();
Global.setParameter("parallel.enable", "true");
ArithExpr a = ctx.mkDiv(ctx.mkReal(3),ctx.mkReal(5));
System.out.println(a.simplify());
};
};
以下是如何从 Java 检查 z3 安装版本的方法:
import com.microsoft.z3.*;
class JavaZ3Example {
public static void main(String [] args) {
System.out.println(Version.getFullVersion());
};
};
确保当你运行它时,你会得到类似的东西:
Z3 4.8.11.0
或更新。
推荐阅读
- ios - Swift UITableView:如何删除最后一个单元格下的空间
- java - 如何让 Intellj Idea 将依赖项写入 POM 文件?
- c - 当我尝试编译 yacc 和 lex 文件时出现一些错误
- python - sqlite3.operationalError:没有这样的列:sales_id
- python-3.x - 抓取 twitter 数据中的各种特征
- javascript - 如何在 nuxt 中为每种可用语言创建动态链接?
- c++ - 如何正确初始化此指针以避免分段错误?
- javascript - 如何在 .val() jquery 函数中添加多个变量
- node.js - 在'"db": "json-server -w db.json -p 3001"'中,这里的'-w'是什么意思?
- power-automate - 带有提醒的定期电子邮件