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);
@@ -29,7 +29,7 @@ std::string from_expr(
   return "forall " + from_expr(ns, identifier, expr.univ_var) + " in [" +
          from_expr(ns, identifier, expr.lower_bound) + ", " +
          from_expr(ns, identifier, expr.upper_bound) + "). " +
-         from_expr(ns, identifier, expr.premise) + " => " +
+         from_expr(ns, identifier, expr.index_guard) + " => " +
          from_expr(ns, identifier, expr.body);
 }
 
@@ -143,11 +143,12 @@ bool is_valid_string_constraint(
   const string_constraintt &expr)
 {
   const auto eom = messaget::eom;
-  // Condition 1: The premise cannot contain any string indices
-  const array_index_mapt premise_indices = gather_indices(expr.premise);
+  // Condition 1: The index guard cannot contain any string indices
+  const array_index_mapt premise_indices = gather_indices(expr.index_guard);
   if(!premise_indices.empty())
   {
-    stream << "Premise has indices: " << from_expr(ns, "", expr) << ", map: {";
+    stream << "Index guard has indices: " << from_expr(ns, "", expr)
+           << ", map: {";
     for(const auto &pair : premise_indices)
     {
       stream << from_expr(ns, "", pair.first) << ": {";

src/solvers/refinement/string_constraint.h

@@ -58,8 +58,8 @@ 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
+  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());
@@ -69,7 +69,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_constraint_generator_comparison.cpp

@@ -46,7 +46,7 @@ exprt string_constraint_generatort::add_axioms_for_equals(
   string_constraintt a2;
   a2.univ_var = qvar;
   a2.upper_bound = s1.length();
-  a2.premise = eq;
+  a2.index_guard = eq;
   a2.body = equal_exprt(s1[qvar], s2[qvar]);
   constraints.push_back(a2);
 
@@ -137,7 +137,7 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
   string_constraintt a2;
   a2.univ_var = qvar;
   a2.upper_bound = s1.length();
-  a2.premise = eq;
+  a2.index_guard = eq;
   a2.body = constr2;
   constraints.push_back(a2);
 
@@ -234,7 +234,7 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
   string_constraintt a2;
   a2.univ_var = i;
   a2.upper_bound = s1.length();
-  a2.premise = res_null;
+  a2.index_guard = res_null;
   a2.body = equal_exprt(s1[i], s2[i]);
   constraints.push_back(a2);
 
@@ -268,7 +268,7 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
   string_constraintt a4;
   a4.univ_var = i2;
   a4.upper_bound = x;
-  a4.premise = not_exprt(res_null);
+  a4.index_guard = not_exprt(res_null);
   a4.body = equal_exprt(s1[i2], s2[i2]);
   constraints.push_back(a4);
 

src/solvers/refinement/string_constraint_generator_indexof.cpp

@@ -68,7 +68,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   a4.univ_var = n;
   a4.lower_bound = lower_bound;
   a4.upper_bound = index;
-  a4.premise = contains;
+  a4.index_guard = contains;
   a4.body = not_exprt(equal_exprt(str[n], c));
   constraints.push_back(a4);
 
@@ -77,7 +77,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   a5.univ_var = m;
   a5.lower_bound = lower_bound;
   a5.upper_bound = str.length();
-  a5.premise = not_exprt(contains);
+  a5.index_guard = not_exprt(contains);
   a5.body = notequal_exprt(str[m], c);
   constraints.push_back(a5);
 
@@ -134,7 +134,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   string_constraintt a3;
   a3.univ_var = qvar;
   a3.upper_bound = needle.length();
-  a3.premise = contains;
+  a3.index_guard = contains;
   a3.body = equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar]);
   constraints.push_back(a3);
 
@@ -228,7 +228,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   string_constraintt a3;
   a3.univ_var = qvar;
   a3.upper_bound = needle.length();
-  a3.premise = contains;
+  a3.index_guard = contains;
   a3.body = constr3;
   constraints.push_back(a3);
 
@@ -372,15 +372,15 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   a4.univ_var = n;
   a4.lower_bound = plus_exprt(index, index1);
   a4.upper_bound = end_index;
-  a4.premise = contains;
+  a4.index_guard = contains;
   a4.body = notequal_exprt(str[n], c);
   constraints.push_back(a4);
 
   const symbol_exprt m = fresh_univ_index("QA_last_index_of2", index_type);
   string_constraintt a5;
   a5.univ_var = m;
   a5.upper_bound = end_index;
-  a5.premise = not_exprt(contains);
+  a5.index_guard = not_exprt(contains);
   a5.body = notequal_exprt(str[m], c);
   constraints.push_back(a5);
 

src/solvers/refinement/string_constraint_generator_testing.cpp

@@ -46,7 +46,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
   string_constraintt a2;
   a2.univ_var = qvar;
   a2.upper_bound = prefix.length();
-  a2.premise = isprefix;
+  a2.index_guard = isprefix;
   a2.body = equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]);
   constraints.push_back(a2);
 
