Merge pull request #5158 from diffblue/smt2_function_scoping_test

SMT-LIB2 parameter/let/quantifier scopes

Author: Daniel 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)

regression/smt2_solver/quanitfiers/quantifier-scoping.desc

@@ -0,0 +1,7 @@
+CORE
+quantifier-scoping.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

regression/smt2_solver/quanitfiers/quantifier-scoping.smt2

@@ -0,0 +1,12 @@
+(set-logic QF_BV)
+
+; the quantified identifiers are in a separate scope
+(define-fun q1 () Bool (exists ((a Bool)) a))
+(declare-const a (_ BitVec 32))
+(assert (not (= a a)))
+
+; declare-const first
+(declare-const b (_ BitVec 32))
+(define-fun q2 () Bool (exists ((b Bool)) 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);
@@ -258,12 +262,16 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
   if(next_token() != smt2_tokenizert::CLOSE)
     throw error("expected ')' at end of bindings");
 
-  // go forwards, add to id_map
-  for(const auto &b : bindings)
+  // save the renaming map
+  renaming_mapt old_renaming_map = renaming_map;
+
+  // go forwards, add to id_map, renaming if need be
+  for(auto &b : bindings)
   {
     const irep_idt id =
       add_fresh_id(b.get_identifier(), exprt(ID_nil, b.type()));
-    CHECK_RETURN(id == b.get_identifier());
+
+    b.set_identifier(id);
   }
 
   exprt expr=expression();
@@ -277,6 +285,9 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
   for(const auto &b : bindings)
     id_map.erase(b.get_identifier());
 
+  // restore renaming map
+  renaming_map = old_renaming_map;
+
   // go backwards, build quantified expression
   for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
   {
@@ -1241,8 +1252,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
@@ -1256,8 +1266,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]() {
@@ -1278,8 +1287,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]() {
@@ -1316,8 +1324,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