1 files changed, 0 insertions, 120 deletions
diff --git a/src/proof/dimacs.cpp b/src/proof/dimacs.cpp
deleted file mode 100644
index d9d9f8c1c..000000000
--- a/src/proof/dimacs.cpp
+++ /dev/null
@@ -1,120 +0,0 @@
-/*********************                                                        */
-/*! \file dimacs.cpp
- ** \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 DIMACS SAT Problem Format
- **
- ** Defines serialization for SAT problems as DIMACS
- **/
-
-#include "proof/dimacs.h"
-
-#include "base/check.h"
-
-#include <iostream>
-
-namespace CVC4 {
-namespace proof {
-
-// Prints the literal as a (+) or (-) int
-// Not operator<< b/c that represents negation as ~
-std::ostream& textOut(std::ostream& o, const prop::SatLiteral& l)
-{
-  if (l.isNegated())
-  {
-    o << "-";
-  }
-  return o << l.getSatVariable() + 1;
-}
-
-// Prints the clause as a space-separated list of ints
-// Not operator<< b/c that represents negation as ~
-std::ostream& textOut(std::ostream& o, const prop::SatClause& c)
-{
-  for (const auto& l : c)
-  {
-    textOut(o, l) << " ";
-  }
-  return o << "0";
-}
-
-void printDimacs(std::ostream& o,
-                 const std::unordered_map<ClauseId, prop::SatClause>& clauses,
-                 const std::vector<ClauseId>& usedIndices)
-{
-  size_t maxVar = 0;
-  for (const ClauseId i : usedIndices)
-  {
-    const prop::SatClause& c = clauses.at(i);
-    for (const auto& l : c)
-    {
-      if (l.getSatVariable() + 1 > maxVar)
-      {
-        maxVar = l.getSatVariable() + 1;
-      }
-    }
-  }
-  o << "p cnf " << maxVar << " " << usedIndices.size() << '\n';
-  for (const ClauseId i : usedIndices)
-  {
-    const prop::SatClause& c = clauses.at(i);
-    for (const auto& l : c)
-    {
-      if (l.isNegated())
-      {
-        o << '-';
-      }
-      o << l.getSatVariable() + 1 << " ";
-    }
-    o << "0\n";
-  }
-}
-
-std::vector<prop::SatClause> parseDimacs(std::istream& in)
-{
-  std::string tag;
-  uint64_t nVars;
-  uint64_t nClauses;
-
-  in >> tag;
-  Assert(in.good());
-  Assert(tag == "p");
-
-  in >> tag;
-  Assert(in.good());
-  Assert(tag == "cnf");
-
-  in >> nVars;
-  Assert(nVars >= 0);
-
-  in >> nClauses;
-  Assert(nClauses >= 0);
-
-  std::vector<prop::SatClause> cnf;
-  for (uint64_t i = 0; i < nClauses; ++i)
-  {
-    cnf.emplace_back();
-    int64_t lit;
-    in >> lit;
-    Assert(in.good());
-    while (lit != 0)
-    {
-      cnf.back().emplace_back(std::abs(lit) - 1, lit < 0);
-      in >> lit;
-      Assert(static_cast<uint64_t>(std::abs(lit)) <= nVars);
-      Assert(in.good());
-    }
-  }
-
-  return cnf;
-}
-
-}  // namespace proof
-}  // namespace CVC4