Function find_synth 

pub unsafe extern "C" fn find_synth(
    cvc5: *mut Solver,
    target: FindSynthTarget,
) -> Term

Find a target term of interest using sygus enumeration, with no provided grammar.

The solver will infer which grammar to use in this call, which by default will be the grammars specified by the function(s)-to-synthesize in the current context.

SyGuS v2:

\verbatim embed:rst:leading-asterisk .. code:: smtlib

(find-synth :target)

\endverbatim

@param cvc5 The solver instance. @param target The identifier specifying what kind of term to find @return The result of the find, which is the null term if this call failed.

@warning This function is experimental and may change in future versions.