mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-15 13:28:59 +00:00
Code Activity

qbfsat: Fix illegal use of 'stdout' identifier

Browse source 
Signed-off-by: David Shah <dave@ds0.me>
This commit is contained in:
David Shah 2020-04-17 08:42:39 +01:00
parent c69db910ac
commit 586739ecf3
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
passes/sat/qbfsat.cc
View file

@ -39,7 +39,7 @@ USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN PRIVATE_NAMESPACE_BEGIN
struct QbfSolutionType { struct QbfSolutionType {
std::vector<std::string> stdout; std::vector<std::string> stdout_lines;
dict<std::string, std::string> hole_to_value; dict<std::string, std::string> hole_to_value;
bool sat; bool sat;
bool unknown; //true if neither 'sat' nor 'unsat' bool unknown; //true if neither 'sat' nor 'unsat'
@ -72,7 +72,7 @@ void recover_solution(QbfSolutionType &sol) {
bool sat_regex_found = false; bool sat_regex_found = false;
bool unsat_regex_found = false; bool unsat_regex_found = false;
dict<std::string, bool> hole_value_recovered; dict<std::string, bool> hole_value_recovered;
for (const std::string &x : sol.stdout) { for (const std::string &x : sol.stdout_lines) {
if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) { if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
std::string loc = m[1].str(); std::string loc = m[1].str();
std::string val = m[2].str(); std::string val = m[2].str();
@ -294,7 +294,7 @@ QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
{ {
const std::string cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem.smt2 2>&1"; const std::string cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem.smt2 2>&1";
auto process_line = [&ret, &smtbmc_warning, &show_smtbmc](const std::string &line) { auto process_line = [&ret, &smtbmc_warning, &show_smtbmc](const std::string &line) {
ret.stdout.push_back(line.substr(0, line.size()-1)); //don't include trailing newline ret.stdout_lines.push_back(line.substr(0, line.size()-1)); //don't include trailing newline
auto warning_pos = line.find(smtbmc_warning); auto warning_pos = line.find(smtbmc_warning);
if (warning_pos != std::string::npos) if (warning_pos != std::string::npos)
log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str()); log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str());