Constraint generator doxygen

Author: Lukasz A.J. Wrona

src/solvers/refinement/string_constraint_generator.h

@@ -49,17 +49,17 @@ class string_constraint_generatort final
 
   explicit string_constraint_generatort(const infot& info);
 
-  // Axioms are of three kinds: universally quantified string constraint,
-  // not contains string constraints and simple formulas.
+  /// Axioms are of three kinds: universally quantified string constraint,
+  /// not contains string constraints and simple formulas.
   const std::vector<exprt> &get_axioms() const;
 
-  // Boolean symbols for the results of some string functions
+  /// Boolean symbols for the results of some string functions
   const std::vector<symbol_exprt> &get_boolean_symbols() const;
 
   /// Symbols used in existential quantifications
   const std::vector<symbol_exprt> &get_index_symbols() const;
 
-  // Set of strings that have been created by the generator
+  /// Set of strings that have been created by the generator
   const std::set<string_exprt> &get_created_strings() const;
 
   exprt get_witness_of(
@@ -73,8 +73,7 @@ class string_constraint_generatort final
     const irep_idt &prefix, const typet &type=bool_typet());
   symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type);
 
-  // Maps unresolved symbols to the string_exprt that was created for them
-
+  /// Maps unresolved symbols to the string_exprt that was created for them
   string_exprt add_axioms_for_refined_string(const exprt &expr);
 
   exprt add_axioms_for_function_application(

src/solvers/refinement/string_refinement.h

@@ -42,7 +42,7 @@ class string_refinementt final: public bv_refinementt
     size_t string_max_length=std::numeric_limits<size_t>::max();
     /// Make non-deterministic character arrays have at least one character
     bool string_non_empty=false;
-    // Concretize strings after solver is finished
+    /// Concretize strings after solver is finished
     bool trace=false;
     /// Make non-deterministic characters printable
     bool string_printable=false;