Added string_constraintt invariant checking

Updated the documentation to explicitly state the invariants (and turned on MathJax in Doxygen). Created a function to check the invariant and added a check in `string_refinementt::dec_solve`.

Author: jasigal

src/doxyfile

@@ -1473,7 +1473,7 @@ FORMULA_TRANSPARENT    = YES
 # The default value is: NO.
 # This tag requires that the tag GENERATE_HTML is set to YES.
 
-USE_MATHJAX            = NO
+USE_MATHJAX            = YES
 
 # When MathJax is enabled you can set the default output format to be used for
 # the MathJax output. See the MathJax site (see:

src/solvers/refinement/string_constraint.h

@@ -24,6 +24,30 @@ Author: Romain Brenguier, [email protected]
 #include <solvers/refinement/bv_refinement.h>
 #include <solvers/refinement/string_refinement_invariant.h>
 #include <util/refined_string_type.h>
+#include <langapi/language_util.h>
+
+/*! \brief Universally quantified string constraint
+
+    This represents a universally quantified string constraint as laid out in
+    DOI: 10.1007/978-3-319-03077-7. The paper seems to specify a universal
+    constraint as follows.
+
+    A universal constraint is of the form \f$\forall n. L(n) \rightarrow
+    P(n, s_0,\ldots, s_k)\f$ where
+
+    1. \f$L(n)\f$ does not contain string indices [possibly not required, but
+       implied by examples]
+    2. \f$\forall n. L(n) \rightarrow P'\left(s_0[f_0(n)],\ldots, s_k[f_k(n)]
+       \right)\f$, i.e. when focusing on one specific string, all indices are
+       the same [stated in a roundabout manner]
+    3. Each \f$f\f$ is linear and therefore has an inverse [explicitly stated]
+    4. \f$L(n)\f$ and \f$P(n, s_0,\ldots, s_k)\f$ may contain other (free)
+       variables, but in \f$P\f$, \f$n\f$ can only occur as an argument to an
+       \f$f\f$ [explicitly stated, implied]
+
+    We extend this slightly by restricting n to be in a specific range, but this
+    is another implication which can be pushed in to \f$L(n)\f$.
+*/
 
 class string_constraintt: public exprt
 {
@@ -114,6 +138,15 @@ extern inline string_constraintt &to_string_constraint(exprt &expr)
   return static_cast<string_constraintt &>(expr);
 }
 
+inline static std::string from_expr(
+  const namespacet &ns,
+  const irep_idt &identifier,
+  const string_constraintt &expr)
+{
+  return from_expr(ns, identifier, expr.premise())+" => "+
+    from_expr(ns, identifier, expr.body());
+}
+
 class string_not_contains_constraintt: public exprt
 {
 public:

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -293,8 +293,9 @@ string_exprt string_constraint_generatort::add_axioms_for_to_upper_case(
 
   // We add axioms:
   // a1 : |res| = |str|
-  // a2 : forall idx<str.length, 'a'<=str[idx]<='z' => res[idx]=str[idx]+'A'-'a'
-  // a3 : forall idx<str.length, !('a'<=str[idx]<='z') => res[idx]=str[idx]
+  // a2 : forall idx1<str.length, 'a'<=str[idx1]<='z' =>
+  //                                res[idx1]=str[idx1]+'A'-'a'
+  // a3 : forall idx2<str.length, !('a'<=str[idx2]<='z') => res[idx2]=str[idx2]
   // Note that index expressions are only allowed in the body of universal
   // axioms, so we use a trivial premise and push our premise into the body.