Plugin 

This class encapsulates a user-specified solver plugin. It is configured via cvc5.Solver.addPlugin() .

class cvc5. Plugin 

A cvc5 plugin.

Wrapper class for cvc5::Plugin .

check ( ) 

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

Returns :

The list of lemmas to add to the SAT solver.

getName ( ) 

Get the name of the plugin (for debugging).

Returns :

The name of the plugin.

notifySatClause ( ) 

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

Parameters :

cl – The learned clause.

notifyTheoryLemma ( ) 

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

Parameters :

lem – The theory lemma.