Debugging

Author: tautschnig

jbmc/regression/jbmc-strings/ConstantEvaluationTrim/noprop.desc

@@ -1,6 +1,6 @@
 CORE
 Main
---function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--verbosity 10 --function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$

src/solvers/strings/string_refinement.cpp

@@ -26,6 +26,7 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <unordered_set>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
+#include <util/format_expr.h>
 #include <util/magic.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
@@ -92,12 +93,14 @@ exprt simplify_sum(const exprt &f);
 static void update_index_set(
   index_set_pairt &index_set,
   const namespacet &ns,
-  const std::vector<exprt> &current_constraints);
+  const std::vector<exprt> &current_constraints,
+  messaget &log);
 
 static void update_index_set(
   index_set_pairt &index_set,
   const namespacet &ns,
-  const exprt &formula);
+  const exprt &formula,
+  messaget &log);
 
 static std::vector<exprt> instantiate(
   const string_not_contains_constraintt &axiom,
@@ -808,7 +811,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   }
 
   initial_index_set(index_sets, ns, axioms);
-  update_index_set(index_sets, ns, current_constraints);
+  update_index_set(index_sets, ns, current_constraints, log);
   current_constraints.clear();
   const auto initial_instances =
     generate_instantiations(index_sets, axioms, not_contain_witnesses);
@@ -850,7 +853,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
       // and instantiating universal formulas with this indices.
       // We will then relaunch the solver with these added lemmas.
       index_sets.current.clear();
-      update_index_set(index_sets, ns, current_constraints);
+      update_index_set(index_sets, ns, current_constraints, log);
 
       display_index_set(log.debug(), index_sets);
 
@@ -1526,10 +1529,11 @@ static void initial_index_set(
 static void update_index_set(
   index_set_pairt &index_set,
   const namespacet &ns,
-  const std::vector<exprt> &current_constraints)
+  const std::vector<exprt> &current_constraints,
+  messaget &log)
 {
   for(const auto &axiom : current_constraints)
-    update_index_set(index_set, ns, axiom);
+    update_index_set(index_set, ns, axiom, log);
 }
 
 /// An expression representing an array of characters can be in the form of an
@@ -1685,7 +1689,8 @@ static void initial_index_set(
 static void update_index_set(
   index_set_pairt &index_set,
   const namespacet &ns,
-  const exprt &formula)
+  const exprt &formula,
+  messaget &log)
 {
   std::list<exprt> to_process;
   to_process.push_back(formula);
@@ -1694,6 +1699,7 @@ static void update_index_set(
   {
     exprt cur = to_process.back();
     to_process.pop_back();
+    log.debug() << format(cur) << messaget::eom;
     if(cur.id() == ID_index && is_char_type(cur.type()))
     {
       const exprt &s = to_index_expr(cur).array();
@@ -1702,6 +1708,7 @@ static void update_index_set(
         s.type().id() == ID_array,
         string_refinement_invariantt("index expressions must index on arrays"));
       exprt simplified = simplify_sum(i);
+      log.debug() << "simplified: " << format(simplified) << messaget::eom;
       if(s.id() != ID_array) // do not update index set of constant arrays
         add_to_index_set(index_set, ns, s, simplified);
     }