Turn string constraints into a struct

src/solvers/Makefile

@@ -180,6 +180,7 @@ SRC = $(BOOLEFORCE_SRC) \
       refinement/refine_arithmetic.cpp \
       refinement/refine_arrays.cpp \
       refinement/string_refinement.cpp \
+      refinement/string_constraint.cpp \
       refinement/string_refinement_util.cpp \
       refinement/string_constraint_generator_code_points.cpp \
       refinement/string_constraint_generator_comparison.cpp \

src/solvers/refinement/string_constraint.cpp

@@ -0,0 +1,203 @@
+// Author: DiffBlue Ltd.
+
+#include <stack>
+#include "string_constraint.h"
+#include <util/simplify_expr.h>
+#include <util/expr_iterator.h>
+
+exprt string_constraintt::get_lower_bound() const
+{
+  return lower_bound ? *lower_bound : from_integer(0, upper_bound.type());
+}
+
+void replace(string_constraintt &axiom, const replace_mapt &symbol_resolve)
+{
+  replace_expr(symbol_resolve, axiom.index_guard);
+  replace_expr(symbol_resolve, axiom.body);
+  replace_expr(symbol_resolve, axiom.univ_var);
+  replace_expr(symbol_resolve, axiom.upper_bound);
+  if(axiom.lower_bound)
+    replace_expr(symbol_resolve, *axiom.lower_bound);
+}
+
+exprt univ_within_bounds(const string_constraintt &axiom)
+{
+  return and_exprt(
+    binary_relation_exprt(axiom.get_lower_bound(), ID_le, axiom.univ_var),
+    binary_relation_exprt(axiom.upper_bound, ID_gt, axiom.univ_var));
+}
+
+std::string to_string(const string_constraintt &expr)
+{
+  std::ostringstream out;
+  out << "forall " << format(expr.univ_var) << " in ["
+      << format(expr.get_lower_bound()) << ", " << format(expr.upper_bound)
+      << "). " << format(expr.index_guard) << " => " << format(expr.body);
+  return out.str();
+}
+
+std::string to_string(const string_not_contains_constraintt &expr)
+{
+  std::ostringstream out;
+  out << "forall x in [" << format(expr.univ_lower_bound()) << ", "
+      << format(expr.univ_upper_bound()) << "). " << format(expr.premise())
+      << " => ("
+      << "exists y in [" << format(expr.exists_lower_bound()) << ", "
+      << format(expr.exists_upper_bound()) << "). " << format(expr.s0())
+      << "[x+y] != " << format(expr.s1()) << "[y])";
+  return out.str();
+}
+
+const string_not_contains_constraintt &
+to_string_not_contains_constraint(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_string_not_contains_constraint);
+  DATA_INVARIANT(
+    expr.operands().size() == 7,
+    string_refinement_invariantt(
+      "string_not_contains_constraintt must have 7 "
+      "operands"));
+  return static_cast<const string_not_contains_constraintt &>(expr);
+}
+
+string_not_contains_constraintt &to_string_not_contains_constraint(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_string_not_contains_constraint);
+  DATA_INVARIANT(
+    expr.operands().size() == 7,
+    string_refinement_invariantt(
+      "string_not_contains_constraintt must have 7 "
+      "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 index guard cannot contain any string indices
+  const array_index_mapt premise_indices =
+    gather_indices(constraint.index_guard);
+  if(!premise_indices.empty())
+  {
+    stream << "Index guard 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

@@ -27,6 +27,8 @@ Author: Romain Brenguier, [email protected]
 #include <util/format_type.h>
 #include <util/refined_string_type.h>
 #include <util/string_expr.h>
+#include <langapi/language_util.h>
+#include <util/union_find_replace.h>
 
 ///  ### Universally quantified string constraint
 ///
@@ -54,100 +56,53 @@ Author: Romain Brenguier, [email protected]
 ///      \f$f\f$ [explicitly stated, implied].
 ///
 /// \todo The fact that we follow this grammar is not enforced at the moment.
-class string_constraintt : public exprt
+class string_constraintt final
 {
 public:
-  // String constraints are of the form
-  // forall univ_var in [lower_bound,upper_bound[. premise => body
-
-  const exprt &premise() const
-  {
-    return op0();
-  }
-
-  const exprt &body() const
-  {
-    return op1();
-  }
-
-  const symbol_exprt &univ_var() const
-  {
-    return to_symbol_expr(op2());
-  }
-
-  const exprt &upper_bound() const
-  {
-    return op3();
-  }
-
-  const exprt &lower_bound() const
-  {
-    return operands()[4];
-  }
-
- private:
-  string_constraintt();
-
- public:
-  string_constraintt(
-    const symbol_exprt &_univ_var,
-    const exprt &bound_inf,
-    const exprt &bound_sup,
-    const exprt &body):
-    exprt(ID_string_constraint)
-  {
-    copy_to_operands(true_exprt(), body);
-    copy_to_operands(_univ_var, bound_sup, bound_inf);
-  }
-
-  // Default bound inferior is 0
-  string_constraintt(
-    const symbol_exprt &_univ_var,
-    const exprt &bound_sup,
-    const exprt &body):
-    string_constraintt(
-      _univ_var,
-      from_integer(0, _univ_var.type()),
-      bound_sup,
-      body)
-  {}
-
-  exprt univ_within_bounds() const
-  {
-    return and_exprt(
-      binary_relation_exprt(lower_bound(), ID_le, univ_var()),
-      binary_relation_exprt(upper_bound(), ID_gt, univ_var()));
-  }
+  /// String constraints are of the form
+  /// forall univ_var in [lower_bound,upper_bound[. index_guard => body
+  exprt index_guard = true_exprt(); // Index guard
+  exprt body;                       // value constraint
+  symbol_exprt univ_var;
+  exprt upper_bound;
+  optionalt<exprt> lower_bound; // empty defaults to 0
+
+  /// \return lower_bound if it has been set, expression for 0 otherwise
+  exprt get_lower_bound() const;
 };
 
-extern inline const string_constraintt &to_string_constraint(const exprt &expr)
+inline void
+replace(string_constraintt &axiom, const union_find_replacet &symbol_resolve)
 {
-  PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5);
-  return static_cast<const string_constraintt &>(expr);
+  symbol_resolve.replace_expr(axiom.index_guard);
+  symbol_resolve.replace_expr(axiom.body);
+  symbol_resolve.replace_expr(axiom.univ_var);
+  symbol_resolve.replace_expr(axiom.upper_bound);
+  if(axiom.lower_bound)
+    symbol_resolve.replace_expr(*axiom.lower_bound);
 }
 
-extern inline string_constraintt &to_string_constraint(exprt &expr)
-{
-  PRECONDITION(expr.id()==ID_string_constraint && expr.operands().size()==5);
-  return static_cast<string_constraintt &>(expr);
-}
+exprt univ_within_bounds(const string_constraintt &axiom);
 
 /// Used for debug printing.
 /// \param [in] ns: namespace for `from_expr`
 /// \param [in] identifier: identifier for `from_expr`
 /// \param [in] expr: constraint to render
 /// \return rendered string
-inline std::string to_string(const string_constraintt &expr)
-{
-  std::ostringstream out;
-  out << "forall " << format(expr.univ_var()) << " in ["
-      << format(expr.lower_bound()) << ", " << format(expr.upper_bound())
-      << "). " << format(expr.premise()) << " => " << format(expr.body());
-  return out.str();
-}
+std::string to_string(const string_constraintt &expr);
+
+/// Checks the data invariant for string_constraintt
+/// \param stream : output stream
+/// \param [in] ns: namespace for `from_expr`
+/// \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 : public exprt
+class string_not_contains_constraintt final : public exprt
 {
 public:
   // string_not contains_constraintt are formula of the form:
@@ -209,38 +164,11 @@ class string_not_contains_constraintt : public exprt
 /// \param [in] identifier: identifier for `from_expr`
 /// \param [in] expr: constraint to render
 /// \return rendered string
-inline std::string to_string(const string_not_contains_constraintt &expr)
-{
-  std::ostringstream out;
-  out << "forall x in [" << format(expr.univ_lower_bound()) << ", "
-      << format(expr.univ_upper_bound()) << "). " << format(expr.premise())
-      << " => ("
-      << "exists y in [" << format(expr.exists_lower_bound()) << ", "
-      << format(expr.exists_upper_bound()) << "). " << format(expr.s0())
-      << "[x+y] != " << format(expr.s1()) << "[y])";
-  return out.str();
-}
+std::string to_string(const string_not_contains_constraintt &expr);
 
-inline const string_not_contains_constraintt
-&to_string_not_contains_constraint(const exprt &expr)
-{
-  PRECONDITION(expr.id()==ID_string_not_contains_constraint);
-  DATA_INVARIANT(
-    expr.operands().size()==7,
-    string_refinement_invariantt("string_not_contains_constraintt must have 7 "
-      "operands"));
-  return static_cast<const string_not_contains_constraintt &>(expr);
-}
+const string_not_contains_constraintt &
+to_string_not_contains_constraint(const exprt &expr);
 
-inline string_not_contains_constraintt
-&to_string_not_contains_constraint(exprt &expr)
-{
-  PRECONDITION(expr.id()==ID_string_not_contains_constraint);
-  DATA_INVARIANT(
-    expr.operands().size()==7,
-    string_refinement_invariantt("string_not_contains_constraintt must have 7 "
-      "operands"));
-  return static_cast<string_not_contains_constraintt &>(expr);
-}
+string_not_contains_constraintt &to_string_not_contains_constraint(exprt &expr);
 
 #endif