aboutsummaryrefslogtreecommitdiffstats
path: root/libs/minisat/Heap.h
blob: 057a3cdf247be9b4b18357cb738fee7e20b2b80b (plain)
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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
/******************************************************************************************[Heap.h]
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/

#ifndef Minisat_Heap_h
#define Minisat_Heap_h

#include "Vec.h"
#include "IntMap.h"

namespace Minisat {

//=================================================================================================
// A heap implementation with support for decrease/increase key.


template<class K, class Comp, class MkIndex = MkIndexDefault<K> >
class Heap {
    vec<K>                heap;     // Heap of Keys
    IntMap<K,int,MkIndex> indices;  // Each Key's position (index) in the Heap
    Comp                  lt;       // The heap is a minimum-heap with respect to this comparator

    // Index "traversal" functions
    static inline int left  (int i) { return i*2+1; }
    static inline int right (int i) { return (i+1)*2; }
    static inline int parent(int i) { return (i-1) >> 1; }


    void percolateUp(int i)
    {
        K   x  = heap[i];
        int p  = parent(i);
        
        while (i != 0 && lt(x, heap[p])){
            heap[i]          = heap[p];
            indices[heap[p]] = i;
            i                = p;
            p                = parent(p);
        }
        heap   [i] = x;
        indices[x] = i;
    }


    void percolateDown(int i)
    {
        K x = heap[i];
        while (left(i) < heap.size()){
            int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
            if (!lt(heap[child], x)) break;
            heap[i]          = heap[child];
            indices[heap[i]] = i;
            i                = child;
        }
        heap   [i] = x;
        indices[x] = i;
    }


  public:
    Heap(const Comp& c, MkIndex _index = MkIndex()) : indices(_index), lt(c) {}

    int  size      ()          const { return heap.size(); }
    bool empty     ()          const { return heap.size() == 0; }
    bool inHeap    (K k)       const { return indices.has(k) && indices[k] >= 0; }
    int  operator[](int index) const { assert(index < heap.size()); return heap[index]; }

    void decrease  (K k) { assert(inHeap(k)); percolateUp  (indices[k]); }
    void increase  (K k) { assert(inHeap(k)); percolateDown(indices[k]); }


    // Safe variant of insert/decrease/increase:
    void update(K k)
    {
        if (!inHeap(k))
            insert(k);
        else {
            percolateUp(indices[k]);
            percolateDown(indices[k]); }
    }


    void insert(K k)
    {
        indices.reserve(k, -1);
        assert(!inHeap(k));

        indices[k] = heap.size();
        heap.push(k);
        percolateUp(indices[k]);
    }


    void remove(K k)
    {
        assert(inHeap(k));

        int k_pos  = indices[k];
        indices[k] = -1;

        if (k_pos < heap.size()-1){
            heap[k_pos]          = heap.last();
            indices[heap[k_pos]] = k_pos;
            heap.pop();
            percolateDown(k_pos);
        }else
            heap.pop();
    }


    K removeMin()
    {
        K x              = heap[0];
        heap[0]          = heap.last();
        indices[heap[0]] = 0;
        indices[x]       = -1;
        heap.pop();
        if (heap.size() > 1) percolateDown(0);
        return x; 
    }


    // Rebuild the heap from scratch, using the elements in 'ns':
    void build(const vec<K>& ns) {
        for (int i = 0; i < heap.size(); i++)
            indices[heap[i]] = -1;
        heap.clear();

        for (int i = 0; i < ns.size(); i++){
            // TODO: this should probably call reserve instead of relying on it being reserved already.
            assert(indices.has(ns[i]));
            indices[ns[i]] = i;
            heap.push(ns[i]); }

        for (int i = heap.size() / 2 - 1; i >= 0; i--)
            percolateDown(i);
    }

    void clear(bool dispose = false) 
    { 
        // TODO: shouldn't the 'indices' map also be dispose-cleared?
        for (int i = 0; i < heap.size(); i++)
            indices[heap[i]] = -1;
        heap.clear(dispose); 
    }
};


//=================================================================================================
}

#endif
ss="p">(); extern "C" const char *prompt(); int main(int argc, char **argv) { EM_ASM( if (ENVIRONMENT_IS_NODE) { FS.mkdir('/hostcwd'); FS.mount(NODEFS, { root: '.' }, '/hostcwd'); FS.mkdir('/hostfs'); FS.mount(NODEFS, { root: '/' }, '/hostfs'); } ); mkdir("/work", 0777); chdir("/work"); log_files.push_back(stdout); log_error_stderr = true; yosys_banner(); yosys_setup(); if (argc == 2) { // Run the first argument as a script file run_frontend(argv[1], "script", 0, 0, 0); } } void run(const char *command) { int selSize = GetSize(yosys_get_design()->selection_stack); try { log_last_error = "Internal error (see JavaScript console for details)"; run_pass(command); log_last_error = ""; } catch (...) { while (GetSize(yosys_get_design()->selection_stack) > selSize) yosys_get_design()->selection_stack.pop_back(); throw; } } const char *errmsg() { return log_last_error.c_str(); } const char *prompt() { const char *p = create_prompt(yosys_get_design(), 0); while (*p == '\n') p++; return p; } #else /* EMSCRIPTEN */ #if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE) int yosys_history_offset = 0; std::string yosys_history_file; #endif void yosys_atexit() { #if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE) if (!yosys_history_file.empty()) { #if defined(YOSYS_ENABLE_READLINE) if (yosys_history_offset > 0) { history_truncate_file(yosys_history_file.c_str(), 100); append_history(where_history() - yosys_history_offset, yosys_history_file.c_str()); } else write_history(yosys_history_file.c_str()); #else write_history(yosys_history_file.c_str()); #endif } clear_history(); #if defined(YOSYS_ENABLE_READLINE) HIST_ENTRY **hist_list = history_list(); if (hist_list != NULL) free(hist_list); #endif #endif } int main(int argc, char **argv) { std::string frontend_command = "auto"; std::string backend_command = "auto"; std::vector<std::string> passes_commands; std::vector<std::string> plugin_filenames; std::string output_filename = ""; std::string scriptfile = ""; std::string depsfile = ""; bool scriptfile_tcl = false; bool got_output_filename = false; bool print_banner = true; bool print_stats = true; bool call_abort = false; bool timing_details = false; bool mode_v = false; bool mode_q = false; #if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE) if (getenv("HOME") != NULL) { yosys_history_file = stringf("%s/.yosys_history", getenv("HOME")); read_history(yosys_history_file.c_str()); yosys_history_offset = where_history(); } #endif if (argc == 2 && (!strcmp(argv[1], "-h") || !strcmp(argv[1], "-help") || !strcmp(argv[1], "--help"))) { printf("\n"); printf("Usage: %s [options] [<infile> [..]]\n", argv[0]); printf("\n"); printf(" -Q\n"); printf(" suppress printing of banner (copyright, disclaimer, version)\n"); printf("\n"); printf(" -T\n"); printf(" suppress printing of footer (log hash, version, timing statistics)\n"); printf("\n"); printf(" -q\n"); printf(" quiet operation. only write warnings and error messages to console\n"); printf(" use this option twice to also quiet warning messages\n"); printf("\n"); printf(" -v <level>\n"); printf(" print log headers up to level <level> to the console. (this\n"); printf(" implies -q for everything except the 'End of script.' message.)\n"); printf("\n"); printf(" -t\n"); printf(" annotate all log messages with a time stamp\n"); printf("\n"); printf(" -d\n"); printf(" print more detailed timing stats at exit\n"); printf("\n"); printf(" -l logfile\n"); printf(" write log messages to the specified file\n"); printf("\n"); printf(" -L logfile\n"); printf(" like -l but open log file in line buffered mode\n"); printf("\n"); printf(" -o outfile\n"); printf(" write the design to the specified file on exit\n"); printf("\n"); printf(" -b backend\n"); printf(" use this backend for the output file specified on the command line\n"); printf("\n"); printf(" -f frontend\n"); printf(" use the specified frontend for the input files on the command line\n"); printf("\n"); printf(" -H\n"); printf(" print the command list\n"); printf("\n"); printf(" -h command\n"); printf(" print the help message for the specified command\n"); printf("\n"); printf(" -s scriptfile\n"); printf(" execute the commands in the script file\n"); printf("\n"); printf(" -c tcl_scriptfile\n"); printf(" execute the commands in the tcl script file (see 'help tcl' for details)\n"); printf("\n"); printf(" -p command\n"); printf(" execute the commands\n"); printf("\n"); printf(" -m module_file\n"); printf(" load the specified module (aka plugin)\n"); printf("\n"); printf(" -X\n"); printf(" enable tracing of core data structure changes. for debugging\n"); printf("\n"); printf(" -M\n"); printf(" will slightly randomize allocated pointer addresses. for debugging\n"); printf("\n"); printf(" -A\n"); printf(" will call abort() at the end of the script. for debugging\n"); printf("\n"); printf(" -D <header_id>[:<filename>]\n"); printf(" dump the design when printing the specified log header to a file.\n"); printf(" yosys_dump_<header_id>.il is used as filename if none is specified.\n"); printf(" Use 'ALL' as <header_id> to dump at every header.\n"); printf("\n"); printf(" -W regex\n"); printf(" print a warning for all log messages matching the regex.\n"); printf("\n"); printf(" -w regex\n"); printf(" if a warning message matches the regex, it is printed as regular\n"); printf(" message instead.\n"); printf("\n"); printf(" -e regex\n"); printf(" if a warning message matches the regex, it is printed as error\n"); printf(" message instead and the tool terminates with a nonzero return code.\n"); printf("\n"); printf(" -E <depsfile>\n"); printf(" write a Makefile dependencies file with in- and output file names\n"); printf("\n"); printf(" -V\n"); printf(" print version information and exit\n"); printf("\n"); printf("The option -S is an shortcut for calling the \"synth\" command, a default\n"); printf("script for transforming the Verilog input to a gate-level netlist. For example:\n"); printf("\n"); printf(" yosys -o output.blif -S input.v\n"); printf("\n"); printf("For more complex synthesis jobs it is recommended to use the read_* and write_*\n"); printf("commands in a script file instead of specifying input and output files on the\n"); printf("command line.\n"); printf("\n"); printf("When no commands, script files or input files are specified on the command\n"); printf("line, yosys automatically enters the interactive command mode. Use the 'help'\n"); printf("command to get information on the individual commands.\n"); printf("\n"); exit(0); } int opt; while ((opt = getopt(argc, argv, "MXAQTVSm:f:Hh:b:o:p:l:L:qv:tds:c:W:w:e:D:E:")) != -1) { switch (opt) { case 'M': memhasher_on(); break; case 'X': yosys_xtrace++; break; case 'A': call_abort = true; break; case 'Q': print_banner = false; break; case 'T': print_stats = false; break; case 'V': printf("%s\n", yosys_version_str); exit(0); case 'S': passes_commands.push_back("synth"); break; case 'm': plugin_filenames.push_back(optarg); break; case 'f': frontend_command = optarg; break; case 'H': passes_commands.push_back("help"); break; case 'h': passes_commands.push_back(stringf("help %s", optarg)); break; case 'b': backend_command = optarg; break; case 'p': passes_commands.push_back(optarg); break; case 'o': output_filename = optarg; got_output_filename = true; break; case 'l': case 'L': log_files.push_back(fopen(optarg, "wt")); if (log_files.back() == NULL) { fprintf(stderr, "Can't open log file `%s' for writing!\n", optarg); exit(1); } if (opt == 'L') setvbuf(log_files.back(), NULL, _IOLBF, 0); break; case 'q': mode_q = true; if (log_errfile == stderr) log_quiet_warnings = true; log_errfile = stderr; break; case 'v': mode_v = true; log_errfile = stderr; log_verbose_level = atoi(optarg); break; case 't': log_time = true; break; case 'd': timing_details = true; break; case 's': scriptfile = optarg; scriptfile_tcl = false; break; case 'c': scriptfile = optarg; scriptfile_tcl = true; break; case 'W': log_warn_regexes.push_back(std::regex(optarg, std::regex_constants::nosubs | std::regex_constants::optimize | std::regex_constants::egrep)); break; case 'w': log_nowarn_regexes.push_back(std::regex(optarg, std::regex_constants::nosubs | std::regex_constants::optimize | std::regex_constants::egrep)); break; case 'e': log_werror_regexes.push_back(std::regex(optarg, std::regex_constants::nosubs | std::regex_constants::optimize | std::regex_constants::egrep)); break; case 'D': { auto args = split_tokens(optarg, ":"); if (!args.empty() && args[0] == "ALL") { if (GetSize(args) != 1) { fprintf(stderr, "Invalid number of tokens in -D ALL.\n"); exit(1); } log_hdump_all = true; } else { if (!args.empty() && !args[0].empty() && args[0].back() == '.') args[0].pop_back(); if (GetSize(args) == 1) args.push_back("yosys_dump_" + args[0] + ".il"); if (GetSize(args) != 2) { fprintf(stderr, "Invalid number of tokens in -D.\n"); exit(1); } log_hdump[args[0]].insert(args[1]); } } break; case 'E': depsfile = optarg; break; default: fprintf(stderr, "Run '%s -h' for help.\n", argv[0]); exit(1); } } if (log_errfile == NULL) { log_files.push_back(stdout); log_error_stderr = true; } if (print_banner) yosys_banner(); if (print_stats) log_hasher = new SHA1; #if defined(__linux__) // set stack size to >= 128 MB { struct rlimit rl; const rlim_t stack_size = 128L * 1024L * 1024L; if (getrlimit(RLIMIT_STACK, &rl) == 0 && rl.rlim_cur < stack_size) { rl.rlim_cur = stack_size; setrlimit(RLIMIT_STACK, &rl); } } #endif yosys_setup(); log_error_atexit = yosys_atexit; for (auto &fn : plugin_filenames) load_plugin(fn, {}); if (optind == argc && passes_commands.size() == 0 && scriptfile.empty()) { if (!got_output_filename) backend_command = ""; shell(yosys_design); } while (optind < argc) run_frontend(argv[optind++], frontend_command, output_filename == "-" ? &backend_command : NULL); if (!scriptfile.empty()) { if (scriptfile_tcl) { #ifdef YOSYS_ENABLE_TCL if (Tcl_EvalFile(yosys_get_tcl_interp(), scriptfile.c_str()) != TCL_OK) log_error("TCL interpreter returned an error: %s\n", Tcl_GetStringResult(yosys_get_tcl_interp())); #else log_error("Can't exectue TCL script: this version of yosys is not built with TCL support enabled.\n"); #endif } else run_frontend(scriptfile, "script", output_filename == "-" ? &backend_command : NULL); } for (auto it = passes_commands.begin(); it != passes_commands.end(); it++) run_pass(*it); if (!backend_command.empty()) run_backend(output_filename, backend_command); if (!depsfile.empty()) { FILE *f = fopen(depsfile.c_str(), "wt"); if (f == nullptr) log_error("Can't open dependencies file for writing: %s\n", strerror(errno)); bool first = true; for (auto fn : yosys_output_files) { fprintf(f, "%s%s", first ? "" : " ", fn.c_str()); first = false; } fprintf(f, ":"); for (auto fn : yosys_input_files) { if (yosys_output_files.count(fn) == 0) fprintf(f, " %s", fn.c_str()); } fprintf(f, "\n"); } if (print_stats) { std::string hash = log_hasher->final().substr(0, 10); delete log_hasher; log_hasher = nullptr; log_time = false; yosys_xtrace = 0; log_spacer(); if (mode_v && !mode_q) log_files.push_back(stderr); if (log_warnings_count) log("Warnings: %d unique messages, %d total\n", GetSize(log_warnings), log_warnings_count); #ifdef _WIN32 log("End of script. Logfile hash: %s\n", hash.c_str()); #else std::string meminfo; std::string stats_divider = ", "; # if defined(__linux__) std::ifstream statm; statm.open(stringf("/proc/%lld/statm", (long long)getpid())); if (statm.is_open()) { int sz_total, sz_resident; statm >> sz_total >> sz_resident; meminfo = stringf(", MEM: %.2f MB total, %.2f MB resident", sz_total * (getpagesize() / 1024.0 / 1024.0), sz_resident * (getpagesize() / 1024.0 / 1024.0)); stats_divider = "\n"; } # elif defined(__FreeBSD__) pid_t pid = getpid(); int mib[4] = {CTL_KERN, KERN_PROC, KERN_PROC_PID, (int)pid}; struct kinfo_proc kip; size_t kip_len = sizeof(kip); if (sysctl(mib, 4, &kip, &kip_len, NULL, 0) == 0) { vm_size_t sz_total = kip.ki_size; segsz_t sz_resident = kip.ki_rssize; meminfo = stringf(", MEM: %.2f MB total, %.2f MB resident", (int)sz_total / 1024.0 / 1024.0, (int)sz_resident * (getpagesize() / 1024.0 / 1024.0)); stats_divider = "\n"; } # endif struct rusage ru_buffer; getrusage(RUSAGE_SELF, &ru_buffer); log("End of script. Logfile hash: %s%sCPU: user %.2fs system %.2fs%s\n", hash.c_str(), stats_divider.c_str(), ru_buffer.ru_utime.tv_sec + 1e-6 * ru_buffer.ru_utime.tv_usec, ru_buffer.ru_stime.tv_sec + 1e-6 * ru_buffer.ru_stime.tv_usec, meminfo.c_str()); #endif log("%s\n", yosys_version_str); int64_t total_ns = 0; std::set<tuple<int64_t, int, std::string>> timedat; for (auto &it : pass_register) if (it.second->call_counter) { total_ns += it.second->runtime_ns + 1; timedat.insert(make_tuple(it.second->runtime_ns + 1, it.second->call_counter, it.first)); } if (timing_details) { log("Time spent:\n"); for (auto it = timedat.rbegin(); it != timedat.rend(); it++) { log("%5d%% %5d calls %8.3f sec %s\n", int(100*std::get<0>(*it) / total_ns), std::get<1>(*it), std::get<0>(*it) / 1000000000.0, std::get<2>(*it).c_str()); } } else { int out_count = 0; log("Time spent:"); for (auto it = timedat.rbegin(); it != timedat.rend() && out_count < 4; it++, out_count++) { if (out_count >= 2 && (std::get<0>(*it) < 1000000000 || int(100*std::get<0>(*it) / total_ns) < 20)) { log(", ..."); break; } log("%s %d%% %dx %s (%d sec)", out_count ? "," : "", int(100*std::get<0>(*it) / total_ns), std::get<1>(*it), std::get<2>(*it).c_str(), int(std::get<0>(*it) / 1000000000)); } log("%s\n", out_count ? "" : " no commands executed"); } } #if defined(YOSYS_ENABLE_COVER) && (defined(__linux__) || defined(__FreeBSD__)) if (getenv("YOSYS_COVER_DIR") || getenv("YOSYS_COVER_FILE")) { string filename; FILE *f; if (getenv("YOSYS_COVER_DIR")) { filename = stringf("%s/yosys_cover_%d_XXXXXX.txt", getenv("YOSYS_COVER_DIR"), getpid()); filename = make_temp_file(filename); } else { filename = getenv("YOSYS_COVER_FILE"); } f = fopen(filename.c_str(), "a+"); if (f == NULL) log_error("Can't create coverage file `%s'.\n", filename.c_str()); log("<writing coverage file \"%s\">\n", filename.c_str()); for (auto &it : get_coverage_data()) fprintf(f, "%-60s %10d %s\n", it.second.first.c_str(), it.second.second, it.first.c_str()); fclose(f); } #endif yosys_atexit(); memhasher_off(); if (call_abort) abort(); log_flush(); #if defined(_MSC_VER) _exit(0); #elif defined(_WIN32) _Exit(0); #endif yosys_shutdown(); return 0; } #endif /* EMSCRIPTEN */