Cvc5Plugin

This structs encapsulates a user-specified solver plugin. It is configured via cvc5_add_plugin().

typedef struct Cvc5Plugin Cvc5Plugin

struct Cvc5Plugin

A cvc5 plugin.

Public Members

const Cvc5Term *(*check)(size_t *size, void *state)

Call to check, return list of lemmas to add to the SAT solver. This method is called periodically, roughly at every SAT decision.

Note

This function pointer may be NULL to use the default implementation.

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.

void (*notify_sat_clause)(const Cvc5Term clause, void *state)

Notify SAT clause, called when clause is learned by the SAT solver.

Note

This function pointer may be NULL to use the default implementation.

Param clause:

The learned clause.

Param state:

The state data for the function, may be NULL.

void (*notify_theory_lemma)(const Cvc5Term lemma, void *state)

Notify theory lemma, called when lemma is sent by a theory solver.

Note

This function pointer may be NULL to use the default implementation.

Param lemma:

The theory lemma.

Param state:

The state data for the function, may be NULL.

const char *(*get_name)()

Get the name of the plugin (for debugging).

Note

This function pointer may NOT be NULL.

Return:

The name of the plugin.

void *d_check_state

The state to pass into check.

void *d_notify_sat_clause_state

The state to pass into notify_sat_clause.

void *d_notify_theory_lemma_state

The state to pass into notify_theory_lemma.