Skip to main content

get_synth_solution

cvc5_sys

Function get_synth_solution 

Source 
pub unsafe extern "C" fn get_synth_solution(
    cvc5: *mut Solver,
    term: Term,
) -> Term
Expand description

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