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

Question

我正在努力改进我的 Z3 代码的时间。 Java在我的环境Z3中使用，Z3的版本是4.8.10。为了设置并行模式，我使用了全局class，设置如下。

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 编写代码来设置并行模式？

另外，有样品吗？

Answer 1

根据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

或更高版本。

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

How to set parallel mode of Z3 by Java

java

api

parallel-processing

solver

z3