Remove java dependency

Lower bound should not use java_type

Author: romainbrenguier

src/solvers/refinement/string_constraint.cpp

@@ -5,19 +5,37 @@
 #include <util/simplify_expr.h>
 #include <util/expr_iterator.h>
 
+exprt * string_constraintt::lower_bound()
+{
+  return lower_bound_value.is_nil() ? nullptr : &lower_bound_value;
+}
+
+exprt string_constraintt::get_lower_bound() const
+{
+  return lower_bound_value.is_nil()
+         ? from_integer(0, upper_bound.type())
+         : lower_bound_value;
+}
+
+void string_constraintt::lower_bound(const exprt &e)
+{
+  lower_bound_value = e;
+}
+
 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);
-  replace_expr(symbol_resolve, axiom.lower_bound);
+  if(const auto lower_bound = axiom.lower_bound())
+    replace_expr(symbol_resolve, *lower_bound);
 }
 
 exprt univ_within_bounds(const string_constraintt &axiom)
 {
   return and_exprt(
-    binary_relation_exprt(axiom.lower_bound, ID_le, axiom.univ_var),
+    binary_relation_exprt(axiom.get_lower_bound(), ID_le, axiom.univ_var),
     binary_relation_exprt(axiom.upper_bound, ID_gt, axiom.univ_var));
 }
 
@@ -27,7 +45,7 @@ std::string from_expr(
   const string_constraintt &expr)
 {
   return "forall " + from_expr(ns, identifier, expr.univ_var) + " in [" +
-         from_expr(ns, identifier, expr.lower_bound) + ", " +
+         from_expr(ns, identifier, expr.get_lower_bound()) + ", " +
          from_expr(ns, identifier, expr.upper_bound) + "). " +
          from_expr(ns, identifier, expr.index_guard) + " => " +
          from_expr(ns, identifier, expr.body);

src/solvers/refinement/string_constraint.h

@@ -61,9 +61,19 @@ class string_constraintt final
   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());
   exprt upper_bound;
+
+  /// \return lower_bound if it has been set, nullptr if undefined
+  exprt * lower_bound();
+
+  /// \return lower_bound if it has been set, expression for 0 otherwise
+  exprt get_lower_bound() const;
+
+  /// Set lower bound to `e`
+  void lower_bound(const exprt &e);
+
+private:
+  exprt lower_bound_value = nil_exprt(); // nil_exprt defaults to 0
 };
 
 inline void
@@ -73,7 +83,8 @@ replace(string_constraintt &axiom, const union_find_replacet &symbol_resolve)
   symbol_resolve.replace_expr(axiom.body);
   symbol_resolve.replace_expr(axiom.univ_var);
   symbol_resolve.replace_expr(axiom.upper_bound);
-  symbol_resolve.replace_expr(axiom.lower_bound);
+  if(axiom.lower_bound())
+    symbol_resolve.replace_expr(*axiom.lower_bound());
 }
 
 exprt univ_within_bounds(const string_constraintt &axiom);

src/solvers/refinement/string_constraint_generator_indexof.cpp

@@ -66,7 +66,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   symbol_exprt n=fresh_univ_index("QA_index_of", index_type);
   string_constraintt a4;
   a4.univ_var = n;
-  a4.lower_bound = lower_bound;
+  a4.lower_bound(lower_bound);
   a4.upper_bound = index;
   a4.index_guard = contains;
   a4.body = not_exprt(equal_exprt(str[n], c));
@@ -75,7 +75,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
   symbol_exprt m=fresh_univ_index("QA_index_of", index_type);
   string_constraintt a5;
   a5.univ_var = m;
-  a5.lower_bound = lower_bound;
+  a5.lower_bound(lower_bound);
   a5.upper_bound = str.length();
   a5.index_guard = not_exprt(contains);
   a5.body = notequal_exprt(str[m], c);
@@ -370,7 +370,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   const symbol_exprt n = fresh_univ_index("QA_last_index_of1", index_type);
   string_constraintt a4;
   a4.univ_var = n;
-  a4.lower_bound = plus_exprt(index, index1);
+  a4.lower_bound(plus_exprt(index, index1));
   a4.upper_bound = end_index;
   a4.index_guard = contains;
   a4.body = notequal_exprt(str[n], c);

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -372,7 +372,7 @@ void string_constraint_generatort::add_constraint_on_characters(
     binary_relation_exprt(chr, ID_le, from_integer(high_char, chr.type())));
   string_constraintt sc;
   sc.univ_var = qvar;
-  sc.lower_bound = start;
+  sc.lower_bound(start);
   sc.upper_bound = end;
   sc.body = char_in_set;
   constraints.push_back(sc);

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -438,7 +438,6 @@ exprt string_constraint_generatort::add_axioms_for_char_set(
 
   string_constraintt a3;
   a3.univ_var = q;
-  a3.lower_bound = from_integer(0, q.type());
   a3.upper_bound = res.length();
   a3.index_guard = a3_guard;
   a3.body = a3_body;

src/solvers/refinement/string_refinement.cpp

@@ -30,11 +30,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <java_bytecode/java_types.h>
 #include <unordered_set>
 
-static bool is_valid_string_constraint(
-  messaget::mstreamt &stream,
-  const namespacet &ns,
-  const string_constraintt &expr);
-
 static optionalt<exprt> find_counter_example(
   const namespacet &ns,
   ui_message_handlert::uit ui,
@@ -1569,7 +1564,7 @@ static exprt negation_of_not_contains_constraint(
 static exprt negation_of_constraint(const string_constraintt &axiom)
 {
   // If the for all is vacuously true, the negation is false.
-  const exprt &lb = axiom.lower_bound;
+  const exprt &lb = axiom.get_lower_bound();
   const exprt &ub = axiom.upper_bound;
   if(lb.id()==ID_constant && ub.id()==ID_constant)
   {
@@ -1707,14 +1702,14 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
   {
     const string_constraintt &axiom=axioms.universal[i];
     const symbol_exprt &univ_var = axiom.univ_var;
-    const exprt &bound_inf = axiom.lower_bound;
+    const exprt &bound_inf = axiom.get_lower_bound();
     const exprt &bound_sup = axiom.upper_bound;
     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.lower_bound(get(bound_inf));
     axiom_in_model.upper_bound = get(bound_sup);
     axiom_in_model.index_guard = get(prem);
     axiom_in_model.body = get(body);