Corrections on generated axioms

Corrected axiom on positive length not added to axiom list

Added missing addition of default axioms in fresh string

Removing lemma that makes conditions too strong on strings

This was causing the verfication of several goal fail after the first
one is concretized.
Also added some debugging information.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -177,6 +177,7 @@ string_exprt string_constraint_generatort::fresh_string(
   symbol_exprt content=fresh_symbol("string_content", type.get_content_type());
   string_exprt str(length, content, type);
   created_strings.insert(str);
+  add_default_axioms(str);
   return str;
 }
 
@@ -246,7 +247,7 @@ string_exprt string_constraint_generatort::convert_java_string_to_string_exprt(
 
 /*******************************************************************\
 
-Function: string_constraint_generatort::add_default_constraints
+Function: string_constraint_generatort::add_default_axioms
 
   Inputs:
     s - a string expression
@@ -267,7 +268,8 @@ Function: string_constraint_generatort::add_default_constraints
 void string_constraint_generatort::add_default_axioms(
   const string_exprt &s)
 {
-  s.axiom_for_is_longer_than(from_integer(0, s.length().type()));
+  axioms.push_back(
+    s.axiom_for_is_longer_than(from_integer(0, s.length().type())));
   if(max_string_length!=std::numeric_limits<size_t>::max())
     axioms.push_back(s.axiom_for_is_shorter_than(max_string_length));
 

src/solvers/refinement/string_refinement.cpp

@@ -332,7 +332,6 @@ void string_refinementt::concretize_string(const exprt &expr)
   {
     string_exprt str=to_string_expr(expr);
     exprt length=get(str.length());
-    add_lemma(equal_exprt(str.length(), length));
     exprt content=str.content();
     replace_expr(symbol_resolve, content);
     found_length[content]=length;
@@ -350,6 +349,7 @@ void string_refinementt::concretize_string(const exprt &expr)
       else
       {
         size_t concretize_limit=found_length.to_long();
+        assert(concretize_limit<=generator.max_string_length);
         concretize_limit=concretize_limit>generator.max_string_length?
               generator.max_string_length:concretize_limit;
         exprt content_expr=str.content();
@@ -596,7 +596,11 @@ decision_proceduret::resultt string_refinementt::dec_solve()
           do_concretizing=false;
         }
         else
+        {
+          debug() << "check_SAT: the model is correct and "
+                  << "does not need concretizing" << eom;
           return D_SATISFIABLE;
+        }
       }
 
       display_index_set();
@@ -611,6 +615,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       }
       break;
     default:
+      debug() << "check_SAT: default return " << res << eom;
       return res;
     }
   }