1

I want to set up a system that will be fully dedicated to Z3. Let's say it has 4 cores and I would like to use all the power of the machine.

I will be solving large formulas that have around 1000 incremental asserts.

I would like to solve the formulas in a parallel fashion. I've read this question and I see that a unique Context should be created for every instance solving a formula.

My question then is, what is the most optimal way to use the full system resources (4 cores) and solving formulas with incremental asserts? Should I create a context per core and somehow sync the push and pops along them to incrementally solve the formulas?

Thanks

Community
  • 1
  • 1
user1618465
  • 1,813
  • 2
  • 32
  • 58
  • I don't think there is a "most optimal" way, it really depends on the problems you're trying to solve. If you're using the API you have to use separate contexts for every thread/process. I don't think there's a good reason for having more than one context per thread/process. – Christoph Wintersteiger Oct 05 '16 at 14:49
  • So you would create a Context per core? Will each context use a different core? Since there will be 1000 asserts that will be incrementally solved having 4 Contexts means having duplicated information 4 times (1 per core). I that right? Is there a better way to do it than just having every assert in every Context? Thank you @ChristophWintersteiger – user1618465 Oct 05 '16 at 18:05

1 Answers1

1

Expressions created via one context can not be used in another context. So, yes, if those cores/contexts need the same expressions, they will have to be copied and/or translated (see also Z3_translate).

Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30