Function proof_to_string 

pub unsafe extern "C" fn proof_to_string(
    cvc5: *mut Solver,
    proof: Proof,
    format: ProofFormat,
    size: usize,
    assertions: *const Term,
    names: *mut *const c_char,
) -> *const c_char

Prints a proof as a string in a selected proof format mode. Other aspects of printing are taken from the solver options.

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

@param cvc5 The solver instance. @param proof A proof, usually obtained from Solver::getProof(). @param format The proof format used to print the proof. Must be modes::ProofFormat::NONE if the proof is from a component other than modes::ProofComponent::FULL. @param size The number of assertions to names mappings given. @param assertions The list of assertions that are mapped to assertions_names. May be NULL if assertions_size is 0. @param names The names of the assertions (1:1 mapping). May by NULL if assertions is NULL.

@return The string representation of the proof in the given format.

@note The returned char* pointer is only valid until the next call to this function.