when encountering an SMT-unsupported expression, include it in the de…

…bug message

When diagnosing why a model you expect to be SMT-simplified is not getting
simplified, it is helpful for Rumur to actually tell you the reason it gave up.

Github: related to #130 "interact with SMT solver"

rumur/src/main.cc

@@ -569,8 +569,8 @@ int main(int argc, char **argv) {
       smt::simplify(*m);
     } catch (smt::BudgetExhausted&) {
       *info << "SMT solver budget (" << options.smt.budget << "ms) exhausted\n";
-    } catch (smt::Unsupported&) {
-      *info << "SMT solver encountered an unsupported expression\n";
+    } catch (smt::Unsupported &e) {
+      *info << e.what() << "\n";
     }
   }
 

rumur/src/smt/except.h

@@ -4,6 +4,7 @@
 
 #include <cstddef>
 #include <stdexcept>
+#include <string>
 
 namespace smt {
 
@@ -15,7 +16,10 @@ class BudgetExhausted : public std::runtime_error {
 class Unsupported : public std::runtime_error {
  public:
   Unsupported(): std::runtime_error("part of an expression was outside the "
-    "currently implemented functionality") { }
+    "currently implemented SMT functionality") { }
+
+  Unsupported(const std::string &expr): std::runtime_error("SMT solver "
+    "encountered unsupported expression \"" + expr + "\"") { }
 };
 
 }

rumur/src/smt/simplify.cc

@@ -105,7 +105,7 @@ namespace { class Simplifier : public BaseTraversal {
     if (n == *Boolean)
       return;
 
-    throw Unsupported();
+    throw Unsupported(n.to_string());
   }
 
   void visit_eq(Eq &n) final { visit_bexpr(n); }

rumur/src/smt/translate.cc

@@ -37,8 +37,8 @@ namespace { class Translator : public ConstExprTraversal {
     *this << "(and " << *n.lhs << " " << *n.rhs << ")";
   }
 
-  void visit_element(const Element&) {
-    throw Unsupported();
+  void visit_element(const Element &n) {
+    throw Unsupported(n.to_string());
   }
 
   void visit_exprid(const ExprID &n) {
@@ -49,24 +49,24 @@ namespace { class Translator : public ConstExprTraversal {
     *this << "(= " << *n.lhs << " " << *n.rhs << ")";
   }
 
-  void visit_exists(const Exists&) {
-    throw Unsupported();
+  void visit_exists(const Exists &n) {
+    throw Unsupported(n.to_string());
   }
 
   void visit_div(const Div &n) {
     *this << "(div " << *n.lhs << " " << *n.rhs << ")";
   }
 
-  void visit_field(const Field&) {
-    throw Unsupported();
+  void visit_field(const Field &n) {
+    throw Unsupported(n.to_string());
   }
 
-  void visit_forall(const Forall&) {
-    throw Unsupported();
+  void visit_forall(const Forall &n) {
+    throw Unsupported(n.to_string());
   }
 
-  void visit_functioncall(const FunctionCall&) {
-    throw Unsupported();
+  void visit_functioncall(const FunctionCall &n) {
+    throw Unsupported(n.to_string());
   }
 
   void visit_geq(const Geq &n) {
@@ -81,8 +81,8 @@ namespace { class Translator : public ConstExprTraversal {
     *this << "(=> " << *n.lhs << " " << *n.rhs << ")";
   }
 
-  void visit_isundefined(const IsUndefined&) {
-    throw Unsupported();
+  void visit_isundefined(const IsUndefined &n) {
+    throw Unsupported(n.to_string());
   }
 
   void visit_leq(const Leq &n) {