Skip to content

move floating-point-related expression classes into separate header file #5760

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jan 18, 2021
Merged

move floating-point-related expression classes into separate header file #5760

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ Author: Daniel Kroening, [email protected]
#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>
Expand Down
1 change: 1 addition & 0 deletions jbmc/src/java_bytecode/java_string_library_preprocess.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down
2 changes: 1 addition & 1 deletion scripts/expected_doxygen_warnings.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
1 change: 1 addition & 0 deletions src/analyses/goto_check.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
#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>
Expand Down
1 change: 1 addition & 0 deletions src/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
#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>
Expand Down
1 change: 1 addition & 0 deletions src/ansi-c/expr2c.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
#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>
Expand Down
5 changes: 3 additions & 2 deletions src/goto-programs/adjust_float_expressions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,12 +11,13 @@ Author: Daniel Kroening, [email protected]

#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"

Expand Down
1 change: 1 addition & 0 deletions src/solvers/flattening/boolbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]

#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>
Expand Down
2 changes: 2 additions & 0 deletions src/solvers/flattening/boolbv.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why are these forward declared when other types are not. I can see cases for forward declaration or inclusion but the mix seems unclear.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The algorithm is to count the .cpp files that includes this .h file that include the omitted header file. If that is a high percentage, then use the include, otherwise use the forward declaration.

In this case, a lot of .cpp files (46) include boolbv.h but do not need the full floatbv_expr.h (32).

class member_exprt;
class replication_exprt;

Expand Down
1 change: 1 addition & 0 deletions src/solvers/flattening/boolbv_floatbv_op.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
#include <algorithm>
#include <iostream>

#include <util/floatbv_expr.h>
#include <util/std_types.h>

#include <solvers/floatbv/float_utils.h>
Expand Down
1 change: 1 addition & 0 deletions src/solvers/floatbv/float_bv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]

#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
Expand Down
5 changes: 3 additions & 2 deletions src/solvers/refinement/refine_arithmetic.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,11 @@ Author: Daniel Kroening, [email protected]

#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>

Expand Down
3 changes: 2 additions & 1 deletion src/solvers/smt2/smt2_conv.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,9 @@ Author: Daniel Kroening, [email protected]
#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>
Expand Down
1 change: 1 addition & 0 deletions src/solvers/smt2/smt2_parser.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]

#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>
Expand Down
1 change: 1 addition & 0 deletions src/solvers/strings/string_constraint_generator_float.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ Author: Romain Brenguier, [email protected]
#include "string_constraint_generator.h"

#include <util/bitvector_expr.h>
#include <util/floatbv_expr.h>

#include <solvers/floatbv/float_bv.h>

Expand Down
Loading