Move string_constraint functions out of string_refinement

Author: Lukasz A.J. Wrona

src/solvers/refinement/string_constraint.cpp

@@ -1,4 +1,9 @@
+// Author: DiffBlue Ltd.
+
+#include <stack>
 #include "string_constraint.h"
+#include <util/simplify_expr.h>
+#include <util/expr_iterator.h>
 
 void replace(string_constraintt &axiom, const replace_mapt &symbol_resolve)
 {
@@ -59,3 +64,132 @@ string_not_contains_constraintt &to_string_not_contains_constraint(exprt &expr)
       "operands"));
   return static_cast<string_not_contains_constraintt &>(expr);
 }
+
+typedef std::map<exprt, std::vector<exprt>> array_index_mapt;
+
+static array_index_mapt gather_indices(const exprt &expr)
+{
+  array_index_mapt indices;
+  std::for_each(
+    expr.depth_begin(),
+    expr.depth_end(),
+    [&](const exprt &expr) { // NOLINT
+      if(const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr))
+        indices[index_expr->array()].push_back(index_expr->index());
+    });
+  return indices;
+}
+
+/// \param expr: an expression
+/// \param var: a symbol
+/// \return Boolean telling whether `expr` is a linear function of `var`.
+/// \todo Add unit tests
+/// \related string_constraintt
+static bool
+is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
+{
+  for(auto it = expr.depth_begin(); it != expr.depth_end();)
+  {
+    if(
+      it->id() != ID_plus && it->id() != ID_minus &&
+      it->id() != ID_unary_minus && *it != var)
+    {
+      const auto find_qvar = std::find(it->depth_begin(), it->depth_end(), var);
+      if(find_qvar != it->depth_end())
+        return false;
+      else
+        it.next_sibling_or_parent();
+    }
+    else
+      ++it;
+  }
+  return true;
+}
+
+/// The universally quantified variable is only allowed to occur in index
+/// expressions in the body of a string constraint. This function returns true
+/// if this is the case and false otherwise.
+/// \param [in] expr: The string constraint to check
+/// \return true if the universal variable only occurs in index expressions,
+///   false otherwise.
+static bool universal_only_in_index(const string_constraintt &expr)
+{
+  for(auto it = expr.body.depth_begin(); it != expr.body.depth_end();)
+  {
+    if(*it == expr.univ_var)
+      return false;
+    if(it->id() == ID_index)
+      it.next_sibling_or_parent();
+    else
+      ++it;
+  }
+  return true;
+}
+
+/// Checks the data invariant for \link string_constraintt \endlink
+/// \related string_constraintt
+/// \param stream: message stream
+/// \param ns: namespace
+/// \param [in] constraint: the string constraint to check
+/// \return whether the constraint satisfies the invariant
+bool is_valid_string_constraint(
+  messaget::mstreamt &stream,
+  const namespacet &ns,
+  const string_constraintt &constraint)
+{
+  const auto eom = messaget::eom;
+  // Condition 1: The premise cannot contain any string indices
+  const array_index_mapt premise_indices = gather_indices(constraint.premise);
+  if(!premise_indices.empty())
+  {
+    stream << "Premise has indices: " << to_string(constraint) << ", map: {";
+    for(const auto &pair : premise_indices)
+    {
+      stream << format(pair.first) << ": {";
+      for(const auto &i : pair.second)
+        stream << format(i) << ", ";
+    }
+    stream << "}}" << eom;
+    return false;
+  }
+
+  const array_index_mapt body_indices = gather_indices(constraint.body);
+  // Must validate for each string. Note that we have an invariant that the
+  // second value in the pair is non-empty.
+  for(const auto &pair : body_indices)
+  {
+    // Condition 2: All indices of the same string must be the of the same form
+    const exprt rep = pair.second.back();
+    for(size_t j = 0; j < pair.second.size() - 1; j++)
+    {
+      const exprt i = pair.second[j];
+      const equal_exprt equals(rep, i);
+      const exprt result = simplify_expr(equals, ns);
+      if(result.is_false())
+      {
+        stream << "Indices not equal: " << to_string(constraint)
+               << ", str: " << format(pair.first) << eom;
+        return false;
+      }
+    }
+
+    // Condition 3: f must be linear
+    if(!is_linear_arithmetic_expr(rep, constraint.univ_var))
+    {
+      stream << "f is not linear: " << to_string(constraint)
+             << ", str: " << format(pair.first) << eom;
+      return false;
+    }
+
+    // Condition 4: the quantified variable can only occur in indices in the
+    // body
+    if(!universal_only_in_index(constraint))
+    {
+      stream << "Universal variable outside of index:" << to_string(constraint)
+             << eom;
+      return false;
+    }
+  }
+
+  return true;
+}

src/solvers/refinement/string_constraint.h

@@ -89,6 +89,15 @@ exprt univ_within_bounds(const string_constraintt &axiom);
 /// \return rendered string
 std::string to_string(const string_constraintt &expr);
 
