Merge pull request #1126 from diffblue/smv1

SMV word-level output now prints range types

Author: tautschnig

regression/ebmc/smv-word-level/smv1.desc

@@ -0,0 +1,19 @@
+CORE
+smv1.smv
+--smv-word-level
+^MODULE main$
+^VAR unsigned_bit_vector : unsigned word\[20\];$
+^VAR signed_bit_vector : signed word\[20\];$
+^VAR range_type : 1..10;$
+^VAR bool_type : boolean;$
+^INIT bool_type = FALSE$
+^INIT range_type = 1$
+^INIT signed_bit_vector = 0sd20_1$
+^INIT unsigned_bit_vector = 0ud20_1$
+^TRANS next\(bool_type\) = \(!\(bool_type\)\)$
+^TRANS next\(range_type\) = 2$
+^TRANS next\(signed_bit_vector\) = 0sd20_2$
+^TRANS next\(unsigned_bit_vector\) = 0ud20_2$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-word-level/smv1.smv

@@ -0,0 +1,21 @@
+MODULE main
+
+VAR bool_type : boolean;
+
+ASSIGN init(bool_type) := FALSE;
+ASSIGN next(bool_type) := !bool_type;
+
+VAR range_type : 1..10;
+
+ASSIGN init(range_type) := 1;
+ASSIGN next(range_type) := 2;
+
+VAR signed_bit_vector : signed word [20];
+
+ASSIGN init(signed_bit_vector) := swconst(1, 20);
+ASSIGN next(signed_bit_vector) := swconst(2, 20);
+
+VAR unsigned_bit_vector : unsigned word [20];
+
+ASSIGN init(unsigned_bit_vector) := uwconst(1, 20);
+ASSIGN next(unsigned_bit_vector) := uwconst(2, 20);

src/ebmc/output_smv_word_level.cpp

@@ -39,13 +39,15 @@ operator<<(std::ostream &out, const smv_type_printert &type_printer)
 {
   auto &type = type_printer.type();
 
-  if(type.id() == ID_bool)
-    return out << "boolean";
-  else if(type.id() == ID_signedbv)
-    return out << "signed word[" << to_signedbv_type(type).get_width() << "]";
-  else if(type.id() == ID_unsignedbv)
-    return out << "unsigned word[" << to_unsignedbv_type(type).get_width()
-               << "]";
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  if(
+    type.id() == ID_bool || type.id() == ID_signedbv ||
+    type.id() == ID_unsignedbv || type.id() == ID_range)
+  {
+    return out << type2smv(type, ns);
+  }
   else
     throw ebmc_errort{} << "cannot convert type " << type.id() << " to SMV";
 
@@ -146,7 +148,7 @@ static void smv_transition_relation(
   if(expr.id() == ID_and)
   {
     for(auto &conjunct : expr.operands())
-      smv_initial_states(conjunct, ns, out);
+      smv_transition_relation(conjunct, ns, out);
   }
   else if(expr.is_true())
   {