Move MAX_CONCRETE_STRING_SIZE definition to magic

romainbrenguier · romainbrenguier · commit ce43b3e29e18 · 2018-04-18T08:52:07.000+01:00
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
@@ -28,6 +28,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/string_constraint_instantiation.h>
 #include <unordered_set>
+#include <util/magic.h>
 
 static bool is_valid_string_constraint(
   messaget::mstreamt &stream,
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
@@ -31,8 +31,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 
 #define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()
 #define CHARACTER_FOR_UNKNOWN '?'
-// Limit the size of strings in traces to 64M chars to avoid memout
-#define MAX_CONCRETE_STRING_SIZE (1 << 26)
 
 class string_refinementt final: public bv_refinementt
 {
diff --git a/src/util/magic.h b/src/util/magic.h
@@ -10,5 +10,7 @@
 const std::size_t CNF_DUMP_BLOCK_SIZE = 4096;
 const std::size_t MAX_FLATTENED_ARRAY_SIZE=1000;
 const std::size_t STRING_REFINEMENT_MAX_CHAR_WIDTH = 16;
+// Limit the size of strings in traces to 64M chars to avoid memout
+const std::size_t MAX_CONCRETE_STRING_SIZE = 1 << 26;
 
 #endif

Original file line number	Diff line number	Diff line change
`@@ -31,8 +31,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com`
`31`	`31`
`32`	`32`	`#define DEFAULT_MAX_NB_REFINEMENT std::numeric_limits<size_t>::max()`
`33`	`33`	`#define CHARACTER_FOR_UNKNOWN '?'`
`34`		`-// Limit the size of strings in traces to 64M chars to avoid memout`
`35`		`-#define MAX_CONCRETE_STRING_SIZE (1 << 26)`
`36`	`34`
`37`	`35`	`class string_refinementt final: public bv_refinementt`
`38`	`36`	`{`