3

What are the current plans for reactivating the parallel version of Z3?

user1677256
  • 33
  • 3

1 Answers1

8

Z3 never had extensive support for parallelism. In version 2.x, we included an experimental feature that allowed users to execute several copies in parallel using different configuration options. The different copies could also share information and prune each other search space. This feature had some limitations. For example, it was not available in the programmatic API. It also conflicted with long term research goals and directions. Thus, this feature has been removed from recent versions.

That being said, in the Z3 4.x API, it is safe to create multiple contexts (Z3_Context) and access them concurrently from different threads. The previous versions were not thread safe. In Z3 4.x we can define custom strategies using parallel combinators. For example, the combinator (par-or t1 t2) executes the strategies t1 and t2 in parallel. These combinators are available in the programmatic API and SMT 2.0 front-end. The following online tutorial contains additional information: http://rise4fun.com/Z3/tutorial/strategies

The following command (for the SMT 2.0 front-end) will check the asserted formulas using two copies of the tactic smt with different random seeds.

(check-sat-using (par-or (! smt :random-seed 10) (! smt :random-seed 20)))
Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • 2
    Can we expect speedups with `par-or`? Does the tactic share information between two copies and prune search spaces? – pad Sep 17 '12 at 17:53
  • 1
    A bit late, but still: No, currently there is no sharing in par-or or par-and. – Christoph Wintersteiger Jun 14 '15 at 16:39
  • Is the branch of parallelism cut off from z3? Because I found this http://research.microsoft.com/en-us/um/people/leonardo/z3_doc/parallel.html – Mark Jin Oct 06 '15 at 17:09