cvc4-1.4
|
Mechanism for communication about new lemmas. More...
Go to the source code of this file.
Data Structures | |
class | CVC4::LemmaOutputChannel |
This interface describes a mechanism for the propositional and theory engines to communicate with the "outside world" about new lemmas being discovered. More... | |
Namespaces | |
CVC4 | |
Mechanism for communication about new lemmas.
** Original author: Morgan Deters ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.
This file defines an interface for use by the theory and propositional engines to communicate new lemmas to the "outside world," for example for lemma sharing between threads.
Definition in file lemma_output_channel.h.