Skip to main content

get_synth_solutions

Function get_synth_solutions 

Source
pub unsafe extern "C" fn get_synth_solutions(
    cvc5: *mut Solver,
    size: usize,
    terms: *const Term,
) -> *const Term
Expand description

Get the synthesis solutions of the given terms. This function should be called immediately after the solver answers unsat for sygus input. @param cvc5 The solver instance. @param size The size of the terms array. @param terms The terms for which the synthesis solutions is queried. @return The synthesis solutions of the given terms.