Merge pull request #5760 from diffblue/floatbv_expr_h

tautschnig · web-flow · commit 88d8868443c3 · 2021-01-18T21:53:32.000+01:00
move floating-point-related expression classes into separate header file
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -29,6 +29,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
+#include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/namespace.h>
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -23,6 +23,7 @@ Date:   April 2017
 #include <util/bitvector_expr.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
+#include <util/floatbv_expr.h>
 #include <util/fresh_symbol.h>
 #include <util/refined_string_type.h>
 #include <util/std_code.h>
diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt
@@ -96,6 +96,6 @@ warning: Included by graph for 'namespace.h' not generated, too many nodes (112)
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (76), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_expr.h' not generated, too many nodes (248), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (249), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_types.h' not generated, too many nodes (124), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/find_symbols.h>
+#include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/make_unique.h>
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
+#include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cprover_prefix.h>
 #include <util/find_symbols.h>
 #include <util/fixedbv.h>
+#include <util/floatbv_expr.h>
 #include <util/lispexpr.h>
 #include <util/lispirep.h>
 #include <util/namespace.h>
diff --git a/src/goto-programs/adjust_float_expressions.cpp b/src/goto-programs/adjust_float_expressions.cpp
@@ -11,12 +11,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "adjust_float_expressions.h"
 
+#include <util/arith_tools.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
+#include <util/floatbv_expr.h>
+#include <util/ieee_float.h>
 #include <util/std_expr.h>
 #include <util/symbol.h>
-#include <util/ieee_float.h>
-#include <util/arith_tools.h>
 
 #include "goto_model.h"
 
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/floatbv_expr.h>
 #include <util/magic.h>
 #include <util/mp_arith.h>
 #include <util/prefix.h>
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
@@ -31,6 +31,8 @@ class bswap_exprt;
 class concatenation_exprt;
 class extractbit_exprt;
 class extractbits_exprt;
+class floatbv_typecast_exprt;
+class ieee_float_op_exprt;
 class member_exprt;
 class replication_exprt;
 
diff --git a/src/solvers/flattening/boolbv_floatbv_op.cpp b/src/solvers/flattening/boolbv_floatbv_op.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 #include <iostream>
 
+#include <util/floatbv_expr.h>
 #include <util/std_types.h>
 
 #include <solvers/floatbv/float_utils.h>
diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/floatbv_expr.h>
 #include <util/std_expr.h>
 
 exprt float_bvt::convert(const exprt &expr) const
diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp
@@ -8,10 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "bv_refinement.h"
 
+#include <util/arith_tools.h>
 #include <util/bv_arithmetic.h>
-#include <util/ieee_float.h>
 #include <util/expr_util.h>
-#include <util/arith_tools.h>
+#include <util/floatbv_expr.h>
+#include <util/ieee_float.h>
 
 #include <solvers/floatbv/float_utils.h>
 
diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h
@@ -13,8 +13,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <sstream>
 #include <set>
 
-#include <util/std_expr.h>
 #include <util/byte_operators.h>
+#include <util/floatbv_expr.h>
+#include <util/std_expr.h>
 
 #if !HASH_CODE
 #  include <util/irep_hash_container.h>
diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
+#include <util/floatbv_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/mathematical_expr.h>
diff --git a/src/solvers/strings/string_constraint_generator_float.cpp b/src/solvers/strings/string_constraint_generator_float.cpp
@@ -14,6 +14,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include "string_constraint_generator.h"
 
 #include <util/bitvector_expr.h>
+#include <util/floatbv_expr.h>
 
 #include <solvers/floatbv/float_bv.h>
 
diff --git a/src/util/floatbv_expr.h b/src/util/floatbv_expr.h
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
