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.