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.