From 857379db768e39662acba1f7f1b501ab38ad486f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 21 Jul 2017 15:27:53 +0100 Subject: [PATCH 1/3] Better debugging information in string solver This changes the function fill_model to debug model since it should only be used to debug issues with the string solver. --- src/solvers/refinement/string_refinement.cpp | 38 ++++++++++---------- src/solvers/refinement/string_refinement.h | 2 +- 2 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index c04f8185210..c95c26cc852 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -785,17 +785,18 @@ std::string string_refinementt::string_of_array(const array_exprt &arr) return result.str(); } -/// Fill in `current_model` by mapping the variables created by the solver to -/// constant expressions given by the current model -void string_refinementt::fill_model() +/// Display part of the current model by mapping the variables created by the +/// solver to constant expressions given by the current model +void string_refinementt::debug_model() { for(auto it : symbol_resolve) { if(refined_string_typet::is_refined_string_type(it.second.type())) { + debug() << " - " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n"; string_exprt refined=to_string_expr(it.second); - // TODO: check whith this is necessary: - replace_expr(symbol_resolve, refined); + debug() << " in_map: " << from_expr(ns, "", refined) << eom; + debug() << " resolved: " << from_expr(ns, "", refined) << eom; const exprt &econtent=refined.content(); const exprt &elength=refined.length(); @@ -805,15 +806,14 @@ void string_refinementt::fill_model() current_model[elength]=len; current_model[econtent]=arr; - 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(ns, "", len) << ")"<< eom; + debug() << " as_string: \"" << string_of_array(to_array_expr(arr)) + << "\"\n"; else - debug() << " = " << from_expr(ns, "", arr) - << " (size:" << from_expr(ns, "", len) << ")" << eom; + debug() << " as_char_array: " << from_expr(ns, "", arr) << "\n"; + + debug() << " size: " << from_expr(ns, "", len) << eom; } else { @@ -824,32 +824,32 @@ void string_refinementt::fill_model() "handled")); exprt arr=it.second; replace_expr(symbol_resolve, arr); + debug() << " - " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n"; + debug() << " resolved: " << from_expr(ns, "", arr) << "\n"; + replace_expr(current_model, arr); exprt arr_model=get_array(arr); current_model[it.first]=arr_model; - debug() << from_expr(ns, "", to_symbol_expr(it.first)) << "=" - << from_expr(ns, "", arr) << " = " - << from_expr(ns, "", arr_model) << "" << eom; + debug() << " char_array: " << from_expr(ns, "", arr_model) << eom; } } for(auto it : generator.boolean_symbols) { - debug() << "" << it.get_identifier() << " := " + debug() << " - " << it.get_identifier() << ": " << 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(ns, "", supert::get(it)) << eom; + debug() << " - " << it.get_identifier() << ": " + << from_expr(ns, "", supert::get(it)) << eom; current_model[it]=supert::get(it); } } - /// Create a new expression where 'with' expressions on arrays are replaced by /// 'if' expressions. e.g. for an array access arr[x], where: `arr := /// array_of(12) with {0:=24} with {2:=42}` the constructed expression will be: @@ -1084,7 +1084,7 @@ bool string_refinementt::check_axioms() << "===========================================" << eom; debug() << "string_refinementt::check_axioms: build the" << " interpretation from the model of the prop_solver" << eom; - fill_model(); + debug_model(); // Maps from indexes of violated universal axiom to a witness of violation std::map violated; diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 7e534825596..331a68fb287 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -127,7 +127,7 @@ class string_refinementt: public bv_refinementt const exprt &val, const symbol_exprt &univ_var); exprt negation_of_constraint(const string_constraintt &axiom); - void fill_model(); + void debug_model(); bool check_axioms(); bool is_axiom_sat( const exprt &axiom, const symbol_exprt& var, exprt &witness); From bbee1b18c77d7b909923af39a99638ea7c8a9ded Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 21 Jul 2017 16:03:01 +0100 Subject: [PATCH 2/3] Remove field current model This was only filled but never used. --- src/solvers/refinement/string_refinement.cpp | 10 ---------- src/solvers/refinement/string_refinement.h | 4 ---- 2 files changed, 14 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index c95c26cc852..3d011d71cf3 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -803,10 +803,6 @@ void string_refinementt::debug_model() exprt len=supert::get(elength); len=simplify_expr(len, ns); exprt arr=get_array(econtent, len); - - current_model[elength]=len; - current_model[econtent]=arr; - if(arr.id()==ID_array) debug() << " as_string: \"" << string_of_array(to_array_expr(arr)) << "\"\n"; @@ -826,11 +822,7 @@ void string_refinementt::debug_model() replace_expr(symbol_resolve, arr); debug() << " - " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n"; debug() << " resolved: " << from_expr(ns, "", arr) << "\n"; - - replace_expr(current_model, arr); exprt arr_model=get_array(arr); - current_model[it.first]=arr_model; - debug() << " char_array: " << from_expr(ns, "", arr_model) << eom; } } @@ -839,14 +831,12 @@ void string_refinementt::debug_model() { debug() << " - " << it.get_identifier() << ": " << 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(ns, "", supert::get(it)) << eom; - current_model[it]=supert::get(it); } } diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 331a68fb287..743366d628d 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -94,10 +94,6 @@ class string_refinementt: public bv_refinementt std::map reverse_symbol_resolve; std::list> non_string_axioms; - // Valuation in the current model of the symbols that have been created - // by the solver - replace_mapt current_model; - // Length of char arrays found during concretization std::map found_length; // Content of char arrays found during concretization From 317baac162a7a7a522c1be9929f286b06778659c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 21 Jul 2017 17:49:08 +0100 Subject: [PATCH 3/3] Better indentation in string solver debug --- src/solvers/refinement/string_refinement.cpp | 26 ++++++++++++-------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 3d011d71cf3..d7143d3269e 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -789,14 +789,17 @@ std::string string_refinementt::string_of_array(const array_exprt &arr) /// solver to constant expressions given by the current model void string_refinementt::debug_model() { + const std::string indent(" "); for(auto it : symbol_resolve) { if(refined_string_typet::is_refined_string_type(it.second.type())) { - debug() << " - " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n"; + debug() << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n"; string_exprt refined=to_string_expr(it.second); - debug() << " in_map: " << from_expr(ns, "", refined) << eom; - debug() << " resolved: " << from_expr(ns, "", refined) << eom; + debug() << indent << indent << "in_map: " + << from_expr(ns, "", refined) << eom; + debug() << indent << indent << "resolved: " + << from_expr(ns, "", refined) << eom; const exprt &econtent=refined.content(); const exprt &elength=refined.length(); @@ -804,12 +807,13 @@ void string_refinementt::debug_model() len=simplify_expr(len, ns); exprt arr=get_array(econtent, len); if(arr.id()==ID_array) - debug() << " as_string: \"" << string_of_array(to_array_expr(arr)) - << "\"\n"; + debug() << indent << indent << "as_string: \"" + << string_of_array(to_array_expr(arr)) << "\"\n"; else - debug() << " as_char_array: " << from_expr(ns, "", arr) << "\n"; + debug() << indent << indent << "as_char_array: " + << from_expr(ns, "", arr) << "\n"; - debug() << " size: " << from_expr(ns, "", len) << eom; + debug() << indent << indent << "size: " << from_expr(ns, "", len) << eom; } else { @@ -820,10 +824,12 @@ void string_refinementt::debug_model() "handled")); exprt arr=it.second; replace_expr(symbol_resolve, arr); - debug() << " - " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n"; - debug() << " resolved: " << from_expr(ns, "", arr) << "\n"; + debug() << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n"; + debug() << indent << indent << "resolved: " + << from_expr(ns, "", arr) << "\n"; exprt arr_model=get_array(arr); - debug() << " char_array: " << from_expr(ns, "", arr_model) << eom; + debug() << indent << indent << "char_array: " + << from_expr(ns, "", arr_model) << eom; } }