diff options
Diffstat (limited to 'passes/sat')
| -rw-r--r-- | passes/sat/qbfsat.cc | 10 | ||||
| -rw-r--r-- | passes/sat/qbfsat.h | 46 |
2 files changed, 28 insertions, 28 deletions
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 42d3e188a..db6836ea1 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -66,9 +66,9 @@ pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, bool ass } void specialize_from_file(RTLIL::Module *module, const std::string &file) { - YS_REGEX_TYPE hole_bit_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) \\[([0-9]+)] = ([01])$"); - YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) = ([01])$"); //if no index specified - YS_REGEX_MATCH_TYPE bit_m, m; + std::regex hole_bit_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) \\[([0-9]+)] = ([01])$"); + std::regex hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.+) ([0-9]+) ([^ ]+) = ([01])$"); //if no index specified + std::smatch bit_m, m; dict<pool<std::string>, RTLIL::Cell*> anyconst_loc_to_cell; dict<RTLIL::SigBit, RTLIL::State> hole_assignments; @@ -83,9 +83,9 @@ void specialize_from_file(RTLIL::Module *module, const std::string &file) { std::string buf; while (std::getline(fin, buf)) { bool bit_assn = true; - if (!YS_REGEX_NS::regex_search(buf, bit_m, hole_bit_assn_regex)) { + if (!std::regex_search(buf, bit_m, hole_bit_assn_regex)) { bit_assn = false; - if (!YS_REGEX_NS::regex_search(buf, m, hole_assn_regex)) + if (!std::regex_search(buf, m, hole_assn_regex)) log_cmd_error("solution file is not formatted correctly: \"%s\"\n", buf.c_str()); } diff --git a/passes/sat/qbfsat.h b/passes/sat/qbfsat.h index 8fb6093bc..253cecce4 100644 --- a/passes/sat/qbfsat.h +++ b/passes/sat/qbfsat.h @@ -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; } } |