fix for SMT-LIB2 scopes for function definitions and let

SMT-LIB2 function definitions have scopes for the identifiers of the
parameters.  The same holds for let expressions.

This was raised in #5143.

The need to make the scoped identifiers unique will be removed once the IR
bindings have scopes.

Author: kroening

regression/smt2_solver/function-applications/function-scoping1.desc

@@ -0,0 +1,8 @@
+CORE
+function-scoping1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+^\(error

regression/smt2_solver/function-applications/function-scoping1.smt2

@@ -0,0 +1,12 @@
+(set-logic QF_BV)
+
+; the function parameters are in a separate scope
+
+(define-fun min ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 8)
+    (ite (bvule a b) a b))
+
+(declare-const a (_ BitVec 32))
+
+(assert (not (= a a)))
+
+(check-sat)

regression/smt2_solver/let1/let-scoping1.desc

@@ -0,0 +1,8 @@
+CORE
+let-scoping1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+^\(error

regression/smt2_solver/let1/let-scoping1.smt2

@@ -0,0 +1,12 @@
+(set-logic QF_BV)
+
+; the let parameters are in a separate scope
+(define-fun let1 () Bool (let ((a true)) a))
+(declare-const a (_ BitVec 32))
+(assert (not (= a a)))
+
+; declare-const first
+(declare-const b (_ BitVec 32))
+(define-fun let2 () Bool (let ((b true)) b))
+
+(check-sat)

src/solvers/smt2/smt2_parser.cpp

@@ -130,16 +130,6 @@ exprt::operandst smt2_parsert::operands()
 
 irep_idt smt2_parsert::add_fresh_id(const irep_idt &id, const exprt &expr)
 {
-  if(id_map
-       .emplace(
-         std::piecewise_construct,
-         std::forward_as_tuple(id),
-         std::forward_as_tuple(expr))
-       .second)
-  {
-    return id; // id not yet used
-  }
-
   auto &count=renaming_counters[id];
   irep_idt new_id;
   do
@@ -159,6 +149,20 @@ irep_idt smt2_parsert::add_fresh_id(const irep_idt &id, const exprt &expr)
   return new_id;
 }
 
+void smt2_parsert::add_unique_id(const irep_idt &id, const exprt &expr)
+{
+  if(!id_map
+       .emplace(
+         std::piecewise_construct,
+         std::forward_as_tuple(id),
+         std::forward_as_tuple(expr))
+       .second)
+  {
+    // id already used
+    throw error() << "identifier '" << id << "' defined twice";
+  }
+}
+
 irep_idt smt2_parsert::rename_id(const irep_idt &id) const
 {
   auto it=renaming_map.find(id);
@@ -1244,8 +1248,7 @@ void smt2_parsert::setup_commands()
     irep_idt id = smt2_tokenizer.get_buffer();
     auto type = sort();
 
-    if(add_fresh_id(id, exprt(ID_nil, type)) != id)
-      throw error() << "identifier '" << id << "' defined twice";
+    add_unique_id(id, exprt(ID_nil, type));
   };
 
   // declare-var appears to be a synonym for declare-const that is
@@ -1259,8 +1262,7 @@ void smt2_parsert::setup_commands()
     irep_idt id = smt2_tokenizer.get_buffer();
     auto type = function_signature_declaration();
 
-    if(add_fresh_id(id, exprt(ID_nil, type)) != id)
-      throw error() << "identifier '" << id << "' defined twice";
+    add_unique_id(id, exprt(ID_nil, type));
   };
 
   commands["define-const"] = [this]() {
@@ -1281,8 +1283,7 @@ void smt2_parsert::setup_commands()
     }
 
     // create the entry
-    if(add_fresh_id(id, value) != id)
-      throw error() << "identifier '" << id << "' defined twice";
+    add_unique_id(id, value);
   };
 
   commands["define-fun"] = [this]() {
@@ -1319,8 +1320,7 @@ void smt2_parsert::setup_commands()
     }
 
     // create the entry
-    if(add_fresh_id(id, body) != id)
-      throw error() << "identifier '" << id << "' defined twice";
+    add_unique_id(id, body);
 
     id_map.at(id).type = signature.type;
     id_map.at(id).parameters = signature.parameters;

src/solvers/smt2/smt2_parser.h

@@ -90,6 +90,7 @@ class smt2_parsert
   using renaming_counterst=std::map<irep_idt, unsigned>;
   renaming_counterst renaming_counters;
   irep_idt add_fresh_id(const irep_idt &, const exprt &);
+  void add_unique_id(const irep_idt &, const exprt &);
   irep_idt rename_id(const irep_idt &) const;
 
   struct signature_with_parameter_idst