@@ -156,7 +156,7 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix(
   string_constraintt a2;
   a2.univ_var = qvar;
   a2.upper_bound = s0.length();
-  a2.premise = issuffix;
+  a2.index_guard = issuffix;
   a2.body = equal_exprt(s0[qvar], s1[qvar_shifted]);
   constraints.push_back(a2);
 
@@ -228,7 +228,7 @@ exprt string_constraint_generatort::add_axioms_for_contains(
   string_constraintt a4;
   a4.univ_var = qvar;
   a4.upper_bound = s1.length();
-  a4.premise = contains;
+  a4.index_guard = contains;
   a4.body = equal_exprt(s1[qvar], s0[qvar_shifted]);
   constraints.push_back(a4);
 

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -54,15 +54,15 @@ exprt string_constraint_generatort::add_axioms_for_set_length(
   string_constraintt a2;
   a2.univ_var = idx;
   a2.upper_bound = res.length();
-  a2.premise = s1.axiom_for_length_gt(idx);
+  a2.index_guard = s1.axiom_for_length_gt(idx);
   a2.body = equal_exprt(s1[idx], res[idx]);
   constraints.push_back(a2);
 
   symbol_exprt idx2 = fresh_univ_index("QA_index_set_length2", index_type);
   string_constraintt a3;
   a3.univ_var = idx2;
   a3.upper_bound = res.length();
-  a3.premise = s1.axiom_for_length_le(idx2);
+  a3.index_guard = s1.axiom_for_length_le(idx2);
   a3.body = equal_exprt(res[idx2], constant_char(0, char_type));
   constraints.push_back(a3);
 
@@ -440,7 +440,7 @@ exprt string_constraint_generatort::add_axioms_for_char_set(
   a3.univ_var = q;
   a3.lower_bound = from_integer(0, q.type());
   a3.upper_bound = res.length();
-  a3.premise = a3_guard;
+  a3.index_guard = a3_guard;
   a3.body = a3_body;
   constraints.push_back(a3);
 

src/solvers/refinement/string_refinement.cpp

@@ -1581,10 +1581,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;
@@ -1709,14 +1709,14 @@ 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;
     const exprt &body = axiom.body;
 
     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(body);
 
     exprt negaxiom=negation_of_constraint(axiom_in_model);
@@ -1813,7 +1813,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
         exprt bounds = and_exprt(
@@ -2278,7 +2278,7 @@ static exprt instantiate(
     return true_exprt();
 
   exprt r = compute_inverse_function(stream, axiom.univ_var, val, idx);
-  implies_exprt instance(axiom.premise, axiom.body);
+  implies_exprt instance(axiom.index_guard, axiom.body);
   replace_expr(axiom.univ_var, r, instance);
   // We are not sure the index set contains only positive numbers
   exprt bounds = and_exprt(