Updates to theory preprocess equality (#5776)

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

diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index b6d9a19db8fd70121462da88df1f6e4433c4b582..0aa56a381db75dc09a5f651af6f2fd7a3b3535b5 100644 (file)
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -2,10 +2,10 @@
 /*! \file engine_output_channel.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Guy Katz, Tim King
+ **   Andrew Reynolds, Tim King, Morgan Deters
  ** 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
  **
@@ -69,7 +69,7 @@ void EngineOutputChannel::safePoint(ResourceManager::Resource r)
 
 theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
 {
-  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
+  Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
                          << lemma << ")"
                          << ", properties = " << p << std::endl;
   ++d_statistics.lemmas;
@@ -77,32 +77,31 @@ theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
 
   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
   theory::LemmaStatus result = d_engine->lemma(
-      tlem.getNode(),
-      false,
+      tlem,
       p,
-      isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST);
+      isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
+      d_theory);
   return result;
 }
 
 theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
 {
-  Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
+  Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
                          << lemma << ")" << std::endl;
   ++d_statistics.lemmas;
   d_engine->d_outputChannelUsed = true;
 
-  Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )"
+  Trace("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )"
                        << std::endl;
   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
   LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE;
-  theory::LemmaStatus result =
-      d_engine->lemma(tlem.getNode(), false, p, d_theory);
+  theory::LemmaStatus result = d_engine->lemma(tlem, p, d_theory);
   return result;
 }
 
 bool EngineOutputChannel::propagate(TNode literal)
 {
-  Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
+  Trace("theory::propagate") << "EngineOutputChannel<" << d_theory
                              << ">::propagate(" << literal << ")" << std::endl;
   ++d_statistics.propagations;
   d_engine->d_outputChannelUsed = true;
@@ -117,7 +116,7 @@ void EngineOutputChannel::conflict(TNode conflictNode)
   ++d_statistics.conflicts;
   d_engine->d_outputChannelUsed = true;
   TrustNode tConf = TrustNode::mkTrustConflict(conflictNode);
-  d_engine->conflict(tConf.getNode(), d_theory);
+  d_engine->conflict(tConf, d_theory);
 }
 
 void EngineOutputChannel::demandRestart()
@@ -135,7 +134,7 @@ void EngineOutputChannel::demandRestart()
 
 void EngineOutputChannel::requirePhase(TNode n, bool phase)
 {
-  Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase
+  Trace("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase
                   << ")" << std::endl;
   ++d_statistics.requirePhase;
   d_engine->getPropEngine()->requirePhase(n, phase);
@@ -162,19 +161,21 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf)
 {
   Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
   Trace("theory::conflict")
-      << "EngineOutputChannel<" << d_theory << ">::conflict(" << pconf.getNode()
-      << ")" << std::endl;
+      << "EngineOutputChannel<" << d_theory << ">::trustedConflict("
+      << pconf.getNode() << ")" << std::endl;
   if (pconf.getGenerator() != nullptr)
   {
     ++d_statistics.trustedConflicts;
   }
   ++d_statistics.conflicts;
   d_engine->d_outputChannelUsed = true;
-  d_engine->conflict(pconf.getNode(), d_theory);
+  d_engine->conflict(pconf, d_theory);
 }
 
 LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
 {
+  Trace("theory::lemma") << "EngineOutputChannel<" << d_theory
+                         << ">::trustedLemma(" << plem << ")" << std::endl;
   Assert(plem.getKind() == TrustNodeKind::LEMMA);
   if (plem.getGenerator() != nullptr)
   {
@@ -184,10 +185,10 @@ LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
   d_engine->d_outputChannelUsed = true;
   // now, call the normal interface for lemma
   return d_engine->lemma(
-      plem.getNode(),
-      false,
+      plem,
       p,
-      isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST);
+      isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
+      d_theory);
 }
 
 }  // namespace theory