fixes for integers in SMT2

This fixes output of formulas into SMT2 format that contain
unbounded integers; conversely, values in satisfying assignments
generated by SMT2 solvers that contain unbounded integers
are now parsed.

Author: Daniel Kroening

src/goto-programs/goto_trace.cpp

@@ -143,6 +143,12 @@ std::string trace_value_binary(
     {
       return expr.is_true()?"1":"0";
     }
+    else if(type.id()==ID_integer)
+    {
+      mp_integer i;
+      if(!to_integer(expr, i) && i>=0)
+        return integer2string(i, 2);
+    }
   }
   else if(expr.id()==ID_array)
   {

src/solvers/smt2/smt2_conv.cpp

@@ -239,7 +239,15 @@ constant_exprt smt2_convt::parse_literal(
       value=string2integer(s.substr(2), 16);
     }
     else
-      PARSERERROR("smt2_convt::parse_literal can't parse \""+s+"\"");
+    {
+      // Numeral
+      value=string2integer(s);
+    }
+  }
+  else if(src.get_sub().size()==2 &&
+          src.get_sub()[0].id()=="-") // (- 100)
+  {
+    value=-string2integer(src.get_sub()[1].id_string());
   }
   else if(src.get_sub().size()==3 &&
           src.get_sub()[0].id()=="_" &&
@@ -433,6 +441,9 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
 
   if(type.id()==ID_signedbv ||
      type.id()==ID_unsignedbv ||
+     type.id()==ID_integer ||
+     type.id()==ID_rational ||
+     type.id()==ID_real ||
      type.id()==ID_bv ||
      type.id()==ID_fixedbv ||
      type.id()==ID_floatbv)
@@ -970,7 +981,9 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     assert(expr.operands().size()==1);
 
-    if(expr.type().id()==ID_rational)
+    if(expr.type().id()==ID_rational ||
+       expr.type().id()==ID_integer ||
+       expr.type().id()==ID_real)
     {
       out << "(- ";
       convert_expr(expr.op0());
@@ -2898,9 +2911,11 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
 
       out << ")";
     }
-    else if(expr.type().id()==ID_rational)
+    else if(expr.type().id()==ID_rational ||
+            expr.type().id()==ID_integer ||
+            expr.type().id()==ID_real)
     {
-      out << "(+";
+      out << "(+ ";
       convert_expr(expr.op0());
       out << " ";
       convert_expr(expr.op1());
@@ -3285,7 +3300,9 @@ void smt2_convt::convert_mult(const mult_exprt &expr)
 
     out << "))"; // bvmul, extract
   }
-  else if(expr.type().id()==ID_rational)
+  else if(expr.type().id()==ID_rational ||
+          expr.type().id()==ID_integer ||
+          expr.type().id()==ID_real)
   {
     out << "(*";
 
@@ -4378,7 +4395,8 @@ void smt2_convt::convert_type(const typet &type)
       out << "(_ BitVec "
           << floatbv_type.get_width() << ")";
   }
-  else if(type.id()==ID_rational)
+  else if(type.id()==ID_rational ||
+          type.id()==ID_real)
     out << "Real";
   else if(type.id()==ID_integer)
     out << "Int";

src/solvers/smt2/smt2_dec.cpp

@@ -198,6 +198,8 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
       // Examples:
       // ( (B0 true) )
       // ( (|__CPROVER_pipe_count#1| (_ bv0 32)) )
+      // ( (|some_integer| 0) )
+      // ( (|some_integer| (- 10)) )
 
       values[s0.id()]=s1;
     }