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
.
-
const
Cvc5Term
*
(
*
check
)
(
size_t
*
size
,
void
*
state
)