pub unsafe extern "C" fn check_synth(cvc5: *mut Solver) -> SynthResultExpand description
Try to find a solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints.
SyGuS v2:
\verbatim embed:rst:leading-asterisk .. code:: smtlib
(check-synth)\endverbatim
@param cvc5 The solver instance. @return The result of the check, which is “solution” if the check found a solution in which case solutions are available via getSynthSolutions, “no solution” if it was determined there is no solution, or “unknown” otherwise.