+/// Checks the data invariant for \link string_constraintt
+/// \related string_constraintt
+/// \param [in] constraint: the string constraint to check
+/// \return whether the constraint satisfies the invariant
+bool is_valid_string_constraint(
+  messaget::mstreamt &stream,
+  const namespacet &ns,
+  const string_constraintt &constraint);
+
 /// Constraints to encode non containement of strings.
 class string_not_contains_constraintt final : public exprt
 {

src/solvers/refinement/string_refinement.cpp

@@ -29,11 +29,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <solvers/refinement/string_constraint_instantiation.h>
 #include <unordered_set>
 
-static bool is_valid_string_constraint(
-  messaget::mstreamt &stream,
-  const namespacet &ns,
-  const string_constraintt &constraint);
-
 static optionalt<exprt> find_counter_example(
   const namespacet &ns,
   ui_message_handlert::uit ui,
@@ -2327,138 +2322,3 @@ static optionalt<exprt> find_counter_example(
   else
     return { };
 }
-
-/// \related string_constraintt
-typedef std::map<exprt, std::vector<exprt>> array_index_mapt;
-
-/// \related string_constraintt
-static array_index_mapt gather_indices(const exprt &expr)
-{
-  array_index_mapt indices;
-  // clang-format off
-  std::for_each(
-    expr.depth_begin(),
-    expr.depth_end(),
-    [&](const exprt &expr)
-    {
-      const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
-      if(index_expr)
-        indices[index_expr->array()].push_back(index_expr->index());
-    });
-  // clang-format on
-  return indices;
-}
-
-/// \param expr: an expression
-/// \param var: a symbol
-/// \return Boolean telling whether `expr` is a linear function of `var`.
-/// \todo Add unit tests
-/// \related string_constraintt
-static bool
-is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
-{
-  for(auto it = expr.depth_begin(); it != expr.depth_end();)
-  {
-    if(
-      it->id() != ID_plus && it->id() != ID_minus &&
-      it->id() != ID_unary_minus && *it != var)
-    {
-      if(find_qvar(*it, var))
-        return false;
-      else
-        it.next_sibling_or_parent();
-    }
-    else
-      ++it;
-  }
-  return true;
-}
-
-/// The universally quantified variable is only allowed to occur in index
-/// expressions in the body of a string constraint. This function returns true
-/// if this is the case and false otherwise.
-/// \related string_constraintt
-/// \param [in] expr: The string constraint to check
-/// \return true if the universal variable only occurs in index expressions,
-///   false otherwise.
-static bool universal_only_in_index(const string_constraintt &expr)
-{
-  for(auto it = expr.body.depth_begin(); it != expr.body.depth_end();)
-  {
-    if(*it == expr.univ_var)
-      return false;
-    if(it->id() == ID_index)
-      it.next_sibling_or_parent();
-    else
-      ++it;
-  }
-  return true;
-}
-
-/// Checks the data invariant for \link string_constraintt \endlink
-/// \related string_constraintt
-/// \param stream: message stream
-/// \param ns: namespace
-/// \param [in] constraint: the string constraint to check
-/// \return whether the constraint satisfies the invariant
-static bool is_valid_string_constraint(
-  messaget::mstreamt &stream,
-  const namespacet &ns,
-  const string_constraintt &constraint)
-{
-  const auto eom=messaget::eom;
-  // Condition 1: The premise cannot contain any string indices
-  const array_index_mapt premise_indices = gather_indices(constraint.premise);
-  if(!premise_indices.empty())
-  {
-    stream << "Premise has indices: " << to_string(constraint) << ", map: {";
-    for(const auto &pair : premise_indices)
-    {
-      stream << format(pair.first) << ": {";
-      for(const auto &i : pair.second)
-        stream << format(i) << ", ";
-    }
-    stream << "}}" << eom;
-    return false;
-  }
-
-  const array_index_mapt body_indices = gather_indices(constraint.body);
-  // Must validate for each string. Note that we have an invariant that the
-  // second value in the pair is non-empty.
-  for(const auto &pair : body_indices)
-  {
-    // Condition 2: All indices of the same string must be the of the same form
-    const exprt rep=pair.second.back();
-    for(size_t j=0; j<pair.second.size()-1; j++)
-    {
-      const exprt i=pair.second[j];
-      const equal_exprt equals(rep, i);
-      const exprt result=simplify_expr(equals, ns);
-      if(result.is_false())
-      {
-        stream << "Indices not equal: " << to_string(constraint)
-               << ", str: " << format(pair.first) << eom;
-        return false;
-      }
-    }
-
-    // Condition 3: f must be linear in the quantified variable
-    if(!is_linear_arithmetic_expr(rep, constraint.univ_var))
-    {
-      stream << "f is not linear: " << to_string(constraint)
-             << ", str: " << format(pair.first) << eom;
-      return false;
-    }
-
-    // Condition 4: the quantified variable can only occur in indices in the
-    // body
-    if(!universal_only_in_index(constraint))
-    {
-      stream << "Universal variable outside of index:" << to_string(constraint)
-             << eom;
-      return false;
-    }
-  }
-
-  return true;
-}