Struct Cvc5Plugin 

#[repr(C)]
pub struct Cvc5Plugin {
    pub check: Option<unsafe extern "C" fn(size: *mut usize, state: *mut c_void) -> *const Cvc5Term>,
    pub notify_sat_clause: Option<unsafe extern "C" fn(clause: Cvc5Term, state: *mut c_void)>,
    pub notify_theory_lemma: Option<unsafe extern "C" fn(lemma: Cvc5Term, state: *mut c_void)>,
    pub get_name: Option<unsafe extern "C" fn() -> *const c_char>,
    pub d_check_state: *mut c_void,
    pub d_notify_sat_clause_state: *mut c_void,
    pub d_notify_theory_lemma_state: *mut c_void,
}

A cvc5 plugin.

@note A typedef alias with the same name is also available for convenience.

Fields

check: Option<unsafe extern "C" fn(size: *mut usize, state: *mut c_void) -> *const Cvc5Term>

Call to check, return list of lemmas to add to the SAT solver. This method is called periodically, roughly at every SAT decision. @param size The size of the returned array of lemmas. @param state The state data for the function, may be NULL. @return The vector of lemmas to add to the SAT solver. @note This function pointer may be NULL to use the default implementation.

notify_sat_clause: Option<unsafe extern "C" fn(clause: Cvc5Term, state: *mut c_void)>

Notify SAT clause, called when clause is learned by the SAT solver. @param clause The learned clause. @param state The state data for the function, may be NULL. @note This function pointer may be NULL to use the default implementation.

notify_theory_lemma: Option<unsafe extern "C" fn(lemma: Cvc5Term, state: *mut c_void)>

Notify theory lemma, called when lemma is sent by a theory solver. @param lemma The theory lemma. @param state The state data for the function, may be NULL. @note This function pointer may be NULL to use the default implementation.

get_name: Option<unsafe extern "C" fn() -> *const c_char>

Get the name of the plugin (for debugging). @return The name of the plugin. @note This function pointer may NOT be NULL.

d_check_state: *mut c_void

The state to pass into check.

d_notify_sat_clause_state: *mut c_void

The state to pass into notify_sat_clause.

d_notify_theory_lemma_state: *mut c_void

The state to pass into notify_theory_lemma.

Trait Implementations

impl Clone for Cvc5Plugin

fn clone(&self) -> Cvc5Plugin

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Cvc5Plugin

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Cvc5Plugin

fn default() -> Self

Returns the “default value” for a type.

impl Copy for Cvc5Plugin