Stop adding printable constraints on all strings

romainbrenguier · romainbrenguier · commit 542a26dd60b8 · 2017-11-02T09:51:13.000Z
We no longer do that on all strings in the solver.
This is now done during bytecode conversion for Java, and only
for input strings.
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -324,9 +324,6 @@ void string_constraint_generatort::add_default_axioms(
 
   if(max_string_length!=std::numeric_limits<size_t>::max())
     axioms.push_back(s.axiom_for_length_le(max_string_length));
-
-  if(force_printable_characters)
-    add_constraint_on_characters(s, index_zero, s.length(), " -~");
 }
 
 /// Add constraint on characters of a string.

Original file line number	Diff line number	Diff line change
`@@ -324,9 +324,6 @@ void string_constraint_generatort::add_default_axioms(`
`324`	`324`
`325`	`325`	`if(max_string_length!=std::numeric_limits<size_t>::max())`
`326`	`326`	`axioms.push_back(s.axiom_for_length_le(max_string_length));`
`327`		`-`
`328`		`- if(force_printable_characters)`
`329`		`- add_constraint_on_characters(s, index_zero, s.length(), " -~");`
`330`	`327`	`}`
`331`	`328`
`332`	`329`	`/// Add constraint on characters of a string.`