Remove java dependency

Lower bound should not use java_type

Author: romainbrenguier

src/solvers/refinement/string_constraint.cpp

@@ -5,28 +5,45 @@
 #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));
 }
 
 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,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
@@ -77,7 +86,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,15 +66,15 @@ 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.body = implies_exprt(contains, not_exprt(equal_exprt(str[n], c)));
   constraints.push_back(a4);
 
   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.body = implies_exprt(not_exprt(contains), notequal_exprt(str[m], c));
   constraints.push_back(a5);
@@ -366,7 +366,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.body = implies_exprt(contains, notequal_exprt(str[n], c));
   constraints.push_back(a4);

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -371,7 +371,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_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,15 +1529,15 @@ 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(
       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.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(axiom.body);