mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-08-18 17:22:17 +00:00
Code Activity

Deprecate gcc-4.8

Browse source
This commit is contained in:
Miodrag Milanovic 2023-01-11 09:54:19 +01:00
parent 7b476996df
commit 5801152779
10 changed files with 58 additions and 127 deletions
Download patch file Download diff file Expand all files Collapse all files

46
passes/sat/qbfsat.h
View file

@ -154,67 +154,67 @@ struct QbfSolutionType {
}
void recover_solution() {
YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
YS_REGEX_TYPE unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED");
YS_REGEX_TYPE timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)");
YS_REGEX_TYPE timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)");
YS_REGEX_TYPE unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)");
YS_REGEX_TYPE unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver");
YS_REGEX_TYPE memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\"");
YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
std::regex sat_regex = YS_REGEX_COMPILE("Status: PASSED");
std::regex unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
std::regex unsat_regex2 = YS_REGEX_COMPILE("Status: FAILED");
std::regex timeout_regex = YS_REGEX_COMPILE("No solution found! \\(timeout\\)");
std::regex timeout_regex2 = YS_REGEX_COMPILE("No solution found! \\(interrupted\\)");
std::regex unknown_regex = YS_REGEX_COMPILE("No solution found! \\(unknown\\)");
std::regex unknown_regex2 = YS_REGEX_COMPILE("Unexpected EOF response from solver");
std::regex memout_regex = YS_REGEX_COMPILE("Solver Error:.*error \"out of memory\"");
std::regex hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
#ifndef NDEBUG
YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
std::regex hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
std::regex hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
#endif
YS_REGEX_MATCH_TYPE m;
std::smatch m;
bool sat_regex_found = false;
bool unsat_regex_found = false;
dict<std::string, bool> hole_value_recovered;
for (const std::string &x : stdout_lines) {
if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
if(std::regex_search(x, m, hole_value_regex)) {
std::string loc = m[1].str();
std::string val = m[2].str();
#ifndef NDEBUG
log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
log_assert(std::regex_search(loc, hole_loc_regex));
log_assert(std::regex_search(val, hole_val_regex));
#endif
auto locs = split_tokens(loc, "|");
pool<std::string> loc_pool(locs.begin(), locs.end());
hole_to_value[loc_pool] = val;
}
else if (YS_REGEX_NS::regex_search(x, sat_regex)) {
else if (std::regex_search(x, sat_regex)) {
sat_regex_found = true;
sat = true;
unknown = false;
}
else if (YS_REGEX_NS::regex_search(x, unsat_regex)) {
else if (std::regex_search(x, unsat_regex)) {
unsat_regex_found = true;
sat = false;
unknown = false;
}
else if (YS_REGEX_NS::regex_search(x, memout_regex)) {
else if (std::regex_search(x, memout_regex)) {
unknown = true;
log_warning("solver ran out of memory\n");
}
else if (YS_REGEX_NS::regex_search(x, timeout_regex)) {
else if (std::regex_search(x, timeout_regex)) {
unknown = true;
log_warning("solver timed out\n");
}
else if (YS_REGEX_NS::regex_search(x, timeout_regex2)) {
else if (std::regex_search(x, timeout_regex2)) {
unknown = true;
log_warning("solver timed out\n");
}
else if (YS_REGEX_NS::regex_search(x, unknown_regex)) {
else if (std::regex_search(x, unknown_regex)) {
unknown = true;
log_warning("solver returned \"unknown\"\n");
}
else if (YS_REGEX_NS::regex_search(x, unsat_regex2)) {
else if (std::regex_search(x, unsat_regex2)) {
unsat_regex_found = true;
sat = false;
unknown = false;
}
else if (YS_REGEX_NS::regex_search(x, unknown_regex2)) {
else if (std::regex_search(x, unknown_regex2)) {
unknown = true;
}
}