AbstractPlugin

java.lang.Object
- io.github.cvc5.AbstractPlugin

public abstract class AbstractPlugin
extends java.lang.Object

Field Summary

Fields
Modifier and Type Field Description

protected TermManager termManager

Constructor Summary

Constructors
Constructor Description

AbstractPlugin(TermManager tm)
Create plugin instance.

Method Summary

All Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method	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.