Rename premise in index_guard in string constraint

Author: romainbrenguier

src/solvers/refinement/string_constraint.cpp

@@ -7,7 +7,7 @@
 
 void replace(string_constraintt &axiom, const replace_mapt &symbol_resolve)
 {
-  replace_expr(symbol_resolve, axiom.premise);
+  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);
@@ -26,7 +26,7 @@ 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);
+      << format(expr.index_guard) << " => " << format(expr.body);
   return out.str();
 }
 
@@ -138,11 +138,13 @@ bool is_valid_string_constraint(
   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);
+  // 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 << "Premise has indices: " << to_string(constraint) << ", map: {";
+    stream << "Index guard has indices: "
+           << to_string(constraint) << ", map: {";
     for(const auto &pair : premise_indices)
     {
       stream << format(pair.first) << ": {";

src/solvers/refinement/string_constraint.h

@@ -60,10 +60,10 @@ Author: Romain Brenguier, [email protected]
 class string_constraintt final
 {
 public:
-  // String constraints are of the form
-  // forall univ_var in [lower_bound,upper_bound[. premise => body
-  exprt premise = true_exprt(); // Index guard
-  exprt body;                   // value constraint
+  /// 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;
   // \todo avoid depending on java type
   exprt lower_bound = from_integer(0, java_int_type());
@@ -73,7 +73,7 @@ class string_constraintt final
 inline void
 replace(string_constraintt &axiom, const union_find_replacet &symbol_resolve)
 {
-  symbol_resolve.replace_expr(axiom.premise);
+  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);

src/solvers/refinement/string_refinement.cpp

@@ -1405,10 +1405,10 @@ static exprt negation_of_constraint(const string_constraintt &axiom)
 
   // If the premise is false, the implication is trivially true, so the
   // negation is false.
-  if(axiom.premise == false_exprt())
+  if(axiom.index_guard == false_exprt())
     return false_exprt();
 
-  const and_exprt premise(axiom.premise, univ_within_bounds(axiom));
+  const and_exprt premise(axiom.index_guard, univ_within_bounds(axiom));
   const and_exprt negaxiom(premise, not_exprt(axiom.body));
 
   return negaxiom;
@@ -1531,15 +1531,15 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
     const symbol_exprt &univ_var = axiom.univ_var;
     const exprt &bound_inf = axiom.lower_bound;
     const exprt &bound_sup = axiom.upper_bound;
-    const exprt &prem = axiom.premise;
+    const exprt &prem = axiom.index_guard;
     INVARIANT(
       prem == true_exprt(), "string constraint premises are not supported");
 
     string_constraintt axiom_in_model;
     axiom_in_model.univ_var = univ_var;
     axiom_in_model.lower_bound = get(bound_inf);
     axiom_in_model.upper_bound = get(bound_sup);
-    axiom_in_model.premise = get(prem);
+    axiom_in_model.index_guard = get(prem);
     axiom_in_model.body = get(axiom.body);
 
     exprt negaxiom=negation_of_constraint(axiom_in_model);
@@ -1634,7 +1634,7 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
         const exprt &val=v.second;
         const string_constraintt &axiom=axioms.universal[v.first];
 
-        implies_exprt instance(axiom.premise, axiom.body);
+        implies_exprt instance(axiom.index_guard, axiom.body);
         replace_expr(axiom.univ_var, val, instance);
         // We are not sure the index set contains only positive numbers
         and_exprt bounds(
@@ -2135,7 +2135,7 @@ static exprt instantiate(
     and_exprt(
       binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound),
       binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound),
-      axiom.premise),
+      axiom.index_guard),
     axiom.body);
   replace_expr(axiom.univ_var, r, instance);
   return instance;