Search code examples
javaapiparallel-processingz3solver

How to set parallel mode of Z3 by Java


I am trying to improve the time of my Z3 code. Java is used in Z3 of my environment, and the version of Z3 is 4.8.10. In order to set the parallel mode, I used the Global class and set it as follows.

Global.setParameter("parallel.enable", "true");

However, the following warning occurred.

WARNING: invalid parameter, unknown module 'parallel'

Next, I tried the following.

Global.setParameter("parallel", "true");

Now, I get the following warning

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)

It seems that the item "parallel" itself does not exist.

How can I write code to set the parallel mode using the Java API?

Also, are there any samples?


Solution

  • According to https://github.com/Z3Prover/z3/blob/939860148fdfe914b3832127fc190bc2a008e69f/RELEASE_NOTES#L126-L128, parallel mode has been available since z3 4.8.0.

    You might want to double check that you indeed have a recent enough version of z3. For instance, the following code works for me just fine with 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());
       };
    };
    

    And here's how you can check your z3 installed version from Java:

    import com.microsoft.z3.*;
    
    class JavaZ3Example {
       public static void main(String [] args) {
          System.out.println(Version.getFullVersion());
       };
    };
    

    Make sure when you run this you get something like:

    Z3 4.8.11.0
    

    or newer.