SMV: union operator

The SMV union operator computes the union of two set expressions.

Author: kroening

regression/smv/expressions/smv_union2.desc

@@ -1,4 +1,4 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 smv_union2.smv
 
 ^\[spec1\] x != 3: PROVED \(CT=1\)$
@@ -8,4 +8,3 @@ smv_union2.smv
 --
 ^warning: ignoring
 --
-The type checker rejects this.

src/smvlang/smv_typecheck.cpp

@@ -950,6 +950,37 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
     // only get added by type checker
     PRECONDITION(false);
   }
+  else if(expr.id() == ID_smv_union)
+  {
+    auto &lhs = to_binary_expr(expr).lhs();
+    auto &rhs = to_binary_expr(expr).rhs();
+
+    typecheck_expr_rec(lhs, mode);
+    typecheck_expr_rec(rhs, mode);
+
+    // create smv_set expression
+    exprt::operandst elements;
+
+    if(lhs.id() == ID_smv_set)
+    {
+      elements.insert(
+        elements.end(), lhs.operands().begin(), lhs.operands().end());
+    }
+    else
+      elements.push_back(lhs);
+
+    if(rhs.id() == ID_smv_set)
+    {
+      elements.insert(
+        elements.end(), rhs.operands().begin(), rhs.operands().end());
+    }
+    else
+      elements.push_back(rhs);
+
+    expr.id(ID_smv_set);
+    expr.operands() = std::move(elements);
+    expr.type() = typet{ID_smv_set};
+  }
   else if(expr.id() == ID_smv_setin)
   {
     auto &lhs = to_binary_expr(expr).lhs();
@@ -1719,23 +1750,6 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
         expr.id(ID_next_symbol);
     }
   }
-  else if(expr.id()=="smv_nondet_choice" ||
-          expr.id()=="smv_union")
-  {
-    if(expr.operands().size()==0)
-    {
-      throw errort().with_location(expr.find_source_location())
-        << "expected operand here";
-    }
-
-    std::string identifier=
-      module+"::var::"+std::to_string(nondet_count++);
-
-    expr.set(ID_identifier, identifier);
-    expr.set("#smv_nondet_choice", true);
-
-    expr.id(ID_constraint_select_one);
-  }
   else if(expr.id()=="smv_cases") // cases
   {
     if(expr.operands().size()<1)