Thread-Safe API

The Yices library is not re-entrrant by default, but it can be compiled to be re-entrant if Yices is configured with option --thread-safety.

The following function can be called to determine whether the library was compiled with this option or not.

int32_t yices_is_thread_safe(void)

Check whether the Yices library is re-entrant.

This function indicates whether the Yices library you are linking against was built with optoin --thread-safety. It returns 1 for Yes and 0 for No.

If Yices is compiled with this option, it is possible to use the library in multi-threaded applications. All calls to API functions that create terms or types are protected by a global lock, but it is possible to operate on separate contexts and models in parallel. In particular, distinct threads can call yices_check_context on different contexts in parallel without locking.

You still have to ensure that distinct threads do not operate on the same context or model at the same time.