added util/mathematical_expr.h

Following the pattern in util/mathematical_types.h, expression classes that
don't exist immediately in usual programming languages are now in
util/mathematical_expr.h.

Author: Daniel Kroening

jbmc/src/java_bytecode/java_utils.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_root_class.h"
 
 #include <util/invariant.h>
+#include <util/mathematical_expr.h>
 #include <util/message.h>
 #include <util/prefix.h>
 #include <util/std_types.h>

src/ansi-c/expr2c_class.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <unordered_map>
 #include <unordered_set>
 
+#include <util/mathematical_expr.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 

src/goto-programs/builtin_functions.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/expr_initializer.h>
 #include <util/expr_util.h>
+#include <util/mathematical_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/rational.h>
 #include <util/rational_tools.h>

src/goto-symex/symex_main.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/exception_utils.h>
 #include <util/make_unique.h>
+#include <util/mathematical_expr.h>
 #include <util/replace_symbol.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>

src/solvers/flattening/functions.h

@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <set>
 
-#include <util/std_expr.h>
+#include <util/mathematical_expr.h>
 
 #include <solvers/prop/prop_conv.h>
 

src/solvers/smt2/smt2_conv.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/format_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
+#include <util/mathematical_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>

src/solvers/smt2/smt2_parser.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
+#include <util/mathematical_expr.h>
 #include <util/range.h>
 
 #include <numeric>

src/util/Makefile

@@ -41,6 +41,7 @@ SRC = allocate_objects.cpp \
       json_stream.cpp \
       lispexpr.cpp \
       lispirep.cpp \
+      mathematical_expr.cpp \
       mathematical_types.cpp \
       memory_info.cpp \
       merge_irep.cpp \

src/util/format_expr.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include "format_type.h"
 #include "ieee_float.h"
 #include "invariant.h"
+#include "mathematical_expr.h"
 #include "mp_arith.h"
 #include "rational.h"
 #include "rational_tools.h"

src/util/mathematical_expr.cpp

@@ -0,0 +1,9 @@
+/*******************************************************************\
+
+Module: API to expression classes for 'mathematical' expressions
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "mathematical_expr.h"