Remove java dependency

Lower bound should not use java_type

Author: romainbrenguier

src/solvers/refinement/string_constraint.cpp

@@ -5,28 +5,34 @@
 #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);
-  replace_expr(symbol_resolve, axiom.lower_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.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));
 }
 
 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.index_guard) << " => " << format(expr.body);
+      << format(expr.get_lower_bound()) << ", " << format(expr.upper_bound)
+      << "). " << format(expr.index_guard) << " => " << format(expr.body);
   return out.str();
 }
 

src/solvers/refinement/string_constraint.h

@@ -28,7 +28,6 @@ Author: Romain Brenguier, [email protected]
 #include <util/refined_string_type.h>
 #include <util/string_expr.h>
 #include <langapi/language_util.h>
-#include <java_bytecode/java_types.h>
 #include <util/union_find_replace.h>
 
 ///  ### Universally quantified string constraint
@@ -65,9 +64,11 @@ 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;
+  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;
 };
 
 inline void
@@ -77,7 +78,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_refinement.cpp

@@ -1393,7 +1393,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)
   {
@@ -1529,7 +1529,7 @@ 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;
     INVARIANT(
@@ -2133,7 +2133,7 @@ static exprt instantiate(
   const exprt r = compute_inverse_function(stream, axiom.univ_var, val, *idx);
   implies_exprt instance(
     and_exprt(
-      binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound),
+      binary_relation_exprt(axiom.univ_var, ID_ge, axiom.get_lower_bound()),
       binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound),
       axiom.index_guard),
     axiom.body);