cvc4-1.4
CVC4::LemmaOutputChannel Class Referenceabstract

This interface describes a mechanism for the propositional and theory engines to communicate with the "outside world" about new lemmas being discovered. More...

#include <lemma_output_channel.h>

Public Member Functions

virtual ~LemmaOutputChannel () throw ()
 
virtual void notifyNewLemma (Expr lemma)=0
 Notifies this output channel that there's a new lemma. More...
 

Detailed Description

This interface describes a mechanism for the propositional and theory engines to communicate with the "outside world" about new lemmas being discovered.

Definition at line 33 of file lemma_output_channel.h.

Constructor & Destructor Documentation

◆ ~LemmaOutputChannel()

virtual CVC4::LemmaOutputChannel::~LemmaOutputChannel ( )
throw (
)
inlinevirtual

Definition at line 35 of file lemma_output_channel.h.

Member Function Documentation

◆ notifyNewLemma()

virtual void CVC4::LemmaOutputChannel::notifyNewLemma ( Expr  lemma)
pure virtual

Notifies this output channel that there's a new lemma.

The lemma may or may not be in CNF.


The documentation for this class was generated from the following file: