如何通过Java设置Z3的并行模式

67 A 发表于 Dev

67A

我正在尝试改善我的 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());
   };
};

确保当你运行它时，你会得到类似的东西：