Plugin 

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

class Plugin 

A cvc5 plugin.

Public Functions

Plugin ( TermManager & tm ) 

virtual ~Plugin ( ) = default 

virtual std :: vector < Term > check ( ) 

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

Returns :

The vector of lemmas to add to the SAT solver.

virtual void notifySatClause ( const Term & clause ) 

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

Parameters :

clause – The learned clause.

virtual void notifyTheoryLemma ( const Term & lemma ) 

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

Parameters :

lemma – The theory lemma.

virtual std :: string getName ( ) = 0 

Get the name of the plugin (for debugging).

Returns :

The name of the plugin.