Skip to content

Refactor string refinement constructors #1300

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 32 commits into from
Aug 31, 2017
Merged

Refactor string refinement constructors #1300

Changes from 1 commit
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
22b4885
Remove usage of static in the header file
Aug 25, 2017
848f2a5
Constraint gen cosmetics
Aug 25, 2017
3217fe3
constraint_generator message is a member
Aug 25, 2017
c51e35e
Use C++11 initialization for constraint generator members
Aug 25, 2017
cf950ab
Use vector instead of list for constraint_generator data
Aug 25, 2017
8043a0d
Hide index_symbols and boolean_symbols in constraint generator
Aug 25, 2017
16a0a34
constraint generator const namespace
Aug 25, 2017
51d897a
Better string_refinement constructor Act 1
Aug 26, 2017
9146575
Better string_refinement constructor Act II
Aug 26, 2017
a00b2db
String refinement - remove unused public methods, fix comments
Aug 26, 2017
30fe11b
Better string_constraint_generator constructor
Aug 26, 2017
99c815e
Make string_constraint_generatort::fresh_symbol non-static
Aug 26, 2017
abe4046
Better bv_refinement constructor
Aug 26, 2017
792a70d
Hide bv_refinement members, add override specifier
Aug 26, 2017
07f6b39
Remove unnecessary typedef
Aug 26, 2017
50173d6
Make some string_constraint_generator methods static
Aug 26, 2017
aa85392
Make more generator methods private
Aug 26, 2017
5368c8c
Private get_created_strings
Aug 26, 2017
a440da7
Group generator's member variables
Aug 26, 2017
01c6767
Rename axioms to m_axioms
Aug 26, 2017
e5c45a5
Prefix all generator member variables with "m_"
Aug 26, 2017
1282d03
Update unit tests with new constructors
Aug 29, 2017
4087187
Don't pass language_uit::uit as a pointer
Aug 29, 2017
83a29dc
Fix linter errors
Aug 29, 2017
107704a
Fix is_in_conflict with conflict override
Aug 29, 2017
fd59d47
Preprocess constexpr
Aug 29, 2017
acaad4f
Remove dead bv_refinementt::set_to
Aug 30, 2017
04fae6d
Correct comment
Aug 30, 2017
7fd2bfa
Use_counter_example assignable via constructor
Aug 30, 2017
22d699c
Move constexpr ifdef into a util header
Aug 30, 2017
8da7c30
Constraint generator doxygen
Aug 30, 2017
0838f61
Fix function declaration slicing
Aug 30, 2017
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
14 changes: 10 additions & 4 deletions src/solvers/refinement/string_constraint_generator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,12 @@ Author: Romain Brenguier, [email protected]
#include <util/refined_string_type.h>
#include <solvers/refinement/string_constraint.h>

#if defined(__GNUC__) || defined(__clang__)
Copy link
Contributor

Choose a reason for hiding this comment

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

Put that into util/

#define CBMC_CONSTEXPR constexpr
#else
#define CBMC_CONSTEXPR
#endif

class string_constraint_generatort final
{
public:
Expand Down Expand Up @@ -340,10 +346,10 @@ class string_constraint_generatort final
// that is -2147483648 so takes 11 characters to write.
// The long with the longest string is Long.MIN_VALUE which is -2^63,
// approximately -9.223372037*10^18 so takes 20 characters to write.
constexpr static const std::size_t MAX_INTEGER_LENGTH=11;
constexpr static const std::size_t MAX_LONG_LENGTH=20;
constexpr static const std::size_t MAX_FLOAT_LENGTH=15;
constexpr static const std::size_t MAX_DOUBLE_LENGTH=30;
CBMC_CONSTEXPR static const std::size_t MAX_INTEGER_LENGTH=11;
CBMC_CONSTEXPR static const std::size_t MAX_LONG_LENGTH=20;
CBMC_CONSTEXPR static const std::size_t MAX_FLOAT_LENGTH=15;
CBMC_CONSTEXPR static const std::size_t MAX_DOUBLE_LENGTH=30;
std::set<string_exprt> m_created_strings;
unsigned m_symbol_count=0;
const messaget m_message;
Expand Down