ParaHCEC/sweep.hpp at main · shaowei-cai-group/ParaHCEC · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
#ifndef sweep_hpp_INCLUDED
#define sweep_hpp_INCLUDED
#include <chrono>
#include <bits/stdc++.h>
#include <cstring>
#include <sys/resource.h>
#include <unistd.h>
#include "vec.hpp"
#include "bitset.h"

struct kissat;

struct aiger;
enum gate_type {And, Xor, UNUSE};
const std::string gate_type[6] = {"and", "xor", "majority", "HA", "FA", "UNUSE"};
class Bitset;

struct type_gate {
    vec<int> in;
    int ins, out, type;
    type_gate() : ins(0), out(0), type(0) {}
    void push_in (int x) { in .push(x); ins++; }
    int       &operator [] (int index)       { return in[index]; }
    const int& operator [] (int index) const { return in[index]; }
    type_gate& operator = (const type_gate& other) {
        ins = other.ins;
        out = other.out;
        type = other.type;
        in.growTo(ins);
        for (int i = 0; i < ins; i++) in[i] = other.in[i];
        return *this;
    }
};

struct type_cell {
    int fanouts = 0;
    int gate = 0;
    int is_carrier = 0;
};

struct cal_info {
    int vars = 0, gates = 0;
    int pairs = 0;
    int pairs_ec = 0, pairs_sat = 0;
    int pairs_ec_ver = 0, pairs_sat_ver = 0;
    int pairs_act = 0;
    int pairs_fanin = 0;
    int pairs_stru = 0;
    int pairs_ver = 0;
    double times_ec = 0, times_sat = 0;
};

class Sweep {
public:
    FILE* file;
    int nThreads;
    int maxvar, output, inputs, rounds, stamp = 0, xors = 0;
    double max_score = 0, max_connect = 0;
    bool is_sat;
    int *input, *topo_index, *used, *model, *size, *q, *active, *is_input, *topo_counter, *table, *var_stamp, *fanout, *par, *xors_bot, *xors_id, *bucket, *task_sign;
    vec<type_gate> gate;
    type_cell *cell;
    vec<int> *inv_C, *inv_V, cnf_solve, cnf_model;
    int this_epcec = 0, simp_sz = 0;
    int maxR;
    // BitsetPool *pool;
    Bitset*** result;
    int **fanouts;
    int **counter;
    int **used_var;
    int **queue;
    vec<int> epcec_in, epcec_out;
    std::chrono::high_resolution_clock::time_point clk_st = std::chrono::high_resolution_clock::now();
    std::vector<std::pair<int, std::pair<int, int>>> equal_pairs;
    vec<std::pair<int, int>> verified_pairs;
    std::map<int, int> M;
    std::map<std::pair<int, int>, int> M_pair;
    aiger *aig;
    kissat * ksolver;
    cal_info info;

    // 内存监控相关变量
    size_t peak_memory_usage = 0;
    size_t initial_memory_usage = 0;
    size_t peak_virtual_memory = 0;
    size_t initial_virtual_memory = 0;
    void pre_seq_CEC();
    void show_struct();
    int  find_par(int x);
    void cal_xor();
    void cal_size();
    void cal_topo_index();
    void identify();
    void recalculate_outs();
    bool match_xor(int x);
    int  merge(int x, int y);
    void fix_var(int x);

    void cal_xor_and_pis(int x, int y, int &pis, double &score);
    int  sign(int x);
    void print_model();
    void print_result_and_exit(const char* reason, int* input_vector);
    void solve();
    void aiger_preprocess();
    bool pcec();
    bool exact_pcec();
    bool _simulate(Bitset** result, int len_size, int thread_id);
    bool check_var_struct(int x, int y);
    bool seq_CEC();
    bool seq_check_var_equal(int x, int y);
    bool seq_miter();

    void generate_input(Bitset** result, const vec<int> &input_list, void* _pool);

    int  parallel_solve(int nThreads, int model = 0);
    int  test_parallel_solve(int nThreads);
    int  parallel_epcec(int nThreads);
};


#endif