From 26d25a46ec98d4a42f1b5b9c343bf20a0ae31d22 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 15 Jun 2021 12:43:53 +0100 Subject: [PATCH] SMT2 frontend: renaming let bindings is no longer necessary The solver backends no longer require that the symbols bound by let expressions are unique. --- src/solvers/smt2/smt2_parser.cpp | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index e2dea2e9383..cd0dd86e03d 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -208,16 +208,22 @@ exprt smt2_parsert::let_expression() if(next_token() != smt2_tokenizert::CLOSE) throw error("expected ')' at end of bindings"); - // save the renaming map - renaming_mapt old_renaming_map=renaming_map; + // we may hide identifiers in outer scopes + std::vector> saved_ids; - // go forwards, add to id_map, renaming if need be + // add the bindings to the id_map for(auto &b : bindings) { - // get a fresh id for it - b.first = add_fresh_id(b.first, idt::BINDING, b.second); + auto insert_result = id_map.insert({b.first, idt{idt::BINDING, b.second}}); + if(!insert_result.second) // already there + { + auto &id_entry = *insert_result.first; + saved_ids.emplace_back(id_entry.first, std::move(id_entry.second)); + id_entry.second = idt{idt::BINDING, b.second}; + } } + // now parse, with bindings in place exprt where = expression(); if(next_token() != smt2_tokenizert::CLOSE) @@ -232,11 +238,13 @@ exprt smt2_parsert::let_expression() values.push_back(b.second); } - // we keep these in the id_map in order to retain globally - // unique identifiers + // delete the bindings from the id_map + for(const auto &binding : bindings) + id_map.erase(binding.first); - // restore renamings - renaming_map=old_renaming_map; + // restore any previous ids + for(auto &saved_id : saved_ids) + id_map.insert(std::move(saved_id)); return let_exprt(variables, values, where); }