Merge pull request #1051 from smowton/smowton/fix/strings_debug_output

smowton · web-flow · commit 9ac5dff9d49d · 2017-06-23T10:55:03.000+01:00
Always pass namespace to from_expr
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
@@ -72,7 +72,7 @@ void string_refinementt::display_index_set()
   for(const auto &i : index_set)
   {
     const exprt &s=i.first;
-    debug() << "IS(" << from_expr(s) << ")=={" << eom;
+    debug() << "IS(" << from_expr(ns, "", s) << ")=={" << eom;
 
     for(auto j : i.second)
     {
@@ -81,7 +81,7 @@ void string_refinementt::display_index_set()
         count_current++;
         debug() << "**";
       }
-      debug() << "  " << from_expr(j) << ";" << eom;
+      debug() << "  " << from_expr(ns, "", j) << ";" << eom;
       count++;
     }
     debug() << "}"  << eom;
@@ -99,10 +99,10 @@ void string_refinementt::add_instantiations()
   for(const auto &i : current_index_set)
   {
     const exprt &s=i.first;
-    debug() << "IS(" << from_expr(s) << ")=={";
+    debug() << "IS(" << from_expr(ns, "", s) << ")=={";
 
     for(const auto &j : i.second)
-      debug() << from_expr(j) << "; ";
+      debug() << from_expr(ns, "", j) << "; ";
     debug() << "}"  << eom;
 
     for(const auto &j : i.second)
@@ -227,7 +227,7 @@ bool string_refinementt::add_axioms_for_string_assigns(
     else
     {
       debug() << "string_refinement warning: not handling char_array: "
-              << from_expr(rhs) << eom;
+              << from_expr(ns, "", rhs) << eom;
       return true;
     }
   }
@@ -291,7 +291,7 @@ void string_refinementt::concretize_string(const exprt &expr)
            mp_index>=concretize_limit)
         {
           debug() << "concretize_string: ignoring out of bound index: "
-                  << from_expr(simple_i) << eom;
+                  << from_expr(ns, "", simple_i) << eom;
         }
         else
         {
@@ -311,8 +311,8 @@ void string_refinementt::concretize_string(const exprt &expr)
 
       array_exprt arr(to_array_type(content.type()));
       arr.operands()=result;
-      debug() << "Concretized " << from_expr(content_expr)
-              << " = " << from_expr(arr) << eom;
+      debug() << "Concretized " << from_expr(ns, "", content_expr)
+              << " = " << from_expr(ns, "", arr) << eom;
       found_content[content]=arr;
     }
   }
@@ -371,7 +371,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)
     if(eq_expr.lhs().type()!=eq_expr.rhs().type())
     {
       debug() << "(sr::set_to) WARNING: ignoring "
-              << from_expr(expr) << " [inconsistent types]" << eom;
+              << from_expr(ns, "", expr) << " [inconsistent types]" << eom;
       debug() << "lhs has type: " << eq_expr.lhs().type().pretty(12) << eom;
       debug() << "rhs has type: " << eq_expr.rhs().type().pretty(12) << eom;
       return;
@@ -393,7 +393,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)
     if(lhs.id()!=ID_symbol)
     {
       debug() << "(sr::set_to) WARNING: ignoring "
-              << from_expr(expr) << eom;
+              << from_expr(ns, "", expr) << eom;
       return;
     }
 
@@ -405,7 +405,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)
          eq_expr.lhs().type().subtype() != subst_rhs.type().subtype())
       {
         debug() << "(sr::set_to) WARNING: ignoring "
-                << from_expr(expr) << " [inconsistent types after substitution]"
+                << from_expr(ns, "", expr) << " [inconsistent types after substitution]"
                 << eom;
         return;
       }
@@ -602,7 +602,7 @@ void string_refinementt::add_lemma(
     return;
   }
 
-  debug() << "adding lemma " << from_expr(simple_lemma) << eom;
+  debug() << "adding lemma " << from_expr(ns, "", simple_lemma) << eom;
 
   prop.l_set_to_true(convert(simple_lemma));
 }
@@ -626,7 +626,7 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const
   {
 #if 0
     debug() << "(sr::get_array) string of unknown size: "
-            << from_expr(size_val) << eom;
+            << from_expr(ns, "", size_val) << eom;
 #endif
     return empty_ret;
   }
