The MCSAT solver is an optional component of Yices that requires the libpoly library. The MCSAT solver is necessary if you want Yices to handle non-linear arithmetic constraints.
Some functions in the Yices API convert real values to the
algebraic-number representation used by libpoly (structures of type
lp_algebraic_number_t). To use these functions, you must first
make sure that Yices is compiled with MCSAT support. You must also
install libpoly and include the appropriate header in you code
#include <poly/algebraic_number.h> #include <yices.h>
It is important to include
examples/example_mcsat.c included in the distribution
shows how to use these functions and how to solve a simple problem in
Check whether the Yices library was compiled with MCSAT support.
This function indicates whether the Yices library you are linking against was built with MCSAT support. It returns 1 for Yes and 0 for No.