Remove java dependency

Lower bound should not use java_type

Author: romainbrenguier

src/solvers/refinement/string_constraint.cpp

@@ -5,6 +5,12 @@
 #include <util/simplify_expr.h>
 #include <util/expr_iterator.h>
 
+exprt string_constraintt::get_lower_bound() const
+{
+  return lower_bound.is_nil() ? from_integer(0, upper_bound.type())
+                              : lower_bound;
+}
+
 void replace(string_constraintt &axiom, const replace_mapt &symbol_resolve)
 {
   replace_expr(symbol_resolve, axiom.index_guard);
@@ -17,16 +23,16 @@ void replace(string_constraintt &axiom, const replace_mapt &symbol_resolve)
 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;
+  exprt lower_bound = nil_exprt(); // nil_exprt defaults to 0
+
+  /// \return lower_bound if it has been set, expression for 0 otherwise
+  exprt get_lower_bound() const;
 };
 
 inline void

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(