@@ -699,7 +699,7 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const
   else
   {
 #if 0
-    debug() << "unable to get array-list value of " << from_expr(arr)
+    debug() << "unable to get array-list value of " << from_expr(ns, "", arr)
             << " of size " << n << eom;
 #endif
     return array_of_exprt(from_integer(0, char_type), ret_type);
@@ -787,14 +787,14 @@ void string_refinementt::fill_model()
 
       current_model[elength]=len;
       current_model[econtent]=arr;
-      debug() << from_expr(to_symbol_expr(it.first)) << "="
-              << from_expr(refined);
+      debug() << from_expr(ns, "", to_symbol_expr(it.first)) << "="
+              << from_expr(ns, "", refined);
 
       if(arr.id()==ID_array)
         debug() << " = \"" << string_of_array(to_array_expr(arr))
-                << "\" (size:" << from_expr(len) << ")"<< eom;
+                << "\" (size:" << from_expr(ns, "", len) << ")"<< eom;
       else
-        debug() << " = " << from_expr(arr) << " (size:" << from_expr(len)
+        debug() << " = " << from_expr(ns, "", arr) << " (size:" << from_expr(ns, "", len)
                 << ")" << eom;
     }
     else
@@ -806,22 +806,22 @@ void string_refinementt::fill_model()
       exprt arr_model=get_array(arr);
       current_model[it.first]=arr_model;
 
-      debug() << from_expr(to_symbol_expr(it.first)) << "="
-              << from_expr(arr) << " = " << from_expr(arr_model) << "" << eom;
+      debug() << from_expr(ns, "", to_symbol_expr(it.first)) << "="
+              << from_expr(ns, "", arr) << " = " << from_expr(ns, "", arr_model) << "" << eom;
     }
   }
 
   for(auto it : generator.boolean_symbols)
   {
       debug() << "" << it.get_identifier() << " := "
-              << from_expr(supert::get(it)) << eom;
+              << from_expr(ns, "", supert::get(it)) << eom;
       current_model[it]=supert::get(it);
   }
 
   for(auto it : generator.index_symbols)
   {
      debug() << "" << it.get_identifier() << " := "
-              << from_expr(supert::get(it)) << eom;
+              << from_expr(ns, "", supert::get(it)) << eom;
      current_model[it]=supert::get(it);
   }
 }
@@ -956,7 +956,7 @@ void string_refinementt::add_negation_of_constraint_to_solver(
   and_exprt premise(axiom.premise(), axiom.univ_within_bounds());
   and_exprt negaxiom(premise, not_exprt(axiom.body()));
 
-  debug() << "(sr::check_axioms) negated axiom: " << from_expr(negaxiom) << eom;
+  debug() << "(sr::check_axioms) negated axiom: " << from_expr(ns, "", negaxiom) << eom;
   substitute_array_access(negaxiom);
   solver << negaxiom;
 }
@@ -1000,7 +1000,7 @@ bool string_refinementt::check_axioms()
         exprt val=solver.get(axiom_in_model.univ_var());
         debug() << "string constraint can be violated for "
                 << axiom_in_model.univ_var().get_identifier()
-                << " = " << from_expr(val) << eom;
+                << " = " << from_expr(ns, "", val) << eom;
         violated[i]=val;
       }
       break;
@@ -1047,7 +1047,7 @@ bool string_refinementt::check_axioms()
         implies_exprt instance(premise, body);
         replace_expr(symbol_resolve, instance);
         replace_expr(axiom.univ_var(), val, instance);
-        debug() << "adding counter example " << from_expr(instance) << eom;
+        debug() << "adding counter example " << from_expr(ns, "", instance) << eom;
         add_lemma(instance);
       }
     }
@@ -1282,8 +1282,8 @@ void string_refinementt::add_to_index_set(const exprt &s, exprt i)
   }
   if(index_set[s].insert(i).second)
   {
-    debug() << "adding to index set of " << from_expr(s)
-            << ": " << from_expr(i) << eom;
+    debug() << "adding to index set of " << from_expr(ns, "", s)
+            << ": " << from_expr(ns, "", i) << eom;
     current_index_set[s].insert(i);
   }
 }
