SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
363 stars 45 forks source link

To do: upgrade per-thread-state #454

Closed disteph closed 9 months ago

disteph commented 11 months ago

...to the latest master. Then I'd like to propose to make it the new master. It seems that any single-threaded usage of Yices API is a valid use of the per-thread-state API, except that yices_init should become yices_global_init and yices_exit should become yices_global_exit. If no workers threads are involved, it looks like we should get the same behavior as with the single-threaded API. Am I missing anything?

ianamason commented 11 months ago

The main thread will need to do a thread init and thread exit if it wants to do some SAT solving.

disteph commented 11 months ago

It seems that yices_init() from the singly-threaded API can be redefined as

{
  yices_global_init();
  yices_per_thread_init();
}

from the multi-threaded API, no? And same thing for exits.

ianamason commented 11 months ago

I guess it depends on whether you want the main thread to be considered a worker thread. If it makes things simpler I guess it doesn't hurt.

disteph commented 11 months ago

With the above, call yices_global_init(); if you don't, and yices_init(); if you do.

disteph commented 11 months ago

and that's backward compatible with both branches.

ianamason commented 11 months ago

One aspect that may require some work, I'm not absolutely sure, but the configure stuff will need work I think. Since per-thread-state conflicts with thread-safety...

ahmed-irfan commented 9 months ago

merged master into the per-thread-state branch.

Currently the CI is disabled for this branch

ahmed-irfan commented 9 months ago

up-to-date 789e1a5b54d78e8c55c804e49c47dd001ff1b895