使用 z3 <smt2-file > CC_NUM_THREADS=3 配置并行 Z3 时出现问题

Question

使用 z3 CC_NUM_THREADS=3 配置并行 Z3 时出现问题

我正在尝试为我的 smt2 文件运行带有 CC_NUM_THREADS=3 的 z3 并行版本 弹出以下错误。

ERROR: unknown parameter 'cc_num_threads'
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: 4294967295)
 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)

Answer 1

不再支持此功能（并且已经很久没有支持了）。您可以制定自己的并行策略，例如，请参阅 Strategies Tutorial 的策略部分中的 par-or 示例。