mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
Merge pull request #1858 from waywardmonkeys/remove-unused-sat-par
Remove unused sat_par files.
This commit is contained in:
commit
b2430f5a0a
|
@ -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();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
};
|
|
||||||
|
|
|
@ -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
|
|
|
@ -37,7 +37,6 @@ Revision History:
|
||||||
#include "sat/sat_drat.h"
|
#include "sat/sat_drat.h"
|
||||||
#include "sat/sat_parallel.h"
|
#include "sat/sat_parallel.h"
|
||||||
#include "sat/sat_local_search.h"
|
#include "sat/sat_local_search.h"
|
||||||
#include "sat/sat_par.h"
|
|
||||||
#include "util/params.h"
|
#include "util/params.h"
|
||||||
#include "util/statistics.h"
|
#include "util/statistics.h"
|
||||||
#include "util/stopwatch.h"
|
#include "util/stopwatch.h"
|
||||||
|
|
Loading…
Reference in a new issue