1 files changed, 0 insertions, 118 deletions
diff --git a/test/unit/proof/lfsc_proof_printer_black.h b/test/unit/proof/lfsc_proof_printer_black.h
deleted file mode 100644
index 74fda4996..000000000
--- a/test/unit/proof/lfsc_proof_printer_black.h
+++ /dev/null
@@ -1,118 +0,0 @@
-/*********************                                                        */
-/*! \file lfsc_proof_printer_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Alex Ozdemir
- ** 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.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of LFSC proof printing
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "proof/lfsc_proof_printer.h"
-#include "prop/sat_solver_types.h"
-#include "proof/clause_id.h"
-
-using namespace CVC4::proof;
-using namespace CVC4::prop;
-
-class LfscProofPrinterBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override {}
-  void tearDown() override {}
-
-  void testPrintClause();
-  void testPrintSatInputProof();
-  void testPrintCMapProof();
-};
-
-void LfscProofPrinterBlack::testPrintClause()
-{
-  SatClause clause{
-      SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, false)};
-  std::ostringstream lfsc;
-
-  LFSCProofPrinter::printSatClause(clause, lfsc, "");
-
-  std::string expectedLfsc =
-      "(clc (pos .v0) "
-      "(clc (neg .v1) "
-      "(clc (pos .v3) "
-      "cln)))";
-
-  TS_ASSERT_EQUALS(lfsc.str(), expectedLfsc);
-}
-
-void LfscProofPrinterBlack::testPrintSatInputProof()
-{
-  std::vector<CVC4::ClauseId> ids{2, 40, 3};
-  std::ostringstream lfsc;
-
-  LFSCProofPrinter::printSatInputProof(ids, lfsc, "");
-
-  std::string expectedLfsc =
-      "(cnfc_proof _ _ _ .pb2 "
-      "(cnfc_proof _ _ _ .pb40 "
-      "(cnfc_proof _ _ _ .pb3 "
-      "cnfn_proof)))";
-
-  std::ostringstream lfscWithoutWhitespace;
-  for (char c : lfsc.str())
-  {
-    if (!std::isspace(c))
-    {
-      lfscWithoutWhitespace << c;
-    }
-  }
-  std::ostringstream expectedLfscWithoutWhitespace;
-  for (char c : expectedLfsc)
-  {
-    if (!std::isspace(c))
-    {
-      expectedLfscWithoutWhitespace << c;
-    }
-  }
-
-  TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(),
-                   expectedLfscWithoutWhitespace.str());
-}
-
-void LfscProofPrinterBlack::testPrintCMapProof()
-{
-  std::vector<CVC4::ClauseId> ids{2, 40, 3};
-  std::ostringstream lfsc;
-
-  LFSCProofPrinter::printCMapProof(ids, lfsc, "");
-
-  std::string expectedLfsc =
-      "(CMapc_proof 1 _ _ _ .pb2 "
-      "(CMapc_proof 2 _ _ _ .pb40 "
-      "(CMapc_proof 3 _ _ _ .pb3 "
-      "CMapn_proof)))";
-
-  std::ostringstream lfscWithoutWhitespace;
-  for (char c : lfsc.str())
-  {
-    if (!std::isspace(c))
-    {
-      lfscWithoutWhitespace << c;
-    }
-  }
-  std::ostringstream expectedLfscWithoutWhitespace;
-  for (char c : expectedLfsc)
-  {
-    if (!std::isspace(c))
-    {
-      expectedLfscWithoutWhitespace << c;
-    }
-  }
-
-  TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(),
-                   expectedLfscWithoutWhitespace.str());
-}