@@ -1429,15 +1429,16 @@ void string_refinementt::instantiate_not_contains(
   exprt s0=axiom.s0();
   exprt s1=axiom.s1();
 
-  debug() << "instantiate not contains " << from_expr(s0) << " : "
-          << from_expr(s1) << eom;
+  debug() << "instantiate not contains " << from_expr(ns, "", s0) << " : "
+          << from_expr(ns, "", s1) << eom;
   expr_sett index_set0=index_set[to_string_expr(s0).content()];
   expr_sett index_set1=index_set[to_string_expr(s1).content()];
 
   for(auto it0 : index_set0)
     for(auto it1 : index_set1)
     {
-      debug() << from_expr(it0) << " : " << from_expr(it1) << eom;
+      debug() << from_expr(ns, "", it0) << " : " << from_expr(ns, "", it1)
+              << eom;
       exprt val=minus_exprt(it0, it1);
       exprt witness=generator.get_witness_of(axiom, val);
       and_exprt prem_and_is_witness(

Original file line number	Diff line number	Diff line change
`@@ -72,7 +72,7 @@ void string_refinementt::display_index_set()`
`72`	`72`	`for(const auto &i : index_set)`
`73`	`73`	`{`
`74`	`74`	`const exprt &s=i.first;`
`75`		`- debug() << "IS(" << from_expr(s) << ")=={" << eom;`
	`75`	`+ debug() << "IS(" << from_expr(ns, "", s) << ")=={" << eom;`
`76`	`76`
`77`	`77`	`for(auto j : i.second)`
`78`	`78`	`{`
`@@ -81,7 +81,7 @@ void string_refinementt::display_index_set()`
`81`	`81`	`count_current++;`
`82`	`82`	`debug() << "**";`
`83`	`83`	`}`
`84`		`- debug() << " " << from_expr(j) << ";" << eom;`
	`84`	`+ debug() << " " << from_expr(ns, "", j) << ";" << eom;`
`85`	`85`	`count++;`
`86`	`86`	`}`
`87`	`87`	`debug() << "}" << eom;`
`@@ -99,10 +99,10 @@ void string_refinementt::add_instantiations()`
`99`	`99`	`for(const auto &i : current_index_set)`
`100`	`100`	`{`
`101`	`101`	`const exprt &s=i.first;`
`102`		`- debug() << "IS(" << from_expr(s) << ")=={";`
	`102`	`+ debug() << "IS(" << from_expr(ns, "", s) << ")=={";`
`103`	`103`
`104`	`104`	`for(const auto &j : i.second)`
`105`		`- debug() << from_expr(j) << "; ";`
	`105`	`+ debug() << from_expr(ns, "", j) << "; ";`
`106`	`106`	`debug() << "}" << eom;`
`107`	`107`
`108`	`108`	`for(const auto &j : i.second)`
`@@ -227,7 +227,7 @@ bool string_refinementt::add_axioms_for_string_assigns(`
`227`	`227`	`else`
`228`	`228`	`{`
`229`	`229`	`debug() << "string_refinement warning: not handling char_array: "`
`230`		`- << from_expr(rhs) << eom;`
	`230`	`+ << from_expr(ns, "", rhs) << eom;`
`231`	`231`	`return true;`
`232`	`232`	`}`
`233`	`233`	`}`
`@@ -291,7 +291,7 @@ void string_refinementt::concretize_string(const exprt &expr)`
`291`	`291`	`mp_index>=concretize_limit)`
`292`	`292`	`{`
`293`	`293`	`debug() << "concretize_string: ignoring out of bound index: "`
`294`		`- << from_expr(simple_i) << eom;`
	`294`	`+ << from_expr(ns, "", simple_i) << eom;`
`295`	`295`	`}`
`296`	`296`	`else`
`297`	`297`	`{`
`@@ -311,8 +311,8 @@ void string_refinementt::concretize_string(const exprt &expr)`
`311`	`311`
`312`	`312`	`array_exprt arr(to_array_type(content.type()));`
`313`	`313`	`arr.operands()=result;`
`314`		`- debug() << "Concretized " << from_expr(content_expr)`
`315`		`- << " = " << from_expr(arr) << eom;`
	`314`	`+ debug() << "Concretized " << from_expr(ns, "", content_expr)`
	`315`	`+ << " = " << from_expr(ns, "", arr) << eom;`
`316`	`316`	`found_content[content]=arr;`
`317`	`317`	`}`
`318`	`318`	`}`
`@@ -371,7 +371,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)`
`371`	`371`	`if(eq_expr.lhs().type()!=eq_expr.rhs().type())`
`372`	`372`	`{`
`373`	`373`	`debug() << "(sr::set_to) WARNING: ignoring "`
`374`		`- << from_expr(expr) << " [inconsistent types]" << eom;`
	`374`	`+ << from_expr(ns, "", expr) << " [inconsistent types]" << eom;`
`375`	`375`	`debug() << "lhs has type: " << eq_expr.lhs().type().pretty(12) << eom;`
`376`	`376`	`debug() << "rhs has type: " << eq_expr.rhs().type().pretty(12) << eom;`
`377`	`377`	`return;`
`@@ -393,7 +393,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)`
`393`	`393`	`if(lhs.id()!=ID_symbol)`
`394`	`394`	`{`
`395`	`395`	`debug() << "(sr::set_to) WARNING: ignoring "`
`396`		`- << from_expr(expr) << eom;`
	`396`	`+ << from_expr(ns, "", expr) << eom;`
`397`	`397`	`return;`
`398`	`398`	`}`
`399`	`399`
`@@ -405,7 +405,7 @@ void string_refinementt::set_to(const exprt &expr, bool value)`
`405`	`405`	`eq_expr.lhs().type().subtype() != subst_rhs.type().subtype())`
`406`	`406`	`{`
`407`	`407`	`debug() << "(sr::set_to) WARNING: ignoring "`
`408`		`- << from_expr(expr) << " [inconsistent types after substitution]"`
	`408`	`+ << from_expr(ns, "", expr) << " [inconsistent types after substitution]"`
`409`	`409`	`<< eom;`
`410`	`410`	`return;`
`411`	`411`	`}`
`@@ -602,7 +602,7 @@ void string_refinementt::add_lemma(`
`602`	`602`	`return;`
`603`	`603`	`}`
`604`	`604`
`605`		`- debug() << "adding lemma " << from_expr(simple_lemma) << eom;`
	`605`	`+ debug() << "adding lemma " << from_expr(ns, "", simple_lemma) << eom;`
`606`	`606`
`607`	`607`	`prop.l_set_to_true(convert(simple_lemma));`
`608`	`608`	`}`
`@@ -626,7 +626,7 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const`
`626`	`626`	`{`
`627`	`627`	`#if 0`
`628`	`628`	`debug() << "(sr::get_array) string of unknown size: "`
`629`		`- << from_expr(size_val) << eom;`
	`629`	`+ << from_expr(ns, "", size_val) << eom;`
`630`	`630`	`#endif`
`631`	`631`	`return empty_ret;`
`632`	`632`	`}`
`@@ -699,7 +699,7 @@ exprt string_refinementt::get_array(const exprt &arr, const exprt &size) const`
`699`	`699`	`else`
`700`	`700`	`{`
`701`	`701`	`#if 0`
`702`		`- debug() << "unable to get array-list value of " << from_expr(arr)`
	`702`	`+ debug() << "unable to get array-list value of " << from_expr(ns, "", arr)`
`703`	`703`	`<< " of size " << n << eom;`
`704`	`704`	`#endif`
`705`	`705`	`return array_of_exprt(from_integer(0, char_type), ret_type);`
`@@ -787,14 +787,14 @@ void string_refinementt::fill_model()`
`787`	`787`
`788`	`788`	`current_model[elength]=len;`
`789`	`789`	`current_model[econtent]=arr;`
`790`		`- debug() << from_expr(to_symbol_expr(it.first)) << "="`
`791`		`- << from_expr(refined);`
	`790`	`+ debug() << from_expr(ns, "", to_symbol_expr(it.first)) << "="`
	`791`	`+ << from_expr(ns, "", refined);`
`792`	`792`
`793`	`793`	`if(arr.id()==ID_array)`
`794`	`794`	`debug() << " = \"" << string_of_array(to_array_expr(arr))`
`795`		`- << "\" (size:" << from_expr(len) << ")"<< eom;`
	`795`	`+ << "\" (size:" << from_expr(ns, "", len) << ")"<< eom;`
`796`	`796`	`else`
`797`		`- debug() << " = " << from_expr(arr) << " (size:" << from_expr(len)`
	`797`	`+ debug() << " = " << from_expr(ns, "", arr) << " (size:" << from_expr(ns, "", len)`
`798`	`798`	`<< ")" << eom;`
`799`	`799`	`}`
`800`	`800`	`else`
`@@ -806,22 +806,22 @@ void string_refinementt::fill_model()`
`806`	`806`	`exprt arr_model=get_array(arr);`
`807`	`807`	`current_model[it.first]=arr_model;`
`808`	`808`
`809`		`- debug() << from_expr(to_symbol_expr(it.first)) << "="`
`810`		`- << from_expr(arr) << " = " << from_expr(arr_model) << "" << eom;`
	`809`	`+ debug() << from_expr(ns, "", to_symbol_expr(it.first)) << "="`
	`810`	`+ << from_expr(ns, "", arr) << " = " << from_expr(ns, "", arr_model) << "" << eom;`
`811`	`811`	`}`
`812`	`812`	`}`
`813`	`813`
`814`	`814`	`for(auto it : generator.boolean_symbols)`
`815`	`815`	`{`
`816`	`816`	`debug() << "" << it.get_identifier() << " := "`
`817`		`- << from_expr(supert::get(it)) << eom;`
	`817`	`+ << from_expr(ns, "", supert::get(it)) << eom;`
`818`	`818`	`current_model[it]=supert::get(it);`
`819`	`819`	`}`
`820`	`820`
`821`	`821`	`for(auto it : generator.index_symbols)`
`822`	`822`	`{`
`823`	`823`	`debug() << "" << it.get_identifier() << " := "`
`824`		`- << from_expr(supert::get(it)) << eom;`
	`824`	`+ << from_expr(ns, "", supert::get(it)) << eom;`
`825`	`825`	`current_model[it]=supert::get(it);`
`826`	`826`	`}`
`827`	`827`	`}`
`@@ -956,7 +956,7 @@ void string_refinementt::add_negation_of_constraint_to_solver(`
`956`	`956`	`and_exprt premise(axiom.premise(), axiom.univ_within_bounds());`
`957`	`957`	`and_exprt negaxiom(premise, not_exprt(axiom.body()));`
`958`	`958`
`959`		`- debug() << "(sr::check_axioms) negated axiom: " << from_expr(negaxiom) << eom;`
	`959`	`+ debug() << "(sr::check_axioms) negated axiom: " << from_expr(ns, "", negaxiom) << eom;`
`960`	`960`	`substitute_array_access(negaxiom);`
`961`	`961`	`solver << negaxiom;`
`962`	`962`	`}`
`@@ -1000,7 +1000,7 @@ bool string_refinementt::check_axioms()`
`1000`	`1000`	`exprt val=solver.get(axiom_in_model.univ_var());`
`1001`	`1001`	`debug() << "string constraint can be violated for "`
`1002`	`1002`	`<< axiom_in_model.univ_var().get_identifier()`
`1003`		`- << " = " << from_expr(val) << eom;`
	`1003`	`+ << " = " << from_expr(ns, "", val) << eom;`
`1004`	`1004`	`violated[i]=val;`
`1005`	`1005`	`}`
`1006`	`1006`	`break;`
`@@ -1047,7 +1047,7 @@ bool string_refinementt::check_axioms()`
`1047`	`1047`	`implies_exprt instance(premise, body);`
`1048`	`1048`	`replace_expr(symbol_resolve, instance);`
`1049`	`1049`	`replace_expr(axiom.univ_var(), val, instance);`
`1050`		`- debug() << "adding counter example " << from_expr(instance) << eom;`
	`1050`	`+ debug() << "adding counter example " << from_expr(ns, "", instance) << eom;`
`1051`	`1051`	`add_lemma(instance);`
`1052`	`1052`	`}`
`1053`	`1053`	`}`
`@@ -1282,8 +1282,8 @@ void string_refinementt::add_to_index_set(const exprt &s, exprt i)`
`1282`	`1282`	`}`
`1283`	`1283`	`if(index_set[s].insert(i).second)`
`1284`	`1284`	`{`
`1285`		`- debug() << "adding to index set of " << from_expr(s)`
`1286`		`- << ": " << from_expr(i) << eom;`
	`1285`	`+ debug() << "adding to index set of " << from_expr(ns, "", s)`
	`1286`	`+ << ": " << from_expr(ns, "", i) << eom;`
`1287`	`1287`	`current_index_set[s].insert(i);`
`1288`	`1288`	`}`
`1289`	`1289`	`}`
`@@ -1429,15 +1429,16 @@ void string_refinementt::instantiate_not_contains(`
`1429`	`1429`	`exprt s0=axiom.s0();`
`1430`	`1430`	`exprt s1=axiom.s1();`
`1431`	`1431`
`1432`		`- debug() << "instantiate not contains " << from_expr(s0) << " : "`
`1433`		`- << from_expr(s1) << eom;`
	`1432`	`+ debug() << "instantiate not contains " << from_expr(ns, "", s0) << " : "`
	`1433`	`+ << from_expr(ns, "", s1) << eom;`
`1434`	`1434`	`expr_sett index_set0=index_set[to_string_expr(s0).content()];`
`1435`	`1435`	`expr_sett index_set1=index_set[to_string_expr(s1).content()];`
`1436`	`1436`
`1437`	`1437`	`for(auto it0 : index_set0)`
`1438`	`1438`	`for(auto it1 : index_set1)`
`1439`	`1439`	`{`
`1440`		`- debug() << from_expr(it0) << " : " << from_expr(it1) << eom;`
	`1440`	`+ debug() << from_expr(ns, "", it0) << " : " << from_expr(ns, "", it1)`
	`1441`	`+ << eom;`
`1441`	`1442`	`exprt val=minus_exprt(it0, it1);`
`1442`	`1443`	`exprt witness=generator.get_witness_of(axiom, val);`
`1443`	`1444`	`and_exprt prem_and_is_witness(`