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.