From 489582f7fa9986e6576442ebce4943a754f7bdbd Mon Sep 17 00:00:00 2001
From: Bruce Mitchener <bruce.mitchener@gmail.com>
Date: Tue, 2 Oct 2018 09:19:14 +0700
Subject: [PATCH] Remove unused sat_par files.

These look like they were replaced by `sat_parallel` files and
aren't currently built or used.
---
 src/sat/sat_par.cpp  | 45 --------------------------------------------
 src/sat/sat_par.h    | 39 --------------------------------------
 src/sat/sat_solver.h |  1 -
 3 files changed, 85 deletions(-)
 delete mode 100644 src/sat/sat_par.cpp
 delete mode 100644 src/sat/sat_par.h

diff --git a/src/sat/sat_par.cpp b/src/sat/sat_par.cpp
deleted file mode 100644
index e3d5727ed..000000000
--- a/src/sat/sat_par.cpp
+++ /dev/null
@@ -1,45 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    sat_par.cpp
-
-Abstract:
-
-    Utilities for parallel SAT solving.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2017-1-29.
-
-Revision History:
-
---*/
-#include "sat/sat_par.h"
-
-
-namespace sat {
-
-    par::par() {}
-
-    void par::exchange(literal_vector const& in, unsigned& limit, literal_vector& out) {
-        #pragma omp critical (par_solver)
-        {
-            if (limit < m_units.size()) {
-                // this might repeat some literals.
-                out.append(m_units.size() - limit, m_units.c_ptr() + limit);
-            }
-            for (unsigned i = 0; i < in.size(); ++i) {
-                literal lit = in[i];
-                if (!m_unit_set.contains(lit.index())) {
-                    m_unit_set.insert(lit.index());
-                    m_units.push_back(lit);
-                }
-            }
-            limit = m_units.size();
-        }
-    }
-    
-};
-
diff --git a/src/sat/sat_par.h b/src/sat/sat_par.h
deleted file mode 100644
index 001036a98..000000000
--- a/src/sat/sat_par.h
+++ /dev/null
@@ -1,39 +0,0 @@
-/*++
-Copyright (c) 2017 Microsoft Corporation
-
-Module Name:
-
-    sat_par.h
-
-Abstract:
-
-    Utilities for parallel SAT solving.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2017-1-29.
-
-Revision History:
-
---*/
-#ifndef SAT_PAR_H_
-#define SAT_PAR_H_
-
-#include "sat/sat_types.h"
-#include "util/hashtable.h"
-#include "util/map.h"
-
-namespace sat {
-
-    class par {
-        typedef hashtable<unsigned, u_hash, u_eq> index_set;
-        literal_vector m_units;
-        index_set      m_unit_set;
-    public:
-        par();
-        void exchange(literal_vector const& in, unsigned& limit, literal_vector& out);
-    };
-
-};
-
-#endif
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index ad972b2af..e6e6c9d7b 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -37,7 +37,6 @@ Revision History:
 #include "sat/sat_drat.h"
 #include "sat/sat_parallel.h"
 #include "sat/sat_local_search.h"
-#include "sat/sat_par.h"
 #include "util/params.h"
 #include "util/statistics.h"
 #include "util/stopwatch.h"