SMV: further support for assignments of sets to scalars

This extends the support for assignments of sets to scalars in the SMV type
checker, via recursive conversion to a predicate.

Author: kroening

src/smvlang/smv_typecheck.cpp

@@ -96,6 +96,7 @@ class smv_typecheckt:public typecheckt
   void typecheck_expr_rec(exprt &, modet, bool next);
   void convert_expr_to(exprt &, const typet &dest);
   void typecheck_assignment(exprt &);
+  exprt assign_set_rec(const exprt &lhs, const exprt &set_expression);
   exprt convert_word_constant(const constant_exprt &) const;
 
   smv_parse_treet::modulet *modulep;
@@ -1868,25 +1869,56 @@ void smv_typecheckt::typecheck_assignment(exprt &expr)
   auto &lhs = equal_expr.lhs();
   auto &rhs = equal_expr.rhs();
 
-  if(rhs.type().id() == ID_smv_set && rhs.id() == ID_smv_set)
+  if(rhs.type().id() == ID_smv_set)
   {
     // Sets can be assigned to scalars, which yields a nondeterministic
-    // choice. First check the set elements.
-    for(auto &op : rhs.operands())
-      convert_expr_to(op, lhs.type());
+    // choice. This converts the rhs into a predicate over the lhs.
+    expr = assign_set_rec(lhs, rhs);
+  }
+  else
+  {
+    convert_expr_to(rhs, lhs.type());
+  }
+}
 
-    // Now turn the nondeterministic choice into a top-level
-    // disjunctive constraint.
-    exprt::operandst disjuncts;
+/*******************************************************************\
 
-    for(auto &op : rhs.operands())
-      disjuncts.push_back(equal_exprt{lhs, op});
+Function: smv_typecheckt::assign_set_rec
 
-    expr = disjunction(disjuncts);
-    return;
-  }
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+exprt smv_typecheckt::assign_set_rec(
+  const exprt &lhs,
+  const exprt &set_expression)
+{
+  if(set_expression.type().id() == ID_smv_set)
+  {
+    if(set_expression.id() == ID_smv_set)
+    {
+      // Turn the nondeterministic choice into a
+      // disjunctive constraint.
+      exprt::operandst disjuncts;
+
+      for(auto &element : set_expression.operands())
+        disjuncts.push_back(assign_set_rec(lhs, element));
 
-  convert_expr_to(rhs, lhs.type());
+      return disjunction(disjuncts);
+    }
+    else
+      PRECONDITION(false);
+  }
+  else
+  {
+    exprt copy = set_expression;
+    convert_expr_to(copy, lhs.type());
+    return equal_exprt{lhs, copy};
+  }
 }
 
 /*******************************************************************\