Simplify interface to instantiate (#5926)

[cvc5.git] / src / theory / engine_output_channel.h

diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index 99f812ed4586833e854f573078e75d601a0fbafd..c53feabc5704702ef16802bddfd58f5e393bcf11 100644 (file)
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -2,10 +2,10 @@
 /*! \file engine_output_channel.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Dejan Jovanovic
+ **   Andrew Reynolds, Tim King, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
@@ -48,10 +48,9 @@ class EngineOutputChannel : public theory::OutputChannel
   void conflict(TNode conflictNode) override;
   bool propagate(TNode literal) override;
 
-  theory::LemmaStatus lemma(TNode lemma,
-                            LemmaProperty p = LemmaProperty::NONE) override;
+  void lemma(TNode lemma, LemmaProperty p = LemmaProperty::NONE) override;
 
-  theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) override;
+  void splitLemma(TNode lemma, bool removable = false) override;
 
   void demandRestart() override;
 
@@ -76,8 +75,8 @@ class EngineOutputChannel : public theory::OutputChannel
    * by the generator pfg. Apart from pfg, the interface for this method is
    * the same as calling OutputChannel::lemma on lem.
    */
-  LemmaStatus trustedLemma(TrustNode plem,
-                           LemmaProperty p = LemmaProperty::NONE) override;
+  void trustedLemma(TrustNode plem,
+                    LemmaProperty p = LemmaProperty::NONE) override;
 
  protected:
   /**