2022-08-30 15:42:35 +08:00
|
|
|
#ifndef _light_hpp_INCLUDED
|
|
|
|
#define _light_hpp_INCLUDED
|
|
|
|
|
|
|
|
#include "utils/paras.hpp"
|
2023-03-20 21:40:19 +08:00
|
|
|
#include "utils/parse.hpp"
|
2023-02-24 07:58:40 +00:00
|
|
|
#include "preprocess/preprocess.hpp"
|
2022-08-30 15:42:35 +08:00
|
|
|
#include <atomic>
|
|
|
|
#include <iostream>
|
2023-03-15 14:15:44 +08:00
|
|
|
#include <boost/thread.hpp>
|
|
|
|
#include <boost/thread/thread.hpp>
|
|
|
|
#include <boost/lockfree/spsc_queue.hpp>
|
2022-08-30 15:42:35 +08:00
|
|
|
typedef long long ll;
|
|
|
|
|
|
|
|
class basesolver;
|
2022-09-08 13:54:29 +08:00
|
|
|
class sharer;
|
|
|
|
|
2022-09-15 10:31:41 +08:00
|
|
|
extern std::atomic<int> terminated;
|
2022-12-04 23:30:36 +08:00
|
|
|
extern std::mutex mtx;
|
2022-08-30 15:42:35 +08:00
|
|
|
|
2023-03-20 21:40:19 +08:00
|
|
|
enum Solver_Type {KISSAT};
|
|
|
|
|
2022-08-31 09:16:12 +00:00
|
|
|
struct thread_inf{
|
|
|
|
int id, inf;
|
|
|
|
bool operator < ( const thread_inf &other ) const
|
|
|
|
{
|
|
|
|
return inf > other.inf;
|
|
|
|
}
|
|
|
|
};
|
|
|
|
|
2022-08-30 15:42:35 +08:00
|
|
|
struct light
|
|
|
|
{
|
|
|
|
public:
|
|
|
|
light();
|
|
|
|
~light();
|
|
|
|
|
|
|
|
char *filename;
|
|
|
|
paras *opt;
|
|
|
|
preprocess *pre;
|
2023-03-20 21:40:19 +08:00
|
|
|
vec<int> solver_type;
|
2022-08-31 09:16:12 +00:00
|
|
|
vec<basesolver *> workers;
|
2022-09-08 13:54:29 +08:00
|
|
|
vec<sharer *> sharers;
|
2023-03-20 21:40:19 +08:00
|
|
|
|
|
|
|
vec<char*> *configure_name;
|
|
|
|
vec<double> *configure_val;
|
2022-08-30 15:42:35 +08:00
|
|
|
|
|
|
|
int finalResult;
|
2023-03-15 14:15:44 +08:00
|
|
|
int winner_period, winner_id;
|
|
|
|
mutable boost::mutex winner_mtx;
|
2022-08-30 15:42:35 +08:00
|
|
|
int maxtime;
|
2023-03-15 14:15:44 +08:00
|
|
|
void update_winner(int id, int period) {
|
|
|
|
boost::mutex::scoped_lock lock(winner_mtx);
|
|
|
|
if (period < winner_period || (period == winner_period && id < winner_id)) {
|
|
|
|
winner_period = period;
|
|
|
|
winner_id = id;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
int get_winner_period() {
|
|
|
|
boost::mutex::scoped_lock lock(winner_mtx);
|
|
|
|
return winner_period;
|
|
|
|
}
|
2022-08-30 15:42:35 +08:00
|
|
|
void arg_parse(int argc, char **argv);
|
2023-03-20 21:40:19 +08:00
|
|
|
void configure_from_file(const char* file);
|
2022-08-31 09:16:12 +00:00
|
|
|
void init_workers();
|
|
|
|
void diversity_workers();
|
2022-08-30 15:42:35 +08:00
|
|
|
void parse_input();
|
|
|
|
int run();
|
2022-09-08 13:54:29 +08:00
|
|
|
void share();
|
2022-08-30 15:42:35 +08:00
|
|
|
int solve();
|
2022-08-31 09:16:12 +00:00
|
|
|
void terminate_workers();
|
2022-08-30 15:42:35 +08:00
|
|
|
void print_model();
|
|
|
|
};
|
|
|
|
|
|
|
|
#endif
|