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.