io.github.cvc5

Class AbstractPlugin

java.lang.Object

io.github.cvc5.AbstractPlugin

public abstract class AbstractPlugin
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
protected TermManager	termManager

Constructor Summary

Constructors

Constructor and Description
AbstractPlugin(TermManager tm) Create plugin instance.

Method Summary

Modifier and Type	Method and Description
Term[]	check() Call to check, return vector of lemmas to add to the SAT solver.
abstract java.lang.String	getName() Get the name of the plugin (for debugging).
TermManager	getTermManager() Get the associated term manager instance
void	notifySatClause(Term cl) Notify SAT clause, called when cl is a clause learned by the SAT solver.
void	notifyTheoryLemma(Term lem) Notify theory lemma, called when lem is a theory lemma sent by a theory solver.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

termManager

protected final TermManager termManager

Constructor Detail

AbstractPlugin

public AbstractPlugin(TermManager tm)

Create plugin instance.

Parameters:

tm - The associated term manager.

Method Detail

getTermManager

public TermManager getTermManager()

Get the associated term manager instance

Returns:

The term manager.

check

public 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.

notifySatClause

public void notifySatClause(Term cl)

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

Parameters:

cl - The learned clause.

notifyTheoryLemma

public void notifyTheoryLemma(Term lem)

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

Parameters:

lem - The theory lemma.

getName

public abstract java.lang.String getName()

Get the name of the plugin (for debugging).

Returns:

The name of the plugin.